The quadratic norm subgroup

For a : R over a commutative ring R, this file packages the unit norms from the quadratic algebra R[√a] = QuadraticAlgebra R a 0 as a subgroup of Rˣ. Over a field the norm-equation Hilbert symbol is exactly the sign indicator of this subgroup.

This separates the ring-generic group theory from the arithmetic input used over a nonarchimedean local field. Once the quadratic norm subgroup is known to have index two, its sign indicator is multiplicative, which is the group-theoretic step in the bimultiplicativity of the local Hilbert symbol, and it takes the value -1 off the subgroup, which is the group-theoretic step in the nondegeneracy of that symbol.

The diagonal entry of the symbol, TauCeti.hilbertSymbol_self, needs no arithmetic input at all: the norm subgroup for the radicand a contains the norm -a of the square-root generator, so it contains a exactly when it contains -1.

The subgroup contains every square and, when a is a unit, -a, the norm of the square-root generator. Thus its index may be computed in the square-class group, as in O'Meara, Introduction to Quadratic Forms, §63A.

The unit values of a binary diagonal form ⟨a, b⟩ are the coset a N of the norm subgroup N of its discriminant algebra R[√(-a b)] (TauCeti.mem_unitValueSet_binary_iff_mul_mem_quadraticNormSubgroup); this is how the norm subgroup computes the spinor norms of binary forms. In particular the unit values of the norm form ⟨1, -b⟩ of the quadratic algebra K[√b] are the units c with (b, c) = 1 (TauCeti.mem_unitValueSet_binary_one_neg_iff_hilbertSymbol_eq_one); this algebra is the field K(√b) only when b is not a square.

noncomputable def TauCeti.quadraticNormHom {R : Type u_1} [CommRing R] (a : R) : (QuadraticAlgebra R a 0)ˣ →* Rˣ

The norm on the units of the quadratic algebra R[√a], with values in Rˣ.

@[simp]

theorem TauCeti.quadraticNormHom_apply {R : Type u_1} [CommRing R] (a : R) (z : (QuadraticAlgebra R a 0)ˣ) : ↑((quadraticNormHom a) z) = QuadraticAlgebra.norm ↑z

The quadratic norm homomorphism evaluates to the quadratic-algebra norm.

noncomputable def TauCeti.quadraticNormSubgroup {R : Type u_1} [CommRing R] (a : R) : Subgroup Rˣ

The subgroup of Rˣ consisting of unit norms from R[√a].

theorem TauCeti.quadraticNormSubgroup_def {R : Type u_1} [CommRing R] (a : R) : quadraticNormSubgroup a = (quadraticNormHom a).range

The quadratic norm subgroup is the range of the norm homomorphism on units.

@[simp]

theorem TauCeti.mem_quadraticNormSubgroup_iff {R : Type u_1} [CommRing R] (a : R) (b : Rˣ) : b ∈ quadraticNormSubgroup a ↔ ∃ (z : (QuadraticAlgebra R a 0)ˣ), QuadraticAlgebra.norm ↑z = ↑b

Membership in the quadratic norm subgroup is the existence of a unit with the given norm.

theorem TauCeti.mem_quadraticNormSubgroup_iff_exists_norm_eq {R : Type u_1} [CommRing R] (a : R) (b : Rˣ) : b ∈ quadraticNormSubgroup a ↔ ∃ (z : QuadraticAlgebra R a 0), QuadraticAlgebra.norm z = ↑b

An element of R[√a] whose norm is a unit already witnesses membership in the quadratic norm subgroup, so no unit hypothesis on the witness is needed.

theorem TauCeti.square_le_quadraticNormSubgroup {R : Type u_1} [CommRing R] (a : R) : Subgroup.square Rˣ ≤ quadraticNormSubgroup a

Every square is a norm from a quadratic algebra.

theorem TauCeti.quadraticNormSubgroup_index_dvd_square_index {R : Type u_1} [CommRing R] (a : R) : (quadraticNormSubgroup a).index ∣ (Subgroup.square Rˣ).index

The index of the quadratic norm subgroup divides the number of square classes.

theorem TauCeti.finiteIndex_quadraticNormSubgroup {R : Type u_1} [CommRing R] (a : R) [(Subgroup.square Rˣ).FiniteIndex] : (quadraticNormSubgroup a).FiniteIndex

Finiteness of the square-class group implies finite index for the quadratic norm subgroup.

theorem TauCeti.sq_sub_mem_quadraticNormSubgroup {R : Type u_1} [CommRing R] (a ξ : R) {x : Rˣ} (hx : ↑x = ξ ^ 2 - a) : x ∈ quadraticNormSubgroup a

A unit equal to ξ² - a is a norm from R[√a].

theorem TauCeti.neg_radicand_mem_quadraticNormSubgroup {R : Type u_1} [CommRing R] (a : Rˣ) : -a ∈ quadraticNormSubgroup ↑a

The element -a is the norm of the square-root generator of R[√a].

theorem TauCeti.quadraticNormSubgroup_index_lt_square_index {R : Type u_1} [CommRing R] (a : Rˣ) (ha : ¬IsSquare (-a)) [(Subgroup.square Rˣ).FiniteIndex] : (quadraticNormSubgroup ↑a).index < (Subgroup.square Rˣ).index

If -a is not a square, the norm -a of the square-root generator lies outside the squares, so the quadratic norm subgroup has strictly smaller index than the subgroup of squares.

@[simp]

theorem TauCeti.quadraticNormSubgroup_mul_sq {R : Type u_1} [CommRing R] (a : R) (c : Rˣ) : quadraticNormSubgroup (a * ↑c ^ 2) = quadraticNormSubgroup a

Rescaling the radicand by a square does not change the quadratic norm subgroup.

theorem TauCeti.mem_unitValueSet_binary_iff_mul_mem_quadraticNormSubgroup {R : Type u_1} [CommRing R] (a : Rˣ) (b : R) (c : Rˣ) : c ∈ (QuadraticMap.weightedSumSquares R ![↑a, b]).unitValueSet ↔ a * c ∈ quadraticNormSubgroup (-(↑a * b))

The values of a binary form are a coset of norms. A unit c is represented by the binary diagonal form ⟨a, b⟩ exactly when a * c is a norm from the discriminant algebra R[√(-a b)], because a (a x² + b y²) = (a x)² + a b y². Over a field this says that the nonzero values of ⟨a, b⟩ are the coset a N of the norm group N of R[√(-a b)].

theorem TauCeti.quadraticNormSubgroup_eq_of_isSquare_mul {K : Type u_1} [Field K] {a Δ : Kˣ} (h : IsSquare (a * Δ)) : quadraticNormSubgroup ↑a = quadraticNormSubgroup ↑Δ

The quadratic norm subgroup depends only on the square class of the radicand: radicands whose product is a square have the same norm subgroup. This is the square-class form of TauCeti.quadraticNormSubgroup_mul_sq.

@[simp]

theorem TauCeti.hilbertSymbol_eq_one_iff_mem_quadraticNormSubgroup {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbol a b = 1 ↔ b ∈ quadraticNormSubgroup ↑a

The Hilbert symbol is positive exactly on the quadratic norm subgroup.

theorem TauCeti.mem_unitValueSet_binary_one_neg_iff_hilbertSymbol_eq_one {K : Type u_1} [Field K] (b c : Kˣ) : c ∈ (QuadraticMap.weightedSumSquares K ![1, -↑b]).unitValueSet ↔ hilbertSymbol b c = 1

The values of the norm form. The binary form ⟨1, -b⟩, the norm form of the quadratic algebra K[√b], represents a unit c exactly when the Hilbert symbol (b, c) is 1.

@[simp]

theorem TauCeti.hilbertSymbol_self {K : Type u_1} [Field K] (a : Kˣ) : hilbertSymbol a a = hilbertSymbol a (-1)

The diagonal entry of the Hilbert symbol. The sign of (a, a) is the sign of (a, -1) for every a, with no hypothesis beyond K being a field, so the diagonal entry is no separate choice of normalization.

theorem TauCeti.hilbertSymbol_eq_signIndicator {K : Type u_1} [Field K] (a b : Kˣ) : hilbertSymbol a b = (quadraticNormSubgroup ↑a).signIndicator b

The Hilbert symbol is the sign indicator of the quadratic norm subgroup.

theorem TauCeti.hilbertSymbol_mul_iff_quadraticNormSubgroup_index_dvd_two {K : Type u_1} [Field K] (a : Kˣ) : (∀ (b c : Kˣ), hilbertSymbol a (b * c) = hilbertSymbol a b * hilbertSymbol a c) ↔ (quadraticNormSubgroup ↑a).index ∣ 2

The Hilbert symbol is multiplicative in its second argument exactly when the quadratic norm subgroup has index dividing two.

noncomputable def TauCeti.hilbertSymbolHom {K : Type u_1} [Field K] (a : Kˣ) (hindex : (quadraticNormSubgroup ↑a).index ∣ 2) : Kˣ →* ℤˣ

When the quadratic norm subgroup has index dividing two, the Hilbert symbol in the second argument is a multiplicative character.

@[simp]

theorem TauCeti.hilbertSymbolHom_apply {K : Type u_1} [Field K] (a : Kˣ) (hindex : (quadraticNormSubgroup ↑a).index ∣ 2) (b : Kˣ) : (hilbertSymbolHom a hindex) b = hilbertSymbol a b

Evaluation of the Hilbert-symbol character.

@[simp]

theorem TauCeti.ker_hilbertSymbolHom {K : Type u_1} [Field K] (a : Kˣ) (hindex : (quadraticNormSubgroup ↑a).index ∣ 2) : (hilbertSymbolHom a hindex).ker = quadraticNormSubgroup ↑a

The kernel of the Hilbert-symbol character is the quadratic norm subgroup.

theorem TauCeti.exists_hilbertSymbol_eq_neg_one_of_index_eq_two {K : Type u_1} [Field K] (a : Kˣ) (hindex : (quadraticNormSubgroup ↑a).index = 2) : ∃ (b : Kˣ), hilbertSymbol a b = -1

Nondegeneracy of the Hilbert symbol for a radicand of norm index two. If the quadratic norm subgroup of a has index two, then the Hilbert symbol with first argument a is a nontrivial sign-valued character, so it takes the value -1. This is the field-level form: no arithmetic beyond the index is needed.