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} [AddZeroClass M] (x : AddSubmonoid M) : ∀ {a b : Mᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑x.toAddSubsemigroup → b ∈ AddOpposite.unop ⁻¹' ↑x.toAddSubsemigroup → AddOpposite.unop b + AddOpposite.unop a ∈ x

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubmonoid.op_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) : ↑(AddSubmonoid.op x) = AddOpposite.unop ⁻¹' ↑x.toAddSubsemigroup

@[simp]

theorem Submonoid.op_coe {M : Type u_2} [MulOneClass M] (x : Submonoid M) : ↑(Submonoid.op x) = MulOpposite.unop ⁻¹' ↑x.toSubsemigroup

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

• One or more equations did not get rendered due to their size.

theorem AddSubmonoid.unop.proof_1 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) : ∀ {a b : M}, a ∈ AddOpposite.op ⁻¹' ↑x.toAddSubsemigroup → b ∈ AddOpposite.op ⁻¹' ↑x.toAddSubsemigroup → { unop' := b } + { unop' := a } ∈ x

theorem AddSubmonoid.unop.proof_2 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) : 0 ∈ x.carrier

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubmonoid.unop_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) : ↑(AddSubmonoid.unop x) = AddOpposite.op ⁻¹' ↑x.toAddSubsemigroup

@[simp]

theorem Submonoid.unop_coe {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) : ↑(Submonoid.unop x) = MulOpposite.op ⁻¹' ↑x.toSubsemigroup

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

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubmonoid.opEquiv.proof_2 {M : Type u_1} [AddZeroClass M] : ∀ (x : AddSubmonoid Mᵃᵒᵖ), AddSubmonoid.op (AddSubmonoid.unop x) = x

theorem AddSubmonoid.opEquiv.proof_1 {M : Type u_1} [AddZeroClass M] : ∀ (x : AddSubmonoid M), AddSubmonoid.unop (AddSubmonoid.op x) = x

@[simp]

theorem AddSubmonoid.opEquiv_symm_apply {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) : ↑AddSubmonoid.opEquiv.symm x = AddSubmonoid.unop x

@[simp]

theorem AddSubmonoid.opEquiv_apply {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid M) : ↑AddSubmonoid.opEquiv x = AddSubmonoid.op x

@[simp]

theorem Submonoid.opEquiv_symm_apply {M : Type u_1} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) : ↑Submonoid.opEquiv.symm x = Submonoid.unop x

@[simp]

theorem Submonoid.opEquiv_apply {M : Type u_1} [MulOneClass M] (x : Submonoid M) : ↑Submonoid.opEquiv x = Submonoid.op x

def Submonoid.opEquiv {M : Type u_1} [MulOneClass M] : Submonoid M ≃ Submonoid Mᵐᵒᵖ

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

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubmonoid.equivOp.proof_1 {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) : ∀ (x : M), x ∈ H ↔ x ∈ H

def AddSubmonoid.equivOp {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) : { x // x ∈ H } ≃ { x // x ∈ AddSubmonoid.op H }

Bijection between an additive submonoid H and its opposite.

Equations

• AddSubmonoid.equivOp H = Equiv.subtypeEquiv AddOpposite.opEquiv (_ : ∀ (x : M), x ∈ H ↔ x ∈ H)

@[simp]

theorem AddSubmonoid.equivOp_symm_apply_coe {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) (b : { b // (fun x => x ∈ AddSubmonoid.op H) b }) : ↑(↑(AddSubmonoid.equivOp H).symm b) = AddOpposite.unop ↑b

@[simp]

theorem Submonoid.equivOp_symm_apply_coe {M : Type u_1} [MulOneClass M] (H : Submonoid M) (b : { b // (fun x => x ∈ Submonoid.op H) b }) : ↑(↑(Submonoid.equivOp H).symm b) = MulOpposite.unop ↑b

@[simp]

theorem Submonoid.equivOp_apply_coe {M : Type u_1} [MulOneClass M] (H : Submonoid M) (a : { a // (fun x => x ∈ H) a }) : ↑(↑(Submonoid.equivOp H) a) = MulOpposite.op ↑a

@[simp]

theorem AddSubmonoid.equivOp_apply_coe {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) (a : { a // (fun x => x ∈ H) a }) : ↑(↑(AddSubmonoid.equivOp H) a) = AddOpposite.op ↑a

def Submonoid.equivOp {M : Type u_1} [MulOneClass M] (H : Submonoid M) : { x // x ∈ H } ≃ { x // x ∈ Submonoid.op H }

Bijection between a submonoid H and its opposite.

Equations

• Submonoid.equivOp H = Equiv.subtypeEquiv MulOpposite.opEquiv (_ : ∀ (x : M), x ∈ H ↔ x ∈ H)