Abelian groups

Structure of abelian groups: finite and finitely generated abelian groups (invariant factors, elementary divisors, torsion, ranks, dual groups), torsion-free and infinite abelian groups (Baer–Specker group, pure subgroups, direct-sum cancellation, ultraproducts of abelian groups); colourings and partitions of abelian groups go to Combinatorics in groups.

• Baer–Specker group
• Cyclic sublattices of abelian groups
• Direct-sum cancellation for torsion-free abelian groups
• Dual groups of finite abelian groups
• Homomorphic images of ultraproducts of groups
• Increasing unions of isomorphic subgroups
• Structure of finitely generated abelian groups
• Two-power ranks of finite abelian groups

TheoremCardinality of the \(n\)-torsion of a vector space modulo a lattice#✓fully proved

The n-torsion of the quotient of a vector space by a free finite lattice has cardinality n ^ finrank L.

This counts torsion points: for a lattice L of rank r in a vector space, the n-torsion subgroup of V ⧸ L has n ^ r elements. It is used for torsion in abelian varieties and elliptic curves, for class group computations, and for lattice index arguments.

theorem natCard_torsionBy_quotient_eq_pow_finrank {K : Type*} [DivisionRing K]
    [CharZero K] {V : Type*} [AddCommGroup V] [Module K V] (L : Submodule ℤ V)
    [Module.Free ℤ L] [Module.Finite ℤ L] (n : ℕ) (hn : n ≠ 0) :
    Nat.card (Submodule.torsionBy ℤ (V ⧸ L) (n : ℤ)) = n ^ Module.finrank ℤ L

DefinitionPure subgroups of abelian groups#✓fully proved

A subgroup \(B\) of an abelian group \(A\) is pure when \(nA \cap B = nB\) for every integer \(n\): for every integer \(n\) and every \(a \in A\) with \(na \in B\) there is some \(b \in B\) with \(nb = na\).

def IsPureSubgroup {A : Type} [AddCommGroup A] (B : AddSubgroup A) : Prop :=
  ∀ (n : ℤ) (a : A), n • a ∈ B → ∃ b ∈ B, n • b = n • a

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.