# Submonoid of opposite monoids #

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

theorem AddSubmonoid.op.proof_1 {M : Type u_1} [] (x : ) :
∀ {a b : Mᵃᵒᵖ}, a AddOpposite.unop ⁻¹' xb AddOpposite.unop ⁻¹' xb.unop + a.unop x
def AddSubmonoid.op {M : Type u_2} [] (x : ) :

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
@[simp]
theorem AddSubmonoid.op_coe {M : Type u_2} [] (x : ) :
@[simp]
theorem Submonoid.op_coe {M : Type u_2} [] (x : ) :
x.op = MulOpposite.unop ⁻¹' x
def Submonoid.op {M : Type u_2} [] (x : ) :

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

Equations
• x.op = { carrier := MulOpposite.unop ⁻¹' x, mul_mem' := , one_mem' := }
Instances For
@[simp]
theorem AddSubmonoid.mem_op {M : Type u_2} [] {x : Mᵃᵒᵖ} {S : } :
x S.op x.unop S
@[simp]
theorem Submonoid.mem_op {M : Type u_2} [] {x : Mᵐᵒᵖ} {S : } :
x S.op x.unop S
def AddSubmonoid.unop {M : Type u_2} [] (x : ) :

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
theorem AddSubmonoid.unop.proof_2 {M : Type u_1} [] (x : ) :
0 x.carrier
theorem AddSubmonoid.unop.proof_1 {M : Type u_1} [] (x : ) :
∀ {a b : M}, a AddOpposite.op ⁻¹' xb AddOpposite.op ⁻¹' x{ unop' := b } + { unop' := a } x
@[simp]
theorem AddSubmonoid.unop_coe {M : Type u_2} [] (x : ) :
@[simp]
theorem Submonoid.unop_coe {M : Type u_2} [] (x : ) :
x.unop = MulOpposite.op ⁻¹' x
def Submonoid.unop {M : Type u_2} [] (x : ) :

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

Equations
• x.unop = { carrier := MulOpposite.op ⁻¹' x, mul_mem' := , one_mem' := }
Instances For
@[simp]
theorem AddSubmonoid.mem_unop {M : Type u_2} [] {x : M} {S : } :
x S.unop
@[simp]
theorem Submonoid.mem_unop {M : Type u_2} [] {x : M} {S : } :
x S.unop
@[simp]
theorem AddSubmonoid.unop_op {M : Type u_2} [] (S : ) :
S.op.unop = S
@[simp]
theorem Submonoid.unop_op {M : Type u_2} [] (S : ) :
S.op.unop = S
@[simp]
theorem AddSubmonoid.op_unop {M : Type u_2} [] (S : ) :
S.unop.op = S
@[simp]
theorem Submonoid.op_unop {M : Type u_2} [] (S : ) :
S.unop.op = S

### Lattice results #

theorem AddSubmonoid.op_le_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁.op S₂ S₁ S₂.unop
theorem Submonoid.op_le_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁.op S₂ S₁ S₂.unop
theorem AddSubmonoid.le_op_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁ S₂.op S₁.unop S₂
theorem Submonoid.le_op_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁ S₂.op S₁.unop S₂
@[simp]
theorem AddSubmonoid.op_le_op_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁.op S₂.op S₁ S₂
@[simp]
theorem Submonoid.op_le_op_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁.op S₂.op S₁ S₂
@[simp]
theorem AddSubmonoid.unop_le_unop_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁.unop S₂.unop S₁ S₂
@[simp]
theorem Submonoid.unop_le_unop_iff {M : Type u_2} [] {S₁ : } {S₂ : } :
S₁.unop S₂.unop S₁ S₂
def AddSubmonoid.opEquiv {M : Type u_2} [] :

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
@[simp]
theorem Submonoid.opEquiv_symm_apply {M : Type u_2} [] (x : ) :
(RelIso.symm Submonoid.opEquiv) x = x.unop
@[simp]
theorem AddSubmonoid.opEquiv_symm_apply {M : Type u_2} [] (x : ) :
@[simp]
theorem AddSubmonoid.opEquiv_apply {M : Type u_2} [] (x : ) :
@[simp]
theorem Submonoid.opEquiv_apply {M : Type u_2} [] (x : ) :
Submonoid.opEquiv x = x.op
def Submonoid.opEquiv {M : Type u_2} [] :

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
@[simp]
theorem AddSubmonoid.op_bot {M : Type u_2} [] :
.op =
@[simp]
theorem Submonoid.op_bot {M : Type u_2} [] :
.op =
@[simp]
theorem AddSubmonoid.unop_bot {M : Type u_2} [] :
.unop =
@[simp]
theorem Submonoid.unop_bot {M : Type u_2} [] :
.unop =
@[simp]
theorem AddSubmonoid.op_top {M : Type u_2} [] :
.op =
@[simp]
theorem Submonoid.op_top {M : Type u_2} [] :
.op =
@[simp]
theorem AddSubmonoid.unop_top {M : Type u_2} [] :
.unop =
@[simp]
theorem Submonoid.unop_top {M : Type u_2} [] :
.unop =
theorem AddSubmonoid.op_sup {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).op = S₁.op S₂.op
theorem Submonoid.op_sup {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).op = S₁.op S₂.op
theorem AddSubmonoid.unop_sup {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).unop = S₁.unop S₂.unop
theorem Submonoid.unop_sup {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).unop = S₁.unop S₂.unop
theorem AddSubmonoid.op_inf {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).op = S₁.op S₂.op
theorem Submonoid.op_inf {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).op = S₁.op S₂.op
theorem AddSubmonoid.unop_inf {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).unop = S₁.unop S₂.unop
theorem Submonoid.unop_inf {M : Type u_2} [] (S₁ : ) (S₂ : ) :
(S₁ S₂).unop = S₁.unop S₂.unop
theorem AddSubmonoid.op_sSup {M : Type u_2} [] (S : Set ()) :
(sSup S).op = sSup (AddSubmonoid.unop ⁻¹' S)
theorem Submonoid.op_sSup {M : Type u_2} [] (S : Set ()) :
(sSup S).op = sSup (Submonoid.unop ⁻¹' S)
theorem AddSubmonoid.unop_sSup {M : Type u_2} [] (S : ) :
(sSup S).unop = sSup (AddSubmonoid.op ⁻¹' S)
theorem Submonoid.unop_sSup {M : Type u_2} [] (S : Set ()) :
(sSup S).unop = sSup (Submonoid.op ⁻¹' S)
theorem AddSubmonoid.op_sInf {M : Type u_2} [] (S : Set ()) :
(sInf S).op = sInf (AddSubmonoid.unop ⁻¹' S)
theorem Submonoid.op_sInf {M : Type u_2} [] (S : Set ()) :
(sInf S).op = sInf (Submonoid.unop ⁻¹' S)
theorem AddSubmonoid.unop_sInf {M : Type u_2} [] (S : ) :
(sInf S).unop = sInf (AddSubmonoid.op ⁻¹' S)
theorem Submonoid.unop_sInf {M : Type u_2} [] (S : Set ()) :
(sInf S).unop = sInf (Submonoid.op ⁻¹' S)
theorem AddSubmonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iSup S).op = ⨆ (i : ι), (S i).op
theorem Submonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iSup S).op = ⨆ (i : ι), (S i).op
theorem AddSubmonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iSup S).unop = ⨆ (i : ι), (S i).unop
theorem Submonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iSup S).unop = ⨆ (i : ι), (S i).unop
theorem AddSubmonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iInf S).op = ⨅ (i : ι), (S i).op
theorem Submonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iInf S).op = ⨅ (i : ι), (S i).op
theorem AddSubmonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iInf S).unop = ⨅ (i : ι), (S i).unop
theorem Submonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [] (S : ι) :
(iInf S).unop = ⨅ (i : ι), (S i).unop
theorem AddSubmonoid.op_closure {M : Type u_2} [] (s : Set M) :
theorem Submonoid.op_closure {M : Type u_2} [] (s : Set M) :
.op = Submonoid.closure (MulOpposite.unop ⁻¹' s)
theorem AddSubmonoid.unop_closure {M : Type u_2} [] (s : ) :
theorem Submonoid.unop_closure {M : Type u_2} [] (s : ) :
.unop = Submonoid.closure (MulOpposite.op ⁻¹' s)
def AddSubmonoid.equivOp {M : Type u_2} [] (H : ) :
H H.op

Bijection between an additive submonoid H and its opposite.

Equations
Instances For
theorem AddSubmonoid.equivOp.proof_1 {M : Type u_1} [] (H : ) :
∀ (x : M), x H x H
@[simp]
theorem AddSubmonoid.equivOp_symm_apply_coe {M : Type u_2} [] (H : ) (b : { b : Mᵃᵒᵖ // (fun (x : Mᵃᵒᵖ) => x H.op) b }) :
(H.equivOp.symm b) = (b).unop
@[simp]
theorem Submonoid.equivOp_symm_apply_coe {M : Type u_2} [] (H : ) (b : { b : Mᵐᵒᵖ // (fun (x : Mᵐᵒᵖ) => x H.op) b }) :
(H.equivOp.symm b) = (b).unop
@[simp]
theorem Submonoid.equivOp_apply_coe {M : Type u_2} [] (H : ) (a : { a : M // (fun (x : M) => x H) a }) :
(H.equivOp a) =
@[simp]
theorem AddSubmonoid.equivOp_apply_coe {M : Type u_2} [] (H : ) (a : { a : M // (fun (x : M) => x H) a }) :
(H.equivOp a) =
def Submonoid.equivOp {M : Type u_2} [] (H : ) :
H H.op

Bijection between a submonoid H and its opposite.

Equations
• H.equivOp = MulOpposite.opEquiv.subtypeEquiv
Instances For