The signature is additive over an orthogonal decomposition

Mathlib at the pin has Sylvester's law of inertia — sigPos, sigNeg, and sigPos_add_sigNeg_add_radical — but not the additivity of the signature over an orthogonal direct sum. This file supplies it for a nondegenerate orthogonal decomposition of a finite-dimensional real quadratic space.

It is what turns a signature hypothesis on a summand into one on the whole space: the Mukai extension is a hyperbolic plane orthogonal to V, so the (2, n - 2) signature the period domain assumes should follow from the (1, n - 1) signature of V rather than being asserted.

The proof, which is a squeeze rather than a construction

Only the easy direction is proved directly, twice:

• a positive definite subspace of W and one of W' span a positive definite subspace of M, because the cross terms vanish — so sigPos (Q|W) + sigPos (Q|W') ≤ sigPos Q;
• the same for -Q, which is sigNeg.

Then sigPos_add_sigNeg_add_radical on all three spaces, with the radicals trivial, gives

finrank M = sigPos Q + sigNeg Q ≥ (sigPos₁ + sigPos₂) + (sigNeg₁ + sigNeg₂)
          = finrank W + finrank W' = finrank M,

so both inequalities are equalities. The hard direction — bounding an arbitrary positive definite subspace of M — is never needed.

Scope

The restrictions are assumed nondegenerate, which is the case the application has and which keeps the counting to two terms. The degenerate version follows the same squeeze with the radical as a third term and a third inequality finrank (radical Q|W) + finrank (radical Q|W') ≤ finrank (radical Q); it is not proved here because nothing needs it.

theorem QuadraticMap.sigPos_add_le {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} {W W' : Submodule ℝ M} (hcompl : IsCompl W W') (horth : ∀ w ∈ W, ∀ w' ∈ W', polar (⇑Q) w w' = 0) : sigPos (restrict Q W) + sigPos (restrict Q W') ≤ sigPos Q

The easy half of additivity for sigPos.

theorem QuadraticMap.sigNeg_add_le {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} {W W' : Submodule ℝ M} (hcompl : IsCompl W W') (horth : ∀ w ∈ W, ∀ w' ∈ W', polar (⇑Q) w w' = 0) : sigNeg (restrict Q W) + sigNeg (restrict Q W') ≤ sigNeg Q

The easy half of additivity for sigNeg, which is sigPos of -Q.

theorem QuadraticMap.nondegenerate_of_isCompl {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {W W' : Submodule ℝ M} (hcompl : IsCompl W W') (horth : ∀ w ∈ W, ∀ w' ∈ W', polar (⇑Q) w w' = 0) (h₁ : Nondegenerate) (h₂ : Nondegenerate) : Nondegenerate

An orthogonal decomposition into nondegenerate pieces is nondegenerate.

theorem QuadraticMap.sigPos_eq_add {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} {W W' : Submodule ℝ M} (hcompl : IsCompl W W') (horth : ∀ w ∈ W, ∀ w' ∈ W', polar (⇑Q) w w' = 0) (h₁ : Nondegenerate) (h₂ : Nondegenerate) : sigPos Q = sigPos (restrict Q W) + sigPos (restrict Q W') ∧ sigNeg Q = sigNeg (restrict Q W) + sigNeg (restrict Q W')

The signature is additive over a nondegenerate orthogonal decomposition.

Definite forms and their indices of inertia

Sylvester's law pins the two indices for a definite form. Mathlib has the defining maximality property of sigPos and the counting identity, but not the two corollaries every consumer wants, so they are proved here beside the additivity they are used with.

theorem QuadraticMap.nondegenerate_of_anisotropic {N : Type u_2} [AddCommGroup N] [Module ℝ N] {Q : QuadraticForm ℝ N} (h : Anisotropic Q) : Nondegenerate

An anisotropic form is nondegenerate: the radical sits inside the zero locus.

theorem QuadraticMap.sigPos_eq_finrank_of_posDef {N : Type u_2} [AddCommGroup N] [Module ℝ N] [FiniteDimensional ℝ N] {Q : QuadraticForm ℝ N} (h : PosDef Q) : sigPos Q = Module.finrank ℝ N ∧ sigNeg Q = 0 ∧ Nondegenerate

A positive definite form has sigPos = dim and sigNeg = 0.

theorem QuadraticMap.sigNeg_eq_finrank_of_negDef {N : Type u_2} [AddCommGroup N] [Module ℝ N] [FiniteDimensional ℝ N] {Q : QuadraticForm ℝ N} (h : PosDef (-Q)) : sigNeg Q = Module.finrank ℝ N ∧ sigPos Q = 0 ∧ Nondegenerate

A negative definite form has sigNeg = dim and sigPos = 0.

"Negative definite" is spelled the way sigNeg is defined, as positive definiteness of -Q.

theorem QuadraticMap.negDef_of_sigNeg_eq_finrank {N : Type u_2} [AddCommGroup N] [Module ℝ N] [FiniteDimensional ℝ N] {Q : QuadraticForm ℝ N} (h : sigNeg Q = Module.finrank ℝ N) : PosDef (-Q)

A form of full negative index is negative definite. The converse of sigNeg_eq_finrank_of_negDef: a negative definite subspace of full dimension is the whole space.

Restricting a nondegenerate form to an orthogonal summand

theorem QuadraticMap.nondegenerate_restrict_of_isCompl {M : Type u_2} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {W W' : Submodule ℝ M} (hcompl : IsCompl W W') (horth : ∀ w ∈ W, ∀ w' ∈ W', polar (⇑Q) w w' = 0) (hnd : Nondegenerate) : Nondegenerate

A summand of a nondegenerate orthogonal decomposition is nondegenerate.

This is the converse direction of nondegenerate_of_isCompl: a class of the radical of one summand is orthogonal to that summand by definition and to the other by hypothesis, hence to everything.