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, TauCeti.squareClassHom: the class of a unit, as a function and a multiplicative homomorphism, with squareClass_eq_zero_iff characterising the trivial class as the squares, ker_squareClassHom identifying the kernel of the quotient map with the subgroup of squares, and squareClass_mul, squareClass_prod, squareClass_pow computing it on products and powers.
• TauCeti.squareClass_eq_iff_isSquare_mul: equality of square classes read as a square product.
• TauCeti.SquareClassGroup.two_nsmul_eq_zero: the square-class group is killed by two.
• 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ˣ))

@[instance_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)

theorem TauCeti.squareClass_def {K : Type u_1} [Field K] (u : Kˣ) : squareClass u = ↑(Additive.ofMul u)

The square class of a unit is its image under the additive quotient map.

@[simp]

theorem TauCeti.squareClass_toMul_out {K : Type u_1} [Field K] (x : SquareClassGroup K) : squareClass (Additive.toMul (Quotient.out x)) = x

The unit underlying a quotient representative has the original square class.

def TauCeti.squareClassHom {K : Type u_1} [Field K] : Kˣ →* Multiplicative (SquareClassGroup K)

The square-class quotient map, written multiplicatively between the unit group and the multiplicative form of the additive square-class group.

Equations

• TauCeti.squareClassHom = AddMonoidHom.toMultiplicativeRight (QuotientAddGroup.mk' (Subgroup.toAddSubgroup (Subgroup.square Kˣ)))

@[simp]

theorem TauCeti.squareClassHom_apply {K : Type u_1} [Field K] (u : Kˣ) : squareClassHom u = Multiplicative.ofAdd (squareClass 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.

@[simp]

theorem TauCeti.ker_squareClassHom {K : Type u_1} [Field K] : squareClassHom.ker = Subgroup.square Kˣ

The kernel of the square-class quotient map is the subgroup of squares.

@[simp]

theorem TauCeti.squareClass_one {K : Type u_1} [Field K] : squareClass 1 = 0

The unit 1 has trivial square class.

@[simp]

theorem TauCeti.squareClass_mul {K : Type u_1} [Field K] (u v : Kˣ) : squareClass (u * v) = squareClass u + squareClass v

The square class of a product of two units is the sum of their square classes.

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.squareClass_eq_iff_isSquare_mul {K : Type u_1} [Field K] (u v : Kˣ) : squareClass u = squareClass v ↔ IsSquare (u * v)

Two units have the same square class exactly when their product is a square. This is the quotient-free reading of equality in the square-class group.

@[simp]

theorem TauCeti.squareClass_pow {K : Type u_1} [Field K] (u : Kˣ) (n : ℕ) : squareClass (u ^ n) = n • squareClass u

The square class of a power is the corresponding multiple of the square class.

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.