Mathlib.Algebra.Group.Submonoid.Membership

Submonoid.mem_iSup_of_directed theorem

 {ι} [hι : Nonempty ι] {S : ι → Submonoid M} (hS : Directed (· ≤ ·) S) {x : M} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Full source

@[to_additive]
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Submonoid M} (hS : Directed (· ≤ ·) S)
    {x : M} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i := by
  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
  refine closure_induction (fun _ ↦ mem_iUnion.1) ?_ ?_
  · exact hι.elim fun i ↦ ⟨i, (S i).one_mem⟩
  · rintro x y - - ⟨i, hi⟩ ⟨j, hj⟩
    rcases hS i j with ⟨k, hki, hkj⟩
    exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩

Characterization of Membership in Directed Supremum of Submonoids: $x \in \bigsqcup_i S_i \leftrightarrow \exists i, x \in S_i$

Informal description

Let $M$ be a monoid, $\iota$ a nonempty index set, and $(S_i)_{i \in \iota}$ a directed family of submonoids of $M$ with respect to the inclusion relation $\leq$. For any element $x \in M$, we have $x \in \bigsqcup_i S_i$ if and only if there exists an index $i \in \iota$ such that $x \in S_i$.

Submonoid.coe_iSup_of_directed theorem

 {ι} [Nonempty ι] {S : ι → Submonoid M} (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : Submonoid M) : Set M) = ⋃ i, S i

Full source

@[to_additive]
theorem coe_iSup_of_directed {ι} [Nonempty ι] {S : ι → Submonoid M} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Submonoid M) : Set M) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Supremum of Directed Family of Submonoids Equals Union of Their Underlying Sets

Informal description

Let $M$ be a monoid, $\iota$ a nonempty index set, and $(S_i)_{i \in \iota}$ a directed family of submonoids of $M$ with respect to the inclusion relation $\leq$. Then the underlying set of the supremum of the submonoids $\bigsqcup_i S_i$ is equal to the union of the underlying sets $\bigcup_i S_i$.

Submonoid.mem_sSup_of_directedOn theorem

 {S : Set (Submonoid M)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Full source

@[to_additive]
theorem mem_sSup_of_directedOn {S : Set (Submonoid M)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) {x : M} : x ∈ sSup Sx ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
  haveI : Nonempty S := Sne.to_subtype
  simp [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk]

Characterization of Membership in Directed Supremum of Submonoids: $x \in \bigvee S \leftrightarrow \exists s \in S, x \in s$

Informal description

Let $M$ be a monoid and $S$ a nonempty set of submonoids of $M$ that is directed with respect to the inclusion relation $\leq$. For any element $x \in M$, we have $x \in \bigvee S$ if and only if there exists a submonoid $s \in S$ such that $x \in s$.

Submonoid.coe_sSup_of_directedOn theorem

{S : Set (Submonoid M)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s

Full source

@[to_additive]
theorem coe_sSup_of_directedOn {S : Set (Submonoid M)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Supremum of Directed Set of Submonoids Equals Union of Their Underlying Sets

Informal description

Let $M$ be a monoid and $S$ a nonempty set of submonoids of $M$ that is directed with respect to the inclusion relation $\leq$. Then the underlying set of the supremum $\bigvee S$ is equal to the union of the underlying sets of all submonoids in $S$, i.e., \[ \bigvee S = \bigcup_{s \in S} s. \]

Submonoid.mem_sup_left theorem

{S T : Submonoid M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Full source

@[to_additive]
theorem mem_sup_left {S T : Submonoid M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T := by
  rw [← SetLike.le_def]
  exact le_sup_left

Element in Left Submonoid is in Supremum

Informal description

For any submonoids $S$ and $T$ of a monoid $M$, if an element $x \in M$ belongs to $S$, then $x$ also belongs to the supremum $S \sqcup T$.

Submonoid.mem_sup_right theorem

{S T : Submonoid M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Full source

@[to_additive]
theorem mem_sup_right {S T : Submonoid M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T := by
  rw [← SetLike.le_def]
  exact le_sup_right

Membership in Right Submonoid Implies Membership in Supremum

Informal description

For any submonoids $S$ and $T$ of a monoid $M$, if an element $x \in M$ belongs to $T$, then $x$ also belongs to the supremum $S \sqcup T$ of the two submonoids.

Submonoid.mul_mem_sup theorem

{S T : Submonoid M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

Full source

@[to_additive]
theorem mul_mem_sup {S T : Submonoid M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
  (S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)

Product of Elements from Two Submonoids Belongs to Their Supremum

Informal description

For any submonoids $S$ and $T$ of a monoid $M$, if $x \in S$ and $y \in T$, then their product $x * y$ belongs to the supremum $S \sqcup T$ of the two submonoids.

Submonoid.mem_iSup_of_mem theorem

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

Full source

@[to_additive]
theorem mem_iSup_of_mem {ι : Sort*} {S : ι → Submonoid M} (i : ι) :
    ∀ {x : M}, x ∈ S i → x ∈ iSup S := by
  rw [← SetLike.le_def]
  exact le_iSup _ _

Element in Submonoid Implies Element in Supremum of Submonoids

Informal description

For any indexed family of submonoids $S_i$ of a monoid $M$ and any index $i$, if an element $x \in M$ belongs to $S_i$, then $x$ also belongs to the supremum $\bigsqcup_i S_i$ of the family.

Submonoid.mem_sSup_of_mem theorem

{S : Set (Submonoid M)} {s : Submonoid M} (hs : s ∈ S) : ∀ {x : M}, x ∈ s → x ∈ sSup S

Full source

@[to_additive]
theorem mem_sSup_of_mem {S : Set (Submonoid M)} {s : Submonoid M} (hs : s ∈ S) :
    ∀ {x : M}, x ∈ s → x ∈ sSup S := by
  rw [← SetLike.le_def]
  exact le_sSup hs

Element in Submonoid Implies Element in Supremum of Submonoid Set

Informal description

Let $S$ be a set of submonoids of a monoid $M$, and let $s$ be a submonoid in $S$. For any element $x \in M$, if $x$ belongs to $s$, then $x$ also belongs to the supremum (join) of all submonoids in $S$.

Submonoid.iSup_induction theorem

 {ι : Sort*} (S : ι → Submonoid M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ i, S i) (mem : ∀ (i), ∀ x ∈ S i, motive x)
  (one : motive 1) (mul : ∀ x y, motive x → motive y → motive (x * y)) : motive x

Full source

/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `1` and all elements of `S i` for all `i`, and is preserved under multiplication,
then it holds for all elements of the supremum of `S`. -/
@[to_additive (attr := elab_as_elim)
      " An induction principle for elements of `⨆ i, S i`.
      If `C` holds for `0` and all elements of `S i` for all `i`, and is preserved under addition,
      then it holds for all elements of the supremum of `S`. "]
theorem iSup_induction {ι : Sort*} (S : ι → Submonoid M) {motive : M → Prop} {x : M}
    (hx : x ∈ ⨆ i, S i) (mem : ∀ (i), ∀ x ∈ S i, motive x) (one : motive 1)
    (mul : ∀ x y, motive x → motive y → motive (x * y)) : motive x := by
  rw [iSup_eq_closure] at hx
  refine closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
  exact mem _ _ hi

Induction Principle for Elements in the Supremum of Submonoids

Informal description

Let $M$ be a monoid and $(S_i)_{i \in \iota}$ be a family of submonoids of $M$. For any property $\text{motive}$ on $M$, if: 1. $\text{motive}(x)$ holds for all $x \in S_i$ for every $i \in \iota$, 2. $\text{motive}(1)$ holds, and 3. For any $x, y \in M$, if $\text{motive}(x)$ and $\text{motive}(y)$ hold, then $\text{motive}(x \cdot y)$ holds, then $\text{motive}(x)$ holds for every $x$ in the supremum $\bigsqcup_i S_i$ of the family $(S_i)$.

Submonoid.iSup_induction' theorem

 {ι : Sort*} (S : ι → Submonoid M) {motive : ∀ x, (x ∈ ⨆ i, S i) → Prop}
  (mem : ∀ (i), ∀ (x) (hxS : x ∈ S i), motive x (mem_iSup_of_mem i hxS)) (one : motive 1 (one_mem _))
  (mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem ‹_› ‹_›)) {x : M} (hx : x ∈ ⨆ i, S i) :
  motive x hx

Full source

/-- A dependent version of `Submonoid.iSup_induction`. -/
@[to_additive (attr := elab_as_elim) "A dependent version of `AddSubmonoid.iSup_induction`. "]
theorem iSup_induction' {ι : Sort*} (S : ι → Submonoid M) {motive : ∀ x, (x ∈ ⨆ i, S i) → Prop}
    (mem : ∀ (i), ∀ (x) (hxS : x ∈ S i), motive x (mem_iSup_of_mem i hxS))
    (one : motive 1 (one_mem _))
    (mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem ‹_› ‹_›)) {x : M}
    (hx : x ∈ ⨆ i, S i) : motive x hx := by
  refine Exists.elim (?_ : ∃ Hx, motive x Hx) fun (hx : x ∈ ⨆ i, S i) (hc : motive x hx) => hc
  refine @iSup_induction _ _ ι S (fun m => ∃ hm, motive m hm) _ hx (fun i x hx => ?_) ?_
      fun x y => ?_
  · exact ⟨_, mem _ _ hx⟩
  · exact ⟨_, one⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, mul _ _ _ _ Cx Cy⟩

Dependent Induction Principle for Elements in the Supremum of Submonoids

Informal description

Let $M$ be a monoid and $(S_i)_{i \in \iota}$ be a family of submonoids of $M$. For any property $\text{motive}(x)$ depending on $x \in M$ and its membership in $\bigsqcup_i S_i$, if: 1. For every $i \in \iota$ and every $x \in S_i$, $\text{motive}(x)$ holds (with proof that $x \in \bigsqcup_i S_i$), 2. $\text{motive}(1)$ holds (with proof that $1 \in \bigsqcup_i S_i$), and 3. For any $x, y \in M$ with proofs $hx$ and $hy$ that they belong to $\bigsqcup_i S_i$, if $\text{motive}(x)$ and $\text{motive}(y)$ hold, then $\text{motive}(x \cdot y)$ holds (with proof that $x \cdot y \in \bigsqcup_i S_i$), then $\text{motive}(x)$ holds for every $x \in \bigsqcup_i S_i$ with proof $hx$.

FreeMonoid.closure_range_of theorem

: closure (Set.range <| @of α) = ⊤

Full source

@[to_additive]
theorem closure_range_of : closure (Set.range <| @of α) = ⊤ :=
  eq_top_iff.2 fun x _ =>
    FreeMonoid.recOn x (one_mem _) fun _x _xs hxs =>
      mul_mem (subset_closure <| Set.mem_range_self _) hxs

Submonoid Generated by Canonical Embedding Equals Free Monoid

Informal description

The submonoid generated by the range of the canonical embedding `of : α → FreeMonoid α` is equal to the entire free monoid, i.e., $\text{closure}(\text{range}(\text{of})) = \top$.

Submonoid.closure_singleton_eq theorem

(x : M) : closure ({ x } : Set M) = mrange (powersHom M x)

Full source

theorem closure_singleton_eq (x : M) : closure ({x} : Set M) = mrange (powersHom M x) :=
  closure_eq_of_le (Set.singleton_subset_iff.2 ⟨Multiplicative.ofAdd 1, pow_one x⟩) fun _ ⟨_, hn⟩ =>
    hn ▸ pow_mem (subset_closure <| Set.mem_singleton _) _

Submonoid Generated by a Single Element Equals its Powers

Informal description

For any element $x$ in a monoid $M$, the submonoid generated by the singleton set $\{x\}$ is equal to the range of the monoid homomorphism that sends each natural number $n$ to $x^n$. In other words: $$\text{closure}(\{x\}) = \{x^n \mid n \in \mathbb{N}\}.$$

Submonoid.mem_closure_singleton theorem

{x y : M} : y ∈ closure ({ x } : Set M) ↔ ∃ n : ℕ, x ^ n = y

Full source

/-- The submonoid generated by an element of a monoid equals the set of natural number powers of
    the element. -/
theorem mem_closure_singleton {x y : M} : y ∈ closure ({x} : Set M)y ∈ closure ({x} : Set M) ↔ ∃ n : ℕ, x ^ n = y := by
  rw [closure_singleton_eq, mem_mrange]; rfl

Characterization of Elements in the Submonoid Generated by a Single Element via Powers

Informal description

For any elements $x$ and $y$ in a monoid $M$, the element $y$ belongs to the submonoid generated by $\{x\}$ if and only if there exists a natural number $n$ such that $x^n = y$. In other words: $$ y \in \langle \{x\} \rangle \leftrightarrow \exists n \in \mathbb{N}, x^n = y. $$

Submonoid.mem_closure_singleton_self theorem

{y : M} : y ∈ closure ({ y } : Set M)

Full source

theorem mem_closure_singleton_self {y : M} : y ∈ closure ({y} : Set M) :=
  mem_closure_singleton.2 ⟨1, pow_one y⟩

Self-membership in Submonoid Generated by a Single Element

Informal description

For any element $y$ in a monoid $M$, the element $y$ belongs to the submonoid generated by the singleton set $\{y\}$.

Submonoid.closure_singleton_one theorem

: closure ({ 1 } : Set M) = ⊥

Full source

theorem closure_singleton_one : closure ({1} : Set M) = ⊥ := by
  simp [eq_bot_iff_forall, mem_closure_singleton]

Triviality of Submonoid Generated by Identity Element

Informal description

The submonoid generated by the singleton set $\{1\}$ in a monoid $M$ is equal to the trivial submonoid $\bot$, which consists only of the multiplicative identity element.

Submonoid.card_bot theorem

{_ : Fintype (⊥ : Submonoid M)} : card (⊥ : Submonoid M) = 1

Full source

@[to_additive]
theorem card_bot {_ : Fintype (⊥ : Submonoid M)} : card (⊥ : Submonoid M) = 1 :=
  card_eq_one_iff.2
    ⟨⟨(1 : M), Set.mem_singleton 1⟩, fun ⟨_y, hy⟩ => Subtype.eq <| mem_bot.1 hy⟩

Cardinality of Trivial Submonoid is One

Informal description

For any monoid $M$ where the trivial submonoid $\{\1\}$ is finite, the cardinality of the trivial submonoid is $1$.

Submonoid.card_le_one_iff_eq_bot theorem

: card S ≤ 1 ↔ S = ⊥

Full source

@[to_additive card_le_one_iff_eq_bot]
theorem card_le_one_iff_eq_bot : cardcard S ≤ 1 ↔ S = ⊥ :=
  ⟨fun h =>
    (eq_bot_iff_forall _).2 fun x hx => by
      simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1,
    fun h => by simp [h]⟩

Submonoid Cardinality Bound: $|S| \leq 1 \iff S = \{1\}$

Informal description

For a submonoid $S$ of a monoid $M$, the cardinality of $S$ is at most 1 if and only if $S$ is the trivial submonoid $\{1\}$.

FreeMonoid.mrange_lift theorem

{α} (f : α → M) : mrange (FreeMonoid.lift f) = closure (Set.range f)

Full source

@[to_additive]
theorem _root_.FreeMonoid.mrange_lift {α} (f : α → M) :
    mrange (FreeMonoid.lift f) = closure (Set.range f) := by
  rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]

Range of Free Monoid Lift Equals Generated Submonoid of Range

Informal description

For any function $f \colon \alpha \to M$ from a set $\alpha$ to a monoid $M$, the range of the monoid homomorphism $\mathrm{lift}(f) \colon \mathrm{FreeMonoid}(\alpha) \to M$ is equal to the submonoid of $M$ generated by the range of $f$. In symbols: $$ \mathrm{range}(\mathrm{lift}(f)) = \langle f(\alpha) \rangle $$

Submonoid.closure_eq_mrange theorem

(s : Set M) : closure s = mrange (FreeMonoid.lift ((↑) : s → M))

Full source

@[to_additive]
theorem closure_eq_mrange (s : Set M) : closure s = mrange (FreeMonoid.lift ((↑) : s → M)) := by
  rw [FreeMonoid.mrange_lift, Subtype.range_coe]

Submonoid Generation as Range of Free Monoid Lift

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by $s$ is equal to the range of the monoid homomorphism obtained by lifting the inclusion map $(\uparrow) : s \to M$ to the free monoid on $s$. In symbols: $$ \langle s \rangle = \mathrm{range}(\mathrm{lift}(\uparrow)) $$ where $\langle s \rangle$ denotes the submonoid generated by $s$, $\mathrm{lift}$ is the free monoid lift operation, and $\uparrow$ is the inclusion map from $s$ to $M$.

Submonoid.closure_eq_image_prod theorem

(s : Set M) : (closure s : Set M) = List.prod '' {l : List M | ∀ x ∈ l, x ∈ s}

Full source

@[to_additive]
theorem closure_eq_image_prod (s : Set M) :
    (closure s : Set M) = List.prodList.prod '' { l : List M | ∀ x ∈ l, x ∈ s } := by
  rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]
  exact congrArg _ (funext <| FreeMonoid.lift_apply _)

Submonoid Generation as Product Image of Lists

Informal description

For any subset $s$ of a monoid $M$, the underlying set of the submonoid generated by $s$ is equal to the image of the product operation applied to the set of all finite lists of elements from $s$. In other words: $$ \langle s \rangle = \{ \prod_{i=1}^n x_i \mid n \in \mathbb{N}, x_i \in s \text{ for all } i \} $$ where $\langle s \rangle$ denotes the submonoid generated by $s$ and $\prod$ denotes the product of the list elements.

Submonoid.exists_list_of_mem_closure theorem

{s : Set M} {x : M} (hx : x ∈ closure s) : ∃ l : List M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Full source

@[to_additive]
theorem exists_list_of_mem_closure {s : Set M} {x : M} (hx : x ∈ closure s) :
    ∃ l : List M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x := by
  rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx

Factorization of Submonoid Elements into Products of Generators

Informal description

For any subset $s$ of a monoid $M$ and any element $x$ in the submonoid generated by $s$, there exists a finite list $l$ of elements of $M$ such that every element of $l$ belongs to $s$ and the product of the elements of $l$ equals $x$.

Submonoid.exists_multiset_of_mem_closure theorem

 {M : Type*} [CommMonoid M] {s : Set M} {x : M} (hx : x ∈ closure s) : ∃ l : Multiset M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Full source

@[to_additive]
theorem exists_multiset_of_mem_closure {M : Type*} [CommMonoid M] {s : Set M} {x : M}
    (hx : x ∈ closure s) : ∃ l : Multiset M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x := by
  obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
  exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩

Factorization in Commutative Submonoids via Multisets

Informal description

Let $M$ be a commutative monoid and $s$ a subset of $M$. For any element $x$ in the submonoid generated by $s$, there exists a finite multiset $l$ of elements of $M$ such that every element of $l$ belongs to $s$ and the product of the elements of $l$ equals $x$.

Submonoid.closure_induction_left theorem

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

Full source

@[to_additive (attr := elab_as_elim)]
theorem closure_induction_left {s : Set M} {p : (m : M) → m ∈ closure s → Prop}
    (one : p 1 (one_mem _))
    (mul_left : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy → p (x * y) (mul_mem (subset_closure hx) hy))
    {x : M} (h : x ∈ closure s) :
    p x h := by
  simp_rw [closure_eq_mrange] at h
  obtain ⟨l, rfl⟩ := h
  induction l using FreeMonoid.inductionOn' with
  | one => exact one
  | mul_of x y ih =>
    simp only [map_mul, FreeMonoid.lift_eval_of]
    refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
    simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

Left Induction Principle for Submonoid Generation

Informal description

Let $M$ be a monoid and $s$ a subset of $M$. For any predicate $p$ on elements of the submonoid generated by $s$, if: 1. $p$ holds for the identity element $1 \in M$, and 2. For any $x \in s$ and any $y$ in the submonoid generated by $s$, if $p$ holds for $y$, then $p$ holds for $x * y$, then $p$ holds for every element $x$ in the submonoid generated by $s$.

Submonoid.induction_of_closure_eq_top_left theorem

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

Full source

@[to_additive (attr := elab_as_elim)]
theorem induction_of_closure_eq_top_left {s : Set M} {p : M → Prop} (hs : closure s = ⊤) (x : M)
    (one : p 1) (mul : ∀ x ∈ s, ∀ (y), p y → p (x * y)) : p x := by
  have : x ∈ closure s := by simp [hs]
  induction this using closure_induction_left with
  | one => exact one
  | mul_left x hx y _ ih => exact mul x hx y ih

Left Induction Principle for Monoid with Full Submonoid Generated by a Set

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., $\mathrm{closure}(s) = \top$). For any predicate $p$ on $M$, if: 1. $p$ holds for the identity element $1 \in M$, and 2. For any $x \in s$ and any $y \in M$, if $p$ holds for $y$, then $p$ holds for $x * y$, then $p$ holds for every element $x \in M$.

Submonoid.closure_induction_right theorem

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

Full source

@[to_additive (attr := elab_as_elim)]
theorem closure_induction_right {s : Set M} {p : (m : M) → m ∈ closure s → Prop}
    (one : p 1 (one_mem _))
    (mul_right : ∀ x hx, ∀ (y) (hy : y ∈ s), p x hx → p (x * y) (mul_mem hx (subset_closure hy)))
    {x : M} (h : x ∈ closure s) : p x h :=
  closure_induction_left (s := MulOpposite.unopMulOpposite.unop ⁻¹' s)
    (p := fun m hm => p m.unop <| by rwa [← op_closure] at hm)
    one
    (fun _x hx _y _ => mul_right _ _ _ hx)
    (by rwa [← op_closure])

Right Induction Principle for Submonoid Generation

Informal description

Let $M$ be a monoid and $s$ a subset of $M$. For any predicate $p$ on elements of the submonoid generated by $s$, if: 1. $p$ holds for the identity element $1 \in M$, and 2. For any $x$ in the submonoid generated by $s$ and any $y \in s$, if $p$ holds for $x$, then $p$ holds for $x * y$, then $p$ holds for every element $x$ in the submonoid generated by $s$.

Submonoid.induction_of_closure_eq_top_right theorem

 {s : Set M} {p : M → Prop} (hs : closure s = ⊤) (x : M) (H1 : p 1) (Hmul : ∀ (x), ∀ y ∈ s, p x → p (x * y)) : p x

Full source

@[to_additive (attr := elab_as_elim)]
theorem induction_of_closure_eq_top_right {s : Set M} {p : M → Prop} (hs : closure s = ⊤) (x : M)
    (H1 : p 1) (Hmul : ∀ (x), ∀ y ∈ s, p x → p (x * y)) : p x := by
  have : x ∈ closure s := by simp [hs]
  induction this using closure_induction_right with
  | one => exact H1
  | mul_right x _ y hy ih => exact Hmul x y hy ih

Right Induction Principle for Monoid with Full Submonoid Generated by a Set

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., $\mathrm{closure}(s) = \top$). For any predicate $p$ on $M$, if: 1. $p$ holds for the identity element $1 \in M$, and 2. For any $x \in M$ and any $y \in s$, if $p$ holds for $x$, then $p$ holds for $x * y$, then $p$ holds for every element $x \in M$.

Submonoid.powers definition

(n : M) : Submonoid M

Full source

/-- The submonoid generated by an element. -/
def powers (n : M) : Submonoid M :=
  Submonoid.copy (mrange (powersHom M n)) (Set.range (n ^ · : ℕ → M)) <|
    Set.ext fun n => exists_congr fun i => by simp; rfl

Submonoid generated by powers of an element

Informal description

The submonoid generated by a single element $n$ in a monoid $M$ consists of all natural number powers of $n$, i.e., the set $\{n^k \mid k \in \mathbb{N}\}$.

Submonoid.mem_powers theorem

(n : M) : n ∈ powers n

Full source

theorem mem_powers (n : M) : n ∈ powers n :=
  ⟨1, pow_one _⟩

Element Belongs to Its Own Powers Submonoid

Informal description

For any element $n$ in a monoid $M$, the element $n$ belongs to the submonoid generated by its powers, i.e., $n \in \langle n \rangle_{\text{powers}}$.

Submonoid.coe_powers theorem

(x : M) : ↑(powers x) = Set.range fun n : ℕ => x ^ n

Full source

theorem coe_powers (x : M) : ↑(powers x) = Set.range fun n : ℕ => x ^ n :=
  rfl

Submonoid of Powers as Range of Exponentiation Function

Informal description

For any element $x$ in a monoid $M$, the underlying set of the submonoid generated by $x$ (i.e., the set of all powers of $x$) is equal to the range of the function $n \mapsto x^n$ where $n$ ranges over the natural numbers. In other words, $\overline{\langle x \rangle} = \{x^n \mid n \in \mathbb{N}\}$.

Submonoid.mem_powers_iff theorem

(x z : M) : x ∈ powers z ↔ ∃ n : ℕ, z ^ n = x

Full source

theorem mem_powers_iff (x z : M) : x ∈ powers zx ∈ powers z ↔ ∃ n : ℕ, z ^ n = x :=
  Iff.rfl

Characterization of Membership in Powers Submonoid: $x \in \langle z \rangle \leftrightarrow \exists n \in \mathbb{N}, z^n = x$

Informal description

For any elements $x$ and $z$ in a monoid $M$, the element $x$ belongs to the submonoid generated by $z$ if and only if there exists a natural number $n$ such that $z^n = x$.

Submonoid.decidableMemPowers instance

: DecidablePred (· ∈ Submonoid.powers a)

Full source

noncomputable instance decidableMemPowers : DecidablePred (· ∈ Submonoid.powers a) :=
  Classical.decPred _

Decidability of Membership in Powers Submonoid

Informal description

For any element $a$ in a monoid $M$, the predicate "belongs to the submonoid generated by powers of $a$" is decidable. That is, for any $x \in M$, it is decidable whether there exists a natural number $n$ such that $x = a^n$.

Submonoid.fintypePowers instance

[Fintype M] : Fintype (powers a)

Full source

noncomputable instance fintypePowers [Fintype M] : Fintype (powers a) :=
  inferInstanceAs <| Fintype {y // y ∈ powers a}

Finiteness of Powers Submonoid in Finite Monoids

Informal description

For any monoid $M$ with a finite underlying set and any element $a \in M$, the submonoid generated by powers of $a$ is finite.

Submonoid.powers_eq_closure theorem

(n : M) : powers n = closure { n }

Full source

theorem powers_eq_closure (n : M) : powers n = closure {n} := by
  ext
  exact mem_closure_singleton.symm

Submonoid Generated by Powers Equals Submonoid Generated by Singleton

Informal description

For any element $n$ in a monoid $M$, the submonoid generated by the powers of $n$ is equal to the submonoid generated by the singleton set $\{n\}$. That is: $$ \langle n \rangle = \langle \{n\} \rangle $$ where $\langle n \rangle$ denotes the submonoid consisting of all powers of $n$ and $\langle \{n\} \rangle$ denotes the smallest submonoid containing $n$.

Submonoid.powers_le theorem

{n : M} {P : Submonoid M} : powers n ≤ P ↔ n ∈ P

Full source

lemma powers_le {n : M} {P : Submonoid M} : powerspowers n ≤ P ↔ n ∈ P := by simp [powers_eq_closure]

Submonoid Generated by Powers is Contained in Submonoid if and only if Generator is in Submonoid

Informal description

For any element $n$ in a monoid $M$ and any submonoid $P$ of $M$, the submonoid generated by the powers of $n$ is contained in $P$ if and only if $n$ belongs to $P$. In other words: $$ \langle n \rangle \subseteq P \leftrightarrow n \in P $$ where $\langle n \rangle$ denotes the submonoid consisting of all powers of $n$.

Submonoid.powers_one theorem

: powers (1 : M) = ⊥

Full source

lemma powers_one : powers (1 : M) = ⊥ := bot_unique <| powers_le.2 <| one_mem _

Powers of Identity Element Generate Trivial Submonoid

Informal description

The submonoid generated by the powers of the multiplicative identity element $1$ in a monoid $M$ is equal to the trivial submonoid $\{1\}$ (denoted as $\bot$ in the lattice of submonoids).

IsIdempotentElem.coe_powers theorem

{a : M} (ha : IsIdempotentElem a) : (Submonoid.powers a : Set M) = { 1, a }

Full source

theorem _root_.IsIdempotentElem.coe_powers {a : M} (ha : IsIdempotentElem a) :
    (Submonoid.powers a : Set M) = {1, a} :=
  let S : Submonoid M :=
  { carrier := {1, a},
    mul_mem' := by
      rintro _ _ (rfl|rfl) (rfl|rfl)
      · rw [one_mul]; exact .inl rfl
      · rw [one_mul]; exact .inr rfl
      · rw [mul_one]; exact .inr rfl
      · rw [ha]; exact .inr rfl
    one_mem' := .inl rfl }
  suffices Submonoid.powers a = S from congr_arg _ this
  le_antisymm (Submonoid.powers_le.mpr <| .inr rfl)
    (by rintro _ (rfl|rfl); exacts [one_mem _, Submonoid.mem_powers _])

Powers Submonoid of an Idempotent Element Equals $\{1, a\}$

Informal description

For any idempotent element $a$ in a monoid $M$ (i.e., $a^2 = a$), the set of elements in the submonoid generated by the powers of $a$ is exactly $\{1, a\}$.

Submonoid.groupPowers abbrev

{x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (powers x)

Full source

/-- The submonoid generated by an element is a group if that element has finite order. -/
abbrev groupPowers {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (powers x) where
  inv x := x ^ (n - 1)
  inv_mul_cancel y := Subtype.ext <| by
    obtain ⟨_, k, rfl⟩ := y
    simp only [coe_one, coe_mul, SubmonoidClass.coe_pow]
    rw [← pow_succ, Nat.sub_add_cancel hpos, ← pow_mul, mul_comm, pow_mul, hx, one_pow]
  zpow z x := x ^ z.natMod n
  zpow_zero' z := by simp only [Int.natMod, Int.zero_emod, Int.toNat_zero, pow_zero]
  zpow_neg' m x := Subtype.ext <| by
    obtain ⟨_, k, rfl⟩ := x
    simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
    rw [Int.negSucc_eq, ← Int.natCast_succ, ← Int.add_mul_emod_self_right (b := (m + 1 : ℕ))]
    nth_rw 1 [← mul_one ((m + 1 : ℕ) : ℤ)]
    rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
    simp only [Int.toNat_natCast]
    rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _),
      ← pow_eq_pow_mod _ hx, pow_mul, pow_mul]
  zpow_succ' m x := Subtype.ext <| by
    obtain ⟨_, k, rfl⟩ := x
    simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]
    norm_cast
    iterate 2 rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]
    rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]

Powers Submonoid Forms a Group under Finite Order Condition

Informal description

For any element $x$ in a monoid $M$ and any positive integer $n$ such that $x^n = 1$, the submonoid generated by the powers of $x$ forms a group.

Submonoid.pow definition

(n : M) (m : ℕ) : powers n

Full source

/-- Exponentiation map from natural numbers to powers. -/
@[simps!]
def pow (n : M) (m : ℕ) : powers n :=
  (powersHom M n).mrangeRestrict (Multiplicative.ofAdd m)

Power function in a submonoid

Informal description

The function `Submonoid.pow` maps a natural number $ m $ to the $ m $-th power of an element $ n $ in a monoid $ M $, represented as an element of the submonoid generated by $ n $. More precisely, for a given element $ n \in M $, the function $ \text{Submonoid.pow}(n) $ sends a natural number $ m $ to $ n^m $ considered as an element of the submonoid $ \text{powers}(n) $, which consists of all powers of $ n $.

Submonoid.pow_apply theorem

(n : M) (m : ℕ) : Submonoid.pow n m = ⟨n ^ m, m, rfl⟩

Full source

theorem pow_apply (n : M) (m : ℕ) : Submonoid.pow n m = ⟨n ^ m, m, rfl⟩ :=
  rfl

Power Application in Submonoid: $\text{Submonoid.pow}(n, m) = \langle n^m, m, \text{rfl}\rangle$

Informal description

For any element $n$ in a monoid $M$ and any natural number $m$, the function `Submonoid.pow` applied to $n$ and $m$ yields the element $\langle n^m, m, \text{rfl}\rangle$ in the submonoid generated by $n$, where $\text{rfl}$ is a proof that $n^m$ is indeed in the submonoid.

Submonoid.log definition

[DecidableEq M] {n : M} (p : powers n) : ℕ

Full source

/-- Logarithms from powers to natural numbers. -/
def log [DecidableEq M] {n : M} (p : powers n) : ℕ :=
  Nat.find <| (mem_powers_iff p.val n).mp p.prop

Minimal exponent for a power in a submonoid

Informal description

Given a monoid element $ n $ and an element $ p $ in the submonoid generated by $ n $ (i.e., $ p $ is a power of $ n $), the function returns the minimal natural number $ k $ such that $ n^k = p $.

Submonoid.pow_log_eq_self theorem

[DecidableEq M] {n : M} (p : powers n) : pow n (log p) = p

Full source

@[simp]
theorem pow_log_eq_self [DecidableEq M] {n : M} (p : powers n) : pow n (log p) = p :=
  Subtype.ext <| Nat.find_spec p.prop

Minimal Exponent Reproduces Element in Powers Submonoid

Informal description

For any element $n$ in a monoid $M$ and any element $p$ in the submonoid generated by $n$, the power of $n$ raised to the minimal exponent that produces $p$ equals $p$ itself. That is, if $p = n^k$ for some minimal $k \in \mathbb{N}$, then $n^{\log p} = p$.

Submonoid.pow_right_injective_iff_pow_injective theorem

{n : M} : (Function.Injective fun m : ℕ => n ^ m) ↔ Function.Injective (pow n)

Full source

theorem pow_right_injective_iff_pow_injective {n : M} :
    (Function.Injective fun m : ℕ => n ^ m) ↔ Function.Injective (pow n) :=
  Subtype.coe_injective.of_comp_iff (pow n)

Injectivity of Power Function vs. Natural Number Exponent Function

Informal description

For an element $n$ in a monoid $M$, the function $m \mapsto n^m$ is injective on natural numbers if and only if the power function $\text{pow}(n) : \mathbb{N} \to \text{powers}(n)$ is injective.

Submonoid.log_pow_eq_self theorem

[DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m) (m : ℕ) : log (pow n m) = m

Full source

@[simp]
theorem log_pow_eq_self [DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m)
    (m : ℕ) : log (pow n m) = m :=
  pow_right_injective_iff_pow_injective.mp h <| pow_log_eq_self _

Minimal Exponent of Power Equals Original Exponent

Informal description

Let $M$ be a monoid and $n \in M$ such that the function $m \mapsto n^m$ is injective on natural numbers. Then for any natural number $m$, the minimal exponent $\log(n^m)$ equals $m$.

Submonoid.powLogEquiv definition

[DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m) : Multiplicative ℕ ≃* powers n

Full source

/-- The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers
when it is injective. The inverse is given by the logarithms. -/
@[simps]
def powLogEquiv [DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m) :
    MultiplicativeMultiplicative ℕ ≃* powers n where
  toFun m := pow n m.toAdd
  invFun m := Multiplicative.ofAdd (log m)
  left_inv := log_pow_eq_self h
  right_inv := pow_log_eq_self
  map_mul' _ _ := by simp only [pow, map_mul, ofAdd_add, toAdd_mul]

Isomorphism between natural numbers and powers submonoid

Informal description

Given a monoid $M$ and an element $n \in M$ such that the function $m \mapsto n^m$ is injective on natural numbers, there exists a multiplicative isomorphism between the additive monoid of natural numbers (considered multiplicatively) and the submonoid of $M$ generated by powers of $n$. Specifically, the isomorphism maps a natural number $k$ (in multiplicative form) to $n^k$ in the powers submonoid, and its inverse maps an element $n^k$ back to $k$ (in multiplicative form). This isomorphism preserves the multiplicative structure.

Submonoid.log_mul theorem

 [DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m) (x y : powers (n : M)) :
  log (x * y) = log x + log y

Full source

theorem log_mul [DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m)
    (x y : powers (n : M)) : log (x * y) = log x + log y :=
  map_mul (powLogEquiv h).symm x y

Logarithmic Property of Minimal Exponents in Powers Submonoid

Informal description

Let $M$ be a monoid and $n \in M$ such that the function $m \mapsto n^m$ is injective on natural numbers. For any two elements $x, y$ in the submonoid generated by powers of $n$, the minimal exponent of their product satisfies $\log(x \cdot y) = \log x + \log y$.

Submonoid.log_pow_int_eq_self theorem

{x : ℤ} (h : 1 < x.natAbs) (m : ℕ) : log (pow x m) = m

Full source

theorem log_pow_int_eq_self {x : ℤ} (h : 1 < x.natAbs) (m : ℕ) : log (pow x m) = m :=
  (powLogEquiv (Int.pow_right_injective h)).symm_apply_apply _

Minimal Exponent of Integer Power Equals Exponent When Base Has Absolute Value Greater Than One

Informal description

For any integer $x$ with $|x| > 1$ and any natural number $m$, the minimal exponent $k$ such that $x^k = x^m$ is equal to $m$, i.e., $\log(x^m) = m$.

Submonoid.map_powers theorem

 {N : Type*} {F : Type*} [Monoid N] [FunLike F M N] [MonoidHomClass F M N] (f : F) (m : M) :
  (powers m).map f = powers (f m)

Full source

@[simp]
theorem map_powers {N : Type*} {F : Type*} [Monoid N] [FunLike F M N] [MonoidHomClass F M N]
    (f : F) (m : M) :
    (powers m).map f = powers (f m) := by
  simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]

Image of Powers Submonoid under Homomorphism Equals Powers Submonoid of Image

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any element $m \in M$, the image under $f$ of the submonoid generated by the powers of $m$ equals the submonoid generated by the powers of $f(m)$. In symbols: $$ f(\langle m \rangle) = \langle f(m) \rangle $$ where $\langle \cdot \rangle$ denotes the submonoid generated by powers of an element.

IsScalarTower.of_mclosure_eq_top theorem

 {N α} [Monoid M] [MulAction M N] [SMul N α] [MulAction M α] {s : Set M} (htop : Submonoid.closure s = ⊤)
  (hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z) : IsScalarTower M N α

Full source

@[to_additive]
theorem IsScalarTower.of_mclosure_eq_top {N α} [Monoid M] [MulAction M N] [SMul N α] [MulAction M α]
    {s : Set M} (htop : Submonoid.closure s = ⊤)
    (hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z) : IsScalarTower M N α := by
  refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
  · intro y z
    rw [one_smul, one_smul]
  · clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hs x hx, hx']

Scalar Tower Condition via Submonoid Generation

Informal description

Let $M$ be a monoid acting on a type $N$, and let $N$ act on a type $\alpha$. Suppose $M$ also acts on $\alpha$, and let $s$ be a subset of $M$ such that the submonoid generated by $s$ is the entire monoid $M$ (i.e., $\mathrm{closure}(s) = \top$). If for every $x \in s$, $y \in N$, and $z \in \alpha$, the scalar multiplication satisfies $(x \cdot y) \cdot z = x \cdot (y \cdot z)$, then $M$, $N$, and $\alpha$ form a scalar tower (i.e., the scalar multiplication is associative in this triple).

SMulCommClass.of_mclosure_eq_top theorem

 {N α} [Monoid M] [SMul N α] [MulAction M α] {s : Set M} (htop : Submonoid.closure s = ⊤)
  (hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z) : SMulCommClass M N α

Full source

@[to_additive]
theorem SMulCommClass.of_mclosure_eq_top {N α} [Monoid M] [SMul N α] [MulAction M α] {s : Set M}
    (htop : Submonoid.closure s = ⊤) (hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z) :
    SMulCommClass M N α := by
  refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
  · intro y z
    rw [one_smul, one_smul]
  · clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hx', hs x hx]

Commutativity of Scalar Actions via Submonoid Generation

Informal description

Let $M$ be a monoid, $N$ a type with a scalar multiplication action on a type $\alpha$, and $M$ acting on $\alpha$ via multiplication. Suppose $s$ is a subset of $M$ such that the submonoid generated by $s$ is the entire monoid $M$ (i.e., $\mathrm{closure}(s) = \top$). If for every $x \in s$, $y \in N$, and $z \in \alpha$, the actions commute as $x \cdot (y \cdot z) = y \cdot (x \cdot z)$, then the actions of $M$ and $N$ on $\alpha$ are commutative, i.e., $\mathrm{SMulCommClass}\, M\, N\, \alpha$ holds.

Submonoid.sup_eq_range theorem

(s t : Submonoid N) : s ⊔ t = mrange (s.subtype.coprod t.subtype)

Full source

@[to_additive]
theorem sup_eq_range (s t : Submonoid N) : s ⊔ t = mrange (s.subtype.coprod t.subtype) := by
  rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]

Supremum of Submonoids as Range of Coproduct Homomorphism

Informal description

For any two submonoids $s$ and $t$ of a commutative monoid $N$, the supremum $s \sqcup t$ is equal to the range of the coproduct homomorphism formed by the inclusion homomorphisms of $s$ and $t$. That is, \[ s \sqcup t = \mathrm{range}(s.\mathrm{subtype} \cdot t.\mathrm{subtype}), \] where $s.\mathrm{subtype} \colon s \to N$ and $t.\mathrm{subtype} \colon t \to N$ are the inclusion homomorphisms, and $\cdot$ denotes the coproduct homomorphism.

Submonoid.mem_sup theorem

{s t : Submonoid N} {x : N} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Full source

@[to_additive]
theorem mem_sup {s t : Submonoid N} {x : N} : x ∈ s ⊔ tx ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x := by
  simp only [sup_eq_range, mem_mrange, coprod_apply, coe_subtype, Prod.exists,
    Subtype.exists, exists_prop]

Characterization of Membership in Supremum of Submonoids via Products

Informal description

For any two submonoids $s$ and $t$ of a commutative monoid $N$, an element $x \in N$ belongs to the supremum $s \sqcup t$ if and only if there exist elements $y \in s$ and $z \in t$ such that $y \cdot z = x$.

AddSubmonoid.closure_singleton_eq theorem

(x : A) : closure ({ x } : Set A) = AddMonoidHom.mrange (multiplesHom A x)

Full source

theorem closure_singleton_eq (x : A) :
    closure ({x} : Set A) = AddMonoidHom.mrange (multiplesHom A x) :=
  closure_eq_of_le (Set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) fun _ ⟨_n, hn⟩ =>
    hn ▸ nsmul_mem (subset_closure <| Set.mem_singleton _) _

Additive Closure of Singleton Equals Range of Multiples Homomorphism

Informal description

For any element $x$ in an additive monoid $A$, the additive closure of the singleton set $\{x\}$ is equal to the range of the additive monoid homomorphism $n \mapsto n \cdot x$ from $\mathbb{N}$ to $A$.

AddSubmonoid.mem_closure_singleton theorem

{x y : A} : y ∈ closure ({ x } : Set A) ↔ ∃ n : ℕ, n • x = y

Full source

/-- The `AddSubmonoid` generated by an element of an `AddMonoid` equals the set of
natural number multiples of the element. -/
theorem mem_closure_singleton {x y : A} : y ∈ closure ({x} : Set A)y ∈ closure ({x} : Set A) ↔ ∃ n : ℕ, n • x = y := by
  rw [closure_singleton_eq, AddMonoidHom.mem_mrange]; rfl

Characterization of Additive Closure of a Singleton via Natural Multiples

Informal description

For any elements $x$ and $y$ in an additive monoid $A$, the element $y$ belongs to the additive closure of the singleton set $\{x\}$ if and only if there exists a natural number $n$ such that $n \cdot x = y$.

AddSubmonoid.closure_singleton_zero theorem

: closure ({0} : Set A) = ⊥

Full source

theorem closure_singleton_zero : closure ({0} : Set A) = ⊥ := by
  simp [eq_bot_iff_forall, mem_closure_singleton, nsmul_zero]

Additive Closure of Zero is Trivial Submonoid

Informal description

The additive closure of the singleton set $\{0\}$ in an additive monoid $A$ is equal to the trivial additive submonoid $\bot$.

AddSubmonoid.multiples definition

(x : A) : AddSubmonoid A

Full source

/-- The additive submonoid generated by an element. -/
def multiples (x : A) : AddSubmonoid A :=
  AddSubmonoid.copy (AddMonoidHom.mrange (multiplesHom A x)) (Set.range (fun i => i • x : ℕ → A)) <|
    Set.ext fun n => exists_congr fun i => by simp

Additive submonoid of natural number multiples

Informal description

The additive submonoid generated by an element $x$ in an additive monoid $A$ is the set $\{n \cdot x \mid n \in \mathbb{N}\}$ of all natural number multiples of $x$.

Submonoid.mem_closure_pair theorem

 {A : Type*} [CommMonoid A] (a b c : A) : c ∈ Submonoid.closure ({ a, b } : Set A) ↔ ∃ m n : ℕ, a ^ m * b ^ n = c

Full source

/-- An element is in the closure of a two-element set if it is a linear combination of those two
elements. -/
@[to_additive
      "An element is in the closure of a two-element set if it is a linear combination of
      those two elements."]
theorem mem_closure_pair {A : Type*} [CommMonoid A] (a b c : A) :
    c ∈ Submonoid.closure ({a, b} : Set A)c ∈ Submonoid.closure ({a, b} : Set A) ↔ ∃ m n : ℕ, a ^ m * b ^ n = c := by
  rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]
  simp_rw [mem_closure_singleton, exists_exists_eq_and]

Characterization of Elements in Submonoid Generated by Two Elements via Exponents

Informal description

Let $A$ be a commutative monoid and $a, b, c \in A$. Then $c$ belongs to the submonoid generated by $\{a, b\}$ if and only if there exist natural numbers $m, n \in \mathbb{N}$ such that $c = a^m \cdot b^n$.

ofMul_image_powers_eq_multiples_ofMul theorem

[Monoid M] {x : M} : Additive.ofMul '' (Submonoid.powers x : Set M) = AddSubmonoid.multiples (Additive.ofMul x)

Full source

theorem ofMul_image_powers_eq_multiples_ofMul [Monoid M] {x : M} :
    Additive.ofMulAdditive.ofMul '' (Submonoid.powers x : Set M) = AddSubmonoid.multiples (Additive.ofMul x) := by
  ext
  constructor
  · rintro ⟨y, ⟨n, hy1⟩, hy2⟩
    use n
    simpa [← ofMul_pow, hy1]
  · rintro ⟨n, hn⟩
    refine ⟨x ^ n, ⟨n, rfl⟩, ?_⟩
    rwa [ofMul_pow]

Equality of Additive Image of Powers Submonoid and Multiples Submonoid: $\text{Additive.ofMul}(\{x^n \mid n \in \mathbb{N}\}) = \{n \cdot \text{Additive.ofMul}(x) \mid n \in \mathbb{N}\}$

Informal description

Let $M$ be a monoid and $x \in M$. The image of the submonoid generated by powers of $x$ under the additive map `Additive.ofMul` is equal to the additive submonoid generated by natural number multiples of `Additive.ofMul x`. In other words, the set $\{ \text{Additive.ofMul}(x^n) \mid n \in \mathbb{N} \}$ coincides with the set $\{ n \cdot \text{Additive.ofMul}(x) \mid n \in \mathbb{N} \}$.

ofAdd_image_multiples_eq_powers_ofAdd theorem

 [AddMonoid A] {x : A} :
  Multiplicative.ofAdd '' (AddSubmonoid.multiples x : Set A) = Submonoid.powers (Multiplicative.ofAdd x)

Full source

theorem ofAdd_image_multiples_eq_powers_ofAdd [AddMonoid A] {x : A} :
    Multiplicative.ofAddMultiplicative.ofAdd '' (AddSubmonoid.multiples x : Set A) =
      Submonoid.powers (Multiplicative.ofAdd x) := by
  symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_powers_eq_multiples_ofMul

Equality of Multiplicative Image of Multiples Submonoid and Powers Submonoid: $\text{Multiplicative.ofAdd}(\{n \cdot x \mid n \in \mathbb{N}\}) = \{(\text{Multiplicative.ofAdd}(x))^n \mid n \in \mathbb{N}\}$

Informal description

Let $A$ be an additive monoid and $x \in A$. The image of the additive submonoid generated by natural number multiples of $x$ under the multiplicative map `Multiplicative.ofAdd` is equal to the multiplicative submonoid generated by powers of `Multiplicative.ofAdd x$. In other words, the set $\{ \text{Multiplicative.ofAdd}(n \cdot x) \mid n \in \mathbb{N} \}$ coincides with the set $\{ (\text{Multiplicative.ofAdd}(x))^n \mid n \in \mathbb{N} \}$.

Tags