Documentation

TauCeti.NumberTheory.HilbertSymbol.Archimedean

The Hilbert symbol over ℝ #

This file computes the norm-equation Hilbert symbol TauCeti.hilbertSymbol over ℝ.

Over ℝ the equation b = x² - a y² is solvable unless both a and b are negative, because x² - a y² is then positive for every nonzero (x, y). Hence (a, b) = -1 exactly when a < 0 and b < 0. Bimultiplicativity over ℝ is read off this formula, and so is the value of the product ∏_{i<j} (a_i, a_j) attached to a diagonal real form: it is (-1)^(q(q-1)/2), where q is the number of negative coefficients.

By Sylvester's law of inertia that count is the negative index of the form the family diagonalizes, so the product is an invariant of the isometry class and is the archimedean counterpart of the Hasse invariant of a form over a nonarchimedean local field. Evaluating it on the normal form p⟨1⟩ ⊥ q⟨-1⟩ gives the archimedean Hasse sign (-1)^(q(q-1)/2) of that form.

Main results #

References #

source
theorem TauCeti.hilbertSymbol_real (a b : ℝˣ) :
hilbertSymbol a b = if ↑a < 0 ∧ ↑b < 0 then -1 else 1

The real Hilbert symbol is -1 exactly when both parameters are negative.

source
theorem TauCeti.hilbertSymbol_real_eq_neg_one_iff (a b : ℝˣ) :
hilbertSymbol a b = -1 ↔ ↑a < 0 ∧ ↑b < 0

The real Hilbert symbol is -1 exactly when both parameters are negative.

source
theorem TauCeti.hilbertSymbol_real_eq_one_iff (a b : ℝˣ) :
hilbertSymbol a b = 1 ↔ 0 < ↑a ∨ 0 < ↑b

The real Hilbert symbol is 1 exactly when one of the parameters is positive.

source
@[simp]
theorem TauCeti.hilbertSymbol_real_mul_left (a a' b : ℝˣ) :
hilbertSymbol (a * a') b = hilbertSymbol a b * hilbertSymbol a' b

The real Hilbert symbol is multiplicative in its first parameter. Being [simp], it expands a product in the first parameter of any real symbol, in particular of a symbol read at a real place of a number field through TauCeti.unitAtRealPlace.

source
@[simp]
theorem TauCeti.hilbertSymbol_real_mul_right (a b b' : ℝˣ) :
hilbertSymbol a (b * b') = hilbertSymbol a b * hilbertSymbol a b'

The real Hilbert symbol is multiplicative in its second parameter. Being [simp], it expands a product in the second parameter of any real symbol, in particular of a symbol read at a real place of a number field through TauCeti.unitAtRealPlace.

source
theorem TauCeti.exists_hilbertSymbol_real_eq_neg_one {b : ℝˣ} (hb : ¬IsSquare b) :
∃ (a : ℝˣ), hilbertSymbol a b = -1

Every real nonsquare b has a partner a with (a, b) = -1; one may take a = -1.

source
theorem TauCeti.prod_hilbertSymbol_real {ι : Type u_1} [Fintype ι] [LinearOrder ι] (a : ι → ℝˣ) :
∏ ij : ι × ι with ij.1 < ij.2, hilbertSymbol (a ij.1) (a ij.2) = (-1) ^ {i : ι | ↑(a i) < 0}.card.choose 2

The product of the real Hilbert symbols (a_i, a_j) over the pairs i < j of a finite family is (-1)^(q(q-1)/2), where q is the number of negative members of the family.

source
theorem TauCeti.prod_hilbertSymbol_real_of_equiv_weightedSumSquares {M : Type u_1} [AddCommGroup M] [Module ℝ M] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {Q : QuadraticForm ℝ M} {a : ι → ℝˣ} (h : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun (i : ι) => ↑(a i))) :
∏ ij : ι × ι with ij.1 < ij.2, hilbertSymbol (a ij.1) (a ij.2) = (-1) ^ (sigNeg Q).choose 2

The product of the real Hilbert symbols over the ordered pairs of a diagonalization of a real quadratic form is (-1)^(q(q-1)/2), where q = sigNeg Q is the negative index of the form. In particular the product depends only on the isometry class of Q and not on the chosen diagonalization.

source
theorem TauCeti.prod_hilbertSymbol_realCliffordWeight (p q : ℕ) :
∏ ij : Fin (p + q) × Fin (p + q) with ij.1 < ij.2, hilbertSymbol (Units.mk0 (realCliffordWeight p q ij.1) ⋯) (Units.mk0 (realCliffordWeight p q ij.2) ⋯) = (-1) ^ q.choose 2

The archimedean Hasse sign of the normal form. The product of the real Hilbert symbols over the ordered pairs of the coordinate weights of realCliffordForm p q is (-1)^(q(q-1)/2).