Structure of finitely generated abelian groups

TheoremUniqueness of elementary divisors#✓fully proved

Let \(p\) be a prime and let \(A\) be an abelian group. If \(A \cong \bigoplus_{i=1}^{n} \mathbb{Z}/p^{e_i}\mathbb{Z}\) and \(A \cong \bigoplus_{j=1}^{m} \mathbb{Z}/p^{f_j}\mathbb{Z}\) for positive integers \(e_1, \dots, e_n\) and \(f_1, \dots, f_m\), then \(n = m\) and the multisets \(\{e_1, \dots, e_n\}\) and \(\{f_1, \dots, f_m\}\) are equal.

theorem elementary_divisors_unique {p : ℕ} (hp : p.Prime) {n m : ℕ}
    {e : Fin n → ℕ} {f : Fin m → ℕ} (he : ∀ i, 0 < e i) (hf : ∀ i, 0 < f i)
    {A : Type*} [AddCommGroup A]
    (hA : Nonempty (A ≃+ ⨁ i, ZMod (p ^ e i)))
    (hB : Nonempty (A ≃+ ⨁ i, ZMod (p ^ f i))) :
    n = m ∧ Multiset.map e Finset.univ.val = Multiset.map f Finset.univ.val

TheoremTorsion subgroup of a finitely generated abelian group is finitely generated#✓fully proved

If \(A\) is a finitely generated abelian group, then its torsion subgroup is finitely generated.

public theorem fg_torsion (A : Type*) [AddCommGroup A] [AddGroup.FG A] :
    AddGroup.FG (torsion A)

Used by 1

Used byTorsion subgroup of a finitely generated abelian group is finite

TheoremTorsion subgroup of a finitely generated abelian group is finite#✓fully proved

If \(A\) is a finitely generated abelian group, then its torsion subgroup is finite.

public theorem finite_torsion_of_fg (A : Type*) [AddCommGroup A] [AddGroup.FG A] :
    Finite (torsion A)

Uses 1 · Used by 1

Proof usesTorsion subgroup of a finitely generated abelian group is finitely generated

Used byTorsion subgroup of a finitely generated abelian group as a sum of cyclic groups

TheoremTorsion subgroup of a finitely generated abelian group as a sum of cyclic groups#✓fully proved

If \(A\) is a finitely generated abelian group, then there exist a natural number \(n\) and positive integers \(d_1, \dots, d_n\) such that the torsion subgroup of \(A\) is isomorphic to the direct sum \(\mathbb{Z}/d_1\mathbb{Z} \oplus \cdots \oplus \mathbb{Z}/d_n\mathbb{Z}\) of finite cyclic groups.

public theorem torsion_equiv_directSum_zmod_of_fg (A : Type*) [AddCommGroup A]
    [AddGroup.FG A] :
    ∃ (n : ℕ) (d : Fin n → ℕ) (_ : ∀ i, 0 < d i),
      Nonempty (torsion A ≃+ (⨁ i : Fin n, ZMod (d i)))

Uses 1

Proof usesTorsion subgroup of a finitely generated abelian group is finite

TheoremFundamental theorem of finitely generated abelian groups, invariant factor form#✓fully proved

Every finitely generated abelian group \(A\) is isomorphic to \(\mathbb{Z}^a \times \bigoplus_{i < k} \mathbb{Z}/d_i\mathbb{Z}\) for some \(a, k \in \mathbb{N}\) and natural numbers \(d_0, \dots, d_{k-1}\) with \(d_i > 1\) for every \(i\) and \(d_i \mid d_j\) whenever \(i \le j\).

theorem equiv_free_prod_directSum_invariant_factors (A : Type*) [AddCommGroup A]
    [AddGroup.FG A] :
    ∃ (a : ℕ) (k : ℕ) (d : Fin k → ℕ),
      (∀ i, 1 < d i) ∧
      (∀ i j : Fin k, i ≤ j → d i ∣ d j) ∧
      Nonempty (A ≃+ (Fin a →₀ ℤ) × ⨁ i : Fin k, ZMod (d i))

Uses 1 · Used by 1

Proof usesSmith normal form with a divisibility chain

Used byInvariant factor decomposition of finite abelian groups

TheoremInvariant factor decomposition of finite abelian groups#✓fully proved

Every finite abelian group \(A\) is isomorphic to \(\bigoplus_{i < k} \mathbb{Z}/d_i\mathbb{Z}\) for some \(k \in \mathbb{N}\) and natural numbers \(d_0, \dots, d_{k-1}\) with \(d_i > 1\) for every \(i\) and \(d_i \mid d_j\) whenever \(i \le j\).

theorem equiv_directSum_invariant_factors_of_finite (A : Type*) [AddCommGroup A]
    [Finite A] :
    ∃ (k : ℕ) (d : Fin k → ℕ),
      (∀ i, 1 < d i) ∧ (∀ i j : Fin k, i ≤ j → d i ∣ d j) ∧
      Nonempty (A ≃+ ⨁ i : Fin k, ZMod (d i))

Uses 1 · Used by 1

Proof usesFundamental theorem of finitely generated abelian groups, invariant factor form

Used byFrom elementary divisors to invariant factors

TheoremFrom elementary divisors to invariant factors#✓fully proved

Let \(I\) be a finite set, and for each \(i \in I\) let \(p_i\) be a prime and \(e_i\) a natural number. Then there are \(k \in \mathbb{N}\) and natural numbers \(d_0, \dots, d_{k-1}\) with \(d_j > 1\) for every \(j\) and \(d_j \mid d_l\) whenever \(j \le l\), such that \(\bigoplus_{i \in I} \mathbb{Z}/p_i^{e_i}\mathbb{Z}\) is isomorphic to \(\bigoplus_{j < k} \mathbb{Z}/d_j\mathbb{Z}\).

Exponent zero is allowed, giving a trivial summand.

theorem elementary_divisors_equiv_invariant_factors
    (ι : Type*) [Fintype ι] (p : ι → ℕ) (hp : ∀ i, Nat.Prime (p i)) (e : ι → ℕ) :
    ∃ (k : ℕ) (d : Fin k → ℕ),
      (∀ i, 1 < d i) ∧
      (∀ i j : Fin k, i ≤ j → d i ∣ d j) ∧
      Nonempty ((⨁ i : ι, ZMod (p i ^ e i)) ≃+ (⨁ i : Fin k, ZMod (d i)))

Uses 1

Proof usesInvariant factor decomposition of finite abelian groups

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.