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
@[simp]
theorem Subring.op_toSubsemiring {R : Type u_2} [Ring R] (S : Subring R) :
S.op.toSubsemiring = S.op
source
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
  • S.op = { toSubsemiring := S.op, neg_mem' := ⋯ }
Instances For
    source
    @[simp]
    theorem Subring.op_coe {R : Type u_2} [Ring R] (S : Subring R) :
    ↑S.op = MulOpposite.unop ⁻¹' ↑S
    source
    @[simp]
    theorem Subring.mem_op {R : Type u_2} [Ring R] {x : Rᵐᵒᵖ} {S : Subring R} :
    x ∈ S.op ↔ MulOpposite.unop x ∈ S
    source
    @[simp]
    theorem Subring.unop_toSubsemiring {R : Type u_2} [Ring R] (S : Subring Rᵐᵒᵖ) :
    S.unop.toSubsemiring = S.unop
    source
    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
    • S.unop = { toSubsemiring := S.unop, neg_mem' := ⋯ }
    Instances For
      source
      @[simp]
      theorem Subring.unop_coe {R : Type u_2} [Ring R] (S : Subring Rᵐᵒᵖ) :
      ↑S.unop = MulOpposite.op ⁻¹' ↑S
      source
      @[simp]
      theorem Subring.mem_unop {R : Type u_2} [Ring R] {x : R} {S : Subring Rᵐᵒᵖ} :
      x ∈ S.unop ↔ MulOpposite.op x ∈ S
      source
      @[simp]
      theorem Subring.unop_op {R : Type u_2} [Ring R] (S : Subring R) :
      S.op.unop = S
      source
      @[simp]
      theorem Subring.op_unop {R : Type u_2} [Ring R] (S : Subring Rᵐᵒᵖ) :
      S.unop.op = S

      Lattice results #

      source
      theorem Subring.op_le_iff {R : Type u_2} [Ring R] {S₁ : Subring R} {S₂ : Subring Rᵐᵒᵖ} :
      S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
      source
      theorem Subring.le_op_iff {R : Type u_2} [Ring R] {S₁ : Subring Rᵐᵒᵖ} {S₂ : Subring R} :
      S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
      source
      @[simp]
      theorem Subring.op_le_op_iff {R : Type u_2} [Ring R] {S₁ : Subring R} {S₂ : Subring R} :
      S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
      source
      @[simp]
      theorem Subring.unop_le_unop_iff {R : Type u_2} [Ring R] {S₁ : Subring Rᵐᵒᵖ} {S₂ : Subring Rᵐᵒᵖ} :
      S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
      source
      @[simp]
      theorem Subring.opEquiv_apply {R : Type u_2} [Ring R] (S : Subring R) :
      Subring.opEquiv S = S.op
      source
      @[simp]
      theorem Subring.opEquiv_symm_apply {R : Type u_2} [Ring R] (S : Subring Rᵐᵒᵖ) :
      (RelIso.symm Subring.opEquiv) S = S.unop
      source
      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
      • Subring.opEquiv = { toFun := Subring.op, invFun := Subring.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
      Instances For
        source
        @[simp]
        theorem Subring.op_bot {R : Type u_2} [Ring R] :
        ⊥.op = ⊥
        source
        @[simp]
        theorem Subring.unop_bot {R : Type u_2} [Ring R] :
        ⊥.unop = ⊥
        source
        @[simp]
        theorem Subring.op_top {R : Type u_2} [Ring R] :
        ⊤.op = ⊤
        source
        @[simp]
        theorem Subring.unop_top {R : Type u_2} [Ring R] :
        ⊤.unop = ⊤
        source
        theorem Subring.op_sup {R : Type u_2} [Ring R] (S₁ : Subring R) (S₂ : Subring R) :
        (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
        source
        theorem Subring.unop_sup {R : Type u_2} [Ring R] (S₁ : Subring Rᵐᵒᵖ) (S₂ : Subring Rᵐᵒᵖ) :
        (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
        source
        theorem Subring.op_inf {R : Type u_2} [Ring R] (S₁ : Subring R) (S₂ : Subring R) :
        (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
        source
        theorem Subring.unop_inf {R : Type u_2} [Ring R] (S₁ : Subring Rᵐᵒᵖ) (S₂ : Subring Rᵐᵒᵖ) :
        (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
        source
        theorem Subring.op_sSup {R : Type u_2} [Ring R] (S : Set (Subring R)) :
        (sSup S).op = sSup (Subring.unop ⁻¹' S)
        source
        theorem Subring.unop_sSup {R : Type u_2} [Ring R] (S : Set (Subring Rᵐᵒᵖ)) :
        (sSup S).unop = sSup (Subring.op ⁻¹' S)
        source
        theorem Subring.op_sInf {R : Type u_2} [Ring R] (S : Set (Subring R)) :
        (sInf S).op = sInf (Subring.unop ⁻¹' S)
        source
        theorem Subring.unop_sInf {R : Type u_2} [Ring R] (S : Set (Subring Rᵐᵒᵖ)) :
        (sInf S).unop = sInf (Subring.op ⁻¹' S)
        source
        theorem Subring.op_iSup {ι : Sort u_1} {R : Type u_2} [Ring R] (S : ι → Subring R) :
        (iSup S).op = ⨆ (i : ι), (S i).op
        source
        theorem Subring.unop_iSup {ι : Sort u_1} {R : Type u_2} [Ring R] (S : ι → Subring Rᵐᵒᵖ) :
        (iSup S).unop = ⨆ (i : ι), (S i).unop
        source
        theorem Subring.op_iInf {ι : Sort u_1} {R : Type u_2} [Ring R] (S : ι → Subring R) :
        (iInf S).op = ⨅ (i : ι), (S i).op
        source
        theorem Subring.unop_iInf {ι : Sort u_1} {R : Type u_2} [Ring R] (S : ι → Subring Rᵐᵒᵖ) :
        (iInf S).unop = ⨅ (i : ι), (S i).unop
        source
        theorem Subring.op_closure {R : Type u_2} [Ring R] (s : Set R) :
        (Subring.closure s).op = Subring.closure (MulOpposite.unop ⁻¹' s)
        source
        theorem Subring.unop_closure {R : Type u_2} [Ring R] (s : Set Rᵐᵒᵖ) :
        (Subring.closure s).unop = Subring.closure (MulOpposite.op ⁻¹' s)
        source
        @[simp]
        theorem Subring.addEquivOp_apply_coe {R : Type u_2} [Ring R] (S : Subring R) (a : { a : R // (fun (x : R) => x ∈ S.toSubmonoid) a }) :
        ↑(S.addEquivOp a) = MulOpposite.op ↑a
        source
        @[simp]
        theorem Subring.addEquivOp_symm_apply_coe {R : Type u_2} [Ring R] (S : Subring R) (b : { b : Rᵐᵒᵖ // (fun (x : Rᵐᵒᵖ) => x ∈ S.op) b }) :
        ↑(S.addEquivOp.symm b) = MulOpposite.unop ↑b
        source
        def Subring.addEquivOp {R : Type u_2} [Ring R] (S : Subring R) :
        ↥S ≃+ ↥S.op

        Bijection between a subring S and its opposite.

        Equations
        • S.addEquivOp = S.addEquivOp
        Instances For
          source
          @[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
          @[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
          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
          • S.ringEquivOpMop = S.ringEquivOpMop
          Instances For
            source
            @[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
            @[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)
            source
            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
            • S.mopRingEquivOp = S.mopRingEquivOp
            Instances For