Mathlib.Algebra.Group.Subsemigroup.Defs

Module docstring

{"# Subsemigroups: definition

This file defines bundled multiplicative and additive subsemigroups.

Main definitions

Subsemigroup M: the type of bundled subsemigroup of a magma M; the underlying set is given in the carrier field of the structure, and should be accessed through coercion as in (S : Set M).
AddSubsemigroup M : the type of bundled subsemigroups of an additive magma M.

For each of the following definitions in the Subsemigroup namespace, there is a corresponding definition in the AddSubsemigroup namespace.

Subsemigroup.copy : copy of a subsemigroup with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original Subsemigroup.

Similarly, for each of these definitions in the MulHom namespace, there is a corresponding definition in the AddHom namespace.

MulHom.eqLocus f g: the subsemigroup of those x such that f x = g x

Implementation notes

Subsemigroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a subsemigroup's underlying set.

Note that Subsemigroup M does not actually require Semigroup M, instead requiring only the weaker Mul M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers.

Tags

subsemigroup, subsemigroups "}

MulMemClass structure

(S : Type*) (M : outParam Type*) [Mul M] [SetLike S M]

Full source

/-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)` -/
class MulMemClass (S : Type*) (M : outParam Type*) [Mul M] [SetLike S M] : Prop where
  /-- A substructure satisfying `MulMemClass` is closed under multiplication. -/
  mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s

Multiplication-closed subset of a magma

Informal description

A structure `MulMemClass S M` asserts that `S` is a type of subsets of a magma `M` that are closed under the multiplication operation of `M`. That is, for any subset `s : S` and any elements `x, y ∈ s`, the product `x * y` also belongs to `s`.

AddMemClass structure

(S : Type*) (M : outParam Type*) [Add M] [SetLike S M]

Full source

/-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)` -/
class AddMemClass (S : Type*) (M : outParam Type*) [Add M] [SetLike S M] : Prop where
  /-- A substructure satisfying `AddMemClass` is closed under addition. -/
  add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s

Additive Subset Closed Under Addition

Informal description

The structure `AddMemClass S M` asserts that `S` is a type of subsets of an additive magma `M` that are closed under addition. That is, for any `s : S` (viewed as a subset of `M` via the `SetLike` coercion), if `x` and `y` are elements of `s`, then `x + y` is also an element of `s`.

Subsemigroup structure

(M : Type*) [Mul M]

Full source

/-- A subsemigroup of a magma `M` is a subset closed under multiplication. -/
structure Subsemigroup (M : Type*) [Mul M] where
  /-- The carrier of a subsemigroup. -/
  carrier : Set M
  /-- The product of two elements of a subsemigroup belongs to the subsemigroup. -/
  mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier

Subsemigroup of a magma

Informal description

A subsemigroup of a magma $ M $ is a subset $ S \subseteq M $ that is closed under the multiplication operation of $ M $. That is, for any $ x, y \in S $, the product $ x \cdot y $ also belongs to $ S $.

AddSubsemigroup structure

(M : Type*) [Add M]

Full source

/-- An additive subsemigroup of an additive magma `M` is a subset closed under addition. -/
structure AddSubsemigroup (M : Type*) [Add M] where
  /-- The carrier of an additive subsemigroup. -/
  carrier : Set M
  /-- The sum of two elements of an additive subsemigroup belongs to the subsemigroup. -/
  add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier

Additive subsemigroup

Informal description

An additive subsemigroup of an additive magma $ M $ is a subset of $ M $ that is closed under the addition operation of $ M $. That is, if $ x $ and $ y $ are elements of the subset, then $ x + y $ is also an element of the subset.

Subsemigroup.instSetLike instance

: SetLike (Subsemigroup M) M

Full source

@[to_additive]
instance : SetLike (Subsemigroup M) M :=
  ⟨Subsemigroup.carrier, fun p q h => by cases p; cases q; congr⟩

Subsemigroups as Set-like Structures

Informal description

For any magma $ M $, the type of subsemigroups of $ M $ can be treated as a set-like structure, where each subsemigroup $ S $ is associated with its underlying set $ S \subseteq M $. This allows subsemigroups to inherit properties and operations from sets, such as membership and subset relations.

Subsemigroup.ofClass definition

{S M : Type*} [Mul M] [SetLike S M] [MulMemClass S M] (s : S) : Subsemigroup M

Full source

/-- The actual `Subsemigroup` obtained from an element of a `MulMemClass`. -/
@[to_additive (attr := simps) "The actual `AddSubsemigroup` obtained from an element of a
`AddMemClass`"]
def ofClass {S M : Type*} [Mul M] [SetLike S M] [MulMemClass S M] (s : S) : Subsemigroup M :=
  ⟨s, MulMemClass.mul_mem⟩

Subsemigroup construction from a multiplication-closed subset

Informal description

Given a magma $ M $ and a type $ S $ representing multiplication-closed subsets of $ M $ (i.e., a `MulMemClass`), the function `Subsemigroup.ofClass` constructs a subsemigroup of $ M $ from an element $ s $ of $ S $. The underlying set of the subsemigroup is $ s $, and it is closed under multiplication by the definition of `MulMemClass`.

Subsemigroup.instCanLiftSetCoeForallForallForallMemForallHMul instance

: CanLift (Set M) (Subsemigroup M) (↑) (fun s ↦ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s)

Full source

@[to_additive]
instance (priority := 100) : CanLift (Set M) (Subsemigroup M) (↑)
    (fun s ↦ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) where
  prf s h := ⟨{ carrier := s, mul_mem' := h }, rfl⟩

Lifting Condition for Subsemigroups from Sets

Informal description

For any magma $M$, a subset $s$ of $M$ can be lifted to a subsemigroup of $M$ if and only if $s$ is closed under multiplication, i.e., for any $x, y \in s$, the product $x * y$ also belongs to $s$.

Subsemigroup.instMulMemClass instance

: MulMemClass (Subsemigroup M) M

Full source

@[to_additive]
instance : MulMemClass (Subsemigroup M) M where mul_mem := fun {_ _ _} => Subsemigroup.mul_mem' _

Subsemigroups are Multiplication-Closed Subsets

Informal description

For any magma $M$, the type of subsemigroups of $M$ forms a `MulMemClass`, meaning that every subsemigroup $S$ of $M$ is closed under the multiplication operation of $M$. That is, for any $x, y \in S$, the product $x \cdot y$ also belongs to $S$.

Subsemigroup.mem_carrier theorem

{s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s

Full source

@[to_additive (attr := simp)]
theorem mem_carrier {s : Subsemigroup M} {x : M} : x ∈ s.carrierx ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

Membership in Subsemigroup Carrier Set

Informal description

For any subsemigroup $S$ of a magma $M$ and any element $x \in M$, $x$ belongs to the underlying set of $S$ if and only if $x$ is a member of $S$ as a subsemigroup.

Subsemigroup.mem_mk theorem

{s : Set M} {x : M} (h_mul) : x ∈ mk s h_mul ↔ x ∈ s

Full source

@[to_additive (attr := simp)]
theorem mem_mk {s : Set M} {x : M} (h_mul) : x ∈ mk s h_mulx ∈ mk s h_mul ↔ x ∈ s :=
  Iff.rfl

Membership in Constructed Subsemigroup

Informal description

For any subset $s$ of a magma $M$ and any element $x \in M$, $x$ belongs to the subsemigroup constructed from $s$ (with closure under multiplication given by $h\_mul$) if and only if $x$ belongs to $s$.

Subsemigroup.coe_set_mk theorem

(s : Set M) (h_mul) : (mk s h_mul : Set M) = s

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_set_mk (s : Set M) (h_mul) : (mk s h_mul : Set M) = s :=
  rfl

Subsemigroup Construction Preserves Underlying Set

Informal description

For any subset $s$ of a magma $M$ and any proof $h\_mul$ that $s$ is closed under multiplication, the underlying set of the subsemigroup constructed from $s$ and $h\_mul$ is equal to $s$ itself. In other words, if we create a subsemigroup from a set $s$ with the appropriate closure property, the coercion of this subsemigroup back to a set yields $s$.

Subsemigroup.mk_le_mk theorem

{s t : Set M} (h_mul) (h_mul') : mk s h_mul ≤ mk t h_mul' ↔ s ⊆ t

Full source

@[to_additive (attr := simp)]
theorem mk_le_mk {s t : Set M} (h_mul) (h_mul') : mkmk s h_mul ≤ mk t h_mul' ↔ s ⊆ t :=
  Iff.rfl

Subsemigroup Order Reflects Subset Order

Informal description

For any subsets $s$ and $t$ of a magma $M$ that are closed under multiplication (with closure properties given by $h\_mul$ and $h\_mul'$ respectively), the subsemigroup constructed from $s$ is contained in the subsemigroup constructed from $t$ if and only if $s$ is a subset of $t$. In other words, $S \leq T \leftrightarrow s \subseteq t$ where $S$ and $T$ are the subsemigroups generated from $s$ and $t$ respectively.

Subsemigroup.ext theorem

{S T : Subsemigroup M} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T

Full source

/-- Two subsemigroups are equal if they have the same elements. -/
@[to_additive (attr := ext) "Two `AddSubsemigroup`s are equal if they have the same elements."]
theorem ext {S T : Subsemigroup M} (h : ∀ x, x ∈ Sx ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

Extensionality of Subsemigroups: $S = T \iff \forall x, x \in S \leftrightarrow x \in T$

Informal description

Two subsemigroups $S$ and $T$ of a magma $M$ are equal if and only if they contain the same elements, i.e., for all $x \in M$, $x \in S$ if and only if $x \in T$.

Subsemigroup.copy definition

(S : Subsemigroup M) (s : Set M) (hs : s = S) : Subsemigroup M

Full source

/-- Copy a subsemigroup replacing `carrier` with a set that is equal to it. -/
@[to_additive "Copy an additive subsemigroup replacing `carrier` with a set that is equal to it."]
protected def copy (S : Subsemigroup M) (s : Set M) (hs : s = S) :
    Subsemigroup M where
  carrier := s
  mul_mem' := hs.symm ▸ S.mul_mem'

Copy of a subsemigroup with a new carrier set

Informal description

Given a subsemigroup $ S $ of a magma $ M $ and a set $ s \subseteq M $ that is equal to the underlying set of $ S $, the function returns a new subsemigroup with $ s $ as its carrier set. The multiplication closure property is preserved by transferring it from $ S $ to the new subsemigroup.

Subsemigroup.coe_copy theorem

{s : Set M} (hs : s = S) : (S.copy s hs : Set M) = s

Full source

@[to_additive (attr := simp)]
theorem coe_copy {s : Set M} (hs : s = S) : (S.copy s hs : Set M) = s :=
  rfl

Underlying Set of Subsemigroup Copy Equals Given Set

Informal description

Let $M$ be a magma and $S$ a subsemigroup of $M$. For any subset $s \subseteq M$ that is equal to the underlying set of $S$, the underlying set of the subsemigroup copy $S.copy\ s\ hs$ is equal to $s$.

Subsemigroup.copy_eq theorem

{s : Set M} (hs : s = S) : S.copy s hs = S

Full source

@[to_additive]
theorem copy_eq {s : Set M} (hs : s = S) : S.copy s hs = S :=
  SetLike.coe_injective hs

Equality of Subsemigroup Copy with Original

Informal description

Given a subsemigroup $S$ of a magma $M$ and a subset $s \subseteq M$ such that $s = S$ (as sets), the subsemigroup $S.\text{copy}\ s\ hs$ is equal to $S$.

Subsemigroup.mul_mem theorem

{x y : M} : x ∈ S → y ∈ S → x * y ∈ S

Full source

/-- A subsemigroup is closed under multiplication. -/
@[to_additive "An `AddSubsemigroup` is closed under addition."]
protected theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S :=
  Subsemigroup.mul_mem' S

Closure of Subsemigroup under Multiplication

Informal description

Let $M$ be a magma and $S$ a subsemigroup of $M$. For any elements $x, y \in M$, if $x \in S$ and $y \in S$, then their product $x \cdot y$ also belongs to $S$.

Subsemigroup.instTop instance

: Top (Subsemigroup M)

Full source

/-- The subsemigroup `M` of the magma `M`. -/
@[to_additive "The additive subsemigroup `M` of the magma `M`."]
instance : Top (Subsemigroup M) :=
  ⟨{  carrier := Set.univ
      mul_mem' := fun _ _ => Set.mem_univ _ }⟩

The Whole Set as a Subsemigroup

Informal description

For any magma $M$, the entire set $M$ is a subsemigroup of itself.

Subsemigroup.instBot instance

: Bot (Subsemigroup M)

Full source

/-- The trivial subsemigroup `∅` of a magma `M`. -/
@[to_additive "The trivial `AddSubsemigroup` `∅` of an additive magma `M`."]
instance : Bot (Subsemigroup M) :=
  ⟨{  carrier := ∅
      mul_mem' := False.elim }⟩

The Empty Set as a Subsemigroup

Informal description

For any magma $M$, the empty set is a subsemigroup of $M$.

Subsemigroup.instInhabited instance

: Inhabited (Subsemigroup M)

Full source

@[to_additive]
instance : Inhabited (Subsemigroup M) :=
  ⟨⊥⟩

Inhabitedness of Subsemigroups

Informal description

For any magma $M$, the type of subsemigroups of $M$ is inhabited.

Subsemigroup.not_mem_bot theorem

{x : M} : x ∉ (⊥ : Subsemigroup M)

Full source

@[to_additive]
theorem not_mem_bot {x : M} : x ∉ (⊥ : Subsemigroup M) :=
  Set.not_mem_empty x

No Element Belongs to the Empty Subsemigroup

Informal description

For any element $x$ of a magma $M$, $x$ does not belong to the empty subsemigroup $\bot$ of $M$.

Subsemigroup.mem_top theorem

(x : M) : x ∈ (⊤ : Subsemigroup M)

Full source

@[to_additive (attr := simp)]
theorem mem_top (x : M) : x ∈ (⊤ : Subsemigroup M) :=
  Set.mem_univ x

Membership in the Whole Subsemigroup

Informal description

For any element $x$ in a magma $M$, $x$ belongs to the top subsemigroup of $M$, which is $M$ itself.

Subsemigroup.coe_top theorem

: ((⊤ : Subsemigroup M) : Set M) = Set.univ

Full source

@[to_additive (attr := simp)]
theorem coe_top : ((⊤ : Subsemigroup M) : Set M) = Set.univ :=
  rfl

Top Subsemigroup as Universal Set

Informal description

For any magma $M$, the underlying set of the top subsemigroup $\top$ (which is $M$ itself) is equal to the universal set of $M$.

Subsemigroup.coe_bot theorem

: ((⊥ : Subsemigroup M) : Set M) = ∅

Full source

@[to_additive (attr := simp)]
theorem coe_bot : ((⊥ : Subsemigroup M) : Set M) = ∅ :=
  rfl

Empty Subsemigroup is the Empty Set

Informal description

The underlying set of the bottom subsemigroup (the empty subsemigroup) of a magma $M$ is equal to the empty set, i.e., $(\bot : \text{Subsemigroup } M) = \emptyset$.

Subsemigroup.instMin instance

: Min (Subsemigroup M)

Full source

/-- The inf of two subsemigroups is their intersection. -/
@[to_additive "The inf of two `AddSubsemigroup`s is their intersection."]
instance : Min (Subsemigroup M) :=
  ⟨fun S₁ S₂ =>
    { carrier := S₁ ∩ S₂
      mul_mem' := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ => ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩

Intersection of Subsemigroups as Minimal Operation

Informal description

For any magma $M$, the type of subsemigroups of $M$ has a minimal operation, which corresponds to taking the intersection of two subsemigroups.

Subsemigroup.coe_inf theorem

(p p' : Subsemigroup M) : ((p ⊓ p' : Subsemigroup M) : Set M) = (p : Set M) ∩ p'

Full source

@[to_additive (attr := simp)]
theorem coe_inf (p p' : Subsemigroup M) : ((p ⊓ p' : Subsemigroup M) : Set M) = (p : Set M) ∩ p' :=
  rfl

Intersection of Subsemigroups as Set Intersection

Informal description

For any two subsemigroups $p$ and $p'$ of a magma $M$, the underlying set of their intersection $p \sqcap p'$ is equal to the intersection of their underlying sets, i.e., $(p \sqcap p' : \text{Set } M) = (p : \text{Set } M) \cap p'$.

Subsemigroup.mem_inf theorem

{p p' : Subsemigroup M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Full source

@[to_additive (attr := simp)]
theorem mem_inf {p p' : Subsemigroup M} {x : M} : x ∈ p ⊓ p'x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
  Iff.rfl

Membership in Intersection of Subsemigroups

Informal description

For any subsemigroups $p$ and $p'$ of a magma $M$, and any element $x \in M$, we have $x \in p \sqcap p'$ if and only if $x \in p$ and $x \in p'$.

Subsemigroup.subsingleton_of_subsingleton theorem

[Subsingleton (Subsemigroup M)] : Subsingleton M

Full source

@[to_additive]
theorem subsingleton_of_subsingleton [Subsingleton (Subsemigroup M)] : Subsingleton M := by
  constructor; intro x y
  have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
  exact absurd (this x) not_mem_bot

Subsingleton of Subsemigroups Implies Subsingleton of Magma

Informal description

If the type of subsemigroups of a magma $M$ is a subsingleton (i.e., has at most one element), then $M$ itself is a subsingleton.

Subsemigroup.instNontrivialOfNonempty instance

[hn : Nonempty M] : Nontrivial (Subsemigroup M)

Full source

@[to_additive]
instance [hn : Nonempty M] : Nontrivial (Subsemigroup M) :=
  ⟨⟨⊥, ⊤, fun h => by
      obtain ⟨x⟩ := id hn
      refine absurd (?_ : x ∈ ⊥) not_mem_bot
      simp [h]⟩⟩

Nontriviality of Subsemigroups for Nonempty Magmas

Informal description

For any nonempty magma $M$, the type of subsemigroups of $M$ is nontrivial (contains at least two distinct elements).

MulHom.eqLocus definition

(f g : M →ₙ* N) : Subsemigroup M

Full source

/-- The subsemigroup of elements `x : M` such that `f x = g x` -/
@[to_additive "The additive subsemigroup of elements `x : M` such that `f x = g x`"]
def eqLocus (f g : M →ₙ* N) : Subsemigroup M where
  carrier := { x | f x = g x }
  mul_mem' (hx : _ = _) (hy : _ = _) := by simp [*]

Equalizer subsemigroup of multiplicative homomorphisms

Informal description

Given two non-unital multiplicative homomorphisms $ f, g : M \to N $ between magmas $ M $ and $ N $, the subsemigroup $ \text{eqLocus}(f, g) $ consists of all elements $ x \in M $ such that $ f(x) = g(x) $. This subsemigroup is closed under multiplication in $ M $.

MulMemClass.mul instance

: Mul S'

Full source

/-- A submagma of a magma inherits a multiplication. -/
@[to_additive "An additive submagma of an additive magma inherits an addition."]
instance (priority := 900) mul : Mul S' :=
  ⟨fun a b => ⟨a.1 * b.1, mul_mem a.2 b.2⟩⟩

Multiplication on Multiplication-closed Subsets of a Magma

Informal description

For any subset $S'$ of a magma $M$ that is closed under multiplication (i.e., $x, y \in S'$ implies $x * y \in S'$), the subset $S'$ inherits a multiplication operation from $M$.

MulMemClass.coe_mul theorem

(x y : S') : (↑(x * y) : M) = ↑x * ↑y

Full source

@[to_additive (attr := simp low, norm_cast)]
theorem coe_mul (x y : S') : (↑(x * y) : M) = ↑x * ↑y :=
  rfl

Coercion Preserves Multiplication in Multiplication-closed Subsets

Informal description

For any elements $x$ and $y$ in a multiplication-closed subset $S'$ of a magma $M$, the coercion of their product in $S'$ to $M$ equals the product of their coercions in $M$. That is, $(x * y : M) = (x : M) * (y : M)$.

MulMemClass.mk_mul_mk theorem

(x y : M) (hx : x ∈ S') (hy : y ∈ S') : (⟨x, hx⟩ : S') * ⟨y, hy⟩ = ⟨x * y, mul_mem hx hy⟩

Full source

@[to_additive (attr := simp low)]
theorem mk_mul_mk (x y : M) (hx : x ∈ S') (hy : y ∈ S') :
    (⟨x, hx⟩ : S') * ⟨y, hy⟩ = ⟨x * y, mul_mem hx hy⟩ :=
  rfl

Embedding of Product in Multiplication-closed Subset

Informal description

For any elements $x, y$ in a magma $M$ that belong to a multiplication-closed subset $S'$ (i.e., $x \in S'$ and $y \in S'$), the product of their embeddings into $S'$ equals the embedding of their product in $M$ into $S'$. In other words, if $\langle x, hx \rangle$ and $\langle y, hy \rangle$ are the embeddings of $x$ and $y$ into $S'$ with proofs $hx$ and $hy$ of membership, then their product in $S'$ is $\langle x * y, \text{mul\_mem } hx\ hy \rangle$.

MulMemClass.mul_def theorem

(x y : S') : x * y = ⟨x * y, mul_mem x.2 y.2⟩

Full source

@[to_additive]
theorem mul_def (x y : S') : x * y = ⟨x * y, mul_mem x.2 y.2⟩ :=
  rfl

Definition of Multiplication in Multiplication-closed Subsets

Informal description

For any elements $x$ and $y$ in a multiplication-closed subset $S'$ of a magma $M$, the product $x * y$ in $S'$ is equal to the pair consisting of the product $x * y$ in $M$ and the proof that this product lies in $S'$.

MulMemClass.toSemigroup instance

{M : Type*} [Semigroup M] {A : Type*} [SetLike A M] [MulMemClass A M] (S : A) : Semigroup S

Full source

/-- A subsemigroup of a semigroup inherits a semigroup structure. -/
@[to_additive "An `AddSubsemigroup` of an `AddSemigroup` inherits an `AddSemigroup` structure."]
instance toSemigroup {M : Type*} [Semigroup M] {A : Type*} [SetLike A M] [MulMemClass A M]
    (S : A) : Semigroup S := fast_instance%
  Subtype.coe_injective.semigroup Subtype.val fun _ _ => rfl

Semigroup Structure on Multiplication-closed Subsets

Informal description

For any semigroup $M$ and any subset $S$ of $M$ that is closed under multiplication (i.e., $x, y \in S$ implies $x * y \in S$), the subset $S$ inherits a semigroup structure from $M$.

MulMemClass.toCommSemigroup instance

{M} [CommSemigroup M] {A : Type*} [SetLike A M] [MulMemClass A M] (S : A) : CommSemigroup S

Full source

/-- A subsemigroup of a `CommSemigroup` is a `CommSemigroup`. -/
@[to_additive "An `AddSubsemigroup` of an `AddCommSemigroup` is an `AddCommSemigroup`."]
instance toCommSemigroup {M} [CommSemigroup M] {A : Type*} [SetLike A M] [MulMemClass A M]
    (S : A) : CommSemigroup S := fast_instance%
  Subtype.coe_injective.commSemigroup Subtype.val fun _ _ => rfl

Multiplication-closed Subsets of Commutative Semigroups are Commutative Semigroups

Informal description

For any commutative semigroup $M$ and any multiplication-closed subset $S$ of $M$, the subset $S$ inherits a commutative semigroup structure from $M$.

MulMemClass.subtype definition

: S' →ₙ* M

Full source

/-- The natural semigroup hom from a subsemigroup of semigroup `M` to `M`. -/
@[to_additive "The natural semigroup hom from an `AddSubsemigroup` of
`AddSubsemigroup` `M` to `M`."]
def subtype : S' →ₙ* M where
  toFun := Subtype.val; map_mul' := fun _ _ => rfl

Inclusion homomorphism of a multiplication-closed subset

Informal description

The natural multiplicative homomorphism from a multiplication-closed subset $S'$ of a magma $M$ to $M$ itself, given by the inclusion map that sends each element of $S'$ to itself in $M$.

MulMemClass.subtype_apply theorem

(x : S') : MulMemClass.subtype S' x = x

Full source

@[to_additive (attr := simp)]
lemma subtype_apply (x : S') :
    MulMemClass.subtype S' x = x := rfl

Inclusion Homomorphism Acts as Identity on Elements

Informal description

For any element $x$ in a multiplication-closed subset $S'$ of a magma $M$, the inclusion homomorphism $\text{subtype}(S')$ evaluated at $x$ equals $x$ itself, i.e., $\text{subtype}(S')(x) = x$.

MulMemClass.subtype_injective theorem

: Function.Injective (MulMemClass.subtype S')

Full source

@[to_additive]
lemma subtype_injective :
    Function.Injective (MulMemClass.subtype S') :=
  Subtype.coe_injective

Injectivity of the Inclusion Homomorphism for Multiplication-Closed Subsets

Informal description

The inclusion homomorphism from a multiplication-closed subset $S'$ of a magma $M$ to $M$ itself is injective. That is, if two elements of $S'$ have the same image under the inclusion map, then they are equal in $S'$.

MulMemClass.coe_subtype theorem

: (MulMemClass.subtype S' : S' → M) = Subtype.val

Full source

@[to_additive (attr := simp)]
theorem coe_subtype : (MulMemClass.subtype S' : S' → M) = Subtype.val :=
  rfl

Inclusion Homomorphism as Subtype Projection

Informal description

For any multiplication-closed subset $S'$ of a magma $M$, the underlying function of the inclusion homomorphism $\text{subtype} : S' \to M$ is equal to the canonical projection $\text{val} : S' \to M$ that maps each element of $S'$ to its corresponding element in $M$.