Submonoid of opposite monoids #
For every monoid M
, we construct an equivalence between submonoids of M
and that of Mᵐᵒᵖ
.
Pull a submonoid back to an opposite submonoid along MulOpposite.unop
Instances For
Pull an additive submonoid back to an opposite submonoid along
AddOpposite.unop
Instances For
@[simp]
@[simp]
@[simp]
theorem
Submonoid.mem_op
{M : Type u_2}
[MulOneClass M]
{x : Mᵐᵒᵖ}
{S : Submonoid M}
:
x ∈ S.op ↔ MulOpposite.unop x ∈ S
@[simp]
theorem
AddSubmonoid.mem_op
{M : Type u_2}
[AddZeroClass M]
{x : Mᵃᵒᵖ}
{S : AddSubmonoid M}
:
x ∈ S.op ↔ AddOpposite.unop x ∈ S
Pull an opposite submonoid back to a submonoid along MulOpposite.op
Instances For
Pull an opposite additive submonoid back to a submonoid along
AddOpposite.op
Instances For
@[simp]
@[simp]
@[simp]
theorem
Submonoid.mem_unop
{M : Type u_2}
[MulOneClass M]
{x : M}
{S : Submonoid Mᵐᵒᵖ}
:
x ∈ S.unop ↔ MulOpposite.op x ∈ S
@[simp]
theorem
AddSubmonoid.mem_unop
{M : Type u_2}
[AddZeroClass M]
{x : M}
{S : AddSubmonoid Mᵃᵒᵖ}
:
x ∈ S.unop ↔ AddOpposite.op x ∈ S
@[simp]
@[simp]
@[simp]
@[simp]
Lattice results #
theorem
Submonoid.op_le_iff
{M : Type u_2}
[MulOneClass M]
{S₁ : Submonoid M}
{S₂ : Submonoid Mᵐᵒᵖ}
:
theorem
AddSubmonoid.op_le_iff
{M : Type u_2}
[AddZeroClass M]
{S₁ : AddSubmonoid M}
{S₂ : AddSubmonoid Mᵃᵒᵖ}
:
theorem
Submonoid.le_op_iff
{M : Type u_2}
[MulOneClass M]
{S₁ : Submonoid Mᵐᵒᵖ}
{S₂ : Submonoid M}
:
theorem
AddSubmonoid.le_op_iff
{M : Type u_2}
[AddZeroClass M]
{S₁ : AddSubmonoid Mᵃᵒᵖ}
{S₂ : AddSubmonoid M}
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Submonoid.opEquiv_apply
{M : Type u_2}
[MulOneClass M]
(x : Submonoid M)
:
Submonoid.opEquiv x = x.op
@[simp]
theorem
Submonoid.opEquiv_symm_apply
{M : Type u_2}
[MulOneClass M]
(x : Submonoid Mᵐᵒᵖ)
:
(RelIso.symm Submonoid.opEquiv) x = x.unop
@[simp]
theorem
AddSubmonoid.opEquiv_symm_apply
{M : Type u_2}
[AddZeroClass M]
(x : AddSubmonoid Mᵃᵒᵖ)
:
(RelIso.symm AddSubmonoid.opEquiv) x = x.unop
@[simp]
theorem
AddSubmonoid.opEquiv_apply
{M : Type u_2}
[AddZeroClass M]
(x : AddSubmonoid M)
:
AddSubmonoid.opEquiv x = x.op
theorem
AddSubmonoid.op_injective
{M : Type u_2}
[AddZeroClass M]
:
Function.Injective AddSubmonoid.op
theorem
AddSubmonoid.unop_injective
{M : Type u_2}
[AddZeroClass M]
:
Function.Injective AddSubmonoid.unop
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
AddSubmonoid.op_iSup
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid M)
:
theorem
Submonoid.unop_iSup
{ι : Sort u_1}
{M : Type u_2}
[MulOneClass M]
(S : ι → Submonoid Mᵐᵒᵖ)
:
theorem
AddSubmonoid.unop_iSup
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid Mᵃᵒᵖ)
:
theorem
AddSubmonoid.op_iInf
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid M)
:
theorem
Submonoid.unop_iInf
{ι : Sort u_1}
{M : Type u_2}
[MulOneClass M]
(S : ι → Submonoid Mᵐᵒᵖ)
:
theorem
AddSubmonoid.unop_iInf
{ι : Sort u_1}
{M : Type u_2}
[AddZeroClass M]
(S : ι → AddSubmonoid Mᵃᵒᵖ)
:
theorem
Submonoid.op_closure
{M : Type u_2}
[MulOneClass M]
(s : Set M)
:
(Submonoid.closure s).op = Submonoid.closure (MulOpposite.unop ⁻¹' s)
theorem
AddSubmonoid.op_closure
{M : Type u_2}
[AddZeroClass M]
(s : Set M)
:
(AddSubmonoid.closure s).op = AddSubmonoid.closure (AddOpposite.unop ⁻¹' s)
theorem
Submonoid.unop_closure
{M : Type u_2}
[MulOneClass M]
(s : Set Mᵐᵒᵖ)
:
(Submonoid.closure s).unop = Submonoid.closure (MulOpposite.op ⁻¹' s)
theorem
AddSubmonoid.unop_closure
{M : Type u_2}
[AddZeroClass M]
(s : Set Mᵃᵒᵖ)
:
(AddSubmonoid.closure s).unop = AddSubmonoid.closure (AddOpposite.op ⁻¹' s)
Bijection between a submonoid H
and its opposite.
Equations
- H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯
Instances For
Bijection between an additive submonoid H
and its opposite.
Equations
- H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯
Instances For
@[simp]
theorem
AddSubmonoid.equivOp_symm_apply_coe
{M : Type u_2}
[AddZeroClass M]
(H : AddSubmonoid M)
(b : ↥H.op)
:
↑(H.equivOp.symm b) = AddOpposite.unop ↑b
@[simp]
theorem
AddSubmonoid.equivOp_apply_coe
{M : Type u_2}
[AddZeroClass M]
(H : AddSubmonoid M)
(a : ↥H)
:
↑(H.equivOp a) = AddOpposite.op ↑a
@[simp]
theorem
Submonoid.equivOp_apply_coe
{M : Type u_2}
[MulOneClass M]
(H : Submonoid M)
(a : ↥H)
:
↑(H.equivOp a) = MulOpposite.op ↑a
@[simp]
theorem
Submonoid.equivOp_symm_apply_coe
{M : Type u_2}
[MulOneClass M]
(H : Submonoid M)
(b : ↥H.op)
:
↑(H.equivOp.symm b) = MulOpposite.unop ↑b