The maximal elementary-2 quotient of a free abelian group

For a finite-rank free ℤ-module A, the multiplicative group Multiplicative A has maximal elementary-2 quotient of cardinality 2 ^ rank: squaring is doubling, and A / 2A is an 𝔽₂-vector space with basis the reduction of any ℤ-basis. Correspondingly the 2-rank of Multiplicative A is exactly the ℤ-rank of A.

This is the free building block complementing the finite cyclic one of TauCeti.Algebra.Group.ElementaryTwoQuotient.Cyclic: through a product decomposition of a finitely generated abelian group, the two together compute its number of square classes. The multiquadratic roadmap consumes this file through Dirichlet's unit theorem, whose free part Fin (rank) → ℤ contributes 2 ^ rank square classes of units.

The counting itself is Mathlib's ModN.natCard_eq (|A/nA| = n ^ rank for a free finite-rank ℤ-module); this file transports it along the identification of Additive (Multiplicative A) with A.

Main results

• TauCeti.card_elementaryTwoQuotient_multiplicative: |Multiplicative A / (Multiplicative A)²| = 2 ^ finrank ℤ A, with the corresponding Finite instance (the group is infinite for positive rank, so the generic instance does not apply in general).
• TauCeti.twoRank_multiplicative: the 2-rank of Multiplicative A is finrank ℤ A.

theorem TauCeti.card_elementaryTwoQuotient_multiplicative (A : Type u_1) [AddCommGroup A] [Module.Free ℤ A] [Module.Finite ℤ A] : Nat.card (ElementaryTwoQuotient (Multiplicative A)) = 2 ^ Module.finrank ℤ A

A finite-rank free abelian group has 2 ^ rank square classes. For a free ℤ-module A of finite rank, the maximal elementary-2 quotient of Multiplicative A has cardinality 2 ^ finrank ℤ A. This is Mathlib's ModN.natCard_eq transported along the identification of Additive (Multiplicative A) with A.

instance TauCeti.instFiniteElementaryTwoQuotientMultiplicative (A : Type u_1) [AddCommGroup A] [Module.Free ℤ A] [Module.Finite ℤ A] : Finite (ElementaryTwoQuotient (Multiplicative A))

The elementary-2 quotient of a finite-rank free abelian group is finite. The group is infinite for positive rank, so the generic Finite G → Finite (G/G²) instance does not apply in general; this instance lets consumers combine the free factor with the twoRank-level product and divisibility lemmas.

theorem TauCeti.twoRank_multiplicative (A : Type u_1) [AddCommGroup A] [Module.Free ℤ A] [Module.Finite ℤ A] : twoRank (Multiplicative A) = Module.finrank ℤ A

The 2-rank of a finite-rank free abelian group is its rank: twoRank (Multiplicative A) = finrank ℤ A.