Continuity of localized quadratic forms

Finite, real, and complex localizations of a finite-dimensional quadratic form are continuous for the module topology on their scalar extensions. The statements accept any topology with IsModuleTopology, so they do not depend on a basis or on a chosen construction of that topology.

At a real place, a neighborhood of a vector with nonzero value preserves the square class of that value. This is the real-place input for choosing a global vector by weak approximation while controlling its quadratic value, as in O'Meara, Introduction to Quadratic Forms, §66.

The same conclusion holds at every finite place, including places above two. It uses openness of the square subgroup in the unit group of the nonarchimedean completion.

theorem QuadraticForm.continuous_atFinitePlace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NumberField K] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [TopologicalSpace v.FiniteScalarExtension] [IsModuleTopology (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) v.FiniteScalarExtension] : Continuous ⇑(Q.atFinitePlace v)

A quadratic form localized at a finite place is continuous for the module topology.

theorem QuadraticForm.continuous_atRealPlace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) [TopologicalSpace (TauCeti.RealScalarExtension w)] [IsModuleTopology ℝ (TauCeti.RealScalarExtension w)] : Continuous ⇑(Q.atRealPlace w)

A quadratic form localized at a real place is continuous for the module topology.

theorem QuadraticForm.continuous_atComplexEmbedding {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (w : NumberField.InfinitePlace K) [TopologicalSpace w.ComplexScalarExtension] [IsModuleTopology ℂ w.ComplexScalarExtension] : Continuous ⇑(Q.atComplexEmbedding w)

A quadratic form localized through a complex embedding is continuous for the module topology.

theorem QuadraticForm.exists_isOpen_isSquare_div_atRealPlace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) [TopologicalSpace (TauCeti.RealScalarExtension w)] [IsModuleTopology ℝ (TauCeti.RealScalarExtension w)] {x : TauCeti.RealScalarExtension w} (hx : (Q.atRealPlace w) x ≠ 0) : ∃ (U : Set (TauCeti.RealScalarExtension w)), IsOpen U ∧ x ∈ U ∧ ∀ z ∈ U, (Q.atRealPlace w) z ≠ 0 ∧ IsSquare ((Q.atRealPlace w) z / (Q.atRealPlace w) x)

Around a real local vector with nonzero value there is an open neighborhood on which the quadratic value stays nonzero and in the same square class.

theorem QuadraticForm.exists_isOpen_isSquare_div_atFinitePlace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [NumberField K] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [TopologicalSpace v.FiniteScalarExtension] [IsModuleTopology (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) v.FiniteScalarExtension] {x : v.FiniteScalarExtension} (hx : (Q.atFinitePlace v) x ≠ 0) : ∃ (U : Set v.FiniteScalarExtension), IsOpen U ∧ x ∈ U ∧ ∀ z ∈ U, (Q.atFinitePlace v) z ≠ 0 ∧ IsSquare ((Q.atFinitePlace v) z / (Q.atFinitePlace v) x)

Around a finite local vector with nonzero value there is an open neighborhood on which the quadratic value stays nonzero and in the same square class.