Localization of quadratic forms over number fields

This file defines scalar extension of a quadratic form from a number field to its canonical finite completions and to the real or complex field selected by an infinite place. The definitions use QuadraticForm.baseChange; in particular, their underlying spaces are genuine tensor products over the global field rather than independently chosen local spaces.

The evaluation, nondegeneracy, isometry-transport, localization of diagonal forms, and algebraic-compatibility lemmas make the local forms usable without unfolding the localization definitions. They are the common input for local isotropy, representation, and invariant comparisons over number fields. The class of the localization of a regular form at a real place is the scalar extension of its class (QuadraticForm.formClass_atRealPlace). On square classes of global units the place maps are computed by the localized units v.unitAtFinitePlace a and TauCeti.unitAtRealPlace w a.

noncomputable def IsDedekindDomain.HeightOneSpectrum.unitAtFinitePlace {K : Type u} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) : Kˣ →* (adicCompletion K v)ˣ

The map from global units to units in the completion at a finite place.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.unitAtFinitePlace_apply {K : Type u} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : Kˣ) : ↑(v.unitAtFinitePlace a) = (algebraMap K (adicCompletion K v)) ↑a

The underlying value of a localized unit is its image under the canonical algebra map.

theorem IsDedekindDomain.HeightOneSpectrum.valued_unitAtFinitePlace {K : Type u} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : Kˣ) : Valued.v ↑(v.unitAtFinitePlace a) = (valuation K v) ↑a

The valuation of a localized unit is the v-adic valuation of the global element.

theorem IsDedekindDomain.HeightOneSpectrum.squareClass_unitAtFinitePlace {K : Type u} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : Kˣ) : TauCeti.squareClass (v.unitAtFinitePlace a) = (algebraMap K (adicCompletion K v)).squareClassMap (TauCeti.squareClass a)

The image in K_vˣ/(K_vˣ)² of the square class of a global unit is the square class of its localization.

noncomputable def TauCeti.unitAtRealPlace {K : Type u} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) : Kˣ →* ℝˣ

The map from global units to real units induced by a real place.

@[simp]

theorem TauCeti.unitAtRealPlace_apply {K : Type u} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : Kˣ) : ↑((unitAtRealPlace w) a) = (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a

The underlying value of a localized unit is its image under the real-place embedding.

theorem TauCeti.squareClass_unitAtRealPlace {K : Type u} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : Kˣ) : squareClass ((unitAtRealPlace w) a) = (NumberField.InfinitePlace.embedding_of_isReal ⋯).squareClassMap (squareClass a)

The image in ℝˣ/(ℝˣ)² of the square class of a global unit under a real place is the square class of its image at that place.

noncomputable def QuadraticForm.atFinitePlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) v.FiniteScalarExtension

The localization of a quadratic form at a finite place of a number field.

noncomputable def QuadraticForm.atRealPlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticForm ℝ (TauCeti.RealScalarExtension w)

The localization of a quadratic form at a real place of a number field.

noncomputable def QuadraticForm.atComplexEmbedding {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : NumberField.InfinitePlace K) : QuadraticForm ℂ w.ComplexScalarExtension

The scalar extension of a quadratic form through the chosen complex embedding of an infinite place.

theorem QuadraticForm.atFinitePlace_def {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] (Q : QuadraticForm K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Q.atFinitePlace v = QuadraticForm.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) Q

Finite localization is base change along the canonical map to the completion.

theorem QuadraticForm.atRealPlace_def {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : have x := invertibleOfNonzero ⋯; let x_1 := (NumberField.InfinitePlace.embedding_of_isReal ⋯).toAlgebra; Q.atRealPlace w = QuadraticForm.baseChange ℝ Q

Real localization is base change along the embedding belonging to the real place.

theorem QuadraticForm.atComplexEmbedding_def {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : NumberField.InfinitePlace K) : have x := invertibleOfNonzero ⋯; let x_1 := w.embedding.toAlgebra; Q.atComplexEmbedding w = QuadraticForm.baseChange ℂ Q

Complex localization is base change along the chosen complex embedding.

theorem QuadraticMap.Represents.atFinitePlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] {Q : QuadraticForm K V} {a : K} (h : Represents Q a) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Represents (Q.atFinitePlace v) ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) a)

A scalar represented by a global form is represented by its finite-place localization.

theorem QuadraticMap.Represents.atRealPlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {a : K} (h : Represents Q a) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : Represents (Q.atRealPlace w) ((NumberField.InfinitePlace.embedding_of_isReal ⋯) a)

A scalar represented by a global form is represented by its real-place localization.

theorem QuadraticMap.Represents.atComplexEmbedding {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {a : K} (h : Represents Q a) (w : NumberField.InfinitePlace K) : Represents (Q.atComplexEmbedding w) (w.embedding a)

A scalar represented by a global form is represented after a complex embedding.

theorem QuadraticForm.Nondegenerate.atFinitePlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : QuadraticMap.Nondegenerate

A finite-dimensional nondegenerate quadratic form stays nondegenerate at every finite place.

theorem QuadraticForm.Nondegenerate.atRealPlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Nondegenerate

A finite-dimensional nondegenerate quadratic form stays nondegenerate at every real place.

theorem QuadraticForm.Nondegenerate.atComplexEmbedding {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (w : NumberField.InfinitePlace K) : QuadraticMap.Nondegenerate

A finite-dimensional nondegenerate quadratic form stays nondegenerate after scalar extension through a complex embedding.

theorem QuadraticMap.Equivalent.atFinitePlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] {W : Type v'} [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (h : Equivalent Q R) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Equivalent (Q.atFinitePlace v) (R.atFinitePlace v)

A global isometry of quadratic forms localizes to an isometry at every finite place.

theorem QuadraticMap.Equivalent.atRealPlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type v'} [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (h : Equivalent Q R) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : Equivalent (Q.atRealPlace w) (R.atRealPlace w)

A global isometry of quadratic forms localizes to an isometry at every real place.

theorem QuadraticMap.Equivalent.atComplexEmbedding {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type v'} [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (h : Equivalent Q R) (w : NumberField.InfinitePlace K) : Equivalent (Q.atComplexEmbedding w) (R.atComplexEmbedding w)

A global isometry of quadratic forms localizes to an isometry through the complex embedding of every infinite place.

theorem QuadraticForm.formClass_atRealPlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : TauCeti.formClass (Q.atRealPlace w) ⋯ = TauCeti.RegularFormClass.baseChange ℝ (TauCeti.formClass Q hQ)

The class of the localization of a form at a real place is the scalar extension of the class of the form along the real embedding of the place.

theorem QuadraticForm.formClass_atComplexEmbedding {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (w : NumberField.InfinitePlace K) : TauCeti.formClass (Q.atComplexEmbedding w) ⋯ = TauCeti.RegularFormClass.baseChange ℂ (TauCeti.formClass Q hQ)

The class of the scalar extension of a form along the complex embedding of an infinite place is the scalar extension of the class of the form along that embedding.

noncomputable def QuadraticForm.atFinitePlaceWeightedSumSquares {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : ι → K) : QuadraticMap.IsometryEquiv (atFinitePlace (QuadraticMap.weightedSumSquares K a) v) (QuadraticMap.weightedSumSquares (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) fun (i : ι) => (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (a i))

A diagonal form localized at a finite place is canonically isometric to the diagonal form whose coefficients are mapped into the completion.

noncomputable def QuadraticForm.atRealPlaceWeightedSumSquares {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : ι → K) : QuadraticMap.IsometryEquiv (atRealPlace (QuadraticMap.weightedSumSquares K a) w) (QuadraticMap.weightedSumSquares ℝ fun (i : ι) => (NumberField.InfinitePlace.embedding_of_isReal ⋯) (a i))

A diagonal form localized at a real place is canonically isometric to the diagonal form whose coefficients are evaluated at the place's real embedding.

noncomputable def QuadraticForm.atComplexEmbeddingWeightedSumSquares {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] (w : NumberField.InfinitePlace K) (a : ι → K) : QuadraticMap.IsometryEquiv (atComplexEmbedding (QuadraticMap.weightedSumSquares K a) w) (QuadraticMap.weightedSumSquares ℂ fun (i : ι) => w.embedding (a i))

A diagonal form extended through a complex embedding is canonically isometric to the diagonal form whose coefficients are evaluated at that embedding.

@[simp]

theorem QuadraticForm.atFinitePlaceWeightedSumSquares_apply {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : ι → K) (x : v.FiniteScalarExtension) : (atFinitePlaceWeightedSumSquares v a) x = (TensorProduct.piScalarRightHom K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ι) x

The underlying linear map of the finite-place diagonal isometry is the canonical distribution of tensor product over the finite coordinate space.

@[simp]

theorem QuadraticForm.atRealPlaceWeightedSumSquares_apply {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : ι → K) (x : TauCeti.RealScalarExtension w) : let x_1 := (NumberField.InfinitePlace.embedding_of_isReal ⋯).toAlgebra; (atRealPlaceWeightedSumSquares w a) x = (TensorProduct.piScalarRightHom K ℝ ℝ ι) x

The underlying linear map of the real-place diagonal isometry is the canonical distribution of tensor product over the finite coordinate space.

@[simp]

theorem QuadraticForm.atComplexEmbeddingWeightedSumSquares_apply {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] (w : NumberField.InfinitePlace K) (a : ι → K) (x : w.ComplexScalarExtension) : let x_1 := w.embedding.toAlgebra; (atComplexEmbeddingWeightedSumSquares w a) x = (TensorProduct.piScalarRightHom K ℂ ℂ ι) x

The underlying linear map of the complex-embedding diagonal isometry is the canonical distribution of tensor product over the finite coordinate space.

@[simp]

theorem QuadraticForm.atFinitePlace_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (x : V) : (Q.atFinitePlace v) (a ⊗ₜ[K] x) = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (Q x) * a ^ 2

A finite localization evaluates on a pure tensor by applying the completion map to the coefficient of the original form.

@[simp]

theorem QuadraticForm.atRealPlace_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : ℝ) (x : V) : have x_1 := (NumberField.InfinitePlace.embedding_of_isReal ⋯).toAlgebra; (Q.atRealPlace w) (a ⊗ₜ[K] x) = (NumberField.InfinitePlace.embedding_of_isReal ⋯) (Q x) * a ^ 2

A real localization evaluates on a pure tensor by applying the real embedding to the coefficient of the original form.

@[simp]

theorem QuadraticForm.atComplexEmbedding_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : NumberField.InfinitePlace K) (a : ℂ) (x : V) : have x_1 := w.embedding.toAlgebra; (Q.atComplexEmbedding w) (a ⊗ₜ[K] x) = w.embedding (Q x) * a ^ 2

Scalar extension through a complex embedding evaluates on a pure tensor by applying the chosen embedding to the coefficient of the original form.