Serre's sign functions on ℤ_2ˣ and the square classes of 2-adic units

For a unit u of ℤ_2, Serre (A Course in Arithmetic, Chapter I, §3.2) puts

• ε(u) = (u − 1)/2 mod 2, and
• ω(u) = (u² − 1)/8 mod 2.

Both depend only on u mod 8: on the odd residues 1, 3, 5, 7 they take the values ε = 0, 1, 0, 1 and ω = 0, 1, 1, 0. They are the ZMod 2-valued logarithms of the characters ZMod.χ₄ and ZMod.χ₈ of Mathlib, and they are the exponents in Serre's closed formula for the Hilbert symbol over ℚ_2.

The point of ε and ω is that together they classify 2-adic units up to squares. A unit is the square of a unit exactly when it is 1 mod 8, and every unit u satisfies

u = (-1) ^ ε(u) · 5 ^ ω(u) · w²

for some unit w. Read in ℚ_2, a unit of ℤ_2 is a square of ℚ_2 exactly when it is 1 mod 8.

Main definitions

• TauCeti.serreEps: Serre's ε : ℤ_2ˣ → ZMod 2.
• TauCeti.serreOmega: Serre's ω : ℤ_2ˣ → ZMod 2.

Main results

• TauCeti.serreEps_eq_one_iff, TauCeti.serreOmega_eq_one_iff (and the _eq_zero_iff variants): the values of ε and ω in terms of u mod 8.
• TauCeti.serreEps_eq_natCast_div_two_of_coe_eq_natCast: ε(m) = (m − 1)/2 mod 2 for a natural number m that is a unit of ℤ_2.
• TauCeti.serreEps_mul, TauCeti.serreOmega_mul: ε and ω are homomorphisms to the additive group ZMod 2; TauCeti.serreEps_pow, TauCeti.serreOmega_pow are the power forms.
• TauCeti.coe_neg_one_uzpow_serreEps, TauCeti.coe_neg_one_uzpow_serreOmega: (-1) ^ ε(u) is χ₄(u mod 4) and (-1) ^ ω(u) is χ₈(u mod 8).
• TauCeti.serreEps_eq_zero_and_serreOmega_eq_zero_iff: ε(u) = ω(u) = 0 exactly when u ≡ 1 mod 8.
• TauCeti.exists_eq_neg_one_pow_mul_five_pow_mul_sq: u = (-1) ^ ε(u) · 5 ^ ω(u) · w².
• TauCeti.isSquare_coe_iff_mem_unitsPrincipal_three: a unit of ℤ_2 is a square in ℚ_2 exactly when it lies in U^(3) = 1 + 8ℤ_2, and TauCeti.isSquare_iff_serreEps_eq_zero_and_serreOmega_eq_zero exactly when ε(u) = ω(u) = 0. For instance, -15 is a square in ℚ_2 (TauCeti.isSquare_neg_fifteen_padicTwo).

References

• J.-P. Serre, A Course in Arithmetic, Chapter I, §3.2, Chapter II, §3.3, and Chapter III, §1.2.

noncomputable def TauCeti.serreEps (u : ℤ_[2]ˣ) : ZMod 2

Serre's ε(u) = (u − 1)/2 mod 2 for a unit u of ℤ_2, read off u mod 8. On the odd residues 1, 3, 5, 7 it takes the values 0, 1, 0, 1.

noncomputable def TauCeti.serreOmega (u : ℤ_[2]ˣ) : ZMod 2

Serre's ω(u) = (u² − 1)/8 mod 2 for a unit u of ℤ_2, read off u mod 8. On the odd residues 1, 3, 5, 7 it takes the values 0, 1, 1, 0.

theorem TauCeti.serreEps_mul (u v : ℤ_[2]ˣ) : serreEps (u * v) = serreEps u + serreEps v

ε is a homomorphism from ℤ_2ˣ to the additive group ZMod 2.

theorem TauCeti.serreOmega_mul (u v : ℤ_[2]ˣ) : serreOmega (u * v) = serreOmega u + serreOmega v

ω is a homomorphism from ℤ_2ˣ to the additive group ZMod 2.

theorem TauCeti.serreEps_eq_one_iff (u : ℤ_[2]ˣ) : serreEps u = 1 ↔ (PadicInt.toZModPow 3) ↑u = 3 ∨ (PadicInt.toZModPow 3) ↑u = 7

ε(u) = 1 exactly when u is 3 or 7 modulo 8.

theorem TauCeti.serreEps_eq_zero_iff (u : ℤ_[2]ˣ) : serreEps u = 0 ↔ (PadicInt.toZModPow 3) ↑u = 1 ∨ (PadicInt.toZModPow 3) ↑u = 5

ε(u) = 0 exactly when u is 1 or 5 modulo 8.

theorem TauCeti.serreOmega_eq_one_iff (u : ℤ_[2]ˣ) : serreOmega u = 1 ↔ (PadicInt.toZModPow 3) ↑u = 3 ∨ (PadicInt.toZModPow 3) ↑u = 5

ω(u) = 1 exactly when u is 3 or 5 modulo 8.

theorem TauCeti.serreOmega_eq_zero_iff (u : ℤ_[2]ˣ) : serreOmega u = 0 ↔ (PadicInt.toZModPow 3) ↑u = 1 ∨ (PadicInt.toZModPow 3) ↑u = 7

ω(u) = 0 exactly when u is 1 or 7 modulo 8.

theorem TauCeti.isUnit_five_padicInt : IsUnit 5

5 is a unit of ℤ_2.

theorem TauCeti.serreEps_eq_zero_of_coe_eq_five {u : ℤ_[2]ˣ} (hu : ↑u = 5) : serreEps u = 0

ε(5) = 0, for the unit 5 of ℤ_2.

theorem TauCeti.serreEps_eq_natCast_div_two_of_coe_eq_natCast {u : ℤ_[2]ˣ} {m : ℕ} (hu : ↑u = ↑m) : serreEps u = ↑(m / 2)

ε(m) = ⌊m/2⌋ mod 2 for a unit of ℤ_2 that is a natural number m; as m is odd, this is Serre's (m − 1)/2 mod 2.

theorem TauCeti.serreOmega_eq_one_of_coe_eq_five {u : ℤ_[2]ˣ} (hu : ↑u = 5) : serreOmega u = 1

ω(5) = 1, for the unit 5 of ℤ_2.

@[simp]

theorem TauCeti.serreEps_one : serreEps 1 = 0

ε(1) = 0.

@[simp]

theorem TauCeti.serreOmega_one : serreOmega 1 = 0

ω(1) = 0.

theorem TauCeti.serreEps_pow (u : ℤ_[2]ˣ) (n : ℕ) : serreEps (u ^ n) = n • serreEps u

ε(u ^ n) = n ε(u).

theorem TauCeti.serreOmega_pow (u : ℤ_[2]ˣ) (n : ℕ) : serreOmega (u ^ n) = n • serreOmega u

ω(u ^ n) = n ω(u).

@[simp]

theorem TauCeti.serreEps_neg_one : serreEps (-1) = 1

ε(-1) = 1.

@[simp]

theorem TauCeti.serreOmega_neg_one : serreOmega (-1) = 0

ω(-1) = 0.

theorem TauCeti.coe_neg_one_uzpow_serreEps (u : ℤ_[2]ˣ) : ↑((-1) ^ serreEps u) = ZMod.χ₄ ((PadicInt.toZModPow 2) ↑u)

The sign (-1) ^ ε(u) is Mathlib's character χ₄ of u mod 4.

theorem TauCeti.coe_neg_one_uzpow_serreOmega (u : ℤ_[2]ˣ) : ↑((-1) ^ serreOmega u) = ZMod.χ₈ ((PadicInt.toZModPow 3) ↑u)

The sign (-1) ^ ω(u) is Mathlib's character χ₈ of u mod 8.

theorem TauCeti.serreEps_eq_zero_and_serreOmega_eq_zero_iff (u : ℤ_[2]ˣ) : serreEps u = 0 ∧ serreOmega u = 0 ↔ u ∈ unitsPrincipal 2 3

ε and ω both vanish exactly on the units U^(3) that are 1 mod 8, which are the squares of ℤ_2ˣ by TauCeti.unitsPrincipal_three_eq_range_powMonoidHom_two.

theorem TauCeti.exists_eq_neg_one_pow_mul_five_pow_mul_sq (u : ℤ_[2]ˣ) : ∃ (w : ℤ_[2]ˣ), ↑u = (-1) ^ (serreEps u).val * 5 ^ (serreOmega u).val * ↑w ^ 2

The square classes of ℤ_2ˣ. Every unit u of ℤ_2 is (-1) ^ ε(u) · 5 ^ ω(u) times the square of a unit.

theorem TauCeti.isSquare_coe_iff_mem_unitsPrincipal_three (u : ℤ_[2]ˣ) : IsSquare ↑↑u ↔ u ∈ unitsPrincipal 2 3

Squares of 2-adic units in ℚ_2. A unit of ℤ_2 is a square in ℚ_2 exactly when it is 1 mod 8.

theorem TauCeti.isSquare_neg_fifteen_padicTwo : IsSquare (-15)

-15 is a square in ℚ_2, since it is 1 mod 8.

theorem TauCeti.isSquare_iff_serreEps_eq_zero_and_serreOmega_eq_zero {a : ℚ_[2]ˣ} {u : ℤ_[2]ˣ} (ha : ↑a = ↑↑u) : IsSquare a ↔ serreEps u = 0 ∧ serreOmega u = 0

A unit u of ℤ_2 is a square of ℚ_2ˣ exactly when ε(u) = ω(u) = 0.