Subring of opposite rings #
For every ring R
, we construct an equivalence between subrings of R
and that of Rᵐᵒᵖ
.
Pull a subring back to an opposite subring along MulOpposite.unop
Equations
- S.op = { toSubsemiring := S.op, neg_mem' := ⋯ }
Instances For
@[simp]
theorem
Subring.mem_op
{R : Type u_2}
[Ring R]
{x : Rᵐᵒᵖ}
{S : Subring R}
:
x ∈ S.op ↔ MulOpposite.unop x ∈ S
Pull an opposite subring back to a subring along MulOpposite.op
Equations
- S.unop = { toSubsemiring := S.unop, neg_mem' := ⋯ }
Instances For
@[simp]
theorem
Subring.mem_unop
{R : Type u_2}
[Ring R]
{x : R}
{S : Subring Rᵐᵒᵖ}
:
x ∈ S.unop ↔ MulOpposite.op x ∈ S
Lattice results #
@[simp]
theorem
Subring.opEquiv_symm_apply
{R : Type u_2}
[Ring R]
(S : Subring Rᵐᵒᵖ)
:
(RelIso.symm Subring.opEquiv) S = S.unop
theorem
Subring.op_closure
{R : Type u_2}
[Ring R]
(s : Set R)
:
(Subring.closure s).op = Subring.closure (MulOpposite.unop ⁻¹' s)
theorem
Subring.unop_closure
{R : Type u_2}
[Ring R]
(s : Set Rᵐᵒᵖ)
:
(Subring.closure s).unop = Subring.closure (MulOpposite.op ⁻¹' s)
@[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
@[simp]
theorem
Subring.addEquivOp_apply_coe
{R : Type u_2}
[Ring R]
(S : Subring R)
(a : ↥S.toSubmonoid)
:
↑(S.addEquivOp a) = MulOpposite.op ↑a
@[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)
@[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)
Bijection between a subring S
and MulOpposite
of its opposite.
Equations
- S.ringEquivOpMop = S.ringEquivOpMop
Instances For
@[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)
@[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)
Bijection between MulOpposite
of a subring S
and its opposite.
Equations
- S.mopRingEquivOp = S.mopRingEquivOp