Documentation

TauCeti.NumberTheory.QuadraticForm.Global.Predicates

Local properties of quadratic forms over number fields #

This file defines isotropy, representation, scalar representation, and equivalence at every finite and real place of a number field. The predicates always use the canonical scalar extensions of the global forms, so their witnesses compare actual localizations rather than an independently chosen family of local quadratic spaces.

Global witnesses base-change to local witnesses. The resulting API also records invariance under global equivalence and the rank constraint imposed by local equivalence. These are the common hypotheses used in local-to-global statements for quadratic forms.

Complex places do not occur in the definitions: over ℂ, isotropy is automatic in dimension at least two, representation of regular forms is controlled only by dimension, and regular forms of equal dimension are equivalent. TauCeti.NumberTheory.QuadraticForm.Global.ComplexPlaces makes this omission explicit.

If a form locally represents a scalar a, adjoining ⟨-a⟩ makes it locally isotropic.

source
def QuadraticForm.IsLocallyIsotropic {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) :
Prop

A quadratic form over a number field is locally isotropic if it is isotropic at every finite and real place.

Instances For
    source
    @[simp]
    theorem QuadraticForm.isLocallyIsotropic_iff {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) :
    Q.IsLocallyIsotropic ↔ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ¬QuadraticMap.Anisotropic (Q.atFinitePlace v)) ∧ ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), ¬QuadraticMap.Anisotropic (Q.atRealPlace w)

    Local isotropy is the conjunction of its finite-place and real-place clauses.

    source
    def QuadraticForm.LocallyRepresents {K : Type u} [Field K] [NumberField 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) :
    Prop

    Local representation of one quadratic form by another: Q.LocallyRepresents R holds when every finite and real localization of Q admits an injective isometry into the corresponding localization of R.

    Instances For
      source
      @[simp]
      theorem QuadraticForm.locallyRepresents_iff {K : Type u} [Field K] [NumberField 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) :
      Q.LocallyRepresents R ↔ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.IsRepresentedBy (Q.atFinitePlace v) (R.atFinitePlace v)) ∧ ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), QuadraticMap.IsRepresentedBy (Q.atRealPlace w) (R.atRealPlace w)

      Local representation is the conjunction of its finite-place and real-place clauses.

      source
      def QuadraticForm.LocallyRepresentsScalar {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (a : K) :
      Prop

      A quadratic form locally represents a scalar if each finite and real localization represents the image of that scalar.

      Instances For
        source
        @[simp]
        theorem QuadraticForm.locallyRepresentsScalar_iff {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (a : K) :
        Q.LocallyRepresentsScalar a ↔ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Represents (Q.atFinitePlace v) ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) a)) ∧ ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), QuadraticMap.Represents (Q.atRealPlace w) ((NumberField.InfinitePlace.embedding_of_isReal ⋯) a)

        Local scalar representation is the conjunction of its finite-place and real-place clauses.

        source
        theorem QuadraticForm.LocallyRepresentsScalar.isLocallyIsotropic_smul_sq_prod {K : Type u} [Field K] [NumberField K] {W : Type w} [AddCommGroup W] [Module K W] {W✝ : QuadraticForm K W} {a : K} (h : W✝.LocallyRepresentsScalar a) :
        IsLocallyIsotropic ((-a • QuadraticMap.sq).prod W✝)

        If a quadratic form represents a scalar at every finite and real place, then its orthogonal sum with the corresponding one-dimensional negative form is locally isotropic.

        source
        def QuadraticForm.LocallyEquivalent {K : Type u} [Field K] [NumberField 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) :
        Prop

        Two quadratic forms over a number field are locally equivalent if their localizations are equivalent at every finite and real place.

        Instances For
          source
          @[simp]
          theorem QuadraticForm.locallyEquivalent_iff {K : Type u} [Field K] [NumberField 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) :
          Q.LocallyEquivalent R ↔ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), QuadraticMap.Equivalent (Q.atFinitePlace v) (R.atFinitePlace v)) ∧ ∀ (w : { w : NumberField.InfinitePlace K // w.IsReal }), QuadraticMap.Equivalent (Q.atRealPlace w) (R.atRealPlace w)

          Local equivalence is the conjunction of its finite-place and real-place clauses.

          source
          theorem QuadraticForm.isLocallyIsotropic_of_not_anisotropic {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hQ : ¬QuadraticMap.Anisotropic Q) :
          Q.IsLocallyIsotropic

          A globally isotropic quadratic form is locally isotropic.

          source
          theorem QuadraticForm.LocallyRepresents.of_isRepresentedBy {K : Type u} [Field K] [NumberField 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} (h : QuadraticMap.IsRepresentedBy Q R) :
          Q.LocallyRepresents R

          A global representation of one quadratic form by another induces a representation at every finite and real place.

          source
          theorem QuadraticForm.LocallyRepresentsScalar.of_represents {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {a : K} (h : QuadraticMap.Represents Q a) :
          Q.LocallyRepresentsScalar a

          A globally represented scalar is represented at every finite and real place.

          source
          theorem QuadraticForm.LocallyEquivalent.of_equivalent {K : Type u} [Field K] [NumberField 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} (h : QuadraticMap.Equivalent Q R) :
          Q.LocallyEquivalent R

          Globally equivalent quadratic forms are locally equivalent.

          source
          theorem QuadraticForm.LocallyEquivalent.refl {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) :
          Q.LocallyEquivalent Q

          Local equivalence is reflexive.

          source
          theorem QuadraticForm.LocallyEquivalent.symm {K : Type u} [Field K] [NumberField 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} (h : Q.LocallyEquivalent R) :
          R.LocallyEquivalent Q

          Local equivalence is symmetric.

          source
          theorem QuadraticForm.LocallyEquivalent.trans {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] {X : Type u_1} [AddCommGroup X] [Module K X] {Q : QuadraticForm K V} {R : QuadraticForm K W} {S : QuadraticForm K X} (hQR : Q.LocallyEquivalent R) (hRS : R.LocallyEquivalent S) :
          Q.LocallyEquivalent S

          Local equivalence is transitive.

          source
          theorem QuadraticForm.LocallyRepresents.refl {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) :
          Q.LocallyRepresents Q

          Local representation is reflexive.

          source
          theorem QuadraticForm.LocallyRepresents.trans {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] {X : Type u_1} [AddCommGroup X] [Module K X] {Q : QuadraticForm K V} {R : QuadraticForm K W} {S : QuadraticForm K X} (hQR : Q.LocallyRepresents R) (hRS : R.LocallyRepresents S) :
          Q.LocallyRepresents S

          Local representation is transitive.

          source
          theorem QuadraticForm.LocallyEquivalent.locallyRepresents {K : Type u} [Field K] [NumberField 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} (h : Q.LocallyEquivalent R) :
          Q.LocallyRepresents R

          Local equivalence implies local representation.

          source
          theorem QuadraticForm.LocallyRepresents.isLocallyIsotropic {K : Type u} [Field K] [NumberField 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} (hQR : Q.LocallyRepresents R) (hQ : Q.IsLocallyIsotropic) :
          R.IsLocallyIsotropic

          Local representation carries local isotropy from the represented form to the ambient form.

          source
          theorem QuadraticForm.LocallyRepresents.locallyRepresentsScalar {K : Type u} [Field K] [NumberField 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} (hQR : Q.LocallyRepresents R) {a : K} (hQa : Q.LocallyRepresentsScalar a) :
          R.LocallyRepresentsScalar a

          Local representation carries represented scalars from the represented form to the ambient form.

          source
          theorem QuadraticForm.LocallyEquivalent.isLocallyIsotropic_iff {K : Type u} [Field K] [NumberField 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} (h : Q.LocallyEquivalent R) :
          Q.IsLocallyIsotropic ↔ R.IsLocallyIsotropic

          Locally equivalent forms are locally isotropic simultaneously.

          source
          theorem QuadraticForm.LocallyEquivalent.locallyRepresentsScalar_iff {K : Type u} [Field K] [NumberField 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} (h : Q.LocallyEquivalent R) (a : K) :
          Q.LocallyRepresentsScalar a ↔ R.LocallyRepresentsScalar a

          Locally equivalent forms locally represent the same scalars.

          source
          theorem QuadraticForm.QuadraticMap.Equivalent.isLocallyIsotropic_iff {K : Type u} [Field K] [NumberField 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} (h : QuadraticMap.Equivalent Q R) :
          Q.IsLocallyIsotropic ↔ R.IsLocallyIsotropic

          Global equivalence preserves local isotropy.

          source
          theorem QuadraticForm.QuadraticMap.Equivalent.locallyRepresentsScalar_iff {K : Type u} [Field K] [NumberField 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} (h : QuadraticMap.Equivalent Q R) (a : K) :
          Q.LocallyRepresentsScalar a ↔ R.LocallyRepresentsScalar a

          Global equivalence preserves local scalar representation.

          source
          theorem QuadraticForm.QuadraticMap.Equivalent.locallyRepresents_congr {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] {V' : Type u_1} {W' : Type u_2} [AddCommGroup V'] [Module K V'] [AddCommGroup W'] [Module K W'] {Q : QuadraticForm K V} {Q' : QuadraticForm K V'} {R : QuadraticForm K W} {R' : QuadraticForm K W'} (hQ : QuadraticMap.Equivalent Q Q') (hR : QuadraticMap.Equivalent R R') :
          Q.LocallyRepresents R ↔ Q'.LocallyRepresents R'

          Replacing both global forms by equivalent forms preserves local representation.

          source
          theorem QuadraticForm.LocallyEquivalent.finrank_eq {K : Type u} [Field K] [NumberField 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} (h : Q.LocallyEquivalent R) :
          Module.finrank K V = Module.finrank K W

          Locally equivalent quadratic forms have the same global rank.

          source
          theorem QuadraticForm.LocallyRepresents.finrank_le {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (h : Q.LocallyRepresents R) :
          Module.finrank K V ≤ Module.finrank K W

          Local representation of a form by a form on a finite-dimensional space forces the expected inequality between their global dimensions.