Subsemiring of opposite semirings

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

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

Equations

• S.op = { toSubmonoid := S.op, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subsemiring.coe_op {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) : ↑S.op = MulOpposite.unop ⁻¹' ↑S

@[simp]

theorem Subsemiring.op_toSubmonoid {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) : S.op.toSubmonoid = S.op

@[simp]

theorem Subsemiring.mem_op {R : Type u_2} [NonAssocSemiring R] {x : Rᵐᵒᵖ} {S : Subsemiring R} : x ∈ S.op ↔ MulOpposite.unop x ∈ S

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

Equations

• S.unop = { toSubmonoid := S.unop, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subsemiring.coe_unop {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) : ↑S.unop = MulOpposite.op ⁻¹' ↑S

@[simp]

theorem Subsemiring.unop_toSubmonoid {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) : S.unop.toSubmonoid = S.unop

@[simp]

theorem Subsemiring.mem_unop {R : Type u_2} [NonAssocSemiring R] {x : R} {S : Subsemiring Rᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S

@[simp]

theorem Subsemiring.unop_op {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) : S.op.unop = S

@[simp]

theorem Subsemiring.op_unop {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) : S.unop.op = S

Lattice results

theorem Subsemiring.op_le_iff {R : Type u_2} [NonAssocSemiring R] {S₁ : Subsemiring R} {S₂ : Subsemiring Rᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

theorem Subsemiring.le_op_iff {R : Type u_2} [NonAssocSemiring R] {S₁ : Subsemiring Rᵐᵒᵖ} {S₂ : Subsemiring R} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

@[simp]

theorem Subsemiring.op_le_op_iff {R : Type u_2} [NonAssocSemiring R] {S₁ S₂ : Subsemiring R} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

@[simp]

theorem Subsemiring.unop_le_unop_iff {R : Type u_2} [NonAssocSemiring R] {S₁ S₂ : Subsemiring Rᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

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ᵐᵒᵖ.

Equations

• Subsemiring.opEquiv = { toFun := Subsemiring.op, invFun := Subsemiring.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Subsemiring.opEquiv_symm_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ) : (RelIso.symm opEquiv) S = S.unop

@[simp]

theorem Subsemiring.opEquiv_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) : opEquiv S = S.op

theorem Subsemiring.op_injective {R : Type u_2} [NonAssocSemiring R] : Function.Injective Subsemiring.op

theorem Subsemiring.unop_injective {R : Type u_2} [NonAssocSemiring R] : Function.Injective Subsemiring.unop

@[simp]

theorem Subsemiring.op_inj {R : Type u_2} [NonAssocSemiring R] {S T : Subsemiring R} : S.op = T.op ↔ S = T

@[simp]

theorem Subsemiring.unop_inj {R : Type u_2} [NonAssocSemiring R] {S T : Subsemiring Rᵐᵒᵖ} : S.unop = T.unop ↔ S = T

@[simp]

theorem Subsemiring.op_bot {R : Type u_2} [NonAssocSemiring R] : ⊥.op = ⊥

@[simp]

theorem Subsemiring.op_eq_bot {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring R} : S.op = ⊥ ↔ S = ⊥

@[simp]

theorem Subsemiring.unop_bot {R : Type u_2} [NonAssocSemiring R] : ⊥.unop = ⊥

@[simp]

theorem Subsemiring.unop_eq_bot {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring Rᵐᵒᵖ} : S.unop = ⊥ ↔ S = ⊥

@[simp]

theorem Subsemiring.op_top {R : Type u_2} [NonAssocSemiring R] : ⊤.op = ⊤

@[simp]

theorem Subsemiring.op_eq_top {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring R} : S.op = ⊤ ↔ S = ⊤

@[simp]

theorem Subsemiring.unop_top {R : Type u_2} [NonAssocSemiring R] : ⊤.unop = ⊤

@[simp]

theorem Subsemiring.unop_eq_top {R : Type u_2} [NonAssocSemiring R] {S : Subsemiring Rᵐᵒᵖ} : S.unop = ⊤ ↔ S = ⊤

theorem Subsemiring.op_sup {R : Type u_2} [NonAssocSemiring R] (S₁ S₂ : Subsemiring R) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

theorem Subsemiring.unop_sup {R : Type u_2} [NonAssocSemiring R] (S₁ S₂ : Subsemiring Rᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

theorem Subsemiring.op_inf {R : Type u_2} [NonAssocSemiring R] (S₁ S₂ : Subsemiring R) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

theorem Subsemiring.unop_inf {R : Type u_2} [NonAssocSemiring R] (S₁ S₂ : Subsemiring Rᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

theorem Subsemiring.op_sSup {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring R)) : (sSup S).op = sSup (Subsemiring.unop ⁻¹' S)

theorem Subsemiring.unop_sSup {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring Rᵐᵒᵖ)) : (sSup S).unop = sSup (Subsemiring.op ⁻¹' S)

theorem Subsemiring.op_sInf {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring R)) : (sInf S).op = sInf (Subsemiring.unop ⁻¹' S)

theorem Subsemiring.unop_sInf {R : Type u_2} [NonAssocSemiring R] (S : Set (Subsemiring Rᵐᵒᵖ)) : (sInf S).unop = sInf (Subsemiring.op ⁻¹' S)

theorem Subsemiring.op_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ι → Subsemiring R) : (iSup S).op = ⨆ (i : ι), (S i).op

theorem Subsemiring.unop_iSup {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ι → Subsemiring Rᵐᵒᵖ) : (iSup S).unop = ⨆ (i : ι), (S i).unop

theorem Subsemiring.op_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ι → Subsemiring R) : (iInf S).op = ⨅ (i : ι), (S i).op

theorem Subsemiring.unop_iInf {ι : Sort u_1} {R : Type u_2} [NonAssocSemiring R] (S : ι → Subsemiring Rᵐᵒᵖ) : (iInf S).unop = ⨅ (i : ι), (S i).unop

theorem Subsemiring.op_closure {R : Type u_2} [NonAssocSemiring R] (s : Set R) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

theorem Subsemiring.unop_closure {R : Type u_2} [NonAssocSemiring R] (s : Set Rᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

def Subsemiring.addEquivOp {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) : ↥S ≃+ ↥S.op

Bijection between a subsemiring S and its opposite.

Equations

• S.addEquivOp = { toEquiv := S.equivOp, map_add' := ⋯ }

@[simp]

theorem Subsemiring.addEquivOp_apply_coe {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (a : ↥S.toSubmonoid) : ↑(S.addEquivOp a) = MulOpposite.op ↑a

@[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

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.

Equations

• S.ringEquivOpMop = { toEquiv := (S.addEquivOp.trans MulOpposite.opAddEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem Subsemiring.ringEquivOpMop_apply {R : Type u_2} [NonAssocSemiring R] (S : Subsemiring R) (a✝ : ↥S) : S.ringEquivOpMop a✝ = MulOpposite.op (S.addEquivOp a✝)

@[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✝)

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.

Equations

• S.mopRingEquivOp = { toEquiv := (MulOpposite.opAddEquiv.symm.trans S.addEquivOp).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[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✝)

@[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✝)