Subsemigroup of opposite semigroups

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

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

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

@[simp]

theorem Subsemigroup.coe_op {M : Type u_2} [Mul M] (x : Subsemigroup M) : ↑x.op = MulOpposite.unop ⁻¹' ↑x

@[simp]

theorem AddSubsemigroup.coe_op {M : Type u_2} [Add M] (x : AddSubsemigroup M) : ↑x.op = AddOpposite.unop ⁻¹' ↑x

@[simp]

theorem Subsemigroup.mem_op {M : Type u_2} [Mul M] {x : Mᵐᵒᵖ} {S : Subsemigroup M} : x ∈ S.op ↔ MulOpposite.unop x ∈ S

@[simp]

theorem AddSubsemigroup.mem_op {M : Type u_2} [Add M] {x : Mᵃᵒᵖ} {S : AddSubsemigroup M} : x ∈ S.op ↔ AddOpposite.unop x ∈ S

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

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

@[simp]

theorem AddSubsemigroup.coe_unop {M : Type u_2} [Add M] (x : AddSubsemigroup Mᵃᵒᵖ) : ↑x.unop = AddOpposite.op ⁻¹' ↑x

@[simp]

theorem Subsemigroup.coe_unop {M : Type u_2} [Mul M] (x : Subsemigroup Mᵐᵒᵖ) : ↑x.unop = MulOpposite.op ⁻¹' ↑x

@[simp]

theorem Subsemigroup.mem_unop {M : Type u_2} [Mul M] {x : M} {S : Subsemigroup Mᵐᵒᵖ} : x ∈ S.unop ↔ MulOpposite.op x ∈ S

@[simp]

theorem AddSubsemigroup.mem_unop {M : Type u_2} [Add M] {x : M} {S : AddSubsemigroup Mᵃᵒᵖ} : x ∈ S.unop ↔ AddOpposite.op x ∈ S

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Lattice results

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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ᵐᵒᵖ.

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ᵐᵒᵖ.

@[simp]

theorem AddSubsemigroup.opEquiv_symm_apply {M : Type u_2} [Add M] (x : AddSubsemigroup Mᵃᵒᵖ) : (RelIso.symm opEquiv) x = x.unop

@[simp]

theorem Subsemigroup.opEquiv_symm_apply {M : Type u_2} [Mul M] (x : Subsemigroup Mᵐᵒᵖ) : (RelIso.symm opEquiv) x = x.unop

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Subsemigroup.op_eq_bot {M : Type u_2} [Mul M] {S : Subsemigroup M} : S.op = ⊥ ↔ S = ⊥

@[simp]

theorem AddSubsemigroup.op_eq_bot {M : Type u_2} [Add M] {S : AddSubsemigroup M} : S.op = ⊥ ↔ S = ⊥

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Subsemigroup.op_eq_top {M : Type u_2} [Mul M] {S : Subsemigroup M} : S.op = ⊤ ↔ S = ⊤

@[simp]

theorem AddSubsemigroup.op_eq_top {M : Type u_2} [Add M] {S : AddSubsemigroup M} : S.op = ⊤ ↔ S = ⊤

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

theorem Subsemigroup.op_sSup {M : Type u_2} [Mul M] (S : Set (Subsemigroup M)) : (sSup S).op = sSup (Subsemigroup.unop ⁻¹' S)

theorem AddSubsemigroup.op_sSup {M : Type u_2} [Add M] (S : Set (AddSubsemigroup M)) : (sSup S).op = sSup (AddSubsemigroup.unop ⁻¹' S)

theorem Subsemigroup.unop_sSup {M : Type u_2} [Mul M] (S : Set (Subsemigroup Mᵐᵒᵖ)) : (sSup S).unop = sSup (Subsemigroup.op ⁻¹' S)

theorem AddSubsemigroup.unop_sSup {M : Type u_2} [Add M] (S : Set (AddSubsemigroup Mᵃᵒᵖ)) : (sSup S).unop = sSup (AddSubsemigroup.op ⁻¹' S)

theorem Subsemigroup.op_sInf {M : Type u_2} [Mul M] (S : Set (Subsemigroup M)) : (sInf S).op = sInf (Subsemigroup.unop ⁻¹' S)

theorem AddSubsemigroup.op_sInf {M : Type u_2} [Add M] (S : Set (AddSubsemigroup M)) : (sInf S).op = sInf (AddSubsemigroup.unop ⁻¹' S)

theorem Subsemigroup.unop_sInf {M : Type u_2} [Mul M] (S : Set (Subsemigroup Mᵐᵒᵖ)) : (sInf S).unop = sInf (Subsemigroup.op ⁻¹' S)

theorem AddSubsemigroup.unop_sInf {M : Type u_2} [Add M] (S : Set (AddSubsemigroup Mᵃᵒᵖ)) : (sInf S).unop = sInf (AddSubsemigroup.op ⁻¹' S)

theorem Subsemigroup.op_iSup {ι : Sort u_1} {M : Type u_2} [Mul M] (S : ι → Subsemigroup M) : (iSup S).op = ⨆ (i : ι), (S i).op

theorem AddSubsemigroup.op_iSup {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup M) : (iSup S).op = ⨆ (i : ι), (S i).op

theorem Subsemigroup.unop_iSup {ι : Sort u_1} {M : Type u_2} [Mul M] (S : ι → Subsemigroup Mᵐᵒᵖ) : (iSup S).unop = ⨆ (i : ι), (S i).unop

theorem AddSubsemigroup.unop_iSup {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup Mᵃᵒᵖ) : (iSup S).unop = ⨆ (i : ι), (S i).unop

theorem Subsemigroup.op_iInf {ι : Sort u_1} {M : Type u_2} [Mul M] (S : ι → Subsemigroup M) : (iInf S).op = ⨅ (i : ι), (S i).op

theorem AddSubsemigroup.op_iInf {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup M) : (iInf S).op = ⨅ (i : ι), (S i).op

theorem Subsemigroup.unop_iInf {ι : Sort u_1} {M : Type u_2} [Mul M] (S : ι → Subsemigroup Mᵐᵒᵖ) : (iInf S).unop = ⨅ (i : ι), (S i).unop

theorem AddSubsemigroup.unop_iInf {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup Mᵃᵒᵖ) : (iInf S).unop = ⨅ (i : ι), (S i).unop

theorem Subsemigroup.op_closure {M : Type u_2} [Mul M] (s : Set M) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

theorem AddSubsemigroup.op_closure {M : Type u_2} [Add M] (s : Set M) : (closure s).op = closure (AddOpposite.unop ⁻¹' s)

theorem Subsemigroup.unop_closure {M : Type u_2} [Mul M] (s : Set Mᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

theorem AddSubsemigroup.unop_closure {M : Type u_2} [Add M] (s : Set Mᵃᵒᵖ) : (closure s).unop = closure (AddOpposite.op ⁻¹' s)

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

Bijection between a subsemigroup H and its opposite.

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

Bijection between an additive subsemigroup H and its opposite.

@[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

@[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

@[simp]

theorem Subsemigroup.equivOp_apply_coe {M : Type u_2} [Mul M] (H : Subsemigroup M) (a : ↥H) : ↑(H.equivOp a) = MulOpposite.op ↑a

@[simp]

theorem AddSubsemigroup.equivOp_apply_coe {M : Type u_2} [Add M] (H : AddSubsemigroup M) (a : ↥H) : ↑(H.equivOp a) = AddOpposite.op ↑a