Complex places in local-to-global statements for quadratic forms

The local predicates QuadraticForm.IsLocallyIsotropic, QuadraticForm.LocallyRepresentsScalar, QuadraticForm.LocallyRepresents, and QuadraticForm.LocallyEquivalent only quantify over the finite and real places of a number field. This file proves that each of them already implies the corresponding statement after scalar extension along the complex embedding of every infinite place; for LocallyRepresents and LocallyEquivalent, the forms are finite-dimensional and nondegenerate. Consequently, adjoining complex clauses under these hypotheses changes none of the local-to-global statements formulated with them.

The complex clause is supplied by the classification of quadratic forms over an algebraically closed field: rank at least two forces isotropy, a nonzero form represents every scalar, and regular forms are represented or classified by their dimension alone. The finite-place clauses supply the missing input in the degenerate cases. A form on a space of dimension at most one that is isotropic at one finite place is already isotropic over the number field, and a scalar represented at one finite place is either zero or represented by a nonzero form. Representation is stated for regular forms, where dimension is the only complex invariant.

The complex half of the archimedean classification is therefore stated here as well: through a complex embedding a regular form is classified by its rank alone, and it is isometric to the standard sum of squares on Fin n exactly when its rank is n. The predicate results below are consequences. The real half, which needs the real-signature theory, lives in TauCeti.NumberTheory.QuadraticForm.Global.Signature.

Main results

• QuadraticForm.equivalent_atComplexEmbedding_iff_finrank_eq: through a complex embedding regular forms are classified by their rank.
• QuadraticForm.equivalent_atComplexEmbedding_weightedSumSquares_one_iff_finrank_eq: the localization is the standard sum of squares on Fin n exactly when the rank is n.
• QuadraticForm.IsLocallyIsotropic.not_anisotropic_atComplexEmbedding
• QuadraticForm.LocallyRepresentsScalar.represents_atComplexEmbedding
• QuadraticForm.LocallyRepresents.isRepresentedBy_atComplexEmbedding
• QuadraticForm.LocallyEquivalent.equivalent_atComplexEmbedding

@[simp]

theorem QuadraticForm.equivalent_atComplexEmbedding_iff_finrank_eq {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K V] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) (w : NumberField.InfinitePlace K) : QuadraticMap.Equivalent (Q.atComplexEmbedding w) (R.atComplexEmbedding w) ↔ Module.finrank K V = Module.finrank K W

Through a complex embedding regular quadratic forms are classified by their rank alone.

@[simp]

theorem QuadraticForm.equivalent_atComplexEmbedding_weightedSumSquares_one_iff_finrank_eq {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) (n : ℕ) : QuadraticMap.Equivalent (Q.atComplexEmbedding w) (QuadraticMap.weightedSumSquares ℂ 1) ↔ Module.finrank K V = n

Through a complex embedding a regular quadratic form is isometric to the standard sum of squares on Fin n exactly when its global rank is n.

theorem QuadraticForm.IsLocallyIsotropic.not_anisotropic_atComplexEmbedding {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (h : Q.IsLocallyIsotropic) (w : NumberField.InfinitePlace K) : ¬QuadraticMap.Anisotropic (Q.atComplexEmbedding w)

A locally isotropic quadratic form, on a possibly infinite-dimensional space, is isotropic after scalar extension along the complex embedding of every infinite place.

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

A scalar that a quadratic form represents locally is represented after scalar extension along the complex embedding of every infinite place.

theorem QuadraticForm.LocallyRepresents.isRepresentedBy_atComplexEmbedding {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 V] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) (h : Q.LocallyRepresents R) (w : NumberField.InfinitePlace K) : QuadraticMap.IsRepresentedBy (Q.atComplexEmbedding w) (R.atComplexEmbedding w)

If one regular quadratic form is locally represented by another, then it is represented by the other after scalar extension along the complex embedding of every infinite place.

theorem QuadraticForm.LocallyEquivalent.equivalent_atComplexEmbedding {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 V] [FiniteDimensional K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) (h : Q.LocallyEquivalent R) (w : NumberField.InfinitePlace K) : QuadraticMap.Equivalent (Q.atComplexEmbedding w) (R.atComplexEmbedding w)

Locally equivalent regular quadratic forms are equivalent after scalar extension along the complex embedding of every infinite place.