The index of squares in the unit group of a number field

For a number field F, the subgroup of squares of the unit group has index at most 2^[F:ℚ]:

[O_F^× : (O_F^×)²] ≤ 2^[F:ℚ].

By Dirichlet's unit theorem O_F^× is generated by the fundamental system (of size rank) together with a generator of the finite cyclic torsion subgroup, so it is generated by rank + 1 ≤ [F:ℚ] elements; TauCeti.index_square_le_of_closure_eq_top then controls the index of the squares.

This is the cheap, self-contained upstream bound consumed by the effective class-number estimates. Its sharpening to the exact value [O_F^× : (O_F^×)²] = 2^(rank F + 1) (from Dirichlet's unit theorem) is TauCeti.NumberField.units_sq_index_eq, in the unit-square-class file TauCeti.NumberTheory.NumberField.Units.ElementaryTwoQuotient, kept separate so this bound does not depend on the structural-Dirichlet and elementary-2-quotient machinery the exact value needs.

Main results

• TauCeti.NumberField.units_sq_index_le: [O_F^× : (O_F^×)²] ≤ 2^[F:ℚ].

The remaining declarations are its degree-bounded consumer forms (units_sq_index_le_of_finrank_le, ..._of_finrank_eq, the quadratic ..._le_quadratic, and so on) together with the same estimates transported to the cardinality of the elementary-2 quotient O_F^×/(O_F^×)² via TauCeti.card_elementaryTwoQuotient_eq_index_square. They restate the exact bound above against an external degree bound and add no new content beyond units_sq_index_le.

Provenance

Migrated from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where this bound fed an explicit class-number estimate.

theorem TauCeti.NumberField.units_sq_index_le (F : Type u_1) [Field F] [NumberField F] : (Subgroup.square (NumberField.RingOfIntegers F)ˣ).index ≤ 2 ^ Module.finrank ℚ F

Squares have small index in the unit group. [O_F^× : (O_F^×)²] ≤ 2^[F:ℚ], stated using Mathlib's Subgroup.square for the subgroup of squares. By Dirichlet's unit theorem O_F^× is generated by the rank-element fundamental system together with a torsion generator, so TauCeti.index_square_le_of_closure_eq_top bounds the index by 2^(rank+1), and rank + 1 ≤ [F:ℚ].

theorem TauCeti.NumberField.units_sq_index_le_of_finrank_le (F : Type u_1) [Field F] [NumberField F] {n : ℕ} (hn : Module.finrank ℚ F ≤ n) : (Subgroup.square (NumberField.RingOfIntegers F)ˣ).index ≤ 2 ^ n

If a number field has degree at most n, then the square subgroup of its unit group has index at most 2^n. This is the monotone form of TauCeti.NumberField.units_sq_index_le, useful when the degree has been bounded separately.

theorem TauCeti.NumberField.units_sq_index_le_of_finrank_eq (F : Type u_1) [Field F] [NumberField F] {n : ℕ} (hn : Module.finrank ℚ F = n) : (Subgroup.square (NumberField.RingOfIntegers F)ˣ).index ≤ 2 ^ n

Exact-degree specialization of TauCeti.NumberField.units_sq_index_le: if [F : ℚ] = n, then [O_F^× : (O_F^×)^2] ≤ 2^n.

theorem TauCeti.NumberField.units_sq_index_le_of_finrank_eq_one (F : Type u_1) [Field F] [NumberField F] (hF : Module.finrank ℚ F = 1) : (Subgroup.square (NumberField.RingOfIntegers F)ˣ).index ≤ 2

In a degree-one number field, the square subgroup of the unit group has index at most 2.

theorem TauCeti.NumberField.units_sq_index_rat_le_two : (Subgroup.square (NumberField.RingOfIntegers ℚ)ˣ).index ≤ 2

The square subgroup of ℤˣ has index at most 2, viewed as the unit group of the ring of integers of ℚ.

theorem TauCeti.NumberField.units_sq_index_le_quadratic (F : Type u_1) [Field F] [NumberField F] (hF : Module.finrank ℚ F = 2) : (Subgroup.square (NumberField.RingOfIntegers F)ˣ).index ≤ 4

In a quadratic number field, the square subgroup of the unit group has index at most 4.

theorem TauCeti.NumberField.units_sq_index_le_of_finrank_le_two (F : Type u_1) [Field F] [NumberField F] (hF : Module.finrank ℚ F ≤ 2) : (Subgroup.square (NumberField.RingOfIntegers F)ˣ).index ≤ 4

If a number field has degree at most two, the square subgroup of the unit group has index at most 4. This is the form used when a quadratic-model argument supplies only [F : ℚ] ≤ 2.

theorem TauCeti.NumberField.card_units_elementaryTwoQuotient_le_of_finrank_le (F : Type u_1) [Field F] [NumberField F] {n : ℕ} (hn : Module.finrank ℚ F ≤ n) : Nat.card (ElementaryTwoQuotient (NumberField.RingOfIntegers F)ˣ) ≤ 2 ^ n

If [F : ℚ] ≤ n, then the elementary-2 quotient O_F^×/(O_F^×)^2 has at most 2^n elements. This is just the unit-square index bound translated through TauCeti.card_elementaryTwoQuotient_eq_index_square.

theorem TauCeti.NumberField.card_units_elementaryTwoQuotient_le_of_finrank_eq (F : Type u_1) [Field F] [NumberField F] {n : ℕ} (hn : Module.finrank ℚ F = n) : Nat.card (ElementaryTwoQuotient (NumberField.RingOfIntegers F)ˣ) ≤ 2 ^ n

Exact-degree version of TauCeti.NumberField.card_units_elementaryTwoQuotient_le_of_finrank_le.

theorem TauCeti.NumberField.card_units_elementaryTwoQuotient_le_of_finrank_eq_one (F : Type u_1) [Field F] [NumberField F] (hF : Module.finrank ℚ F = 1) : Nat.card (ElementaryTwoQuotient (NumberField.RingOfIntegers F)ˣ) ≤ 2

In a degree-one number field, the elementary-2 quotient O_F^×/(O_F^×)^2 has at most two elements.

theorem TauCeti.NumberField.card_units_elementaryTwoQuotient_rat_le_two : Nat.card (ElementaryTwoQuotient (NumberField.RingOfIntegers ℚ)ˣ) ≤ 2

The elementary-2 quotient of ℤˣ has at most two elements, viewed as the unit group of the ring of integers of ℚ.

theorem TauCeti.NumberField.card_units_elementaryTwoQuotient_le_of_finrank_le_two (F : Type u_1) [Field F] [NumberField F] (hF : Module.finrank ℚ F ≤ 2) : Nat.card (ElementaryTwoQuotient (NumberField.RingOfIntegers F)ˣ) ≤ 4

If [F : ℚ] ≤ 2, then the elementary-2 quotient O_F^×/(O_F^×)^2 has at most four elements.

theorem TauCeti.NumberField.card_units_elementaryTwoQuotient_le_quadratic (F : Type u_1) [Field F] [NumberField F] (hF : Module.finrank ℚ F = 2) : Nat.card (ElementaryTwoQuotient (NumberField.RingOfIntegers F)ˣ) ≤ 4

For a quadratic number field, the elementary-2 quotient O_F^×/(O_F^×)^2 has at most four elements.