Mathlib.Algebra.Group.Subsemigroup.Basic

Subsemigroup.instInfSet instance

: InfSet (Subsemigroup M)

Full source

@[to_additive]
instance : InfSet (Subsemigroup M) :=
  ⟨fun s =>
    { carrier := ⋂ t ∈ s, ↑t
      mul_mem' := fun hx hy =>
        Set.mem_biInter fun i h =>
          i.mul_mem (by apply Set.mem_iInter₂.1 hx i h) (by apply Set.mem_iInter₂.1 hy i h) }⟩

Complete Lattice Structure on Subsemigroups

Informal description

For any type $M$ with a multiplication operation, the collection of subsemigroups of $M$ forms a complete lattice with respect to inclusion, where the infimum of a family of subsemigroups is given by their intersection.

Subsemigroup.coe_sInf theorem

(S : Set (Subsemigroup M)) : ((sInf S : Subsemigroup M) : Set M) = ⋂ s ∈ S, ↑s

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_sInf (S : Set (Subsemigroup M)) : ((sInf S : Subsemigroup M) : Set M) = ⋂ s ∈ S, ↑s :=
  rfl

Infimum of Subsemigroups as Intersection of Underlying Sets

Informal description

For any collection $S$ of subsemigroups of a type $M$ with a multiplication operation, the underlying set of the infimum of $S$ is equal to the intersection of the underlying sets of all subsemigroups in $S$, i.e., \[ \bigcap_{s \in S} s = \inf S. \]

Subsemigroup.mem_sInf theorem

{S : Set (Subsemigroup M)} {x : M} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Full source

@[to_additive]
theorem mem_sInf {S : Set (Subsemigroup M)} {x : M} : x ∈ sInf Sx ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
  Set.mem_iInter₂

Characterization of Membership in Infimum of Subsemigroups

Informal description

For any collection $S$ of subsemigroups of a multiplicative structure $M$ and any element $x \in M$, the element $x$ belongs to the infimum (greatest lower bound) of $S$ if and only if $x$ belongs to every subsemigroup $p$ in $S$. In symbols: $$x \in \bigwedge S \leftrightarrow \forall p \in S, x \in p$$

Subsemigroup.mem_iInf theorem

{ι : Sort*} {S : ι → Subsemigroup M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Full source

@[to_additive]
theorem mem_iInf {ι : Sort*} {S : ι → Subsemigroup M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

Characterization of Membership in Infimum of Subsemigroups

Informal description

For any indexed family of subsemigroups $(S_i)_{i \in \iota}$ of a multiplicative type $M$ and any element $x \in M$, the element $x$ belongs to the infimum $\bigsqcap_i S_i$ of the family if and only if $x$ belongs to $S_i$ for every index $i \in \iota$.

Subsemigroup.coe_iInf theorem

{ι : Sort*} {S : ι → Subsemigroup M} : (↑(⨅ i, S i) : Set M) = ⋂ i, S i

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_iInf {ι : Sort*} {S : ι → Subsemigroup M} : (↑(⨅ i, S i) : Set M) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]

Infimum of Subsemigroups as Intersection of Underlying Sets

Informal description

For any indexed family of subsemigroups $ S_i $ of a multiplicative structure $ M $, the underlying set of the infimum of the family $ \bigsqcap_i S_i $ is equal to the intersection of the underlying sets $ \bigcap_i S_i $. In symbols: \[ \left( \bigsqcap_i S_i \right) = \bigcap_i S_i. \]

Subsemigroup.instCompleteLattice instance

: CompleteLattice (Subsemigroup M)

Full source

/-- subsemigroups of a monoid form a complete lattice. -/
@[to_additive "The `AddSubsemigroup`s of an `AddMonoid` form a complete lattice."]
instance : CompleteLattice (Subsemigroup M) :=
  { completeLatticeOfInf (Subsemigroup M) fun _ =>
      IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
    le := (· ≤ ·)
    lt := (· < ·)
    bot := ⊥
    bot_le := fun _ _ hx => (not_mem_bot hx).elim
    top := ⊤
    le_top := fun _ x _ => mem_top x
    inf := (· ⊓ ·)
    sInf := InfSet.sInf
    le_inf := fun _ _ _ ha hb _ hx => ⟨ha hx, hb hx⟩
    inf_le_left := fun _ _ _ => And.left
    inf_le_right := fun _ _ _ => And.right }

Complete Lattice Structure on Subsemigroups

Informal description

For any multiplicative structure $M$, the collection of all subsemigroups of $M$ forms a complete lattice under inclusion. In this lattice: - The infimum of a family of subsemigroups is their intersection. - The supremum of a family of subsemigroups is the subsemigroup generated by their union. - The bottom element is the trivial subsemigroup $\{1\}$ (if $M$ has a unit) or $\emptyset$ otherwise. - The top element is $M$ itself.

Subsemigroup.closure definition

(s : Set M) : Subsemigroup M

Full source

/-- The `Subsemigroup` generated by a set. -/
@[to_additive "The `AddSubsemigroup` generated by a set"]
def closure (s : Set M) : Subsemigroup M :=
  sInf { S | s ⊆ S }

Subsemigroup generated by a set

Informal description

The subsemigroup generated by a set $s$ in a multiplicative structure $M$ is the smallest subsemigroup of $M$ containing $s$. It is defined as the infimum of all subsemigroups of $M$ that contain $s$.

Subsemigroup.mem_closure theorem

{x : M} : x ∈ closure s ↔ ∀ S : Subsemigroup M, s ⊆ S → x ∈ S

Full source

@[to_additive]
theorem mem_closure {x : M} : x ∈ closure sx ∈ closure s ↔ ∀ S : Subsemigroup M, s ⊆ S → x ∈ S :=
  mem_sInf

Characterization of Membership in Subsemigroup Closure

Informal description

For any element $x$ in a multiplicative structure $M$, $x$ belongs to the subsemigroup closure of a set $s \subseteq M$ if and only if $x$ is contained in every subsemigroup $S$ of $M$ that includes $s$. In symbols: $$x \in \text{closure}(s) \leftrightarrow \forall S \leq M, s \subseteq S \to x \in S$$

Subsemigroup.subset_closure theorem

: s ⊆ closure s

Full source

/-- The subsemigroup generated by a set includes the set. -/
@[to_additive (attr := simp, aesop safe 20 apply (rule_sets := [SetLike]))
  "The `AddSubsemigroup` generated by a set includes the set."]
theorem subset_closure : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx

Subsemigroup Closure Contains the Generating Set

Informal description

For any subset $s$ of a multiplicative structure $M$, the subsemigroup generated by $s$ contains $s$. In other words, $s$ is a subset of its closure $\text{closure}(s)$.

Subsemigroup.not_mem_of_not_mem_closure theorem

{P : M} (hP : P ∉ closure s) : P ∉ s

Full source

@[to_additive]
theorem not_mem_of_not_mem_closure {P : M} (hP : P ∉ closure s) : P ∉ s := fun h =>
  hP (subset_closure h)

Non-membership in Subsemigroup Closure Implies Non-membership in Generating Set

Informal description

For any element $P$ in a multiplicative structure $M$, if $P$ does not belong to the subsemigroup closure of a set $s \subseteq M$, then $P$ does not belong to $s$. In symbols: $$P \notin \text{closure}(s) \implies P \notin s$$

Subsemigroup.closure_le theorem

: closure s ≤ S ↔ s ⊆ S

Full source

/-- A subsemigroup `S` includes `closure s` if and only if it includes `s`. -/
@[to_additive (attr := simp)
  "An additive subsemigroup `S` includes `closure s` if and only if it includes `s`"]
theorem closure_le : closureclosure s ≤ S ↔ s ⊆ S :=
  ⟨Subset.trans subset_closure, fun h => sInf_le h⟩

Subsemigroup Closure Containment Criterion: $\text{closure}(s) \leq S \leftrightarrow s \subseteq S$

Informal description

For a set $s$ in a multiplicative structure $M$ and a subsemigroup $S$ of $M$, the subsemigroup closure of $s$ is contained in $S$ if and only if $s$ is a subset of $S$.

Subsemigroup.closure_mono theorem

⦃s t : Set M⦄ (h : s ⊆ t) : closure s ≤ closure t

Full source

/-- subsemigroup closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`. -/
@[to_additive (attr := gcongr) "Additive subsemigroup closure of a set is monotone in its argument:
if `s ⊆ t`, then `closure s ≤ closure t`"]
theorem closure_mono ⦃s t : Set M⦄ (h : s ⊆ t) : closure s ≤ closure t :=
  closure_le.2 <| Subset.trans h subset_closure

Monotonicity of Subsemigroup Closure: $s \subseteq t \implies \text{closure}(s) \leq \text{closure}(t)$

Informal description

For any two subsets $s$ and $t$ of a multiplicative structure $M$, if $s$ is a subset of $t$, then the subsemigroup generated by $s$ is contained in the subsemigroup generated by $t$. In symbols: $$s \subseteq t \implies \text{closure}(s) \leq \text{closure}(t)$$

Subsemigroup.closure_eq_of_le theorem

(h₁ : s ⊆ S) (h₂ : S ≤ closure s) : closure s = S

Full source

@[to_additive]
theorem closure_eq_of_le (h₁ : s ⊆ S) (h₂ : S ≤ closure s) : closure s = S :=
  le_antisymm (closure_le.2 h₁) h₂

Subsemigroup Closure Equality Criterion: $\text{closure}(s) = S$ under $s \subseteq S \leq \text{closure}(s)$

Informal description

For a set $s$ in a multiplicative structure $M$ and a subsemigroup $S$ of $M$, if $s$ is a subset of $S$ and $S$ is contained in the subsemigroup closure of $s$, then the closure of $s$ is equal to $S$.

Subsemigroup.closure_induction theorem

 {p : (x : M) → x ∈ closure s → Prop} (mem : ∀ (x) (h : x ∈ s), p x (subset_closure h))
  (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) : p x hx

Full source

/-- An induction principle for closure membership. If `p` holds for all elements of `s`, and
is preserved under multiplication, then `p` holds for all elements of the closure of `s`. -/
@[to_additive (attr := elab_as_elim) "An induction principle for additive closure membership. If `p`
  holds for all elements of `s`, and is preserved under addition, then `p` holds for all
  elements of the additive closure of `s`."]
theorem closure_induction {p : (x : M) → x ∈ closure s → Prop}
    (mem : ∀ (x) (h : x ∈ s), p x (subset_closure h))
    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) :
    p x hx :=
  let S : Subsemigroup M :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩ }
  closure_le (S := S) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Induction Principle for Subsemigroup Closure

Informal description

Let $M$ be a multiplicative structure, $s \subseteq M$ a subset, and $\text{closure}(s)$ the subsemigroup generated by $s$. Given a predicate $p : M \to \text{Prop}$ such that: 1. For all $x \in s$, $p(x)$ holds; 2. For all $x, y \in \text{closure}(s)$, if $p(x)$ and $p(y)$ hold, then $p(x * y)$ holds; then for all $x \in \text{closure}(s)$, $p(x)$ holds.

Subsemigroup.closure_induction₂ theorem

 {p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop}
  (mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy))
  (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
  (mul_right : ∀ x y z hx hy hz, p z x hz hx → p z y hz hy → p z (x * y) hz (mul_mem hx hy)) {x y : M}
  (hx : x ∈ closure s) (hy : y ∈ closure s) : p x y hx hy

Full source

/-- An induction principle for closure membership for predicates with two arguments. -/
@[to_additive (attr := elab_as_elim) "An induction principle for additive closure membership for
  predicates with two arguments."]
theorem closure_induction₂ {p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop}
    (mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy))
    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
    (mul_right : ∀ x y z hx hy hz, p z x hz hx → p z y hz hy → p z (x * y) hz (mul_mem hx hy))
    {x y : M} (hx : x ∈ closure s) (hy : y ∈ closure s) : p x y hx hy := by
  induction hx using closure_induction with
  | mem z hz => induction hy using closure_induction with
    | mem _ h => exact mem _ _ hz h
    | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ hy h₁ h₂

Double Induction Principle for Subsemigroup Closure

Informal description

Let $M$ be a multiplicative structure and $s \subseteq M$ a subset. Let $\text{closure}(s)$ be the subsemigroup generated by $s$. Given a predicate $p : M \times M \to \text{Prop}$ such that: 1. For all $x, y \in s$, $p(x, y)$ holds; 2. For all $x, y, z \in \text{closure}(s)$, if $p(x, z)$ and $p(y, z)$ hold, then $p(x * y, z)$ holds; 3. For all $x, y, z \in \text{closure}(s)$, if $p(z, x)$ and $p(z, y)$ hold, then $p(z, x * y)$ holds; then for all $x, y \in \text{closure}(s)$, $p(x, y)$ holds.

Subsemigroup.dense_induction theorem

 {p : M → Prop} (s : Set M) (closure : closure s = ⊤) (mem : ∀ x ∈ s, p x) (mul : ∀ x y, p x → p y → p (x * y))
  (x : M) : p x

Full source

/-- If `s` is a dense set in a magma `M`, `Subsemigroup.closure s = ⊤`, then in order to prove that
some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x ∈ s`,
and verify that `p x` and `p y` imply `p (x * y)`. -/
@[to_additive (attr := elab_as_elim) "If `s` is a dense set in an additive monoid `M`,
  `AddSubsemigroup.closure s = ⊤`, then in order to prove that some predicate `p` holds
  for all `x : M` it suffices to verify `p x` for `x ∈ s`, and verify that `p x` and `p y` imply
  `p (x + y)`."]
theorem dense_induction {p : M → Prop} (s : Set M) (closure : closure s = ⊤)
    (mem : ∀ x ∈ s, p x) (mul : ∀ x y, p x → p y → p (x * y)) (x : M) :
    p x := by
  induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

Induction Principle for Dense Subsemigroups

Informal description

Let $M$ be a multiplicative structure and $s \subseteq M$ a dense subset such that the subsemigroup closure of $s$ is the entire structure (i.e., $\text{closure}(s) = \top$). To prove that a predicate $p$ holds for all $x \in M$, it suffices to verify: 1. $p(x)$ holds for all $x \in s$; 2. For any $x, y \in M$, if $p(x)$ and $p(y)$ hold, then $p(x * y)$ holds.

Subsemigroup.gi definition

: GaloisInsertion (@closure M _) SetLike.coe

Full source

/-- `closure` forms a Galois insertion with the coercion to set. -/
@[to_additive "`closure` forms a Galois insertion with the coercion to set."]
protected def gi : GaloisInsertion (@closure M _) SetLike.coe :=
  GaloisConnection.toGaloisInsertion (fun _ _ => closure_le) fun _ => subset_closure

Galois insertion between subsemigroup closure and underlying set

Informal description

The pair of functions `closure` (which maps a set to the subsemigroup it generates) and the coercion `SetLike.coe` (which maps a subsemigroup to its underlying set) form a Galois insertion. This means: 1. For any set $s$ and subsemigroup $S$, we have $\text{closure}(s) \leq S$ if and only if $s \subseteq S$ (as sets). 2. The composition $\text{closure} \circ \text{SetLike.coe}$ is the identity on subsemigroups, i.e., the closure of the underlying set of a subsemigroup $S$ is $S$ itself.

Subsemigroup.closure_eq theorem

: closure (S : Set M) = S

Full source

/-- Closure of a subsemigroup `S` equals `S`. -/
@[to_additive (attr := simp) "Additive closure of an additive subsemigroup `S` equals `S`"]
theorem closure_eq : closure (S : Set M) = S :=
  (Subsemigroup.gi M).l_u_eq S

Subsemigroup Closure Identity: $\text{closure}(S) = S$

Informal description

For any subsemigroup $S$ of a multiplicative structure $M$, the closure of $S$ (as a set) is equal to $S$ itself, i.e., $\text{closure}(S) = S$.

Subsemigroup.closure_empty theorem

: closure (∅ : Set M) = ⊥

Full source

@[to_additive (attr := simp)]
theorem closure_empty : closure (∅ : Set M) = ⊥ :=
  (Subsemigroup.gi M).gc.l_bot

Closure of Empty Set is Bottom Subsemigroup

Informal description

The subsemigroup generated by the empty set in a multiplicative structure $M$ is the bottom element of the complete lattice of subsemigroups, i.e., $\text{closure}(\emptyset) = \bot$.

Subsemigroup.closure_univ theorem

: closure (univ : Set M) = ⊤

Full source

@[to_additive (attr := simp)]
theorem closure_univ : closure (univ : Set M) = ⊤ :=
  @coe_top M _ ▸ closure_eq ⊤

Closure of Universal Set is Top Subsemigroup

Informal description

The subsemigroup generated by the universal set in a multiplicative structure $M$ is equal to the top element of the complete lattice of subsemigroups, i.e., $\text{closure}(\text{univ}) = \top$.

Subsemigroup.closure_union theorem

(s t : Set M) : closure (s ∪ t) = closure s ⊔ closure t

Full source

@[to_additive]
theorem closure_union (s t : Set M) : closure (s ∪ t) = closureclosure s ⊔ closure t :=
  (Subsemigroup.gi M).gc.l_sup

Subsemigroup Closure of Union Equals Supremum of Closures: $\text{closure}(s \cup t) = \text{closure}(s) \sqcup \text{closure}(t)$

Informal description

For any two subsets $s$ and $t$ of a multiplicative structure $M$, the subsemigroup generated by their union $s \cup t$ is equal to the supremum of the subsemigroups generated by $s$ and $t$ individually, i.e., $\text{closure}(s \cup t) = \text{closure}(s) \sqcup \text{closure}(t)$.

Subsemigroup.closure_iUnion theorem

{ι} (s : ι → Set M) : closure (⋃ i, s i) = ⨆ i, closure (s i)

Full source

@[to_additive]
theorem closure_iUnion {ι} (s : ι → Set M) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
  (Subsemigroup.gi M).gc.l_iSup

Subsemigroup Closure of Union Equals Supremum of Closures

Informal description

For any indexed family of sets $s_i$ in a multiplicative structure $M$, the subsemigroup generated by the union $\bigcup_i s_i$ is equal to the supremum of the subsemigroups generated by each individual set $s_i$, i.e., \[ \text{closure}\left(\bigcup_i s_i\right) = \bigsqcup_i \text{closure}(s_i). \]

Subsemigroup.closure_singleton_le_iff_mem theorem

(m : M) (p : Subsemigroup M) : closure { m } ≤ p ↔ m ∈ p

Full source

@[to_additive]
theorem closure_singleton_le_iff_mem (m : M) (p : Subsemigroup M) : closureclosure {m} ≤ p ↔ m ∈ p := by
  rw [closure_le, singleton_subset_iff, SetLike.mem_coe]

Singleton Subsemigroup Containment Criterion: $\text{closure}(\{m\}) \leq p \leftrightarrow m \in p$

Informal description

For any element $m$ in a multiplicative structure $M$ and any subsemigroup $p$ of $M$, the subsemigroup generated by the singleton set $\{m\}$ is contained in $p$ if and only if $m$ is an element of $p$.

Subsemigroup.mem_iSup theorem

{ι : Sort*} (p : ι → Subsemigroup M) {m : M} : (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N

Full source

@[to_additive]
theorem mem_iSup {ι : Sort*} (p : ι → Subsemigroup M) {m : M} :
    (m ∈ ⨆ i, p i) ↔ ∀ N, (∀ i, p i ≤ N) → m ∈ N := by
  rw [← closure_singleton_le_iff_mem, le_iSup_iff]
  simp only [closure_singleton_le_iff_mem]

Characterization of Membership in Supremum of Subsemigroups: $m \in \bigsqcup_i p_i \leftrightarrow (\forall N, (\forall i, p_i \leq N) \to m \in N)$

Informal description

Let $M$ be a multiplicative structure, $(p_i)_{i \in \iota}$ a family of subsemigroups of $M$, and $m \in M$. Then $m$ belongs to the supremum $\bigsqcup_i p_i$ of the family $(p_i)$ if and only if for every subsemigroup $N$ of $M$ that contains all $p_i$, we have $m \in N$.

Subsemigroup.iSup_eq_closure theorem

{ι : Sort*} (p : ι → Subsemigroup M) : ⨆ i, p i = Subsemigroup.closure (⋃ i, (p i : Set M))

Full source

@[to_additive]
theorem iSup_eq_closure {ι : Sort*} (p : ι → Subsemigroup M) :
    ⨆ i, p i = Subsemigroup.closure (⋃ i, (p i : Set M)) := by
  simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]

Supremum of Subsemigroups Equals Closure of Their Union

Informal description

For any family of subsemigroups $(p_i)_{i \in \iota}$ of a multiplicative structure $M$, the supremum $\bigsqcup_i p_i$ of the family is equal to the subsemigroup generated by the union $\bigcup_i p_i$ of their underlying sets.

MulHom.eqOn_closure theorem

{f g : M →ₙ* N} {s : Set M} (h : Set.EqOn f g s) : Set.EqOn f g (closure s)

Full source

/-- If two mul homomorphisms are equal on a set, then they are equal on its subsemigroup closure. -/
@[to_additive "If two add homomorphisms are equal on a set,
  then they are equal on its additive subsemigroup closure."]
theorem eqOn_closure {f g : M →ₙ* N} {s : Set M} (h : Set.EqOn f g s) :
    Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocus g from closure_le.2 h

Agreement of Multiplicative Homomorphisms on Subsemigroup Closure

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f, g \colon M \to N$ be non-unital multiplicative homomorphisms. If $f$ and $g$ agree on a subset $s \subseteq M$, then they also agree on the subsemigroup closure of $s$.

MulHom.ofDense definition

 {M N} [Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : closure s = ⊤)
  (hmul : ∀ (x), ∀ y ∈ s, f (x * y) = f x * f y) : M →ₙ* N

Full source

/-- Let `s` be a subset of a semigroup `M` such that the closure of `s` is the whole semigroup.
Then `MulHom.ofDense` defines a mul homomorphism from `M` asking for a proof
of `f (x * y) = f x * f y` only for `y ∈ s`. -/
@[to_additive]
def ofDense {M N} [Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : closure s = ⊤)
    (hmul : ∀ (x), ∀ y ∈ s, f (x * y) = f x * f y) :
    M →ₙ* N where
  toFun := f
  map_mul' x y :=
    dense_induction _ hs (fun y hy x => hmul x y hy)
      (fun y₁ y₂ h₁ h₂ x => by simp only [← mul_assoc, h₁, h₂]) y x

Multiplicative homomorphism defined densely on a generating set

Informal description

Given a semigroup $M$ and a subset $s \subseteq M$ whose closure is the entire semigroup, the function `MulHom.ofDense` constructs a multiplicative homomorphism $f \colon M \to N$ into another semigroup $N$ by only requiring the multiplicative property $f(x * y) = f(x) * f(y)$ to hold for all $x \in M$ and $y \in s$.

MulHom.coe_ofDense theorem

[Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : closure s = ⊤) (hmul) : (ofDense f hs hmul : M → N) = f

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_ofDense [Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : closure s = ⊤)
    (hmul) : (ofDense f hs hmul : M → N) = f :=
  rfl

Underlying Function of Densely Defined Multiplicative Homomorphism

Informal description

Let $M$ and $N$ be semigroups, $s \subseteq M$ a subset whose closure equals $M$, and $f: M \to N$ a function satisfying $f(x * y) = f(x) * f(y)$ for all $x \in M$ and $y \in s$. Then the underlying function of the multiplicative homomorphism `MulHom.ofDense f hs hmul` equals $f$.

Mathlib.Algebra.Group.Subsemigroup.Basic

Main definitions

Implementation notes

Tags