The correction planes ⟨1, -β⟩ and ⟨α, -αβ⟩

For units α, β of a number field K, the binary forms

P = ⟨1, -β⟩,        P' = ⟨α, -αβ⟩ = α P

have the same dimension, and their discriminants -β and -α²β agree modulo squares. This file computes how they differ place by place. Their Hasse signs at a finite place v are

s_v(P) = (1, -β)_v = 1,        s_v(P') = (α, -αβ)_v = (α, β)_v,

and at every finite place and every real place the two localizations are isometric exactly when the local Hilbert symbol (α, β) is trivial there. In particular, if β is positive at a real place then the two planes are isometric there.

Replacing P by P' therefore preserves dimension and discriminant and changes the local isometry class exactly at the places where (α, β) = -1. This is the substitution in O'Meara's construction of a global form with prescribed localizations: when α is chosen with (α, β)_v = -1 exactly on a finite set R of places, swapping P for P' inside an orthogonal sum flips the finite Hasse sign exactly at the finite places of R.

Main results

• QuadraticForm.nondegenerate_weightedSumSquares_one_neg, QuadraticForm.nondegenerate_weightedSumSquares_neg_self_mul: both planes are regular.
• QuadraticForm.discr_formClass_weightedSumSquares_neg_self_mul: they have the same discriminant.
• QuadraticForm.finiteHasse_weightedSumSquares_one_neg: s_v(⟨1, -β⟩) = 1.
• QuadraticForm.finiteHasse_weightedSumSquares_neg_self_mul: s_v(⟨α, -αβ⟩) = (α, β)_v.
• QuadraticForm.equivalent_atFinitePlace_binary_one_neg_iff_hilbertSymbol_eq_one: at a finite place v, ⟨1, -β⟩ ≅ ⟨α, -αβ⟩ over K_v exactly when (α, β)_v = 1.
• QuadraticForm.equivalent_atRealPlace_binary_one_neg_iff_hilbertSymbol_eq_one: the same at a real place.
• QuadraticForm.equivalent_atRealPlace_binary_one_neg_of_pos: the two planes are isometric at every real place at which β is positive.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 72:1.

theorem QuadraticForm.nondegenerate_weightedSumSquares_one_neg {K : Type u_1} [Field K] [Invertible 2] (b : Kˣ) : QuadraticMap.Nondegenerate

The norm plane ⟨1, -β⟩ is regular.

theorem QuadraticForm.nondegenerate_weightedSumSquares_neg_self_mul {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : QuadraticMap.Nondegenerate

The scaled norm plane ⟨α, -αβ⟩ is regular.

@[simp]

theorem QuadraticForm.discr_formClass_weightedSumSquares_one_neg {K : Type u_1} [Field K] [Invertible 2] (b : Kˣ) : (TauCeti.formClass (QuadraticMap.weightedSumSquares K ![1, -↑b]) ⋯).discr = TauCeti.squareClass (-b)

The plain discriminant of the norm plane ⟨1, -β⟩ is the square class of -β.

theorem QuadraticForm.discr_formClass_weightedSumSquares_neg_self_mul {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : (TauCeti.formClass (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) ⋯).discr = (TauCeti.formClass (QuadraticMap.weightedSumSquares K ![1, -↑b]) ⋯).discr

The planes ⟨α, -αβ⟩ and ⟨1, -β⟩ have the same discriminant, since -α²β and -β differ by a square.

@[simp]

theorem QuadraticForm.finiteHasse_weightedSumSquares_one_neg {K : Type u_1} [Field K] [NumberField K] (b : Kˣ) (h : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : finiteHasse (QuadraticMap.weightedSumSquares K ![1, -↑b]) h v = 1

The finite Hasse sign of the norm plane ⟨1, -β⟩ is trivial at every finite place.

@[simp]

theorem QuadraticForm.finiteHasse_weightedSumSquares_neg_self_mul {K : Type u_1} [Field K] [NumberField K] (a b : Kˣ) (h : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : finiteHasse (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) h v = TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)

The finite Hasse sign of the scaled norm plane ⟨α, -αβ⟩ at a finite place v is the Hilbert symbol (α, β)_v.

theorem QuadraticForm.globalInvariants_realHasse_weightedSumSquares_neg_self_mul {K : Type u_1} [Field K] [NumberField K] (a b : Kˣ) (h : QuadraticMap.Nondegenerate) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (globalInvariants (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) h).realHasse w = TauCeti.hilbertSymbol ((TauCeti.unitAtRealPlace w) a) ((TauCeti.unitAtRealPlace w) b)

The real Hasse sign of the scaled norm plane ⟨α, -αβ⟩ at a real place w is the Hilbert symbol (α, β)_w.

theorem QuadraticForm.equivalent_atFinitePlace_binary_one_neg_iff_hilbertSymbol_eq_one {K : Type u_1} [Field K] [NumberField K] (a b : Kˣ) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : QuadraticMap.Equivalent (atFinitePlace (QuadraticMap.weightedSumSquares K ![1, -↑b]) v) (atFinitePlace (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) v) ↔ TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) = 1

The correction planes at a finite place. Over the completion K_v, the planes ⟨1, -β⟩ and ⟨α, -αβ⟩ are isometric exactly when the Hilbert symbol (α, β)_v is 1.

theorem QuadraticForm.equivalent_atRealPlace_binary_one_neg_iff_hilbertSymbol_eq_one {K : Type u_1} [Field K] (a b : Kˣ) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Equivalent (atRealPlace (QuadraticMap.weightedSumSquares K ![1, -↑b]) w) (atRealPlace (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) w) ↔ TauCeti.hilbertSymbol ((TauCeti.unitAtRealPlace w) a) ((TauCeti.unitAtRealPlace w) b) = 1

The correction planes at a real place. Over ℝ, the planes ⟨1, -β⟩ and ⟨α, -αβ⟩ are isometric at the real place w exactly when the real Hilbert symbol (α, β)_w is 1.

theorem QuadraticForm.equivalent_atRealPlace_binary_one_neg_of_pos {K : Type u_1} [Field K] (a : Kˣ) {b : Kˣ} {w : { w : NumberField.InfinitePlace K // w.IsReal }} (hb : 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b) : QuadraticMap.Equivalent (atRealPlace (QuadraticMap.weightedSumSquares K ![1, -↑b]) w) (atRealPlace (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) w)

At a real place where β is positive, the planes ⟨1, -β⟩ and ⟨α, -αβ⟩ are isometric: both are hyperbolic there.