toAddSubsemigroup — Mathlib

English

Subsemigroups of a semigroup M are order-isomorphic to AddSubsemigroups of its Additive M, via the correspondence S ↦ Additive.toMul⁻¹' S.

Русский

Подполугруппы полугруппы M конъюгированы к аддитивным подполугруппам Additive M через отображение S ↦ Additive.toMul⁻¹' S.

LaTeX

$$$\\text{Subsemigroup } M \\; \\cong_o \\; \\text{AddSubsemigroup}(\\text{Additive } M)$$$

Lean4

/-- Subsemigroups of semigroup `M` are isomorphic to additive subsemigroups of `Additive M`. -/
@[simps]
def toAddSubsemigroup : Subsemigroup M ≃o AddSubsemigroup (Additive M)
    where
  toFun
    S :=
    { carrier := Additive.toMul ⁻¹' S
      add_mem' := S.mul_mem' }
  invFun
    S :=
    { carrier := Additive.ofMul ⁻¹' S
      mul_mem' := S.add_mem' }
  map_rel_iff' := Iff.rfl

Похожие утверждения