def Garrett.BilinForm.IsAnisotropic {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) : Prop

A bilinear form B is anisotropic when every isotropic vector (one with B x x = 0) is zero.

def Garrett.BilinForm.IsHyperbolicSubspace {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) (H : Submodule F V) : Prop

A subspace H is hyperbolic for B iff it is spanned by n mutually orthogonal hyperbolic pairs (vs i, ws i) with B (vs i) (ws i) = 1 and all self-pairings and cross-pairings between distinct pairs vanishing.

theorem Garrett.exists_hyperbolic_pair_of_isotropic {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] [Invertible 2] (B : LinearMap.BilinForm F V) (hBnd : B.Nondegenerate) (hBsymm : B.IsSymm) (v : V) (hv : v ≠ 0) (hiso : (B v) v = 0) : ∃ (w : V), (B v) w = 1 ∧ (B w) w = 0 ∧ (B w) v = 1

Given a nondegenerate symmetric form (with 2 invertible) and a nonzero isotropic vector v, there exists w forming a hyperbolic pair with v: B v w = B w v = 1 and B w w = 0.

theorem Garrett.restrict_orthogonal_nondegenerate {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (B : LinearMap.BilinForm F V) (hBnd : B.Nondegenerate) (hBrefl : B.IsRefl) (P : Submodule F V) (hP : (B.restrict P).Nondegenerate) : (B.restrict (B.orthogonal P)).Nondegenerate

If a reflexive nondegenerate form B restricts nondegenerately to a subspace P, then it also restricts nondegenerately to the orthogonal complement of P.

theorem Garrett.restrict_isSymm {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) (hBsymm : B.IsSymm) (W : Submodule F V) : (B.restrict W).IsSymm

Restriction of a symmetric bilinear form to a subspace remains symmetric.

theorem Garrett.restrict_bot_nondegenerate {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) : (B.restrict ⊥).Nondegenerate

The restriction of any bilinear form to ⊥ is vacuously nondegenerate.

theorem Garrett.orthogonal_bot {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) : B.orthogonal ⊥ = ⊤

The orthogonal complement of the trivial subspace ⊥ is the whole space ⊤.

theorem Garrett.restrict_top_anisotropic {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) (hB : BilinForm.IsAnisotropic B) : BilinForm.IsAnisotropic (B.restrict ⊤)

If B is anisotropic on all of V, then its restriction to ⊤ is also anisotropic.

theorem Garrett.orthogonal_sup_map_eq {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) (P Pperp : Submodule F V) (hPperp : Pperp = B.orthogonal P) (H' : Submodule F ↥Pperp) : B.orthogonal (P ⊔ Submodule.map Pperp.subtype H') = Submodule.map Pperp.subtype ((B.restrict Pperp).orthogonal H')

Compatibility of orthogonal complements with the lift Pperp.subtype: the orthogonal of P ⊔ (H' lifted to V) equals the lift of (B|Pperp).orthogonal H'.

theorem Garrett.isCompl_lift_submodule {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (P Pperp : Submodule F V) (hCompl : IsCompl P Pperp) (H' A' : Submodule F ↥Pperp) (hHA : IsCompl H' A') : IsCompl (P ⊔ Submodule.map Pperp.subtype H') (Submodule.map Pperp.subtype A')

Lifting complements through a complement: if P ⊕ Pperp = V and H' ⊕ A' = Pperp, then (P ⊔ H'.map Pperp.subtype) ⊕ (A'.map Pperp.subtype) = V.

theorem Garrett.isAnisotropic_restrict_map {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (B : LinearMap.BilinForm F V) (W : Submodule F V) (A : Submodule F ↥W) (hA : BilinForm.IsAnisotropic ((B.restrict W).restrict A)) : BilinForm.IsAnisotropic (B.restrict (Submodule.map W.subtype A))

Anisotropy transfers through the lift W.subtype: if (B|W)|A is anisotropic, then B restricted to the lifted subspace A.map W.subtype is anisotropic.

theorem Garrett.garrett_7_2_corollary {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] [FiniteDimensional F V] [Invertible 2] (B : LinearMap.BilinForm F V) (hBnd : B.Nondegenerate) (hBsymm : B.IsSymm) : ∃ (H : Submodule F V) (A : Submodule F V), BilinForm.IsHyperbolicSubspace B H ∧ BilinForm.IsAnisotropic (B.restrict A) ∧ IsCompl H A ∧ A = B.orthogonal H

Garrett's Chapter 7 Corollary: every finite-dimensional nondegenerate symmetric formed space decomposes as H ⊕ A where H is hyperbolic, A = H⊥, and the restriction of B to A is anisotropic. Proved by strong induction on Module.finrank F V.