# Submonoid of opposite monoids #

For every monoid `M`, we construct an equivalence between submonoids of `M` and that of `Mᵐᵒᵖ`.

source
def Submonoid.op {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
Submonoid M ᵐᵒᵖ

Pull a submonoid back to an opposite submonoid along `MulOpposite.unop`

Equations

- x.op = { carrier := MulOpposite.unop ⁻¹' ↑x, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source
def AddSubmonoid.op {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
AddSubmonoid M ᵃᵒᵖ

Pull an additive submonoid back to an opposite submonoid along `AddOpposite.unop`

Equations

- x.op = { carrier := AddOpposite.unop ⁻¹' ↑x, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source
@[simp]
theorem Submonoid.coe_op {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
↑x.op = MulOpposite.unop ⁻¹' ↑x
source
@[simp]
theorem AddSubmonoid.coe_op {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
↑x.op = AddOpposite.unop ⁻¹' ↑x
source
@[simp]
theorem Submonoid.mem_op {M : Type u_2} [MulOneClass M] {x : M ᵐᵒᵖ} {S : Submonoid M} :
x ∈ S.op ↔ MulOpposite.unop x ∈ S
source
@[simp]
theorem AddSubmonoid.mem_op {M : Type u_2} [AddZeroClass M] {x : M ᵃᵒᵖ} {S : AddSubmonoid M} :
x ∈ S.op ↔ AddOpposite.unop x ∈ S
source
def Submonoid.unop {M : Type u_2} [MulOneClass M] (x : Submonoid M ᵐᵒᵖ) :
Submonoid M

Pull an opposite submonoid back to a submonoid along `MulOpposite.op`

Equations

- x.unop = { carrier := MulOpposite.op ⁻¹' ↑x, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source
def AddSubmonoid.unop {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M ᵃᵒᵖ) :
AddSubmonoid M

Pull an opposite additive submonoid back to a submonoid along `AddOpposite.op`

Equations

- x.unop = { carrier := AddOpposite.op ⁻¹' ↑x, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source
@[simp]
theorem AddSubmonoid.coe_unop {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M ᵃᵒᵖ) :
↑x.unop = AddOpposite.op ⁻¹' ↑x
source
@[simp]
theorem Submonoid.coe_unop {M : Type u_2} [MulOneClass M] (x : Submonoid M ᵐᵒᵖ) :
↑x.unop = MulOpposite.op ⁻¹' ↑x
source
@[simp]
theorem Submonoid.mem_unop {M : Type u_2} [MulOneClass M] {x : M} {S : Submonoid M ᵐᵒᵖ} :
x ∈ S.unop ↔ MulOpposite.op x ∈ S
source
@[simp]
theorem AddSubmonoid.mem_unop {M : Type u_2} [AddZeroClass M] {x : M} {S : AddSubmonoid M ᵃᵒᵖ} :
x ∈ S.unop ↔ AddOpposite.op x ∈ S
source
@[simp]
theorem Submonoid.unop_op {M : Type u_2} [MulOneClass M] (S : Submonoid M) :
S.op.unop = S
source
@[simp]
theorem AddSubmonoid.unop_op {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid M) :
S.op.unop = S
source
@[simp]
theorem Submonoid.op_unop {M : Type u_2} [MulOneClass M] (S : Submonoid M ᵐᵒᵖ) :
S.unop.op = S
source
@[simp]
theorem AddSubmonoid.op_unop {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid M ᵃᵒᵖ) :
S.unop.op = S

### Lattice results #

source
theorem Submonoid.op_le_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid M ᵐᵒᵖ} :
S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
source
theorem AddSubmonoid.op_le_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid M ᵃᵒᵖ} :
S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
source
theorem Submonoid.le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M ᵐᵒᵖ} {S₂ : Submonoid M} :
S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
source
theorem AddSubmonoid.le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M ᵃᵒᵖ} {S₂ : AddSubmonoid M} :
S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
source
@[simp]
theorem Submonoid.op_le_op_iff {M : Type u_2} [MulOneClass M] {S₁ S₂ : Submonoid M} :
S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
source
@[simp]
theorem AddSubmonoid.op_le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ S₂ : AddSubmonoid M} :
S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
source
@[simp]
theorem Submonoid.unop_le_unop_iff {M : Type u_2} [MulOneClass M] {S₁ S₂ : Submonoid M ᵐᵒᵖ} :
S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
source
@[simp]
theorem AddSubmonoid.unop_le_unop_iff {M : Type u_2} [AddZeroClass M] {S₁ S₂ : AddSubmonoid M ᵃᵒᵖ} :
S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂
source
def Submonoid.opEquiv {M : Type u_2} [MulOneClass M] :
Submonoid M ≃o Submonoid M ᵐᵒᵖ

A submonoid `H` of `G` determines a submonoid `H.op` of the opposite group `Gᵐᵒᵖ`.

Equations

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

Instances For

source
def AddSubmonoid.opEquiv {M : Type u_2} [AddZeroClass M] :
AddSubmonoid M ≃o AddSubmonoid M ᵃᵒᵖ

A additive submonoid `H` of `G` determines an additive submonoid `H.op` of the opposite group `Gᵐᵒᵖ`.

Equations

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

Instances For

source
@[simp]
theorem Submonoid.opEquiv_symm_apply {M : Type u_2} [MulOneClass M] (x : Submonoid M ᵐᵒᵖ) :
(RelIso.symm opEquiv) x = x.unop
source
@[simp]
theorem AddSubmonoid.opEquiv_symm_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M ᵃᵒᵖ) :
(RelIso.symm opEquiv) x = x.unop
source
@[simp]
theorem AddSubmonoid.opEquiv_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :
opEquiv x = x.op
source
@[simp]
theorem Submonoid.opEquiv_apply {M : Type u_2} [MulOneClass M] (x : Submonoid M) :
opEquiv x = x.op
source
theorem Submonoid.op_injective {M : Type u_2} [MulOneClass M] :
Function.Injective Submonoid.op
source
theorem AddSubmonoid.op_injective {M : Type u_2} [AddZeroClass M] :
Function.Injective AddSubmonoid.op
source
theorem Submonoid.unop_injective {M : Type u_2} [MulOneClass M] :
Function.Injective Submonoid.unop
source
theorem AddSubmonoid.unop_injective {M : Type u_2} [AddZeroClass M] :
Function.Injective AddSubmonoid.unop
source
@[simp]
theorem Submonoid.op_inj {M : Type u_2} [MulOneClass M] {S T : Submonoid M} :
S.op = T.op ↔ S = T
source
@[simp]
theorem AddSubmonoid.op_inj {M : Type u_2} [AddZeroClass M] {S T : AddSubmonoid M} :
S.op = T.op ↔ S = T
source
@[simp]
theorem Submonoid.unop_inj {M : Type u_2} [MulOneClass M] {S T : Submonoid M ᵐᵒᵖ} :
S.unop = T.unop ↔ S = T
source
@[simp]
theorem AddSubmonoid.unop_inj {M : Type u_2} [AddZeroClass M] {S T : AddSubmonoid M ᵃᵒᵖ} :
S.unop = T.unop ↔ S = T
source
@[simp]
theorem Submonoid.op_bot {M : Type u_2} [MulOneClass M] :
⊥.op = ⊥
source
@[simp]
theorem AddSubmonoid.op_bot {M : Type u_2} [AddZeroClass M] :
⊥.op = ⊥
source
@[simp]
theorem Submonoid.op_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
S.op = ⊥ ↔ S = ⊥
source
@[simp]
theorem AddSubmonoid.op_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
S.op = ⊥ ↔ S = ⊥
source
@[simp]
theorem Submonoid.unop_bot {M : Type u_2} [MulOneClass M] :
⊥.unop = ⊥
source
@[simp]
theorem AddSubmonoid.unop_bot {M : Type u_2} [AddZeroClass M] :
⊥.unop = ⊥
source
@[simp]
theorem Submonoid.unop_eq_bot {M : Type u_2} [MulOneClass M] {S : Submonoid M ᵐᵒᵖ} :
S.unop = ⊥ ↔ S = ⊥
source
@[simp]
theorem AddSubmonoid.unop_eq_bot {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M ᵃᵒᵖ} :
S.unop = ⊥ ↔ S = ⊥
source
@[simp]
theorem Submonoid.op_top {M : Type u_2} [MulOneClass M] :
⊤.op = ⊤
source
@[simp]
theorem AddSubmonoid.op_top {M : Type u_2} [AddZeroClass M] :
⊤.op = ⊤
source
@[simp]
theorem Submonoid.op_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid M} :
S.op = ⊤ ↔ S = ⊤
source
@[simp]
theorem AddSubmonoid.op_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M} :
S.op = ⊤ ↔ S = ⊤
source
@[simp]
theorem Submonoid.unop_top {M : Type u_2} [MulOneClass M] :
⊤.unop = ⊤
source
@[simp]
theorem AddSubmonoid.unop_top {M : Type u_2} [AddZeroClass M] :
⊤.unop = ⊤
source
@[simp]
theorem Submonoid.unop_eq_top {M : Type u_2} [MulOneClass M] {S : Submonoid M ᵐᵒᵖ} :
S.unop = ⊤ ↔ S = ⊤
source
@[simp]
theorem AddSubmonoid.unop_eq_top {M : Type u_2} [AddZeroClass M] {S : AddSubmonoid M ᵃᵒᵖ} :
S.unop = ⊤ ↔ S = ⊤
source
theorem Submonoid.op_sup {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M) :
(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
source
theorem AddSubmonoid.op_sup {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M) :
(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
source
theorem Submonoid.unop_sup {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M ᵐᵒᵖ) :
(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
source
theorem AddSubmonoid.unop_sup {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M ᵃᵒᵖ) :
(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
source
theorem Submonoid.op_inf {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M) :
(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
source
theorem AddSubmonoid.op_inf {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M) :
(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
source
theorem Submonoid.unop_inf {M : Type u_2} [MulOneClass M] (S₁ S₂ : Submonoid M ᵐᵒᵖ) :
(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
source
theorem AddSubmonoid.unop_inf {M : Type u_2} [AddZeroClass M] (S₁ S₂ : AddSubmonoid M ᵃᵒᵖ) :
(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
source
theorem Submonoid.op_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
(sSup S).op = sSup (Submonoid.unop ⁻¹' S)
source
theorem AddSubmonoid.op_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
(sSup S).op = sSup (AddSubmonoid.unop ⁻¹' S)
source
theorem Submonoid.unop_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M ᵐᵒᵖ)) :
(sSup S).unop = sSup (Submonoid.op ⁻¹' S)
source
theorem AddSubmonoid.unop_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M ᵃᵒᵖ)) :
(sSup S).unop = sSup (AddSubmonoid.op ⁻¹' S)
source
theorem Submonoid.op_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :
(sInf S).op = sInf (Submonoid.unop ⁻¹' S)
source
theorem AddSubmonoid.op_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :
(sInf S).op = sInf (AddSubmonoid.unop ⁻¹' S)
source
theorem Submonoid.unop_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M ᵐᵒᵖ)) :
(sInf S).unop = sInf (Submonoid.op ⁻¹' S)
source
theorem AddSubmonoid.unop_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M ᵃᵒᵖ)) :
(sInf S).unop = sInf (AddSubmonoid.op ⁻¹' S)
source
theorem Submonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :
(iSup S).op = ⨆ (i : ι), (S i).op
source
theorem AddSubmonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :
(iSup S).op = ⨆ (i : ι), (S i).op
source
theorem Submonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M ᵐᵒᵖ) :
(iSup S).unop = ⨆ (i : ι), (S i).unop
source
theorem AddSubmonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M ᵃᵒᵖ) :
(iSup S).unop = ⨆ (i : ι), (S i).unop
source
theorem Submonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :
(iInf S).op = ⨅ (i : ι), (S i).op
source
theorem AddSubmonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :
(iInf S).op = ⨅ (i : ι), (S i).op
source
theorem Submonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M ᵐᵒᵖ) :
(iInf S).unop = ⨅ (i : ι), (S i).unop
source
theorem AddSubmonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M ᵃᵒᵖ) :
(iInf S).unop = ⨅ (i : ι), (S i).unop
source
theorem Submonoid.op_closure {M : Type u_2} [MulOneClass M] (s : Set M) :
(closure s).op = closure (MulOpposite.unop ⁻¹' s)
source
theorem AddSubmonoid.op_closure {M : Type u_2} [AddZeroClass M] (s : Set M) :
(closure s).op = closure (AddOpposite.unop ⁻¹' s)
source
theorem Submonoid.unop_closure {M : Type u_2} [MulOneClass M] (s : Set M ᵐᵒᵖ) :
(closure s).unop = closure (MulOpposite.op ⁻¹' s)
source
theorem AddSubmonoid.unop_closure {M : Type u_2} [AddZeroClass M] (s : Set M ᵃᵒᵖ) :
(closure s).unop = closure (AddOpposite.op ⁻¹' s)
source
def Submonoid.equivOp {M : Type u_2} [MulOneClass M] (H : Submonoid M) :
↥H ≃ ↥H.op

Bijection between a submonoid `H` and its opposite.

Equations

- H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯

Instances For

source
def AddSubmonoid.equivOp {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) :
↥H ≃ ↥H.op

Bijection between an additive submonoid `H` and its opposite.

Equations

- H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯

Instances For

source
@[simp]
theorem Submonoid.equivOp_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (a : ↥H) :
↑(H.equivOp a) = MulOpposite.op ↑a
source
@[simp]
theorem AddSubmonoid.equivOp_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (a : ↥H) :
↑(H.equivOp a) = AddOpposite.op ↑a
source
@[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
source
@[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