Signatures of quadratic forms at real places

This file packages the positive and negative indices of the localization of a quadratic form at a real place. The projections are the real-place invariants used in the local-global theory of quadratic forms over number fields.

The signature is invariant under equivalence, additive under orthogonal products, exchanges its components under negation or negative scaling, and is unchanged by positive scaling. For a nondegenerate form, the two indices add to the global rank.

Sylvester's law of inertia turns that invariant into a complete one: at a real place regular forms are isometric exactly when their signatures agree, so at a fixed global rank the positive index alone separates them, and the localization is isometric to the normal form QuadraticForm.realSignatureForm p q exactly when (p, q) is its signature. This is the real half of the archimedean classification; the complex half is in TauCeti.NumberTheory.QuadraticForm.Global.ComplexPlaces.

Main definitions

• QuadraticForm.realSignature: the positive and negative indices at a real place.
• QuadraticForm.realPositiveIndex: the positive component of the real signature.
• QuadraticForm.realNegativeIndex: the negative component of the real signature.

Main results

• QuadraticForm.realPositiveIndex_add_realNegativeIndex_eq_finrank: the indices of a nondegenerate form add to its rank.
• QuadraticForm.realPositiveIndex_weightedSumSquares, QuadraticForm.realNegativeIndex_weightedSumSquares: the indices of a diagonal form count its coefficients that are positive, respectively negative, at the place.
• QuadraticMap.Equivalent.realSignature_eq: equivalent forms have equal real signatures.
• QuadraticForm.realSignature_prod: real-place signatures are additive under orthogonal products.
• QuadraticForm.equivalent_atRealPlace_iff_realSignature_eq: at a real place regular forms are classified by their signature.
• QuadraticForm.equivalent_atRealPlace_iff_realPositiveIndex_eq_of_finrank_eq: at a fixed global rank the positive index alone classifies them.
• QuadraticForm.equivalent_atRealPlace_realSignatureForm_iff_realSignature_eq and QuadraticForm.equivalent_atRealPlace_realSignatureForm: the localization is the normal form p⟨1⟩ ⊥ q⟨-1⟩ exactly when (p, q) is its signature, hence is always the normal form of its own signature.
• QuadraticForm.anisotropic_atRealPlace_iff_realNegativeIndex_eq_zero_or_realPositiveIndex_eq_zero says that a regular form is anisotropic at a real place exactly when it is definite there.
• QuadraticForm.anisotropic_atRealPlace_weightedSumSquares_iff: a diagonal form is anisotropic at a real place exactly when its coefficients there all have the same sign.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), §61 for the archimedean classification.

noncomputable def QuadraticForm.realSignature {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : ℕ × ℕ

The pair consisting of the positive and negative indices of a quadratic form at a real place.

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

The positive index of a quadratic form at a real place.

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

The negative index of a quadratic form at a real place.

@[simp]

theorem QuadraticForm.realSignature_fst {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (Q.realSignature w).1 = Q.realPositiveIndex w

The first component of the real signature is the positive index.

@[simp]

theorem QuadraticForm.realSignature_snd {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (Q.realSignature w).2 = Q.realNegativeIndex w

The second component of the real signature is the negative index.

@[simp]

theorem QuadraticForm.realSignature_eq_iff {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) (p q : ℕ) : Q.realSignature w = (p, q) ↔ Q.realPositiveIndex w = p ∧ Q.realNegativeIndex w = q

The real signature is a prescribed pair exactly when the two indices are its components.

theorem QuadraticForm.realPositiveIndex_eq_sigPos {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : Q.realPositiveIndex w = sigPos (Q.atRealPlace w)

The positive index at a real place is Mathlib's positive index of the localized form.

theorem QuadraticForm.realNegativeIndex_eq_sigNeg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : Q.realNegativeIndex w = sigNeg (Q.atRealPlace w)

The negative index at a real place is Mathlib's negative index of the localized form.

theorem QuadraticForm.realPositiveIndex_add_realNegativeIndex_eq_finrank {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : Q.realPositiveIndex w + Q.realNegativeIndex w = Module.finrank K V

The positive and negative indices of a nondegenerate form at a real place add to its global rank.

theorem QuadraticForm.realPositiveIndex_weightedSumSquares {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] (a : ι → K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : realPositiveIndex (QuadraticMap.weightedSumSquares K a) w = {i : ι | 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) (a i)}.ncard

The positive index of a diagonal form ⟨a₁, …, aₙ⟩ at a real place w is the number of coefficients that are positive under the real embedding of w.

theorem QuadraticForm.realNegativeIndex_weightedSumSquares {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] (a : ι → K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : realNegativeIndex (QuadraticMap.weightedSumSquares K a) w = {i : ι | (NumberField.InfinitePlace.embedding_of_isReal ⋯) (a i) < 0}.ncard

The negative index of a diagonal form ⟨a₁, …, aₙ⟩ at a real place w is the number of coefficients that are negative under the real embedding of w.

theorem QuadraticMap.Equivalent.realSignature_eq {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 }) : Q.realSignature w = R.realSignature w

Equivalent quadratic forms have the same signature at every real place.

theorem QuadraticMap.Equivalent.realPositiveIndex_eq {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 }) : Q.realPositiveIndex w = R.realPositiveIndex w

Equivalent quadratic forms have the same positive index at every real place.

theorem QuadraticMap.Equivalent.realNegativeIndex_eq {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 }) : Q.realNegativeIndex w = R.realNegativeIndex w

Equivalent quadratic forms have the same negative index at every real place.

@[simp]

theorem QuadraticForm.realPositiveIndex_prod {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) (w : { w : NumberField.InfinitePlace K // w.IsReal }) [FiniteDimensional ℝ (TauCeti.RealScalarExtension w)] [FiniteDimensional ℝ (TauCeti.RealScalarExtension w)] : realPositiveIndex (QuadraticMap.prod Q R) w = Q.realPositiveIndex w + R.realPositiveIndex w

The positive index at a real place is additive under orthogonal products.

@[simp]

theorem QuadraticForm.realNegativeIndex_prod {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) (w : { w : NumberField.InfinitePlace K // w.IsReal }) [FiniteDimensional ℝ (TauCeti.RealScalarExtension w)] [FiniteDimensional ℝ (TauCeti.RealScalarExtension w)] : realNegativeIndex (QuadraticMap.prod Q R) w = Q.realNegativeIndex w + R.realNegativeIndex w

The negative index at a real place is additive under orthogonal products.

@[simp]

theorem QuadraticForm.realSignature_prod {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) (w : { w : NumberField.InfinitePlace K // w.IsReal }) [FiniteDimensional ℝ (TauCeti.RealScalarExtension w)] [FiniteDimensional ℝ (TauCeti.RealScalarExtension w)] : realSignature (QuadraticMap.prod Q R) w = (Q.realPositiveIndex w + R.realPositiveIndex w, Q.realNegativeIndex w + R.realNegativeIndex w)

The real signature of an orthogonal product is the componentwise sum of the signatures.

@[simp]

theorem QuadraticForm.realPositiveIndex_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (-Q).realPositiveIndex w = Q.realNegativeIndex w

Negation exchanges the positive and negative indices at a real place.

@[simp]

theorem QuadraticForm.realNegativeIndex_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (-Q).realNegativeIndex w = Q.realPositiveIndex w

Negation exchanges the negative and positive indices at a real place.

@[simp]

theorem QuadraticForm.realSignature_neg {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : (-Q).realSignature w = (Q.realNegativeIndex w, Q.realPositiveIndex w)

Negation exchanges the two components of the real signature.

@[simp]

theorem QuadraticForm.realPositiveIndex_smul_of_pos {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 : K) (ha : 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) a) : (a • Q).realPositiveIndex w = Q.realPositiveIndex w

Scaling by a scalar positive at a real place preserves its positive index.

@[simp]

theorem QuadraticForm.realNegativeIndex_smul_of_pos {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 : K) (ha : 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) a) : (a • Q).realNegativeIndex w = Q.realNegativeIndex w

Scaling by a scalar positive at a real place preserves its negative index.

@[simp]

theorem QuadraticForm.realSignature_smul_of_pos {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 : K) (ha : 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) a) : (a • Q).realSignature w = Q.realSignature w

Scaling by a scalar positive at a real place preserves its signature.

@[simp]

theorem QuadraticForm.realPositiveIndex_smul_of_neg {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 : K) (ha : (NumberField.InfinitePlace.embedding_of_isReal ⋯) a < 0) : (a • Q).realPositiveIndex w = Q.realNegativeIndex w

Scaling by a scalar negative at a real place exchanges the positive and negative indices.

@[simp]

theorem QuadraticForm.realNegativeIndex_smul_of_neg {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 : K) (ha : (NumberField.InfinitePlace.embedding_of_isReal ⋯) a < 0) : (a • Q).realNegativeIndex w = Q.realPositiveIndex w

Scaling by a scalar negative at a real place exchanges the negative and positive indices.

@[simp]

theorem QuadraticForm.realSignature_smul_of_neg {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 : K) (ha : (NumberField.InfinitePlace.embedding_of_isReal ⋯) a < 0) : (a • Q).realSignature w = (Q.realNegativeIndex w, Q.realPositiveIndex w)

Scaling by a scalar negative at a real place exchanges the signature components.

@[simp]

theorem QuadraticForm.equivalent_atRealPlace_iff_realSignature_eq {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} [FiniteDimensional K V] [FiniteDimensional K W] (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Equivalent (Q.atRealPlace w) (R.atRealPlace w) ↔ Q.realSignature w = R.realSignature w

Sylvester's law of inertia at a real place. Two regular quadratic forms become isometric at a real place exactly when their signatures there agree.

theorem QuadraticForm.equivalent_atRealPlace_iff_realPositiveIndex_eq_of_finrank_eq {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} [FiniteDimensional K V] [FiniteDimensional K W] (hQ : QuadraticMap.Nondegenerate) (hR : QuadraticMap.Nondegenerate) (hrank : Module.finrank K V = Module.finrank K W) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Equivalent (Q.atRealPlace w) (R.atRealPlace w) ↔ Q.realPositiveIndex w = R.realPositiveIndex w

At a real place the positive index is already a complete invariant of regular forms of equal global rank, because the negative index is the rank minus the positive index.

@[simp]

theorem QuadraticForm.equivalent_atRealPlace_realSignatureForm_iff_realSignature_eq {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [FiniteDimensional K V] (hQ : QuadraticMap.Nondegenerate) (w : { w : NumberField.InfinitePlace K // w.IsReal }) (p q : ℕ) : QuadraticMap.Equivalent (Q.atRealPlace w) (realSignatureForm p q) ↔ Q.realSignature w = (p, q)

A regular quadratic form is isometric at a real place to the normal form p⟨1⟩ ⊥ q⟨-1⟩ exactly when (p, q) is its signature there.

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

A regular quadratic form is isometric at a real place to the normal form of its signature there.

theorem QuadraticForm.anisotropic_atRealPlace_iff_realNegativeIndex_eq_zero_or_realPositiveIndex_eq_zero {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [FiniteDimensional K V] (hQ : QuadraticMap.Nondegenerate) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Anisotropic (Q.atRealPlace w) ↔ Q.realNegativeIndex w = 0 ∨ Q.realPositiveIndex w = 0

A regular quadratic form is anisotropic at a real place exactly when it is definite there, that is, when its negative or its positive index there vanishes.

theorem QuadraticForm.anisotropic_atRealPlace_weightedSumSquares_iff {K : Type u} [Field K] {ι : Type u_1} [Fintype ι] (a : ι → K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Anisotropic (atRealPlace (QuadraticMap.weightedSumSquares K a) w) ↔ (∀ (i : ι), 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) (a i)) ∨ ∀ (i : ι), (NumberField.InfinitePlace.embedding_of_isReal ⋯) (a i) < 0

A diagonal form ⟨a₁, …, aₙ⟩ is anisotropic at a real place exactly when its coefficients there are all positive or all negative.