Documentation

Mathlib.Algebra.Ring.Subring.MulOpposite

Subring of opposite rings #

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

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

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

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

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

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

          Lattice results #

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

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

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

              Bijection between a subring S and its opposite.

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

                  Bijection between a subring S and MulOpposite of its opposite.

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

                      Bijection between MulOpposite of a subring S and its opposite.

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