Subsemiring of opposite semirings #
For every semiring R
, we construct an equivalence between subsemirings of R
and that of Rᵐᵒᵖ
.
@[simp]
theorem
Subsemiring.op_toSubmonoid
{R : Type u_2}
[NonAssocSemiring R]
(S : Subsemiring R)
:
S.op.toSubmonoid = S.op
Pull a subsemiring back to an opposite subsemiring along MulOpposite.unop
Equations
- S.op = { toSubmonoid := S.op, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
@[simp]
@[simp]
theorem
Subsemiring.mem_op
{R : Type u_2}
[NonAssocSemiring R]
{x : Rᵐᵒᵖ}
{S : Subsemiring R}
:
x ∈ S.op ↔ MulOpposite.unop x ∈ S
@[simp]
theorem
Subsemiring.unop_toSubmonoid
{R : Type u_2}
[NonAssocSemiring R]
(S : Subsemiring Rᵐᵒᵖ)
:
S.unop.toSubmonoid = S.unop
Pull an opposite subsemiring back to a subsemiring along MulOpposite.op
Equations
- S.unop = { toSubmonoid := S.unop, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
@[simp]
@[simp]
theorem
Subsemiring.mem_unop
{R : Type u_2}
[NonAssocSemiring R]
{x : R}
{S : Subsemiring Rᵐᵒᵖ}
:
x ∈ S.unop ↔ MulOpposite.op x ∈ S
@[simp]
@[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ᵐᵒᵖ}
:
theorem
Subsemiring.le_op_iff
{R : Type u_2}
[NonAssocSemiring R]
{S₁ : Subsemiring Rᵐᵒᵖ}
{S₂ : Subsemiring R}
:
@[simp]
theorem
Subsemiring.op_le_op_iff
{R : Type u_2}
[NonAssocSemiring R]
{S₁ : Subsemiring R}
{S₂ : Subsemiring R}
:
@[simp]
theorem
Subsemiring.unop_le_unop_iff
{R : Type u_2}
[NonAssocSemiring R]
{S₁ : Subsemiring Rᵐᵒᵖ}
{S₂ : Subsemiring Rᵐᵒᵖ}
:
@[simp]
theorem
Subsemiring.opEquiv_symm_apply
{R : Type u_2}
[NonAssocSemiring R]
(S : Subsemiring Rᵐᵒᵖ)
:
(RelIso.symm Subsemiring.opEquiv) S = S.unop
@[simp]
theorem
Subsemiring.opEquiv_apply
{R : Type u_2}
[NonAssocSemiring R]
(S : Subsemiring R)
:
Subsemiring.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 : Subsemiring R}
{T : Subsemiring R}
:
@[simp]
theorem
Subsemiring.unop_inj
{R : Type u_2}
[NonAssocSemiring R]
{S : Subsemiring Rᵐᵒᵖ}
{T : Subsemiring Rᵐᵒᵖ}
:
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Subsemiring.op_sup
{R : Type u_2}
[NonAssocSemiring R]
(S₁ : Subsemiring R)
(S₂ : Subsemiring R)
:
theorem
Subsemiring.unop_sup
{R : Type u_2}
[NonAssocSemiring R]
(S₁ : Subsemiring Rᵐᵒᵖ)
(S₂ : Subsemiring Rᵐᵒᵖ)
:
theorem
Subsemiring.op_inf
{R : Type u_2}
[NonAssocSemiring R]
(S₁ : Subsemiring R)
(S₂ : Subsemiring R)
:
theorem
Subsemiring.unop_inf
{R : Type u_2}
[NonAssocSemiring R]
(S₁ : Subsemiring Rᵐᵒᵖ)
(S₂ : Subsemiring Rᵐᵒᵖ)
:
theorem
Subsemiring.op_iSup
{ι : Sort u_1}
{R : Type u_2}
[NonAssocSemiring R]
(S : ι → Subsemiring R)
:
theorem
Subsemiring.unop_iSup
{ι : Sort u_1}
{R : Type u_2}
[NonAssocSemiring R]
(S : ι → Subsemiring Rᵐᵒᵖ)
:
theorem
Subsemiring.op_iInf
{ι : Sort u_1}
{R : Type u_2}
[NonAssocSemiring R]
(S : ι → Subsemiring R)
:
theorem
Subsemiring.unop_iInf
{ι : Sort u_1}
{R : Type u_2}
[NonAssocSemiring R]
(S : ι → Subsemiring Rᵐᵒᵖ)
:
theorem
Subsemiring.op_closure
{R : Type u_2}
[NonAssocSemiring R]
(s : Set R)
:
(Subsemiring.closure s).op = Subsemiring.closure (MulOpposite.unop ⁻¹' s)
theorem
Subsemiring.unop_closure
{R : Type u_2}
[NonAssocSemiring R]
(s : Set Rᵐᵒᵖ)
:
(Subsemiring.closure s).unop = Subsemiring.closure (MulOpposite.op ⁻¹' s)
@[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
Bijection between a subsemiring S
and its opposite.
Equations
- S.addEquivOp = { toEquiv := S.equivOp, map_add' := ⋯ }
Instances For
@[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)
@[simp]
theorem
Subsemiring.ringEquivOpMop_apply
{R : Type u_2}
[NonAssocSemiring R]
(S : Subsemiring R)
:
∀ (a : ↥S), S.ringEquivOpMop a = MulOpposite.op (S.addEquivOp a)
Bijection between a subsemiring S
and MulOpposite
of its opposite.
Equations
- S.ringEquivOpMop = { toEquiv := (S.addEquivOp.trans MulOpposite.opAddEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯ }
Instances For
@[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)
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' := ⋯ }