Subring of opposite rings #

For every ring R, we construct an equivalence between subrings of R and that of Rᵐᵒᵖ.

source

def Subring.op {R : Type u_2} [NonAssocRing 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_toSubsemiring {R : Type u_2} [NonAssocRing R] (S : Subring R) :

S.op.toSubsemiring = S.op

source

@[simp]

theorem Subring.coe_op {R : Type u_2} [NonAssocRing R] (S : Subring R) :

↑S.op = MulOpposite.unop ⁻¹' ↑S

source

@[simp]

theorem Subring.mem_op {R : Type u_2} [NonAssocRing R] {x : Rᵐᵒᵖ} {S : Subring R} :

x ∈ S.op ↔ MulOpposite.unop x ∈ S

source

def Subring.unop {R : Type u_2} [NonAssocRing 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.coe_unop {R : Type u_2} [NonAssocRing R] (S : Subring Rᵐᵒᵖ) :

↑S.unop = MulOpposite.op ⁻¹' ↑S

source

@[simp]

theorem Subring.unop_toSubsemiring {R : Type u_2} [NonAssocRing R] (S : Subring Rᵐᵒᵖ) :

S.unop.toSubsemiring = S.unop

source

@[simp]

theorem Subring.mem_unop {R : Type u_2} [NonAssocRing R] {x : R} {S : Subring Rᵐᵒᵖ} :

x ∈ S.unop ↔ MulOpposite.op x ∈ S

source

@[simp]

theorem Subring.unop_op {R : Type u_2} [NonAssocRing R] (S : Subring R) :

S.op.unop = S

source

@[simp]

theorem Subring.op_unop {R : Type u_2} [NonAssocRing R] (S : Subring Rᵐᵒᵖ) :

S.unop.op = S

Lattice results #

source

theorem Subring.op_le_iff {R : Type u_2} [NonAssocRing R] {S₁ : Subring R} {S₂ : Subring Rᵐᵒᵖ} :

S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

source

theorem Subring.le_op_iff {R : Type u_2} [NonAssocRing 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} [NonAssocRing R] {S₁ S₂ : Subring R} :

S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

source

@[simp]

theorem Subring.unop_le_unop_iff {R : Type u_2} [NonAssocRing R] {S₁ S₂ : Subring Rᵐᵒᵖ} :

S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

source

def Subring.opEquiv {R : Type u_2} [NonAssocRing 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.opEquiv_symm_apply {R : Type u_2} [NonAssocRing R] (S : Subring Rᵐᵒᵖ) :

(RelIso.symm opEquiv) S = S.unop

source

@[simp]

theorem Subring.opEquiv_apply {R : Type u_2} [NonAssocRing R] (S : Subring R) :

opEquiv S = S.op

source

theorem Subring.op_injective {R : Type u_2} [NonAssocRing R] :

Function.Injective Subring.op

source

theorem Subring.unop_injective {R : Type u_2} [NonAssocRing R] :

Function.Injective Subring.unop

source

@[simp]

theorem Subring.op_inj {R : Type u_2} [NonAssocRing R] {S T : Subring R} :

S.op = T.op ↔ S = T

source

@[simp]

theorem Subring.unop_inj {R : Type u_2} [NonAssocRing R] {S T : Subring Rᵐᵒᵖ} :

S.unop = T.unop ↔ S = T

source

@[simp]

theorem Subring.op_bot {R : Type u_2} [NonAssocRing R] :

⊥.op = ⊥

source

@[simp]

theorem Subring.op_eq_bot {R : Type u_2} [NonAssocRing R] {S : Subring R} :

S.op = ⊥ ↔ S = ⊥

source

@[simp]

theorem Subring.unop_bot {R : Type u_2} [NonAssocRing R] :

⊥.unop = ⊥

source

@[simp]

theorem Subring.unop_eq_bot {R : Type u_2} [NonAssocRing R] {S : Subring Rᵐᵒᵖ} :

S.unop = ⊥ ↔ S = ⊥

source

@[simp]

theorem Subring.op_top {R : Type u_2} [NonAssocRing R] :

⊤.op = ⊤

source

@[simp]

theorem Subring.op_eq_top {R : Type u_2} [NonAssocRing R] {S : Subring R} :

S.op = ⊤ ↔ S = ⊤

source

@[simp]

theorem Subring.unop_top {R : Type u_2} [NonAssocRing R] :

⊤.unop = ⊤

source

@[simp]

theorem Subring.unop_eq_top {R : Type u_2} [NonAssocRing R] {S : Subring Rᵐᵒᵖ} :

S.unop = ⊤ ↔ S = ⊤

source

theorem Subring.op_sup {R : Type u_2} [NonAssocRing R] (S₁ S₂ : Subring R) :

(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

source

theorem Subring.unop_sup {R : Type u_2} [NonAssocRing R] (S₁ S₂ : Subring Rᵐᵒᵖ) :

(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

source

theorem Subring.op_inf {R : Type u_2} [NonAssocRing R] (S₁ S₂ : Subring R) :

(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

source

theorem Subring.unop_inf {R : Type u_2} [NonAssocRing R] (S₁ S₂ : Subring Rᵐᵒᵖ) :

(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

source

theorem Subring.op_sSup {R : Type u_2} [NonAssocRing R] (S : Set (Subring R)) :

(sSup S).op = sSup (Subring.unop ⁻¹' S)

source

theorem Subring.unop_sSup {R : Type u_2} [NonAssocRing R] (S : Set (Subring Rᵐᵒᵖ)) :

(sSup S).unop = sSup (Subring.op ⁻¹' S)

source

theorem Subring.op_sInf {R : Type u_2} [NonAssocRing R] (S : Set (Subring R)) :

(sInf S).op = sInf (Subring.unop ⁻¹' S)

source

theorem Subring.unop_sInf {R : Type u_2} [NonAssocRing R] (S : Set (Subring Rᵐᵒᵖ)) :

(sInf S).unop = sInf (Subring.op ⁻¹' S)

source

theorem Subring.op_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocRing R] (S : ι → Subring R) :

(iSup S).op = ⨆ (i : ι), (S i).op

source

theorem Subring.unop_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocRing R] (S : ι → Subring Rᵐᵒᵖ) :

(iSup S).unop = ⨆ (i : ι), (S i).unop

source

theorem Subring.op_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocRing R] (S : ι → Subring R) :

(iInf S).op = ⨅ (i : ι), (S i).op

source

theorem Subring.unop_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocRing R] (S : ι → Subring Rᵐᵒᵖ) :

(iInf S).unop = ⨅ (i : ι), (S i).unop

source

theorem Subring.op_closure {R : Type u_2} [NonAssocRing R] (s : Set R) :

(closure s).op = closure (MulOpposite.unop ⁻¹' s)

source

theorem Subring.unop_closure {R : Type u_2} [NonAssocRing R] (s : Set Rᵐᵒᵖ) :

(closure s).unop = closure (MulOpposite.op ⁻¹' s)

source

def Subring.addEquivOp {R : Type u_2} [NonAssocRing 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.addEquivOp_symm_apply_coe {R : Type u_2} [NonAssocRing R] (S : Subring R) (b : ↥S.op) :

↑(S.addEquivOp.symm b) = MulOpposite.unop ↑b

source

@[simp]

theorem Subring.addEquivOp_apply_coe {R : Type u_2} [NonAssocRing R] (S : Subring R) (a : ↥S.toSubmonoid) :

↑(S.addEquivOp a) = MulOpposite.op ↑a

source

def Subring.ringEquivOpMop {R : Type u_2} [NonAssocRing 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.ringEquivOpMop_symm_apply_coe {R : Type u_2} [NonAssocRing R] (S : Subring R) (a✝ : (↥S.op)ᵐᵒᵖ) :

↑(S.ringEquivOpMop.symm a✝) = MulOpposite.unop ↑(MulOpposite.unop a✝)

source

@[simp]

theorem Subring.ringEquivOpMop_apply {R : Type u_2} [NonAssocRing R] (S : Subring R) (a✝ : ↥S.toSubsemiring) :

S.ringEquivOpMop a✝ = MulOpposite.op (S.addEquivOp a✝)

source

def Subring.mopRingEquivOp {R : Type u_2} [NonAssocRing R] (S : Subring R) :

(↥S)ᵐᵒᵖ ≃+* ↥S.op

Bijection between MulOpposite of a subring S and its opposite.

Equations

S.mopRingEquivOp = S.mopRingEquivOp

Instances For

source

@[simp]

theorem Subring.mopRingEquivOp_apply_coe {R : Type u_2} [NonAssocRing R] (S : Subring R) (a✝ : (↥S.toSubsemiring)ᵐᵒᵖ) :

↑(S.mopRingEquivOp a✝) = MulOpposite.op ↑(MulOpposite.unop a✝)

source

@[simp]

theorem Subring.mopRingEquivOp_symm_apply {R : Type u_2} [NonAssocRing R] (S : Subring R) (a✝ : ↥S.op) :

S.mopRingEquivOp.symm a✝ = MulOpposite.op (S.addEquivOp.symm a✝)

Documentation

Mathlib.Algebra.Ring.Subring.MulOpposite

Subring of opposite rings #

Lattice results #