Submonoid of opposite monoids #

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

source

theorem AddSubmonoid.op.proof_1 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid M) :

∀ {a b : Mᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑x → b ∈ AddOpposite.unop ⁻¹' ↑x → AddOpposite.unop b + AddOpposite.unop a ∈ x

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

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

Instances For

source

@[simp]

theorem AddSubmonoid.op_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :

↑(AddSubmonoid.op x) = AddOpposite.unop ⁻¹' ↑x

source

@[simp]

theorem Submonoid.op_coe {M : Type u_2} [MulOneClass M] (x : Submonoid M) :

↑(Submonoid.op x) = MulOpposite.unop ⁻¹' ↑x

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

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

Instances For

source

@[simp]

theorem AddSubmonoid.mem_op {M : Type u_2} [AddZeroClass M] {x : Mᵃᵒᵖ} {S : AddSubmonoid M} :

x ∈ AddSubmonoid.op S ↔ AddOpposite.unop x ∈ S

source

@[simp]

theorem Submonoid.mem_op {M : Type u_2} [MulOneClass M] {x : Mᵐᵒᵖ} {S : Submonoid M} :

x ∈ Submonoid.op S ↔ MulOpposite.unop x ∈ S

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

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

Instances For

source

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

0 ∈ x.carrier

source

theorem AddSubmonoid.unop.proof_1 {M : Type u_1} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :

∀ {a b : M}, a ∈ AddOpposite.op ⁻¹' ↑x → b ∈ AddOpposite.op ⁻¹' ↑x → { unop' := b } + { unop' := a } ∈ x

source

@[simp]

theorem AddSubmonoid.unop_coe {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :

↑(AddSubmonoid.unop x) = AddOpposite.op ⁻¹' ↑x

source

@[simp]

theorem Submonoid.unop_coe {M : Type u_2} [MulOneClass M] (x : Submonoid Mᵐᵒᵖ) :

↑(Submonoid.unop x) = MulOpposite.op ⁻¹' ↑x

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

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

Instances For

source

@[simp]

theorem AddSubmonoid.mem_unop {M : Type u_2} [AddZeroClass M] {x : M} {S : AddSubmonoid Mᵃᵒᵖ} :

x ∈ AddSubmonoid.unop S ↔ AddOpposite.op x ∈ S

source

@[simp]

theorem Submonoid.mem_unop {M : Type u_2} [MulOneClass M] {x : M} {S : Submonoid Mᵐᵒᵖ} :

x ∈ Submonoid.unop S ↔ MulOpposite.op x ∈ S

source

@[simp]

theorem AddSubmonoid.unop_op {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid M) :

AddSubmonoid.unop (AddSubmonoid.op S) = S

source

@[simp]

theorem Submonoid.unop_op {M : Type u_2} [MulOneClass M] (S : Submonoid M) :

Submonoid.unop (Submonoid.op S) = S

source

@[simp]

theorem AddSubmonoid.op_unop {M : Type u_2} [AddZeroClass M] (S : AddSubmonoid Mᵃᵒᵖ) :

AddSubmonoid.op (AddSubmonoid.unop S) = S

source

@[simp]

theorem Submonoid.op_unop {M : Type u_2} [MulOneClass M] (S : Submonoid Mᵐᵒᵖ) :

Submonoid.op (Submonoid.unop S) = S

Lattice results #

source

theorem AddSubmonoid.op_le_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid Mᵃᵒᵖ} :

AddSubmonoid.op S₁ ≤ S₂ ↔ S₁ ≤ AddSubmonoid.unop S₂

source

theorem Submonoid.op_le_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} :

Submonoid.op S₁ ≤ S₂ ↔ S₁ ≤ Submonoid.unop S₂

source

theorem AddSubmonoid.le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid M} :

S₁ ≤ AddSubmonoid.op S₂ ↔ AddSubmonoid.unop S₁ ≤ S₂

source

theorem Submonoid.le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} :

S₁ ≤ Submonoid.op S₂ ↔ Submonoid.unop S₁ ≤ S₂

source

@[simp]

theorem AddSubmonoid.op_le_op_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid M} :

AddSubmonoid.op S₁ ≤ AddSubmonoid.op S₂ ↔ S₁ ≤ S₂

source

@[simp]

theorem Submonoid.op_le_op_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid M} {S₂ : Submonoid M} :

Submonoid.op S₁ ≤ Submonoid.op S₂ ↔ S₁ ≤ S₂

source

@[simp]

theorem AddSubmonoid.unop_le_unop_iff {M : Type u_2} [AddZeroClass M] {S₁ : AddSubmonoid Mᵃᵒᵖ} {S₂ : AddSubmonoid Mᵃᵒᵖ} :

AddSubmonoid.unop S₁ ≤ AddSubmonoid.unop S₂ ↔ S₁ ≤ S₂

source

@[simp]

theorem Submonoid.unop_le_unop_iff {M : Type u_2} [MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid Mᵐᵒᵖ} :

Submonoid.unop S₁ ≤ Submonoid.unop S₂ ↔ S₁ ≤ S₂

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 = { toEquiv := { 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 Submonoid.opEquiv) x = Submonoid.unop x

source

@[simp]

theorem AddSubmonoid.opEquiv_symm_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ) :

(RelIso.symm AddSubmonoid.opEquiv) x = AddSubmonoid.unop x

source

@[simp]

theorem AddSubmonoid.opEquiv_apply {M : Type u_2} [AddZeroClass M] (x : AddSubmonoid M) :

AddSubmonoid.opEquiv x = AddSubmonoid.op x

source

@[simp]

theorem Submonoid.opEquiv_apply {M : Type u_2} [MulOneClass M] (x : Submonoid M) :

Submonoid.opEquiv x = Submonoid.op x

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 = { toEquiv := { toFun := Submonoid.op, invFun := Submonoid.unop, left_inv := ⋯, right_inv := ⋯ }, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

theorem AddSubmonoid.op_bot {M : Type u_2} [AddZeroClass M] :

AddSubmonoid.op ⊥ = ⊥

source

@[simp]

theorem Submonoid.op_bot {M : Type u_2} [MulOneClass M] :

Submonoid.op ⊥ = ⊥

source

@[simp]

theorem AddSubmonoid.unop_bot {M : Type u_2} [AddZeroClass M] :

AddSubmonoid.unop ⊥ = ⊥

source

@[simp]

theorem Submonoid.unop_bot {M : Type u_2} [MulOneClass M] :

Submonoid.unop ⊥ = ⊥

source

@[simp]

theorem AddSubmonoid.op_top {M : Type u_2} [AddZeroClass M] :

AddSubmonoid.op ⊤ = ⊤

source

@[simp]

theorem Submonoid.op_top {M : Type u_2} [MulOneClass M] :

Submonoid.op ⊤ = ⊤

source

@[simp]

theorem AddSubmonoid.unop_top {M : Type u_2} [AddZeroClass M] :

AddSubmonoid.unop ⊤ = ⊤

source

@[simp]

theorem Submonoid.unop_top {M : Type u_2} [MulOneClass M] :

Submonoid.unop ⊤ = ⊤

source

theorem AddSubmonoid.op_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :

AddSubmonoid.op (S₁ ⊔ S₂) = AddSubmonoid.op S₁ ⊔ AddSubmonoid.op S₂

source

theorem Submonoid.op_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :

Submonoid.op (S₁ ⊔ S₂) = Submonoid.op S₁ ⊔ Submonoid.op S₂

source

theorem AddSubmonoid.unop_sup {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :

AddSubmonoid.unop (S₁ ⊔ S₂) = AddSubmonoid.unop S₁ ⊔ AddSubmonoid.unop S₂

source

theorem Submonoid.unop_sup {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :

Submonoid.unop (S₁ ⊔ S₂) = Submonoid.unop S₁ ⊔ Submonoid.unop S₂

source

theorem AddSubmonoid.op_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :

AddSubmonoid.op (S₁ ⊓ S₂) = AddSubmonoid.op S₁ ⊓ AddSubmonoid.op S₂

source

theorem Submonoid.op_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid M) (S₂ : Submonoid M) :

Submonoid.op (S₁ ⊓ S₂) = Submonoid.op S₁ ⊓ Submonoid.op S₂

source

theorem AddSubmonoid.unop_inf {M : Type u_2} [AddZeroClass M] (S₁ : AddSubmonoid Mᵃᵒᵖ) (S₂ : AddSubmonoid Mᵃᵒᵖ) :

AddSubmonoid.unop (S₁ ⊓ S₂) = AddSubmonoid.unop S₁ ⊓ AddSubmonoid.unop S₂

source

theorem Submonoid.unop_inf {M : Type u_2} [MulOneClass M] (S₁ : Submonoid Mᵐᵒᵖ) (S₂ : Submonoid Mᵐᵒᵖ) :

Submonoid.unop (S₁ ⊓ S₂) = Submonoid.unop S₁ ⊓ Submonoid.unop S₂

source

theorem AddSubmonoid.op_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :

AddSubmonoid.op (sSup S) = sSup (AddSubmonoid.unop ⁻¹' S)

source

theorem Submonoid.op_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :

Submonoid.op (sSup S) = sSup (Submonoid.unop ⁻¹' S)

source

theorem AddSubmonoid.unop_sSup {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :

AddSubmonoid.unop (sSup S) = sSup (AddSubmonoid.op ⁻¹' S)

source

theorem Submonoid.unop_sSup {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :

Submonoid.unop (sSup S) = sSup (Submonoid.op ⁻¹' S)

source

theorem AddSubmonoid.op_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid M)) :

AddSubmonoid.op (sInf S) = sInf (AddSubmonoid.unop ⁻¹' S)

source

theorem Submonoid.op_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid M)) :

Submonoid.op (sInf S) = sInf (Submonoid.unop ⁻¹' S)

source

theorem AddSubmonoid.unop_sInf {M : Type u_2} [AddZeroClass M] (S : Set (AddSubmonoid Mᵃᵒᵖ)) :

AddSubmonoid.unop (sInf S) = sInf (AddSubmonoid.op ⁻¹' S)

source

theorem Submonoid.unop_sInf {M : Type u_2} [MulOneClass M] (S : Set (Submonoid Mᵐᵒᵖ)) :

Submonoid.unop (sInf S) = sInf (Submonoid.op ⁻¹' S)

source

theorem AddSubmonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :

AddSubmonoid.op (iSup S) = ⨆ (i : ι), AddSubmonoid.op (S i)

source

theorem Submonoid.op_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :

Submonoid.op (iSup S) = ⨆ (i : ι), Submonoid.op (S i)

source

theorem AddSubmonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ) :

AddSubmonoid.unop (iSup S) = ⨆ (i : ι), AddSubmonoid.unop (S i)

source

theorem Submonoid.unop_iSup {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ) :

Submonoid.unop (iSup S) = ⨆ (i : ι), Submonoid.unop (S i)

source

theorem AddSubmonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid M) :

AddSubmonoid.op (iInf S) = ⨅ (i : ι), AddSubmonoid.op (S i)

source

theorem Submonoid.op_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid M) :

Submonoid.op (iInf S) = ⨅ (i : ι), Submonoid.op (S i)

source

theorem AddSubmonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [AddZeroClass M] (S : ι → AddSubmonoid Mᵃᵒᵖ) :

AddSubmonoid.unop (iInf S) = ⨅ (i : ι), AddSubmonoid.unop (S i)

source

theorem Submonoid.unop_iInf {ι : Sort u_1} {M : Type u_2} [MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ) :

Submonoid.unop (iInf S) = ⨅ (i : ι), Submonoid.unop (S i)

source

theorem AddSubmonoid.op_closure {M : Type u_2} [AddZeroClass M] (s : Set M) :

AddSubmonoid.op (AddSubmonoid.closure s) = AddSubmonoid.closure (AddOpposite.unop ⁻¹' s)

source

theorem Submonoid.op_closure {M : Type u_2} [MulOneClass M] (s : Set M) :

Submonoid.op (Submonoid.closure s) = Submonoid.closure (MulOpposite.unop ⁻¹' s)

source

theorem AddSubmonoid.unop_closure {M : Type u_2} [AddZeroClass M] (s : Set Mᵃᵒᵖ) :

AddSubmonoid.unop (AddSubmonoid.closure s) = AddSubmonoid.closure (AddOpposite.op ⁻¹' s)

source

theorem Submonoid.unop_closure {M : Type u_2} [MulOneClass M] (s : Set Mᵐᵒᵖ) :

Submonoid.unop (Submonoid.closure s) = Submonoid.closure (MulOpposite.op ⁻¹' s)

source

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

↥H ≃ ↥(AddSubmonoid.op H)

Bijection between an additive submonoid H and its opposite.

Equations

AddSubmonoid.equivOp H = Equiv.subtypeEquiv AddOpposite.opEquiv ⋯

Instances For

source

theorem AddSubmonoid.equivOp.proof_1 {M : Type u_1} [AddZeroClass M] (H : AddSubmonoid M) :

∀ (x : M), x ∈ H ↔ x ∈ H

source

@[simp]

theorem AddSubmonoid.equivOp_symm_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (b : { b : Mᵃᵒᵖ // (fun (x : Mᵃᵒᵖ) => x ∈ AddSubmonoid.op H) b }) :

↑((AddSubmonoid.equivOp H).symm b) = AddOpposite.unop ↑b

source

@[simp]

theorem Submonoid.equivOp_symm_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (b : { b : Mᵐᵒᵖ // (fun (x : Mᵐᵒᵖ) => x ∈ Submonoid.op H) b }) :

↑((Submonoid.equivOp H).symm b) = MulOpposite.unop ↑b

source

@[simp]

theorem Submonoid.equivOp_apply_coe {M : Type u_2} [MulOneClass M] (H : Submonoid M) (a : { a : M // (fun (x : M) => x ∈ H) a }) :

↑((Submonoid.equivOp H) a) = MulOpposite.op ↑a

source

@[simp]

theorem AddSubmonoid.equivOp_apply_coe {M : Type u_2} [AddZeroClass M] (H : AddSubmonoid M) (a : { a : M // (fun (x : M) => x ∈ H) a }) :

↑((AddSubmonoid.equivOp H) a) = AddOpposite.op ↑a

source

def Submonoid.equivOp {M : Type u_2} [MulOneClass M] (H : Submonoid M) :

↥H ≃ ↥(Submonoid.op H)

Bijection between a submonoid H and its opposite.

Equations

Submonoid.equivOp H = Equiv.subtypeEquiv MulOpposite.opEquiv ⋯

Instances For

Documentation

Mathlib.GroupTheory.Submonoid.MulOpposite

Submonoid of opposite monoids #

Lattice results #