equiv_directSum_zmod_of_finite — Mathlib

English

Any finitely generated abelian group is isomorphic to a direct sum of ZMod(p^e) after choosing appropriate primes p_i and exponents e_i.

Русский

Любая конечная абелева группа изоморфна прямой сумме ZMod(p^e) после выбора подходящих p_i и e_i.

LaTeX

$$$\exists ι\; (Fintype\; ι)\; (p: ι\to\mathbb{N})\; (e: ι\to\mathbb{N})\; G \cong_+ \bigoplus_{i\in ι} \mathbb{Z}/p_i^{e_i}\mathbb{Z}$$$

Lean4

/-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`. -/
theorem equiv_directSum_zmod_of_finite [Finite G] :
    ∃ (ι : Type) (_ : Fintype ι) (p : ι → ℕ) (_ : ∀ i, Nat.Prime <| p i) (e : ι → ℕ),
      Nonempty <| G ≃+ ⨁ i : ι, ZMod (p i ^ e i) :=
  by
  cases nonempty_fintype G
  obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G
  rcases n with - | n
  · have : Unique (Fin Nat.zero →₀ ℤ) := { uniq := by subsingleton }
    exact ⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩
  · haveI := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _
    exact
      (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
          ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim

Похожие утверждения