The square classes of the unit group of a number field

For a number field F, Dirichlet's unit theorem decomposes the unit group of its ring of integers as the product of its torsion subgroup (finite cyclic of even order, as it contains -1) and a free abelian group of rank NumberField.Units.rank F — the structural equivalence TauCeti.NumberField.unitsMulEquivTorsionProdMultiplicative of TauCeti.NumberTheory.NumberField.Units.Dirichlet. Counting square classes in each factor gives the exact number of unit square classes of genus theory:

|𝓞 F^× / (𝓞 F^×)²| = 2 ^ (rank F + 1),

equivalently the exact subgroup index [𝓞 F^× : (𝓞 F^×)²] = 2 ^ (rank F + 1), which sharpens the degree bound TauCeti.NumberField.units_sq_index_le of TauCeti.NumberTheory.EffectiveBounds.UnitSquares.Basic. This is the unit-square-class input of Layer 2 of the multiquadratic roadmap, feeding the ambiguous-class-number formula and the genus-field 2-rank computation.

The counting combines the cyclic and free square-class computations of TauCeti.Algebra.Group.ElementaryTwoQuotient.Cyclic and TauCeti.Algebra.Group.ElementaryTwoQuotient.FreeModule through the product decomposition of TauCeti.Algebra.Group.ElementaryTwoQuotient.Prod.

Main results

• TauCeti.NumberField.card_elementaryTwoQuotient_units: |𝓞 F^× / (𝓞 F^×)²| = 2 ^ (rank F + 1).
• TauCeti.NumberField.twoRank_units: the 2-rank of the unit group is rank F + 1.
• TauCeti.NumberField.units_sq_index_eq: [𝓞 F^× : (𝓞 F^×)²] = 2 ^ (rank F + 1).

theorem TauCeti.NumberField.card_elementaryTwoQuotient_units (F : Type u_1) [Field F] [NumberField F] : Nat.card (ElementaryTwoQuotient (NumberField.RingOfIntegers F)ˣ) = 2 ^ (NumberField.Units.rank F + 1)

The unit group of a number field has 2 ^ (rank + 1) square classes. The torsion subgroup is cyclic of even order (it contains -1), contributing one factor of 2, and the free part of Dirichlet rank contributes 2 ^ rank.

instance TauCeti.NumberField.instFiniteElementaryTwoQuotientUnitsRingOfIntegers (F : Type u_1) [Field F] [NumberField F] : Finite (ElementaryTwoQuotient (NumberField.RingOfIntegers F)ˣ)

The elementary-2 quotient of the unit group of a number field is finite.

theorem TauCeti.NumberField.twoRank_units (F : Type u_1) [Field F] [NumberField F] : twoRank (NumberField.RingOfIntegers F)ˣ = NumberField.Units.rank F + 1

The 2-rank of the unit group of a number field is rank F + 1.

theorem TauCeti.NumberField.units_sq_index_eq (F : Type u_1) [Field F] [NumberField F] : (Subgroup.square (NumberField.RingOfIntegers F)ˣ).index = 2 ^ (NumberField.Units.rank F + 1)

The exact unit-square index of genus theory. For a number field F, [𝓞 F^× : (𝓞 F^×)²] = 2 ^ (rank F + 1). This is the subgroup-index reading of TauCeti.NumberField.card_elementaryTwoQuotient_units; it sharpens the degree bound TauCeti.NumberField.units_sq_index_le to an equality.