The square-class group Kˣ ⧸ (Kˣ)²

For a field K, the square-class group is the quotient of Kˣ by its squares. Every element has order dividing 2, so the quotient is an 𝔽₂ = ZMod 2-vector space (Mathlib's QuotientAddGroup.zmodModule, written additively on Additive Kˣ).

A ZMod 2-linear combination of the classes of a finite family of units is, up to the {0, 1} coefficients, exactly a subset product, and it vanishes precisely when that subset product is a square. So linear independence of the classes is the Finset form of square-class independence (no nonempty subset product is a square), one subset at a time.

Main definitions and results

• TauCeti.SquareClassGroup: the square-class group Kˣ ⧸ (Kˣ)², an 𝔽₂-vector space.
• TauCeti.squareClass: the class of a unit, with squareClass_eq_zero_iff characterising the trivial class as the squares.
• TauCeti.linearIndependent_squareClass_iff: the classes of d : ι → Kˣ are ZMod 2-linearly independent iff no nonempty subset product is a square.

@[reducible, inline]

abbrev TauCeti.SquareClassGroup (K : Type u_2) [Field K] : Type u_2

The square-class group Kˣ ⧸ (Kˣ)², written additively on Additive Kˣ.

Equations

• TauCeti.SquareClassGroup K = (Additive Kˣ ⧸ Subgroup.toAddSubgroup (Subgroup.square Kˣ))

@[implicit_reducible]

instance TauCeti.instModuleZModOfNatNatSquareClassGroup {K : Type u_1} [Field K] : Module (ZMod 2) (SquareClassGroup K)

The square-class group is a ZMod 2-module: every element has order dividing two, since the double of any unit class is the class of a square.

Equations

• TauCeti.instModuleZModOfNatNatSquareClassGroup = QuotientAddGroup.zmodModule ⋯

def TauCeti.squareClass {K : Type u_1} [Field K] (u : Kˣ) : SquareClassGroup K

The square class of a unit.

Equations

• TauCeti.squareClass u = ↑(Additive.ofMul u)

@[simp]

theorem TauCeti.squareClass_eq_zero_iff {K : Type u_1} [Field K] (u : Kˣ) : squareClass u = 0 ↔ IsSquare u

A unit has trivial square class iff it is a square.

theorem TauCeti.squareClass_prod {K : Type u_1} [Field K] {ι : Type u_2} (S : Finset ι) (d : ι → Kˣ) : squareClass (∏ i ∈ S, d i) = ∑ i ∈ S, squareClass (d i)

The square class of a product is the sum of the square classes.

theorem TauCeti.linearIndependent_squareClass_iff {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (d : ι → Kˣ) : (LinearIndependent (ZMod 2) fun (i : ι) => squareClass (d i)) ↔ ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)

Square-class independence is ZMod 2-linear independence. For a finite family of units d : ι → Kˣ, the square classes squareClass (d i) are ZMod 2-linearly independent in the square-class group iff no nonempty subset product ∏_{i ∈ S} d i is a square. The right-hand side is the Finset form of square-class independence that the multiquadratic degree theorem consumes.