Documentation

TauCeti.NumberTheory.QuadraticForm.Global.Operations

Operations on localized quadratic forms #

This file records how the canonical finite, real, and complex localizations of a quadratic form interact with orthogonal products, negation, and scalar multiplication.

The product comparisons are isometries because scalar extension distributes over a product only up to the canonical tensor-product equivalence. The other comparisons are equalities of forms on the same scalar-extended module. Together these results let local-global arguments transport the standard structure of a global quadratic space without unfolding the localization maps.

source
noncomputable def QuadraticForm.atFinitePlaceProd {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] [NumberField K] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
QuadraticMap.IsometryEquiv (atFinitePlace (QuadraticMap.prod Q R) place) (QuadraticMap.prod (Q.atFinitePlace place) (R.atFinitePlace place))

Finite localization carries an orthogonal product to the orthogonal product of the finite localizations.

Instances For
    source
    noncomputable def QuadraticForm.atRealPlaceProd {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : { w : NumberField.InfinitePlace K // w.IsReal }) :
    QuadraticMap.IsometryEquiv (atRealPlace (QuadraticMap.prod Q R) place) (QuadraticMap.prod (Q.atRealPlace place) (R.atRealPlace place))

    Real localization carries an orthogonal product to the orthogonal product of the real localizations.

    Instances For
      source
      noncomputable def QuadraticForm.atComplexEmbeddingProd {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : NumberField.InfinitePlace K) :
      QuadraticMap.IsometryEquiv (atComplexEmbedding (QuadraticMap.prod Q R) place) (QuadraticMap.prod (Q.atComplexEmbedding place) (R.atComplexEmbedding place))

      Complex localization carries an orthogonal product to the orthogonal product of the complex localizations.

      Instances For
        source
        @[simp]
        theorem QuadraticForm.atFinitePlaceProd_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] [NumberField K] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion K place) (x : V × W) :
        (Q.atFinitePlaceProd R place) (a ⊗ₜ[K] x) = (a ⊗ₜ[K] x.1, a ⊗ₜ[K] x.2)

        The finite-place product isometry separates the components of a pure tensor.

        source
        @[simp]
        theorem QuadraticForm.atFinitePlaceProd_symm_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] [NumberField K] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion K place) (x : V) (y : W) :
        (Q.atFinitePlaceProd R place).symm (a ⊗ₜ[K] x, a ⊗ₜ[K] y) = a ⊗ₜ[K] (x, y)

        The inverse finite-place product isometry combines pure tensors with the same scalar.

        source
        @[simp]
        theorem QuadraticForm.atRealPlaceProd_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : { w : NumberField.InfinitePlace K // w.IsReal }) (a : ℝ) (x : V × W) :
        have x_1 := (NumberField.InfinitePlace.embedding_of_isReal ⋯).toAlgebra; (Q.atRealPlaceProd R place) (a ⊗ₜ[K] x) = (a ⊗ₜ[K] x.1, a ⊗ₜ[K] x.2)

        The real-place product isometry separates the components of a pure tensor.

        source
        @[simp]
        theorem QuadraticForm.atRealPlaceProd_symm_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : { w : NumberField.InfinitePlace K // w.IsReal }) (a : ℝ) (x : V) (y : W) :
        have x_1 := (NumberField.InfinitePlace.embedding_of_isReal ⋯).toAlgebra; (Q.atRealPlaceProd R place).symm (a ⊗ₜ[K] x, a ⊗ₜ[K] y) = a ⊗ₜ[K] (x, y)

        The inverse real-place product isometry combines pure tensors with the same scalar.

        source
        @[simp]
        theorem QuadraticForm.atComplexEmbeddingProd_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : NumberField.InfinitePlace K) (a : ℂ) (x : V × W) :
        have x_1 := place.embedding.toAlgebra; (Q.atComplexEmbeddingProd R place) (a ⊗ₜ[K] x) = (a ⊗ₜ[K] x.1, a ⊗ₜ[K] x.2)

        The complex product isometry separates the components of a pure tensor.

        source
        @[simp]
        theorem QuadraticForm.atComplexEmbeddingProd_symm_tmul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] (Q : QuadraticForm K V) (R : QuadraticForm K W) (place : NumberField.InfinitePlace K) (a : ℂ) (x : V) (y : W) :
        have x_1 := place.embedding.toAlgebra; (Q.atComplexEmbeddingProd R place).symm (a ⊗ₜ[K] x, a ⊗ₜ[K] y) = a ⊗ₜ[K] (x, y)

        The inverse complex product isometry combines pure tensors with the same scalar.

        source
        @[simp]
        theorem QuadraticForm.atFinitePlace_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] (Q : QuadraticForm K V) (place : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
        (-Q).atFinitePlace place = -Q.atFinitePlace place

        Finite localization commutes with negation.

        source
        @[simp]
        theorem QuadraticForm.atRealPlace_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (place : { w : NumberField.InfinitePlace K // w.IsReal }) :
        (-Q).atRealPlace place = -Q.atRealPlace place

        Real localization commutes with negation.

        source
        @[simp]
        theorem QuadraticForm.atComplexEmbedding_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (place : NumberField.InfinitePlace K) :
        (-Q).atComplexEmbedding place = -Q.atComplexEmbedding place

        Complex localization commutes with negation.

        source
        @[simp]
        theorem QuadraticForm.atFinitePlace_smul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] (a : K) (Q : QuadraticForm K V) (place : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
        (a • Q).atFinitePlace place = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K place)) a • Q.atFinitePlace place

        Finite localization turns scaling by a global scalar into scaling by its image in the completion.

        source
        @[simp]
        theorem QuadraticForm.atRealPlace_smul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (a : K) (Q : QuadraticForm K V) (place : { w : NumberField.InfinitePlace K // w.IsReal }) :
        (a • Q).atRealPlace place = (NumberField.InfinitePlace.embedding_of_isReal ⋯) a • Q.atRealPlace place

        Real localization turns scaling by a global scalar into scaling by its value at the real place.

        source
        @[simp]
        theorem QuadraticForm.atComplexEmbedding_smul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (a : K) (Q : QuadraticForm K V) (place : NumberField.InfinitePlace K) :
        (a • Q).atComplexEmbedding place = place.embedding a • Q.atComplexEmbedding place

        Complex localization turns scaling by a global scalar into scaling by its value at the chosen embedding.