Documentation

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Subsemiring of opposite semirings #

For every semiring R, we construct an equivalence between subsemirings of R and that of Rแตแต’แต–.

source
๐Ÿ”ธ coverage
def Subsemiring.op {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
Subsemiring Rแตแต’แต–

Pull a subsemiring back to an opposite subsemiring along MulOpposite.unop

Instances For
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem Subsemiring.coe_op {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
    โ†‘S.op = MulOpposite.unop โปยน' โ†‘S
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem Subsemiring.op_toSubmonoid {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
    S.op.toSubmonoid = S.op
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem Subsemiring.mem_op {R : Type u_2} [NonAssocSemiring R] {x : Rแตแต’แต–} {S : Subsemiring R} :
    x โˆˆ S.op โ†” MulOpposite.unop x โˆˆ S
    source
    ๐Ÿ”ธ coverage
    def Subsemiring.unop {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rแตแต’แต–) :
    Subsemiring R

    Pull an opposite subsemiring back to a subsemiring along MulOpposite.op

    Instances For
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subsemiring.coe_unop {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rแตแต’แต–) :
      โ†‘S.unop = MulOpposite.op โปยน' โ†‘S
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subsemiring.unop_toSubmonoid {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rแตแต’แต–) :
      S.unop.toSubmonoid = S.unop
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subsemiring.mem_unop {R : Type u_2} [NonAssocSemiring R] {x : R} {S : Subsemiring Rแตแต’แต–} :
      x โˆˆ S.unop โ†” MulOpposite.op x โˆˆ S
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subsemiring.unop_op {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
      S.op.unop = S
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subsemiring.op_unop {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rแตแต’แต–) :
      S.unop.op = S

      Lattice results #

      source
      ๐Ÿ“ coverage
      theorem Subsemiring.op_le_iff {R : Type u_2} [NonAssocSemiring R] {Sโ‚ : Subsemiring R} {Sโ‚‚ : Subsemiring Rแตแต’แต–} :
      Sโ‚.op โ‰ค Sโ‚‚ โ†” Sโ‚ โ‰ค Sโ‚‚.unop
      source
      ๐Ÿ“ coverage
      theorem Subsemiring.le_op_iff {R : Type u_2} [NonAssocSemiring R] {Sโ‚ : Subsemiring Rแตแต’แต–} {Sโ‚‚ : Subsemiring R} :
      Sโ‚ โ‰ค Sโ‚‚.op โ†” Sโ‚.unop โ‰ค Sโ‚‚
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subsemiring.op_le_op_iff {R : Type u_2} [NonAssocSemiring R] {Sโ‚ Sโ‚‚ : Subsemiring R} :
      Sโ‚.op โ‰ค Sโ‚‚.op โ†” Sโ‚ โ‰ค Sโ‚‚
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem Subsemiring.unop_le_unop_iff {R : Type u_2} [NonAssocSemiring R] {Sโ‚ Sโ‚‚ : Subsemiring Rแตแต’แต–} :
      Sโ‚.unop โ‰ค Sโ‚‚.unop โ†” Sโ‚ โ‰ค Sโ‚‚
      source
      ๐Ÿ”ธ coverage
      def Subsemiring.opEquiv {R : Type u_2} [NonAssocSemiring R] :
      Subsemiring R โ‰ƒo Subsemiring Rแตแต’แต–

      A subsemiring S of R determines a subsemiring S.op of the opposite ring Rแตแต’แต–.

      Instances For
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.opEquiv_symm_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rแตแต’แต–) :
        (RelIso.symm opEquiv) S = S.unop
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.opEquiv_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
        opEquiv S = S.op
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_injective {R : Type u_2} [NonAssocSemiring R] :
        Function.Injective Subsemiring.op
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_injective {R : Type u_2} [NonAssocSemiring R] :
        Function.Injective Subsemiring.unop
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.op_inj {R : Type u_2} [NonAssocSemiring R] {S T : Subsemiring R} :
        S.op = T.op โ†” S = T
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.unop_inj {R : Type u_2} [NonAssocSemiring R] {S T : Subsemiring Rแตแต’แต–} :
        S.unop = T.unop โ†” S = T
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.op_bot {R : Type u_2} [NonAssocSemiring R] :
        โŠฅ.op = โŠฅ
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.op_eq_bot {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring R} :
        S.op = โŠฅ โ†” S = โŠฅ
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.unop_bot {R : Type u_2} [NonAssocSemiring R] :
        โŠฅ.unop = โŠฅ
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.unop_eq_bot {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring Rแตแต’แต–} :
        S.unop = โŠฅ โ†” S = โŠฅ
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.op_top {R : Type u_2} [NonAssocSemiring R] :
        โŠค.op = โŠค
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.op_eq_top {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring R} :
        S.op = โŠค โ†” S = โŠค
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.unop_top {R : Type u_2} [NonAssocSemiring R] :
        โŠค.unop = โŠค
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem Subsemiring.unop_eq_top {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring Rแตแต’แต–} :
        S.unop = โŠค โ†” S = โŠค
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_sup {R : Type u_2} [NonAssocSemiring R] (Sโ‚ Sโ‚‚ : Subsemiring R) :
        (Sโ‚ โŠ” Sโ‚‚).op = Sโ‚.op โŠ” Sโ‚‚.op
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_sup {R : Type u_2} [NonAssocSemiring R] (Sโ‚ Sโ‚‚ : Subsemiring Rแตแต’แต–) :
        (Sโ‚ โŠ” Sโ‚‚).unop = Sโ‚.unop โŠ” Sโ‚‚.unop
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_inf {R : Type u_2} [NonAssocSemiring R] (Sโ‚ Sโ‚‚ : Subsemiring R) :
        (Sโ‚ โŠ“ Sโ‚‚).op = Sโ‚.op โŠ“ Sโ‚‚.op
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_inf {R : Type u_2} [NonAssocSemiring R] (Sโ‚ Sโ‚‚ : Subsemiring Rแตแต’แต–) :
        (Sโ‚ โŠ“ Sโ‚‚).unop = Sโ‚.unop โŠ“ Sโ‚‚.unop
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_sSup {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring R)) :
        (sSup S).op = sSup (Subsemiring.unop โปยน' S)
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_sSup {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring Rแตแต’แต–)) :
        (sSup S).unop = sSup (Subsemiring.op โปยน' S)
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_sInf {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring R)) :
        (sInf S).op = sInf (Subsemiring.unop โปยน' S)
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_sInf {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring Rแตแต’แต–)) :
        (sInf S).unop = sInf (Subsemiring.op โปยน' S)
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_iSup {ฮน : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ฮน โ†’ Subsemiring R) :
        (iSup S).op = โจ† (i : ฮน), (S i).op
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_iSup {ฮน : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ฮน โ†’ Subsemiring Rแตแต’แต–) :
        (iSup S).unop = โจ† (i : ฮน), (S i).unop
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_iInf {ฮน : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ฮน โ†’ Subsemiring R) :
        (iInf S).op = โจ… (i : ฮน), (S i).op
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_iInf {ฮน : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ฮน โ†’ Subsemiring Rแตแต’แต–) :
        (iInf S).unop = โจ… (i : ฮน), (S i).unop
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.op_closure {R : Type u_2} [NonAssocSemiring R] (s : Set R) :
        (closure s).op = closure (MulOpposite.unop โปยน' s)
        source
        ๐Ÿ“ coverage
        theorem Subsemiring.unop_closure {R : Type u_2} [NonAssocSemiring R] (s : Set Rแตแต’แต–) :
        (closure s).unop = closure (MulOpposite.op โปยน' s)
        source
        ๐Ÿ”ธ coverage
        def Subsemiring.addEquivOp {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
        โ†ฅS โ‰ƒ+ โ†ฅS.op

        Bijection between a subsemiring S and its opposite.

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Subsemiring.addEquivOp_symm_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (b : โ†ฅS.op) :
          โ†‘(S.addEquivOp.symm b) = MulOpposite.unop โ†‘b
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem Subsemiring.addEquivOp_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (a : โ†ฅS.toSubmonoid) :
          โ†‘(S.addEquivOp a) = MulOpposite.op โ†‘a
          source
          ๐Ÿ”ธ coverage
          def Subsemiring.ringEquivOpMop {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
          โ†ฅS โ‰ƒ+* (โ†ฅS.op)แตแต’แต–

          Bijection between a subsemiring S and MulOpposite of its opposite.

          Instances For
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem Subsemiring.ringEquivOpMop_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (aโœ : โ†ฅS) :
            S.ringEquivOpMop aโœ = MulOpposite.op (S.addEquivOp aโœ)
            source
            ๐Ÿ“ coverage
            @[simp]
            theorem Subsemiring.ringEquivOpMop_symm_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (aโœ : (โ†ฅS.op)แตแต’แต–) :
            โ†‘(S.ringEquivOpMop.symm aโœ) = MulOpposite.unop โ†‘(MulOpposite.unop aโœ)
            source
            ๐Ÿ”ธ coverage
            def Subsemiring.mopRingEquivOp {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) :
            (โ†ฅS)แตแต’แต– โ‰ƒ+* โ†ฅS.op

            Bijection between MulOpposite of a subsemiring S and its opposite.

            Instances For
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem Subsemiring.mopRingEquivOp_symm_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (aโœ : โ†ฅS.op) :
              S.mopRingEquivOp.symm aโœ = MulOpposite.op (S.addEquivOp.symm aโœ)
              source
              ๐Ÿ“ coverage
              @[simp]
              theorem Subsemiring.mopRingEquivOp_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (aโœ : (โ†ฅS)แตแต’แต–) :
              โ†‘(S.mopRingEquivOp aโœ) = MulOpposite.op โ†‘(MulOpposite.unop aโœ)