Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Subgroup.zpowers definition

(g : G) : Subgroup G

Full source

/-- The subgroup generated by an element. -/
@[to_additive "The additive subgroup generated by an element."]
def zpowers (g : G) : Subgroup G where
  carrier := Set.range (g ^ · : ℤ → G)
  one_mem' := ⟨0, zpow_zero g⟩
  mul_mem' := by rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, zpow_add ..⟩
  inv_mem' := by rintro _ ⟨a, rfl⟩; exact ⟨-a, zpow_neg ..⟩

Cyclic subgroup generated by an element

Informal description

For an element $g$ in a group $G$, the subgroup $\langle g \rangle$ generated by $g$ is the set $\{g^n \mid n \in \mathbb{Z}\}$ of all integer powers of $g$. This set forms a subgroup of $G$ containing the identity element (when $n=0$), closed under multiplication (since $g^a \cdot g^b = g^{a+b}$), and closed under inverses (since $(g^a)^{-1} = g^{-a}$).

Subgroup.mem_zpowers theorem

(g : G) : g ∈ zpowers g

Full source

@[to_additive (attr := simp)]
theorem mem_zpowers (g : G) : g ∈ zpowers g :=
  ⟨1, zpow_one _⟩

Element Belongs to Its Own Cyclic Subgroup: $g \in \langle g \rangle$

Informal description

For any element $g$ in a group $G$, the element $g$ belongs to the cyclic subgroup $\langle g \rangle$ generated by itself, i.e., $g \in \langle g \rangle$.

Subgroup.coe_zpowers theorem

(g : G) : ↑(zpowers g) = Set.range (g ^ · : ℤ → G)

Full source

@[to_additive (attr := norm_cast)] -- TODO: simp?
theorem coe_zpowers (g : G) : ↑(zpowers g) = Set.range (g ^ · : ℤ → G) :=
  rfl

Cyclic Subgroup as Range of Powers: $\langle g \rangle = \{g^n \mid n \in \mathbb{Z}\}$

Informal description

For any element $g$ in a group $G$, the underlying set of the cyclic subgroup $\langle g \rangle$ generated by $g$ is equal to the range of the function $n \mapsto g^n$ from the integers $\mathbb{Z}$ to $G$. In other words, $\langle g \rangle = \{g^n \mid n \in \mathbb{Z}\}$.

Subgroup.decidableMemZPowers instance

{a : G} : DecidablePred (· ∈ Subgroup.zpowers a)

Full source

@[to_additive] -- TODO: delete?
noncomputable instance decidableMemZPowers {a : G} : DecidablePred (· ∈ Subgroup.zpowers a) :=
  Classical.decPred _

Decidability of Membership in Cyclic Subgroups

Informal description

For any element $a$ in a group $G$, the predicate determining membership in the cyclic subgroup generated by $a$ is decidable. That is, for any $h \in G$, it is decidable whether there exists an integer $k$ such that $h = a^k$.

Subgroup.zpowers_eq_closure theorem

(g : G) : zpowers g = closure { g }

Full source

@[to_additive]
theorem zpowers_eq_closure (g : G) : zpowers g = closure {g} := by
  ext
  exact mem_closure_singleton.symm

Cyclic Subgroup as Closure of Singleton: $\langle g \rangle = \text{closure}\{g\}$

Informal description

For any element $g$ in a group $G$, the cyclic subgroup generated by $g$ (denoted $\langle g \rangle$) is equal to the subgroup generated by the singleton set $\{g\}$.

Subgroup.mem_zpowers_iff theorem

{g h : G} : h ∈ zpowers g ↔ ∃ k : ℤ, g ^ k = h

Full source

@[to_additive]
theorem mem_zpowers_iff {g h : G} : h ∈ zpowers gh ∈ zpowers g ↔ ∃ k : ℤ, g ^ k = h :=
  Iff.rfl

Membership Criterion for Cyclic Subgroups: $h \in \langle g \rangle \leftrightarrow \exists k \in \mathbb{Z}, g^k = h$

Informal description

For any elements $g$ and $h$ in a group $G$, the element $h$ belongs to the cyclic subgroup generated by $g$ if and only if there exists an integer $k$ such that $g^k = h$.

Subgroup.zpow_mem_zpowers theorem

(g : G) (k : ℤ) : g ^ k ∈ zpowers g

Full source

@[to_additive (attr := simp)]
theorem zpow_mem_zpowers (g : G) (k : ℤ) : g ^ k ∈ zpowers g :=
  mem_zpowers_iff.mpr ⟨k, rfl⟩

Integer Powers Belong to Generated Cyclic Subgroup

Informal description

For any element $g$ in a group $G$ and any integer $k$, the element $g^k$ belongs to the cyclic subgroup generated by $g$, i.e., $g^k \in \langle g \rangle$.

Subgroup.npow_mem_zpowers theorem

(g : G) (k : ℕ) : g ^ k ∈ zpowers g

Full source

@[to_additive (attr := simp)]
theorem npow_mem_zpowers (g : G) (k : ℕ) : g ^ k ∈ zpowers g :=
  zpow_natCast g k ▸ zpow_mem_zpowers g k

Natural Powers Belong to Generated Cyclic Subgroup

Informal description

For any element $g$ in a group $G$ and any natural number $k$, the element $g^k$ belongs to the cyclic subgroup generated by $g$, i.e., $g^k \in \langle g \rangle$.

Subgroup.forall_zpowers theorem

{x : G} {p : zpowers x → Prop} : (∀ g, p g) ↔ ∀ m : ℤ, p ⟨x ^ m, m, rfl⟩

Full source

@[to_additive (attr := simp 1100)]
theorem forall_zpowers {x : G} {p : zpowers x → Prop} : (∀ g, p g) ↔ ∀ m : ℤ, p ⟨x ^ m, m, rfl⟩ :=
  Set.forall_subtype_range_iff

Universal Quantification over Cyclic Subgroup via Integer Exponents

Informal description

For any element $x$ in a group $G$ and any predicate $p$ defined on the cyclic subgroup $\langle x \rangle$, the statement that $p(g)$ holds for all $g \in \langle x \rangle$ is equivalent to the statement that $p(x^m)$ holds for all integers $m \in \mathbb{Z}$.

Subgroup.exists_zpowers theorem

{x : G} {p : zpowers x → Prop} : (∃ g, p g) ↔ ∃ m : ℤ, p ⟨x ^ m, m, rfl⟩

Full source

@[to_additive (attr := simp 1100)]
theorem exists_zpowers {x : G} {p : zpowers x → Prop} : (∃ g, p g) ↔ ∃ m : ℤ, p ⟨x ^ m, m, rfl⟩ :=
  Set.exists_subtype_range_iff

Existence in Cyclic Subgroup via Integer Powers

Informal description

For any element $x$ in a group $G$ and any predicate $p$ defined on the cyclic subgroup $\langle x \rangle$, there exists an element $g \in \langle x \rangle$ satisfying $p(g)$ if and only if there exists an integer $m \in \mathbb{Z}$ such that $p(x^m)$ holds.

Subgroup.forall_mem_zpowers theorem

{x : G} {p : G → Prop} : (∀ g ∈ zpowers x, p g) ↔ ∀ m : ℤ, p (x ^ m)

Full source

@[to_additive]
theorem forall_mem_zpowers {x : G} {p : G → Prop} : (∀ g ∈ zpowers x, p g) ↔ ∀ m : ℤ, p (x ^ m) :=
  Set.forall_mem_range

Universal Quantification over Cyclic Subgroup via Integer Powers

Informal description

For any element $x$ in a group $G$ and any predicate $p$ on $G$, the statement that $p(g)$ holds for all $g$ in the cyclic subgroup generated by $x$ is equivalent to the statement that $p(x^m)$ holds for all integers $m \in \mathbb{Z}$.

Subgroup.exists_mem_zpowers theorem

{x : G} {p : G → Prop} : (∃ g ∈ zpowers x, p g) ↔ ∃ m : ℤ, p (x ^ m)

Full source

@[to_additive]
theorem exists_mem_zpowers {x : G} {p : G → Prop} : (∃ g ∈ zpowers x, p g) ↔ ∃ m : ℤ, p (x ^ m) :=
  Set.exists_range_iff

Existence in Cyclic Subgroup via Integer Powers

Informal description

For any element $x$ in a group $G$ and any predicate $p$ on $G$, there exists an element $g$ in the cyclic subgroup generated by $x$ such that $p(g)$ holds if and only if there exists an integer $m$ such that $p(x^m)$ holds.

MonoidHom.map_zpowers theorem

(f : G →* N) (x : G) : (Subgroup.zpowers x).map f = Subgroup.zpowers (f x)

Full source

@[to_additive (attr := simp)]
theorem MonoidHom.map_zpowers (f : G →* N) (x : G) :
    (Subgroup.zpowers x).map f = Subgroup.zpowers (f x) := by
  rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]

Image of Cyclic Subgroup under Homomorphism Equals Cyclic Subgroup of Image

Informal description

Let $G$ and $N$ be groups and $f \colon G \to N$ a group homomorphism. For any element $x \in G$, the image under $f$ of the cyclic subgroup generated by $x$ equals the cyclic subgroup generated by $f(x)$. In other words: \[ f(\langle x \rangle) = \langle f(x) \rangle \]

Int.mem_zmultiples_iff theorem

{a b : ℤ} : b ∈ AddSubgroup.zmultiples a ↔ a ∣ b

Full source

theorem Int.mem_zmultiples_iff {a b : ℤ} : b ∈ AddSubgroup.zmultiples ab ∈ AddSubgroup.zmultiples a ↔ a ∣ b :=
  exists_congr fun k => by rw [mul_comm, eq_comm, ← smul_eq_mul]

Characterization of Membership in Integer Multiples Subgroup: $b \in \langle a \rangle \leftrightarrow a \mid b$

Informal description

For any integers $a$ and $b$, the element $b$ belongs to the additive subgroup generated by $a$ (i.e., $b \in \text{AddSubgroup.zmultiples}\, a$) if and only if $a$ divides $b$ (i.e., $a \mid b$).

Int.zmultiples_one theorem

: AddSubgroup.zmultiples (1 : ℤ) = ⊤

Full source

@[simp]
lemma Int.zmultiples_one : AddSubgroup.zmultiples (1 : ℤ) = ⊤ := by
  ext z
  simpa only [AddSubgroup.mem_top, iff_true] using ⟨z, zsmul_int_one z⟩

Integer Additive Subgroup Generated by 1 is the Whole Group

Informal description

The additive subgroup generated by the integer $1$ is equal to the entire additive group of integers $\mathbb{Z}$ (denoted by $\top$ in this context), i.e., $\langle 1 \rangle = \mathbb{Z}$.

ofMul_image_zpowers_eq_zmultiples_ofMul theorem

{x : G} : Additive.ofMul '' (Subgroup.zpowers x : Set G) = AddSubgroup.zmultiples (Additive.ofMul x)

Full source

theorem ofMul_image_zpowers_eq_zmultiples_ofMul {x : G} :
    Additive.ofMulAdditive.ofMul '' (Subgroup.zpowers x : Set G) = AddSubgroup.zmultiples (Additive.ofMul x) := by
  ext y
  constructor
  · rintro ⟨z, ⟨m, hm⟩, hz2⟩
    use m
    simp only at *
    rwa [← ofMul_zpow, hm]
  · rintro ⟨n, hn⟩
    refine ⟨x ^ n, ⟨n, rfl⟩, ?_⟩
    rwa [ofMul_zpow]

Equivalence between multiplicative cyclic subgroup and additive multiples via `Additive.ofMul`

Informal description

For any element $x$ in a group $G$, the image of the cyclic subgroup $\langle x \rangle$ under the additive equivalence `Additive.ofMul` is equal to the additive subgroup generated by `Additive.ofMul x`, i.e., the set of all integer multiples of `Additive.ofMul x$.

ofAdd_image_zmultiples_eq_zpowers_ofAdd theorem

{x : A} : Multiplicative.ofAdd '' (AddSubgroup.zmultiples x : Set A) = Subgroup.zpowers (Multiplicative.ofAdd x)

Full source

theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {x : A} :
    Multiplicative.ofAddMultiplicative.ofAdd '' (AddSubgroup.zmultiples x : Set A) =
      Subgroup.zpowers (Multiplicative.ofAdd x) := by
  symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_zpowers_eq_zmultiples_ofMul

Equivalence between additive multiples and multiplicative cyclic subgroup via `Multiplicative.ofAdd`

Informal description

For any element $x$ in an additive group $A$, the image of the additive subgroup $\mathbb{Z} \cdot x$ (the set of all integer multiples of $x$) under the multiplicative equivalence `Multiplicative.ofAdd` is equal to the multiplicative subgroup generated by `Multiplicative.ofAdd x$, i.e., $\{\text{Multiplicative.ofAdd}(x)^n \mid n \in \mathbb{Z}\}$.

Subgroup.zpowers_isMulCommutative instance

(g : G) : IsMulCommutative (zpowers g)

Full source

@[to_additive]
instance zpowers_isMulCommutative (g : G) : IsMulCommutative (zpowers g) :=
  ⟨⟨fun ⟨_, _, h₁⟩ ⟨_, _, h₂⟩ => by
      rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← h₁, ← h₂,
        zpow_mul_comm]⟩⟩

Commutativity of Multiplication in Cyclic Subgroups

Informal description

For any element $g$ in a group $G$, the cyclic subgroup $\langle g \rangle$ generated by $g$ has commutative multiplication. That is, for any two elements $g^m, g^n \in \langle g \rangle$, we have $g^m \cdot g^n = g^n \cdot g^m$.

Subgroup.zpowers_le theorem

{g : G} {H : Subgroup G} : zpowers g ≤ H ↔ g ∈ H

Full source

@[to_additive (attr := simp)]
theorem zpowers_le {g : G} {H : Subgroup G} : zpowerszpowers g ≤ H ↔ g ∈ H := by
  rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]

Cyclic Subgroup Containment Criterion: $\langle g \rangle \leq H \leftrightarrow g \in H$

Informal description

For any element $g$ in a group $G$ and any subgroup $H$ of $G$, the cyclic subgroup generated by $g$ is contained in $H$ if and only if $g$ is an element of $H$. In other words, $\langle g \rangle \leq H \leftrightarrow g \in H$.

Subgroup.zpowers_eq_bot theorem

{g : G} : zpowers g = ⊥ ↔ g = 1

Full source

@[to_additive (attr := simp)]
theorem zpowers_eq_bot {g : G} : zpowerszpowers g = ⊥ ↔ g = 1 := by rw [eq_bot_iff, zpowers_le, mem_bot]

Triviality Criterion for Cyclic Subgroups: $\langle g \rangle = \{1\} \leftrightarrow g = 1$

Informal description

For any element $g$ in a group $G$, the cyclic subgroup $\langle g \rangle$ generated by $g$ is equal to the trivial subgroup $\{1\}$ if and only if $g$ is the identity element of $G$, i.e., $\langle g \rangle = \{1\} \leftrightarrow g = 1$.

Subgroup.zpowers_ne_bot theorem

: zpowers g ≠ ⊥ ↔ g ≠ 1

Full source

@[to_additive]
theorem zpowers_ne_bot : zpowerszpowers g ≠ ⊥zpowers g ≠ ⊥ ↔ g ≠ 1 :=
  zpowers_eq_bot.not

Nontriviality Criterion for Cyclic Subgroups: $\langle g \rangle \neq \{1\} \leftrightarrow g \neq 1$

Informal description

For any element $g$ in a group $G$, the cyclic subgroup $\langle g \rangle$ generated by $g$ is nontrivial if and only if $g$ is not the identity element, i.e., $\langle g \rangle \neq \{1\} \leftrightarrow g \neq 1$.

Subgroup.zpowers_one_eq_bot theorem

: Subgroup.zpowers (1 : G) = ⊥

Full source

@[to_additive (attr := simp)]
theorem zpowers_one_eq_bot : Subgroup.zpowers (1 : G) = ⊥ :=
  Subgroup.zpowers_eq_bot.mpr rfl

Cyclic Subgroup of Identity is Trivial: $\langle 1 \rangle = \{1\}$

Informal description

The cyclic subgroup generated by the identity element $1$ of a group $G$ is equal to the trivial subgroup $\{1\}$, i.e., $\langle 1 \rangle = \{1\}$.

Subgroup.zpowers_inv theorem

: zpowers g⁻¹ = zpowers g

Full source

@[to_additive (attr := simp)]
theorem zpowers_inv : zpowers g⁻¹ = zpowers g :=
  eq_of_forall_ge_iff fun _ ↦ by simp only [zpowers_le, inv_mem_iff]

Inverse Generates Same Cyclic Subgroup: $\langle g^{-1} \rangle = \langle g \rangle$

Informal description

For any element $g$ in a group $G$, the cyclic subgroup generated by the inverse $g^{-1}$ is equal to the cyclic subgroup generated by $g$, i.e., $\langle g^{-1} \rangle = \langle g \rangle$.

Int.zmultiples_natAbs theorem

(a : ℤ) : AddSubgroup.zmultiples (a.natAbs : ℤ) = AddSubgroup.zmultiples a

Full source

theorem Int.zmultiples_natAbs (a : ℤ) :
    AddSubgroup.zmultiples (a.natAbs : ℤ) = AddSubgroup.zmultiples a := by
  simp [le_antisymm_iff, Int.mem_zmultiples_iff, Int.dvd_natAbs, Int.natAbs_dvd]

Subgroup Generated by Absolute Value Equals Subgroup Generated by Element in Integers

Informal description

For any integer $a$, the additive subgroup generated by the natural absolute value of $a$ (as an integer) is equal to the additive subgroup generated by $a$ itself, i.e., $\langle |a| \rangle = \langle a \rangle$.

AddSubgroup.closure_singleton_int_one_eq_top theorem

: closure ({ 1 } : Set ℤ) = ⊤

Full source

lemma AddSubgroup.closure_singleton_int_one_eq_top : closure ({1} : Set ℤ) = ⊤ := by
  ext
  simp [mem_closure_singleton]

The Additive Subgroup Generated by 1 in $\mathbb{Z}$ is the Whole Group

Informal description

The additive subgroup generated by the singleton set $\{1\}$ in the integers $\mathbb{Z}$ is equal to the entire group $\mathbb{Z}$, i.e., $\text{closure}(\{1\}) = \mathbb{Z}$.

AddSubgroup.zmultiples_one_eq_top theorem

: zmultiples (1 : ℤ) = ⊤

Full source

lemma AddSubgroup.zmultiples_one_eq_top : zmultiples (1 : ℤ) = ⊤ := by
  rw [zmultiples_eq_closure, closure_singleton_int_one_eq_top]

Subgroup Generated by 1 in Integers is the Whole Group

Informal description

The additive subgroup of $\mathbb{Z}$ generated by the integer $1$ is equal to the entire group $\mathbb{Z}$, i.e., $\langle 1 \rangle = \mathbb{Z}$.

Tags