Correcting a global form at finitely many places

Let W be a regular quadratic form over a number field K, and let U_v be regular forms over the completions K_v with the rank of W and with discriminant the image of the discriminant of W. Let α, β ∈ Kˣ, with β positive at every real place, be such that

W_v ≅ U_v   ↔   (α, β)_v = 1     at every finite place v.

With the correction planes P = ⟨1, -β⟩ and P' = ⟨α, -αβ⟩, this file proves:

• P' is represented by P ⊥ W at every finite and real place. Where (α, β)_v = 1 the two planes are isometric; where (α, β)_v = -1, the forms W_v and U_v are two different classes with the same rank and discriminant, and exchanging summands gives (P ⊥ W)_v ≅ P'_v ⊥ U_v.
• If P' is represented by P ⊥ W over K, its orthogonal complement Q is a regular global form of the rank and discriminant of W with Q_v ≅ U_v at every finite place and Q_w ≅ W_w at every real place.

This is the correction step of O'Meara's construction of a global form with prescribed localizations. There W is a first global approximation that matches the targets U_v except at a finite set R of finite places, β is a square at every archimedean place and a nonsquare at every place of R, and α is chosen by Hilbert sign prescription with (α, β)_v = -1 exactly on R. The local representation of P' by P ⊥ W is the input of the local-global principle for representations, whose global representation produces Q.

Main results

• QuadraticForm.locallyRepresents_weightedSumSquares_neg_self_mul_prod: P' is locally represented by P ⊥ W.
• QuadraticForm.atFinitePlace_equivalent_of_weightedSumSquares_neg_self_mul_prod_equivalent, QuadraticForm.atRealPlace_equivalent_of_weightedSumSquares_neg_self_mul_prod_equivalent, QuadraticForm.discr_eq_of_weightedSumSquares_neg_self_mul_prod_equivalent: if P' ⊥ Q ≅ P ⊥ W over K, then Q_v ≅ U_v at every finite place, Q_w ≅ W_w at every real place, and Q and W have the same discriminant.
• QuadraticForm.exists_discr_eq_equivalent_of_isRepresentedBy_prod: a global representation of P' by P ⊥ W produces a regular global form on Fin n → K with these localizations and the discriminant of W.

References

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

theorem QuadraticForm.locallyRepresents_weightedSumSquares_neg_self_mul_prod {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : QuadraticForm K V} (hW : QuadraticMap.Nondegenerate) (a b : Kˣ) (hb : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b) {n : ℕ} (hn : Module.finrank K V = n) (U : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (Fin n → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (hU : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Nondegenerate) (hUd : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass W hW).discr = (TauCeti.formClass (U v) ⋯).discr) (hWU : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) = -1 → ¬QuadraticMap.Equivalent (W.atFinitePlace v) (U v)) : LocallyRepresents (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]) ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W)

The local representation of the correction plane. Let W be a regular form over K and α, β ∈ Kˣ with β positive at every real place. Suppose that at each finite place v with (α, β)_v = -1 the localization W_v is not isometric to a given regular form U_v over K_v having the rank of W and the discriminant of W_v. Then ⟨α, -αβ⟩ is represented by ⟨1, -β⟩ ⊥ W at every finite and real place.

theorem QuadraticForm.atFinitePlace_equivalent_of_weightedSumSquares_neg_self_mul_prod_equivalent {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : QuadraticForm K V} {V' : Type u_3} [AddCommGroup V'] [Module K V'] {Q : QuadraticForm K V'} (hW : QuadraticMap.Nondegenerate) {a b : Kˣ} (h : ((QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]).prod Q).Equivalent ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W)) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {X : Type u_4} [AddCommGroup X] [Module (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X] {U : QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X} (hU : QuadraticMap.Nondegenerate) (hUr : Module.finrank K V = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) X) (hUd : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass W hW).discr = (TauCeti.formClass U hU).discr) (hWU : QuadraticMap.Equivalent (W.atFinitePlace v) U ↔ TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) = 1) : QuadraticMap.Equivalent (Q.atFinitePlace v) U

The corrected form at a finite place. Suppose ⟨α, -αβ⟩ ⊥ Q ≅ ⟨1, -β⟩ ⊥ W over K, and let U be a regular form over K_v with the rank of W and the discriminant of W_v such that W_v ≅ U exactly when (α, β)_v = 1. Then Q_v ≅ U.

theorem QuadraticForm.atRealPlace_equivalent_of_weightedSumSquares_neg_self_mul_prod_equivalent {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] {W : QuadraticForm K V} {V' : Type u_3} [AddCommGroup V'] [Module K V'] {Q : QuadraticForm K V'} {a b : Kˣ} (h : ((QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]).prod Q).Equivalent ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W)) {w : { w : NumberField.InfinitePlace K // w.IsReal }} (hb : 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b) : QuadraticMap.Equivalent (Q.atRealPlace w) (W.atRealPlace w)

The corrected form at a real place. If ⟨α, -αβ⟩ ⊥ Q ≅ ⟨1, -β⟩ ⊥ W over K and β is positive at the real place w, then Q_w ≅ W_w.

theorem QuadraticForm.discr_eq_of_weightedSumSquares_neg_self_mul_prod_equivalent {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : QuadraticForm K V} {V' : Type u_3} [AddCommGroup V'] [Module K V'] {Q : QuadraticForm K V'} [Invertible 2] [FiniteDimensional K V'] (hQ : QuadraticMap.Nondegenerate) (hW : QuadraticMap.Nondegenerate) {a b : Kˣ} (h : ((QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]).prod Q).Equivalent ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W)) : (TauCeti.formClass Q hQ).discr = (TauCeti.formClass W hW).discr

The corrected form has the discriminant of W. If ⟨α, -αβ⟩ ⊥ Q ≅ ⟨1, -β⟩ ⊥ W over K with Q and W regular, then Q and W have the same discriminant, because the two planes do.

theorem QuadraticForm.exists_discr_eq_equivalent_of_isRepresentedBy_prod {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : QuadraticForm K V} (hW : QuadraticMap.Nondegenerate) (a b : Kˣ) (hb : ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b) {n : ℕ} (hn : Module.finrank K V = n) (U : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (Fin n → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (hU : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Nondegenerate) (hUd : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass W hW).discr = (TauCeti.formClass (U v) ⋯).discr) (hWU : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Equivalent (W.atFinitePlace v) (U v) ↔ TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) = 1) (hrep : (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]).IsRepresentedBy ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W)) : ∃ (Q : QuadraticForm K (Fin n → K)) (hQ : QuadraticMap.Nondegenerate), (TauCeti.formClass Q hQ).discr = (TauCeti.formClass W hW).discr ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Equivalent (Q.atFinitePlace v) (U v)) ∧ ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), QuadraticMap.Equivalent (Q.atRealPlace w) (W.atRealPlace w)

The corrected global form. Let W be a regular form over K of rank n, let U_v be regular forms over the completions with rank n and the discriminant of W_v, and let α, β ∈ Kˣ, with β positive at every real place, satisfy W_v ≅ U_v ↔ (α, β)_v = 1 at every finite place. If ⟨α, -αβ⟩ is represented by ⟨1, -β⟩ ⊥ W over K, then there is a regular form Q on Fin n → K with the discriminant of W, with Q_v ≅ U_v at every finite place and with Q_w ≅ W_w at every real place.