Quadratic forms in towers of number-field completions

For an extension of number fields L/K and finite places w above v, localization commutes with scalar extension from K to L. The comparison uses the canonical completion map K_v → L_w, and identifies both iterated tensor-product spaces with L_w ⊗[K] V.

At a real place w of L, the restriction of w to K is again real and its embedding is the restriction of the embedding of w, so the localization at w of the scalar extension to L is isometric to the localization of the original form at the restricted place.

This compatibility is the bridge needed to transfer local properties of a quadratic form over K to the completions of a field extension. In particular, it allows an isotropic vector over K_v to be extended to every L_w above it, so a form which is isotropic at every finite and real place of K stays so at every finite and real place of L.

Main results

• QuadraticForm.atFinitePlaceBaseChange: the finite-place comparison (Q_L)_w ≃ (Q_v)_{L_w}.
• QuadraticForm.atRealPlaceBaseChange: the real-place comparison (Q_L)_w ≃ Q_{w|K}.
• QuadraticForm.IsLocallyIsotropic.baseChange: local isotropy survives scalar extension to a finite extension of number fields.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §6.

noncomputable def QuadraticForm.atFinitePlaceBaseChange {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [NumberField L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : QuadraticMap.IsometryEquiv ((QuadraticForm.baseChange L Q).atFinitePlace w) (QuadraticForm.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (Q.atFinitePlace v))

Localization after extending a quadratic form from K to L is canonically isometric to extending its localization along the completion map K_v → L_w.

@[simp]

theorem QuadraticForm.atFinitePlaceBaseChange_toLinearEquiv {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [NumberField L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : (Q.atFinitePlaceBaseChange v w).toLinearEquiv = TensorProduct.AlgebraTensorModule.cancelBaseChange K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) V ≪≫ₗ (TensorProduct.AlgebraTensorModule.cancelBaseChange K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) V).symm

The localization/base-change isometry is the composite of the two canonical tensor-product cancellations through L_w ⊗[K] V.

@[simp]

theorem QuadraticForm.atFinitePlaceBaseChange_tmul {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [NumberField L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (b : IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (a : L) (x : V) : (Q.atFinitePlaceBaseChange v w) (b ⊗ₜ[L] (a ⊗ₜ[K] x)) = ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) a * b) ⊗ₜ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (1 ⊗ₜ[K] x)

The localization/base-change comparison sends a twice-pure tensor to the same global vector, with the intermediate scalar transported along K_v → L_w.

@[simp]

theorem QuadraticForm.atFinitePlaceBaseChange_symm_tmul {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [NumberField L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (b : IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (x : V) : (Q.atFinitePlaceBaseChange v w).symm (b ⊗ₜ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (a ⊗ₜ[K] x)) = ((algebraMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) a * b) ⊗ₜ[L] (1 ⊗ₜ[K] x)

The inverse localization/base-change comparison multiplies a completion scalar by the image of its intermediate K_v-scalar.

noncomputable def QuadraticForm.atRealPlaceBaseChange {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace L // w.IsReal }) : QuadraticMap.IsometryEquiv ((QuadraticForm.baseChange L Q).atRealPlace w) (Q.atRealPlace ⟨(↑w).comap (algebraMap K L), ⋯⟩)

Localization at a real place w after extending a quadratic form from K to L is canonically isometric to the localization at the restriction of w to K.

@[simp]

theorem QuadraticForm.atRealPlaceBaseChange_toLinearEquiv {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace L // w.IsReal }) : (Q.atRealPlaceBaseChange w).toLinearEquiv = TensorProduct.AlgebraTensorModule.cancelBaseChange K L ℝ ℝ V

The real-place localization/base-change isometry is Mathlib's canonical tensor-product cancellation ℝ ⊗[L] (L ⊗[K] V) ≃ ℝ ⊗[K] V.

@[simp]

theorem QuadraticForm.atRealPlaceBaseChange_tmul {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace L // w.IsReal }) (b : ℝ) (a : L) (x : V) : (Q.atRealPlaceBaseChange w) (b ⊗ₜ[L] (a ⊗ₜ[K] x)) = ((NumberField.InfinitePlace.embedding_of_isReal ⋯) a * b) ⊗ₜ[K] x

The real-place localization/base-change comparison multiplies the intermediate scalar into the real factor through the embedding of the real place.

@[simp]

theorem QuadraticForm.atRealPlaceBaseChange_symm_tmul {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace L // w.IsReal }) (b : ℝ) (x : V) : (Q.atRealPlaceBaseChange w).symm (b ⊗ₜ[K] x) = b ⊗ₜ[L] (1 ⊗ₜ[K] x)

The inverse real-place localization/base-change comparison inserts the unit of L as the intermediate scalar.

theorem QuadraticForm.IsLocallyIsotropic.baseChange {K : Type uK} [Field K] [NumberField K] {L : Type uL} [Field L] [NumberField L] [Algebra K L] {V : Type uV} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (hQ : Q.IsLocallyIsotropic) : (QuadraticForm.baseChange L Q).IsLocallyIsotropic

A quadratic form which is isotropic at every finite and real place of K stays isotropic at every finite and real place of a finite extension L of K.