Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Invertible Hermitian Inertia Pullback

Abstract

Invertible square Hermitian congruence preserves the full finite inertia pair.

Theorem 1.1 (Invertible congruence preserves positive and negative index).

Lean statement: D5/S3/Weil/Pick/InvertibleHermitianInertiaPullback.inertia_invariant_of_isUnit_det

Proof. Machine-checked in Lean as D5/S3/Weil/Pick/InvertibleHermitianInertiaPullback.inertia_invariant_of_isUnit_det (✓ std3). ∎

Source. Repository-derived.

Commentary.

Positive-index pullback monotonicity is applied in both directions through the nonsingular inverse; matrix negation transports the same argument to negative index. The theorem is finite-dimensional and assumes only an invertible square feature matrix.

References