Exchanging orthogonal summands at a place

Let P, P' and W be regular quadratic forms over a number field K, where P and P' have the same rank and the same discriminant at a finite place v. At v there are at most two isometry classes with a given rank and discriminant, distinguished by the local Hasse invariant. So if P_v ≄ P'_v, and U is a regular form over K_v with the rank and discriminant of W_v but W_v ≄ U, the Hasse invariants change twice and

(P ⊥ W)_v ≅ P'_v ⊥ U.

In particular P'_v is represented by (P ⊥ W)_v, with orthogonal complement U.

Now let V be a regular form with P' ⊥ V ≅ P ⊥ W over K. Witt cancellation identifies the localizations of V:

• where P and P' are isometric, at a finite or a real place, V is isometric to W;
• at a finite place v where P_v ≄ P'_v, V_v is isometric to every regular form U of the rank and discriminant of W_v with W_v ≄ U.

This is the local half of O'Meara's construction of a global form with prescribed localizations. There W matches the prescribed local forms U_v except at a finite set R of finite places, and the correction planes P = ⟨1, -β⟩ and P' = ⟨α, -αβ⟩ are chosen to be nonisometric exactly at the places of R. A global representation of P' by P ⊥ W then has an orthogonal complement V with V_v ≅ U_v at every place.

Main results

• QuadraticForm.atFinitePlace_prod_equivalent_prod_of_not_equivalent: the local exchange (P ⊥ W)_v ≅ P'_v ⊥ U.
• QuadraticForm.atFinitePlace_equivalent_of_prod_equivalent_prod_of_equivalent, QuadraticForm.atRealPlace_equivalent_of_prod_equivalent_prod_of_equivalent: if P' ⊥ V ≅ P ⊥ W and P and P' are isometric at a place, so are V and W.
• QuadraticForm.atFinitePlace_equivalent_of_prod_equivalent_prod_of_not_equivalent: if P' ⊥ V ≅ P ⊥ W and P_v ≄ P'_v, then V_v ≅ U for every U as above.

References

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

theorem QuadraticForm.atFinitePlace_prod_equivalent_prod_of_not_equivalent {K : Type u} [Field K] {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {P : QuadraticForm K V₁} {P' : QuadraticForm K V₂} {W : QuadraticForm K V₃} [NumberField K] [FiniteDimensional K V₁] [FiniteDimensional K V₂] [FiniteDimensional K V₃] (hP : QuadraticMap.Nondegenerate) (hP' : QuadraticMap.Nondegenerate) (hW : QuadraticMap.Nondegenerate) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hPr : Module.finrank K V₁ = Module.finrank K V₂) (hPd : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass P hP).discr = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass P' hP').discr) (hPP' : ¬QuadraticMap.Equivalent (P.atFinitePlace v) (P'.atFinitePlace v)) {X : Type u_5} [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) : QuadraticMap.Equivalent (atFinitePlace (QuadraticMap.prod P W) v) (QuadraticMap.prod (P'.atFinitePlace v) U)

Exchanging summands at a finite place. Suppose P and P' have the same rank and the same discriminant at v but P_v ≄ P'_v, and U is a regular form over K_v with the rank and discriminant of W_v but W_v ≄ U. Then (P ⊥ W)_v ≅ P'_v ⊥ U.

theorem QuadraticForm.atFinitePlace_equivalent_of_prod_equivalent_prod_of_equivalent {K : Type u} [Field K] {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} {V₄ : Type u_4} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] [AddCommGroup V₄] [Module K V₄] {P : QuadraticForm K V₁} {P' : QuadraticForm K V₂} {W : QuadraticForm K V₃} {V : QuadraticForm K V₄} [NumberField K] [FiniteDimensional K V₂] (hP' : QuadraticMap.Nondegenerate) (h : (QuadraticMap.prod P' V).Equivalent (QuadraticMap.prod P W)) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hPP' : QuadraticMap.Equivalent (P.atFinitePlace v) (P'.atFinitePlace v)) : QuadraticMap.Equivalent (V.atFinitePlace v) (W.atFinitePlace v)

If P' ⊥ V ≅ P ⊥ W over K and P_v ≅ P'_v at a finite place v, then V_v ≅ W_v.

theorem QuadraticForm.atRealPlace_equivalent_of_prod_equivalent_prod_of_equivalent {K : Type u} [Field K] {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} {V₄ : Type u_4} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] [AddCommGroup V₄] [Module K V₄] {P : QuadraticForm K V₁} {P' : QuadraticForm K V₂} {W : QuadraticForm K V₃} {V : QuadraticForm K V₄} [FiniteDimensional K V₂] (hP' : QuadraticMap.Nondegenerate) (h : (QuadraticMap.prod P' V).Equivalent (QuadraticMap.prod P W)) {w : { w : NumberField.InfinitePlace K // w.IsReal }} (hPP' : QuadraticMap.Equivalent (P.atRealPlace w) (P'.atRealPlace w)) : QuadraticMap.Equivalent (V.atRealPlace w) (W.atRealPlace w)

If P' ⊥ V ≅ P ⊥ W over K and P_w ≅ P'_w at a real place w, then V_w ≅ W_w.

theorem QuadraticForm.atFinitePlace_equivalent_of_prod_equivalent_prod_of_not_equivalent {K : Type u} [Field K] {V₁ : Type u_1} {V₂ : Type u_2} {V₃ : Type u_3} {V₄ : Type u_4} [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] [AddCommGroup V₄] [Module K V₄] {P : QuadraticForm K V₁} {P' : QuadraticForm K V₂} {W : QuadraticForm K V₃} {V : QuadraticForm K V₄} [NumberField K] [FiniteDimensional K V₁] [FiniteDimensional K V₂] [FiniteDimensional K V₃] (hP : QuadraticMap.Nondegenerate) (hP' : QuadraticMap.Nondegenerate) (hW : QuadraticMap.Nondegenerate) (h : (QuadraticMap.prod P' V).Equivalent (QuadraticMap.prod P W)) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hPr : Module.finrank K V₁ = Module.finrank K V₂) (hPd : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass P hP).discr = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap (TauCeti.formClass P' hP').discr) (hPP' : ¬QuadraticMap.Equivalent (P.atFinitePlace v) (P'.atFinitePlace v)) {X : Type u_5} [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) : QuadraticMap.Equivalent (V.atFinitePlace v) U

The local complement after an exchange. Suppose P' ⊥ V ≅ P ⊥ W over K, where P and P' have the same rank and the same discriminant at a finite place v but P_v ≄ P'_v. Then V_v is isometric to every regular form U over K_v with the rank and discriminant of W_v and W_v ≄ U.