Subsemigroup of opposite semigroups #

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

source

def Subsemigroup.op {M : Type u_2} [Mul M] (x : Subsemigroup M) :

Subsemigroup Mᵐᵒᵖ

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

Equations

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

Instances For

source

def AddSubsemigroup.op {M : Type u_2} [Add M] (x : AddSubsemigroup M) :

AddSubsemigroup Mᵃᵒᵖ

Pull an additive subsemigroup back to an opposite subsemigroup along AddOpposite.unop

Equations

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

Instances For

source

@[simp]

theorem AddSubsemigroup.coe_op {M : Type u_2} [Add M] (x : AddSubsemigroup M) :

↑x.op = AddOpposite.unop ⁻¹' ↑x

source

@[simp]

theorem Subsemigroup.coe_op {M : Type u_2} [Mul M] (x : Subsemigroup M) :

↑x.op = MulOpposite.unop ⁻¹' ↑x

source

@[simp]

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

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

source

@[simp]

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

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

source

def Subsemigroup.unop {M : Type u_2} [Mul M] (x : Subsemigroup Mᵐᵒᵖ) :

Subsemigroup M

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

Equations

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

Instances For

source

def AddSubsemigroup.unop {M : Type u_2} [Add M] (x : AddSubsemigroup Mᵃᵒᵖ) :

AddSubsemigroup M

Pull an opposite additive subsemigroup back to a subsemigroup along AddOpposite.op

Equations

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

Instances For

source

@[simp]

theorem Subsemigroup.coe_unop {M : Type u_2} [Mul M] (x : Subsemigroup Mᵐᵒᵖ) :

↑x.unop = MulOpposite.op ⁻¹' ↑x

source

@[simp]

theorem AddSubsemigroup.coe_unop {M : Type u_2} [Add M] (x : AddSubsemigroup Mᵃᵒᵖ) :

↑x.unop = AddOpposite.op ⁻¹' ↑x

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem Subsemigroup.unop_op {M : Type u_2} [Mul M] (S : Subsemigroup M) :

S.op.unop = S

source

@[simp]

theorem AddSubsemigroup.unop_op {M : Type u_2} [Add M] (S : AddSubsemigroup M) :

S.op.unop = S

source

@[simp]

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

S.unop.op = S

source

@[simp]

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

S.unop.op = S

Lattice results #

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

theorem Subsemigroup.op_le_op_iff {M : Type u_2} [Mul M] {S₁ S₂ : Subsemigroup M} :

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

source

@[simp]

theorem AddSubsemigroup.op_le_op_iff {M : Type u_2} [Add M] {S₁ S₂ : AddSubsemigroup M} :

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

source

@[simp]

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

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

source

@[simp]

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

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

source

def Subsemigroup.opEquiv {M : Type u_2} [Mul M] :

Subsemigroup M ≃o Subsemigroup Mᵐᵒᵖ

A subsemigroup H of M determines a subsemigroup H.op of the opposite semigroup Mᵐᵒᵖ.

Equations

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

Instances For

source

def AddSubsemigroup.opEquiv {M : Type u_2} [Add M] :

AddSubsemigroup M ≃o AddSubsemigroup Mᵃᵒᵖ

An additive subsemigroup H of M determines an additive subsemigroup H.op of the opposite semigroup Mᵐᵒᵖ.

Equations

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

Instances For

source

@[simp]

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

(RelIso.symm opEquiv) x = x.unop

source

@[simp]

theorem Subsemigroup.opEquiv_apply {M : Type u_2} [Mul M] (x : Subsemigroup M) :

opEquiv x = x.op

source

@[simp]

theorem Subsemigroup.opEquiv_symm_apply {M : Type u_2} [Mul M] (x : Subsemigroup Mᵐᵒᵖ) :

(RelIso.symm opEquiv) x = x.unop

source

@[simp]

theorem AddSubsemigroup.opEquiv_apply {M : Type u_2} [Add M] (x : AddSubsemigroup M) :

opEquiv x = x.op

source

theorem Subsemigroup.op_injective {M : Type u_2} [Mul M] :

Function.Injective Subsemigroup.op

source

theorem AddSubsemigroup.op_injective {M : Type u_2} [Add M] :

Function.Injective AddSubsemigroup.op

source

theorem Subsemigroup.unop_injective {M : Type u_2} [Mul M] :

Function.Injective Subsemigroup.unop

source

theorem AddSubsemigroup.unop_injective {M : Type u_2} [Add M] :

Function.Injective AddSubsemigroup.unop

source

@[simp]

theorem Subsemigroup.op_inj {M : Type u_2} [Mul M] {S T : Subsemigroup M} :

S.op = T.op ↔ S = T

source

@[simp]

theorem AddSubsemigroup.op_inj {M : Type u_2} [Add M] {S T : AddSubsemigroup M} :

S.op = T.op ↔ S = T

source

@[simp]

theorem Subsemigroup.unop_inj {M : Type u_2} [Mul M] {S T : Subsemigroup Mᵐᵒᵖ} :

S.unop = T.unop ↔ S = T

source

@[simp]

theorem AddSubsemigroup.unop_inj {M : Type u_2} [Add M] {S T : AddSubsemigroup Mᵃᵒᵖ} :

S.unop = T.unop ↔ S = T

source

@[simp]

theorem Subsemigroup.op_bot {M : Type u_2} [Mul M] :

⊥.op = ⊥

source

@[simp]

theorem AddSubsemigroup.op_bot {M : Type u_2} [Add M] :

⊥.op = ⊥

source

@[simp]

theorem Subsemigroup.op_eq_bot {M : Type u_2} [Mul M] {S : Subsemigroup M} :

S.op = ⊥ ↔ S = ⊥

source

@[simp]

theorem AddSubsemigroup.op_eq_bot {M : Type u_2} [Add M] {S : AddSubsemigroup M} :

S.op = ⊥ ↔ S = ⊥

source

@[simp]

theorem Subsemigroup.unop_bot {M : Type u_2} [Mul M] :

⊥.unop = ⊥

source

@[simp]

theorem AddSubsemigroup.unop_bot {M : Type u_2} [Add M] :

⊥.unop = ⊥

source

@[simp]

theorem Subsemigroup.unop_eq_bot {M : Type u_2} [Mul M] {S : Subsemigroup Mᵐᵒᵖ} :

S.unop = ⊥ ↔ S = ⊥

source

@[simp]

theorem AddSubsemigroup.unop_eq_bot {M : Type u_2} [Add M] {S : AddSubsemigroup Mᵃᵒᵖ} :

S.unop = ⊥ ↔ S = ⊥

source

@[simp]

theorem Subsemigroup.op_top {M : Type u_2} [Mul M] :

⊤.op = ⊤

source

@[simp]

theorem AddSubsemigroup.op_top {M : Type u_2} [Add M] :

⊤.op = ⊤

source

@[simp]

theorem Subsemigroup.op_eq_top {M : Type u_2} [Mul M] {S : Subsemigroup M} :

S.op = ⊤ ↔ S = ⊤

source

@[simp]

theorem AddSubsemigroup.op_eq_top {M : Type u_2} [Add M] {S : AddSubsemigroup M} :

S.op = ⊤ ↔ S = ⊤

source

@[simp]

theorem Subsemigroup.unop_top {M : Type u_2} [Mul M] :

⊤.unop = ⊤

source

@[simp]

theorem AddSubsemigroup.unop_top {M : Type u_2} [Add M] :

⊤.unop = ⊤

source

@[simp]

theorem Subsemigroup.unop_eq_top {M : Type u_2} [Mul M] {S : Subsemigroup Mᵐᵒᵖ} :

S.unop = ⊤ ↔ S = ⊤

source

@[simp]

theorem AddSubsemigroup.unop_eq_top {M : Type u_2} [Add M] {S : AddSubsemigroup Mᵃᵒᵖ} :

S.unop = ⊤ ↔ S = ⊤

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem Subsemigroup.op_sSup {M : Type u_2} [Mul M] (S : Set (Subsemigroup M)) :

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

source

theorem AddSubsemigroup.op_sSup {M : Type u_2} [Add M] (S : Set (AddSubsemigroup M)) :

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

source

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

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

source

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

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

source

theorem Subsemigroup.op_sInf {M : Type u_2} [Mul M] (S : Set (Subsemigroup M)) :

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

source

theorem AddSubsemigroup.op_sInf {M : Type u_2} [Add M] (S : Set (AddSubsemigroup M)) :

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem Subsemigroup.op_closure {M : Type u_2} [Mul M] (s : Set M) :

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

source

theorem AddSubsemigroup.op_closure {M : Type u_2} [Add M] (s : Set M) :

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

source

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

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

source

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

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

source

def Subsemigroup.equivOp {M : Type u_2} [Mul M] (H : Subsemigroup M) :

↥H ≃ ↥H.op

Bijection between a subsemigroup H and its opposite.

Equations

H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯

Instances For

source

def AddSubsemigroup.equivOp {M : Type u_2} [Add M] (H : AddSubsemigroup M) :

↥H ≃ ↥H.op

Bijection between an additive subsemigroup H and its opposite.

Equations

H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯

Instances For

source

@[simp]

theorem AddSubsemigroup.equivOp_symm_apply_coe {M : Type u_2} [Add M] (H : AddSubsemigroup M) (b : ↥H.op) :

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

source

@[simp]

theorem Subsemigroup.equivOp_symm_apply_coe {M : Type u_2} [Mul M] (H : Subsemigroup M) (b : ↥H.op) :

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

source

@[simp]

theorem AddSubsemigroup.equivOp_apply_coe {M : Type u_2} [Add M] (H : AddSubsemigroup M) (a : ↥H) :

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

source

@[simp]

theorem Subsemigroup.equivOp_apply_coe {M : Type u_2} [Mul M] (H : Subsemigroup M) (a : ↥H) :

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

Documentation

Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Subsemigroup of opposite semigroups #

Lattice results #