Mathlib.Algebra.Group.Submonoid.Basic

Module docstring

{"# Submonoids: CompleteLattice structure

This file defines a CompleteLattice structure on Submonoids, define the closure of a set as the minimal submonoid that includes this set, and prove a few results about extending properties from a dense set (i.e. a set with closure s = ⊤) to the whole monoid, see Submonoid.dense_induction and MonoidHom.ofClosureEqTopLeft/MonoidHom.ofClosureEqTopRight.

Main definitions

For each of the following definitions in the Submonoid namespace, there is a corresponding definition in the AddSubmonoid namespace.

Submonoid.copy : copy of a submonoid with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original Submonoid.
Submonoid.closure : monoid closure of a set, i.e., the least submonoid that includes the set.
Submonoid.gi : closure : Set M → Submonoid M and coercion coe : Submonoid M → Set M form a GaloisInsertion;
MonoidHom.eqLocus: the submonoid of elements x : M such that f x = g x;
MonoidHom.ofClosureEqTopRight: if a map f : M → N between two monoids satisfies f 1 = 1 and f (x * y) = f x * f y for y from some dense set s, then f is a monoid homomorphism. E.g., if f : ℕ → M satisfies f 0 = 0 and f (x + 1) = f x + f 1, then f is an additive monoid homomorphism.

Implementation notes

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

Note that Submonoid M does not actually require Monoid M, instead requiring only the weaker MulOneClass M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers. Submonoid is implemented by extending Subsemigroup requiring one_mem'.

Tags

submonoid, submonoids "}

Submonoid.instInfSet instance

: InfSet (Submonoid M)

Full source

@[to_additive]
instance : InfSet (Submonoid M) :=
  ⟨fun s =>
    { carrier := ⋂ t ∈ s, ↑t
      one_mem' := Set.mem_biInter fun i _ => i.one_mem
      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 Submonoids

Informal description

The collection of submonoids of a monoid $M$ forms a complete lattice with respect to inclusion, where the infimum of a family of submonoids is given by their intersection.

Submonoid.coe_sInf theorem

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

Full source

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

Infimum of Submonoids as Intersection of Underlying Sets

Informal description

For any collection $S$ of submonoids of a monoid $M$, the underlying set of the infimum of $S$ (as submonoids) is equal to the intersection of the underlying sets of all submonoids in $S$. In other words, \[ \inf S = \bigcap_{s \in S} s. \]

Submonoid.mem_sInf theorem

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

Full source

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

Characterization of Membership in Infimum of Submonoids

Informal description

For any set $S$ of submonoids of a monoid $M$ and any element $x \in M$, $x$ belongs to the infimum of $S$ (i.e., the greatest lower bound of $S$ in the lattice of submonoids) if and only if $x$ belongs to every submonoid $p \in S$. In symbols: $$x \in \bigwedge S \leftrightarrow \forall p \in S, x \in p$$

Submonoid.mem_iInf theorem

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

Full source

@[to_additive]
theorem mem_iInf {ι : Sort*} {S : ι → Submonoid 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 Submonoids

Informal description

For any family of submonoids $\{S_i\}_{i \in \iota}$ of a monoid $M$ and any element $x \in M$, the element $x$ belongs to the infimum $\bigsqcap_i S_i$ if and only if $x$ belongs to every submonoid $S_i$ in the family.

Submonoid.coe_iInf theorem

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

Full source

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

Infimum of Submonoids as Intersection of Underlying Sets

Informal description

For any indexed family of submonoids $(S_i)_{i \in \iota}$ of a monoid $M$, the underlying set of their infimum $\bigsqcap_i S_i$ is equal to the intersection $\bigcap_i S_i$ of their underlying sets.

Submonoid.instCompleteLattice instance

: CompleteLattice (Submonoid M)

Full source

/-- Submonoids of a monoid form a complete lattice. -/
@[to_additive "The `AddSubmonoid`s of an `AddMonoid` form a complete lattice."]
instance : CompleteLattice (Submonoid M) :=
  { (completeLatticeOfInf (Submonoid M)) fun _ =>
      IsGLB.of_image (f := (SetLike.coe : Submonoid M → Set M))
        (@fun S T => show (S : Set M) ≤ T ↔ S ≤ T from SetLike.coe_subset_coe)
        isGLB_biInf with
    le := (· ≤ ·)
    lt := (· < ·)
    bot := ⊥
    bot_le := fun S _ hx => (mem_bot.1 hx).symm ▸ S.one_mem
    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 of Submonoids

Informal description

The collection of all submonoids of a monoid $M$ forms a complete lattice, where the order is given by inclusion, meets are intersections, and joins are submonoid closures of unions.

Submonoid.closure definition

(s : Set M) : Submonoid M

Full source

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

Submonoid generated by a set

Informal description

The submonoid generated by a subset $s$ of a monoid $M$ is the smallest submonoid of $M$ containing $s$, defined as the infimum of all submonoids containing $s$.

Submonoid.mem_closure theorem

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

Full source

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

Characterization of Membership in Submonoid Closure

Informal description

An element $x$ of a monoid $M$ belongs to the submonoid generated by a subset $s \subseteq M$ if and only if $x$ is contained in every submonoid $S$ of $M$ that contains $s$. In symbols: $$x \in \text{closure}(s) \leftrightarrow \forall S \leq M,\ s \subseteq S \to x \in S$$

Submonoid.subset_closure theorem

: s ⊆ closure s

Full source

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

Submonoid Closure Contains Generating Set

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by $s$ contains $s$ itself, i.e., $s \subseteq \text{closure}(s)$.

Submonoid.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)

Contrapositive of Submonoid Closure Membership

Informal description

For any element $P$ of a monoid $M$ and any subset $s \subseteq M$, if $P$ does not belong to the submonoid generated by $s$, then $P$ does not belong to $s$. In symbols: $$P \notin \text{closure}(s) \implies P \notin s$$

Submonoid.closure_le theorem

: closure s ≤ S ↔ s ⊆ S

Full source

/-- A submonoid `S` includes `closure s` if and only if it includes `s`. -/
@[to_additive (attr := simp)
"An additive submonoid `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⟩

Submonoid Closure Containment Criterion

Informal description

For a subset $s$ of a monoid $M$ and a submonoid $S$ of $M$, the submonoid generated by $s$ is contained in $S$ if and only if $s$ is a subset of $S$. In symbols: $$\text{closure}(s) \leq S \leftrightarrow s \subseteq S$$

Submonoid.closure_mono theorem

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

Full source

/-- Submonoid closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`. -/
@[to_additive (attr := gcongr)
      "Additive submonoid 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 Submonoid Closure

Informal description

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

Submonoid.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₂

Submonoid Closure Equality Criterion

Informal description

For a subset $s$ of a monoid $M$ and a submonoid $S$ of $M$, if $s$ is contained in $S$ and $S$ is contained in the submonoid generated by $s$, then the submonoid generated by $s$ is equal to $S$. In symbols: $$ s \subseteq S \text{ and } S \leq \text{closure}(s) \implies \text{closure}(s) = S $$

Submonoid.closure_induction theorem

 {s : Set M} {motive : (x : M) → x ∈ closure s → Prop} (mem : ∀ (x) (h : x ∈ s), motive x (subset_closure h))
  (one : motive 1 (one_mem _)) (mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem hx hy)) {x}
  (hx : x ∈ closure s) : motive x hx

Full source

/-- An induction principle for closure membership. If `p` holds for `1` and 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 `0` and all
      elements of `s`, and is preserved under addition, then `p` holds for all elements of the
      additive closure of `s`."]
theorem closure_induction {s : Set M} {motive : (x : M) → x ∈ closure s → Prop}
    (mem : ∀ (x) (h : x ∈ s), motive x (subset_closure h)) (one : motive 1 (one_mem _))
    (mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem hx hy)) {x}
    (hx : x ∈ closure s) : motive x hx :=
  let S : Submonoid M :=
    { carrier := { x | ∃ hx, motive x hx }
      one_mem' := ⟨_, one⟩
      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 Submonoid Closure Membership

Informal description

Let $M$ be a monoid and $s$ a subset of $M$. Suppose $p$ is a predicate on elements of the submonoid generated by $s$ satisfying: 1. $p(x)$ holds for all $x \in s$, 2. $p(1)$ holds, and 3. For any $x, y$ in the closure of $s$, if $p(x)$ and $p(y)$ hold, then $p(x * y)$ holds. Then $p(x)$ holds for every element $x$ in the submonoid generated by $s$.

Submonoid.closure_induction₂ theorem

 {motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop}
  (mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), motive x y (subset_closure hx) (subset_closure hy))
  (one_left : ∀ x hx, motive 1 x (one_mem _) hx) (one_right : ∀ x hx, motive x 1 hx (one_mem _))
  (mul_left : ∀ x y z hx hy hz, motive x z hx hz → motive y z hy hz → motive (x * y) z (mul_mem hx hy) hz)
  (mul_right : ∀ x y z hx hy hz, motive z x hz hx → motive z y hz hy → motive z (x * y) hz (mul_mem hx hy)) {x y : M}
  (hx : x ∈ closure s) (hy : y ∈ closure s) : motive 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₂ {motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop}
    (mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), motive x y (subset_closure hx) (subset_closure hy))
    (one_left : ∀ x hx, motive 1 x (one_mem _) hx) (one_right : ∀ x hx, motive x 1 hx (one_mem _))
    (mul_left : ∀ x y z hx hy hz,
      motive x z hx hz → motive y z hy hz → motive (x * y) z (mul_mem hx hy) hz)
    (mul_right : ∀ x y z hx hy hz,
      motive z x hz hx → motive z y hz hy → motive z (x * y) hz (mul_mem hx hy))
    {x y : M} (hx : x ∈ closure s) (hy : y ∈ closure s) : motive x y hx hy := by
  induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂

Two-Variable Induction Principle for Submonoid Closure Membership

Informal description

Let $M$ be a monoid and $s$ a subset of $M$. Suppose $p$ is a predicate on pairs of elements of the submonoid generated by $s$ satisfying: 1. $p(x, y)$ holds for all $x, y \in s$, 2. $p(1, x)$ and $p(x, 1)$ hold for all $x$ in the closure of $s$, 3. For any $x, y, z$ in the closure of $s$, if $p(x, z)$ and $p(y, z)$ hold, then $p(x * y, z)$ holds, and 4. For any $x, y, z$ in the closure of $s$, if $p(z, x)$ and $p(z, y)$ hold, then $p(z, x * y)$ holds. Then $p(x, y)$ holds for every pair of elements $x, y$ in the submonoid generated by $s$.

Submonoid.dense_induction theorem

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

Full source

/-- If `s` is a dense set in a monoid `M`, `Submonoid.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`, verify `p 1`,
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`, `AddSubmonoid.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`, verify `p 0`, and verify that `p x` and `p y` imply `p (x + y)`."]
theorem dense_induction {motive : M → Prop} (s : Set M) (closure : closure s = ⊤)
    (mem : ∀ x ∈ s, motive x) (one : motive 1) (mul : ∀ x y, motive x → motive y → motive (x * y))
    (x : M) : motive x := by
  induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | one => exact one
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

Dense Submonoid Induction Principle

Informal description

Let $M$ be a monoid and $s$ a subset of $M$ such that the submonoid generated by $s$ is the entire monoid (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)$ for all $x \in s$, 2. $p(1)$, and 3. For any $x, y \in M$, if $p(x)$ and $p(y)$ hold, then $p(x * y)$ holds.

Submonoid.closure_eq_one_union theorem

(s : Set M) : closure s = {(1 : M)} ∪ (Subsemigroup.closure s : Set M)

Full source

/-- The `Submonoid.closure` of a set is the union of `{1}` and its `Subsemigroup.closure`. -/
lemma closure_eq_one_union (s : Set M) :
    closure s = {(1 : M)}{(1 : M)} ∪ (Subsemigroup.closure s : Set M) := by
  apply le_antisymm
  · intro x hx
    induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      simp only [singleton_union, mem_insert_iff, SetLike.mem_coe] at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all
      exact Or.inr <| mul_mem hx hy
  · rintro x (hx | hx)
    · exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)
    · exact Subsemigroup.closure_le.mpr subset_closure hx

Submonoid Closure as Union of Identity and Subsemigroup Closure

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by $s$ is equal to the union of the singleton set $\{1\}$ and the subsemigroup generated by $s$. That is, \[ \text{closure}(s) = \{1\} \cup \text{Subsemigroup.closure}(s). \]

Submonoid.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 where
  choice s _ := closure s
  gc _ _ := closure_le
  le_l_u _ := subset_closure
  choice_eq _ _ := rfl

Galois Insertion of Submonoid Closure and Coercion

Informal description

The pair consisting of the submonoid closure function and the coercion to a set forms a Galois insertion. That is, for any monoid $M$, the function that maps a subset $s$ of $M$ to the smallest submonoid containing $s$ (denoted $\text{closure}(s)$) and the function that maps a submonoid to its underlying set form a Galois insertion between the complete lattice of subsets of $M$ and the complete lattice of submonoids of $M$. This means: 1. For any subset $s$ of $M$, $s$ is contained in the underlying set of $\text{closure}(s)$. 2. For any submonoid $S$ of $M$, $\text{closure}(S) = S$. 3. For any subset $s$ and submonoid $S$, $\text{closure}(s) \leq S$ if and only if $s \subseteq S$.

Submonoid.closure_eq theorem

: closure (S : Set M) = S

Full source

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

Submonoid Closure Equals Itself

Informal description

For any submonoid $S$ of a monoid $M$, the closure of $S$ (as a set) is equal to $S$ itself. That is, $\text{closure}(S) = S$.

Submonoid.closure_empty theorem

: closure (∅ : Set M) = ⊥

Full source

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

Closure of Empty Set is Trivial Submonoid

Informal description

The submonoid generated by the empty set is the trivial submonoid (i.e., the bottom element of the lattice of submonoids).

Submonoid.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 Submonoid

Informal description

The submonoid generated by the entire set of a monoid $M$ is equal to the top submonoid (i.e., $M$ itself). That is, $\text{closure}(\text{univ}) = \top$.

Submonoid.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 :=
  (Submonoid.gi M).gc.l_sup

Submonoid Closure of Union Equals Supremum of Closures

Informal description

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

Submonoid.sup_eq_closure theorem

(N N' : Submonoid M) : N ⊔ N' = closure ((N : Set M) ∪ (N' : Set M))

Full source

@[to_additive]
theorem sup_eq_closure (N N' : Submonoid M) : N ⊔ N' = closure ((N : Set M) ∪ (N' : Set M)) := by
  simp_rw [closure_union, closure_eq]

Supremum of Submonoids as Closure of Union

Informal description

For any two submonoids $N$ and $N'$ of a monoid $M$, the supremum $N \sqcup N'$ in the lattice of submonoids is equal to the submonoid generated by the union of their underlying sets, i.e., $$N \sqcup N' = \text{closure}(N \cup N').$$

Submonoid.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) :=
  (Submonoid.gi M).gc.l_iSup

Submonoid Closure of Union Equals Supremum of Closures

Informal description

For any indexed family of subsets $(s_i)_{i \in \iota}$ of a monoid $M$, the submonoid generated by their union $\bigcup_i s_i$ is equal to the supremum of the submonoids generated by each individual subset $s_i$. In symbols: $$\text{closure}\left(\bigcup_{i} s_i\right) = \bigsqcup_{i} \text{closure}(s_i)$$

Submonoid.closure_singleton_le_iff_mem theorem

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

Full source

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

Submonoid Membership Criterion via Singleton Closure

Informal description

For any element $m$ of a monoid $M$ and any submonoid $p$ of $M$, the submonoid generated by the singleton set $\{m\}$ is contained in $p$ if and only if $m$ is an element of $p$. In symbols: $$\text{closure}(\{m\}) \leq p \leftrightarrow m \in p$$

Submonoid.closure_insert_one theorem

(s : Set M) : closure (insert 1 s) = closure s

Full source

@[to_additive (attr := simp)]
theorem closure_insert_one (s : Set M) : closure (insert 1 s) = closure s := by
  rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]
  apply one_mem

Submonoid Closure Unaffected by Adding Identity Element

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by the set obtained by inserting the identity element $1$ into $s$ is equal to the submonoid generated by $s$ itself. In symbols: $$\text{closure}(\{1\} \cup s) = \text{closure}(s)$$

Submonoid.mem_iSup theorem

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

Full source

@[to_additive]
theorem mem_iSup {ι : Sort*} (p : ι → Submonoid 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]

Membership in Supremum of Submonoids via Containment in All Upper Bounds

Informal description

For any family of submonoids $(p_i)_{i \in \iota}$ of a monoid $M$ and any element $m \in M$, the element $m$ belongs to the supremum $\bigsqcup_i p_i$ of the family if and only if for every submonoid $N$ of $M$ that contains all $p_i$, we have $m \in N$.

Submonoid.iSup_eq_closure theorem

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

Full source

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

Supremum of Submonoids Equals Closure of Their Union

Informal description

For any indexed family of submonoids $(p_i)_{i \in \iota}$ of a monoid $M$, the supremum $\bigsqcup_i p_i$ of the family is equal to the submonoid generated by the union $\bigcup_i p_i$ of their underlying sets. In other words: $$\bigsqcup_{i} p_i = \text{closure}\left(\bigcup_{i} p_i\right)$$

Submonoid.disjoint_def theorem

{p₁ p₂ : Submonoid M} : Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Full source

@[to_additive]
theorem disjoint_def {p₁ p₂ : Submonoid M} :
    DisjointDisjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1 := by
  simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]

Characterization of Disjoint Submonoids via Identity Element

Informal description

Two submonoids $p₁$ and $p₂$ of a monoid $M$ are disjoint if and only if the only common element between them is the identity element $1$. In other words, for any $x \in M$, if $x \in p₁$ and $x \in p₂$, then $x = 1$.

Submonoid.disjoint_def' theorem

{p₁ p₂ : Submonoid M} : Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 1

Full source

@[to_additive]
theorem disjoint_def' {p₁ p₂ : Submonoid M} :
    DisjointDisjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 1 :=
  disjoint_def.trans ⟨fun h _ _ hx hy hxy => h hx <| hxy.symm ▸ hy, fun h _ hx hx' => h hx hx' rfl⟩

Disjoint Submonoids Characterization via Equal Elements

Informal description

Two submonoids $p_1$ and $p_2$ of a monoid $M$ are disjoint if and only if for any elements $x \in p_1$ and $y \in p_2$, whenever $x = y$, it follows that $x = 1$ (the identity element of $M$).

Submonoid.closure_sdiff_eq_closure theorem

(hts : t ⊆ closure (s \ t)) : closure (s \ t) = closure s

Full source

@[to_additive (attr := simp)]
lemma closure_sdiff_eq_closure (hts : t ⊆ closure (s \ t)) : closure (s \ t) = closure s := by
  refine (closure_mono Set.diff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_
  by_cases hxt : x ∈ t
  · exact hts hxt
  · rw [SetLike.mem_coe, Submonoid.mem_closure]
    exact fun N hN ↦ hN <| Set.mem_diff_of_mem hxs hxt

Submonoid Closure Equality via Set Difference

Informal description

For subsets $s$ and $t$ of a monoid $M$, if $t$ is contained in the submonoid generated by $s \setminus t$, then the submonoid generated by $s \setminus t$ is equal to the submonoid generated by $s$. In symbols: $$ t \subseteq \text{closure}(s \setminus t) \implies \text{closure}(s \setminus t) = \text{closure}(s) $$

Submonoid.closure_sdiff_singleton_one theorem

(s : Set M) : closure (s \ { 1 }) = closure s

Full source

@[to_additive (attr := simp)]
lemma closure_sdiff_singleton_one (s : Set M) : closure (s \ {1}) = closure s :=
  closure_sdiff_eq_closure <| by simp [one_mem]

Submonoid Closure Equality via Removal of Identity Element

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by $s \setminus \{1\}$ is equal to the submonoid generated by $s$. In symbols: $$\text{closure}(s \setminus \{1\}) = \text{closure}(s)$$

MonoidHom.eqOn_closureM theorem

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

Full source

/-- If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure. -/
@[to_additive
      "If two monoid homomorphisms are equal on a set, then they are equal on its submonoid
      closure."]
theorem eqOn_closureM {f g : M →* N} {s : Set M} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocusM g from closure_le.2 h

Agreement of Monoid Homomorphisms on Submonoid Closure

Informal description

Let $M$ and $N$ be monoids, and let $f, g \colon M \to N$ be monoid homomorphisms. If $f$ and $g$ agree on a subset $s \subseteq M$, then they also agree on the submonoid closure of $s$.

IsUnit.submonoid definition

(M : Type*) [Monoid M] : Submonoid M

Full source

/-- The submonoid consisting of the units of a monoid -/
@[to_additive "The additive submonoid consisting of the additive units of an additive monoid"]
def IsUnit.submonoid (M : Type*) [Monoid M] : Submonoid M where
  carrier := setOf IsUnit
  one_mem' := by simp only [isUnit_one, Set.mem_setOf_eq]
  mul_mem' := by
    intro a b ha hb
    rw [Set.mem_setOf_eq] at *
    exact IsUnit.mul ha hb

Submonoid of units

Informal description

The submonoid of a monoid $M$ consisting of all the units (invertible elements) of $M$.

IsUnit.mem_submonoid_iff theorem

{M : Type*} [Monoid M] (a : M) : a ∈ IsUnit.submonoid M ↔ IsUnit a

Full source

@[to_additive]
theorem IsUnit.mem_submonoid_iff {M : Type*} [Monoid M] (a : M) :
    a ∈ IsUnit.submonoid Ma ∈ IsUnit.submonoid M ↔ IsUnit a := by
  change a ∈ setOf IsUnita ∈ setOf IsUnit ↔ IsUnit a
  rw [Set.mem_setOf_eq]

Characterization of Membership in the Submonoid of Units

Informal description

An element $a$ of a monoid $M$ belongs to the submonoid of units if and only if $a$ is a unit (i.e., invertible) in $M$.

MonoidHom.ofClosureMEqTopLeft definition

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

Full source

/-- Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid.
Then `MonoidHom.ofClosureEqTopLeft` defines a monoid homomorphism from `M` asking for
a proof of `f (x * y) = f x * f y` only for `x ∈ s`. -/
@[to_additive
      "Let `s` be a subset of an additive monoid `M` such that the closure of `s` is
      the whole monoid. Then `AddMonoidHom.ofClosureEqTopLeft` defines an additive monoid
      homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `x ∈ s`. "]
def ofClosureMEqTopLeft {M N} [Monoid M] [Monoid N] {s : Set M} (f : M → N) (hs : closure s = ⊤)
    (h1 : f 1 = 1) (hmul : ∀ x ∈ s, ∀ (y), f (x * y) = f x * f y) :
    M →* N where
  toFun := f
  map_one' := h1
  map_mul' x :=
    dense_induction (motive := _) _ hs hmul fun y => by rw [one_mul, h1, one_mul]
      (fun a b ha hb y => by rw [mul_assoc, ha, ha, hb, mul_assoc]) x

Monoid homomorphism from a function defined on a dense subset

Informal description

Given a monoid $M$ and a subset $s$ of $M$ whose closure is the whole monoid, a function $f \colon M \to N$ to another monoid $N$ that satisfies $f(1) = 1$ and the multiplicative property $f(x \cdot y) = f(x) \cdot f(y)$ for all $x \in s$ and all $y \in M$ can be extended to a monoid homomorphism from $M$ to $N$.

MonoidHom.coe_ofClosureMEqTopLeft theorem

(f : M → N) (hs : closure s = ⊤) (h1 hmul) : ⇑(ofClosureMEqTopLeft f hs h1 hmul) = f

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_ofClosureMEqTopLeft (f : M → N) (hs : closure s = ⊤) (h1 hmul) :
    ⇑(ofClosureMEqTopLeft f hs h1 hmul) = f :=
  rfl

Underlying Function of Monoid Homomorphism from Dense Subset Condition (Left Version)

Informal description

Let $M$ and $N$ be monoids, $s$ a subset of $M$ with $\text{closure}(s) = \top$, and $f: M \to N$ a function satisfying $f(1) = 1$ and $f(x \cdot y) = f(x) \cdot f(y)$ for all $x \in s$ and $y \in M$. Then the underlying function of the monoid homomorphism $\text{ofClosureMEqTopLeft}(f, hs, h1, hmul)$ is equal to $f$.

MonoidHom.ofClosureMEqTopRight definition

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

Full source

/-- Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid.
Then `MonoidHom.ofClosureEqTopRight` defines a monoid homomorphism from `M` asking for
a proof of `f (x * y) = f x * f y` only for `y ∈ s`. -/
@[to_additive
      "Let `s` be a subset of an additive monoid `M` such that the closure of `s` is
      the whole monoid. Then `AddMonoidHom.ofClosureEqTopRight` defines an additive monoid
      homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `y ∈ s`. "]
def ofClosureMEqTopRight {M N} [Monoid M] [Monoid N] {s : Set M} (f : M → N) (hs : closure s = ⊤)
    (h1 : f 1 = 1) (hmul : ∀ (x), ∀ y ∈ s, f (x * y) = f x * f y) :
    M →* N where
  toFun := f
  map_one' := h1
  map_mul' x y :=
    dense_induction _ hs (fun y hy x => hmul x y hy) (by simp [h1])
      (fun y₁ y₂ (h₁ : ∀ _, f _ = f _ * f _) (h₂ : ∀ _, f _ = f _ * f _) x => by
        simp [← mul_assoc, h₁, h₂]) y x

Monoid homomorphism from a function defined on a dense subset (right version)

Informal description

Given a monoid $M$ and a subset $s$ of $M$ whose closure is the whole monoid, a function $f \colon M \to N$ to another monoid $N$ that satisfies $f(1) = 1$ and the multiplicative property $f(x \cdot y) = f(x) \cdot f(y)$ for all $x \in M$ and all $y \in s$ can be extended to a monoid homomorphism from $M$ to $N$.

MonoidHom.coe_ofClosureMEqTopRight theorem

(f : M → N) (hs : closure s = ⊤) (h1 hmul) : ⇑(ofClosureMEqTopRight f hs h1 hmul) = f

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_ofClosureMEqTopRight (f : M → N) (hs : closure s = ⊤) (h1 hmul) :
    ⇑(ofClosureMEqTopRight f hs h1 hmul) = f :=
  rfl

Coincidence of constructed homomorphism with original function for dense subset (right version)

Informal description

Let $M$ and $N$ be monoids, $s$ a subset of $M$ whose closure is the entire monoid, and $f \colon M \to N$ a function satisfying $f(1) = 1$ and $f(x \cdot y) = f(x) \cdot f(y)$ for all $x \in M$ and $y \in s$. Then the underlying function of the monoid homomorphism constructed via `ofClosureMEqTopRight` coincides with $f$.