def Formalization.GeometricAlgebra.BilinForm.IsAnisotropicOn {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (W : Submodule k V) : Prop

A bilinear form B is anisotropic on a subspace W iff every isotropic vector in W (one with B x x = 0) is zero.

def Formalization.GeometricAlgebra.BilinForm.IsHyperbolicSubspace' {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (H : Submodule k V) : Prop

A subspace H is a hyperbolic subspace for B iff it is spanned by n mutually orthogonal hyperbolic pairs (vs i, ws i) (i.e. B (vs i) (vs i) = B (ws i) (ws i) = 0, B (vs i) (ws i) = 1, and the cross-pairings between distinct pairs vanish).

theorem Formalization.GeometricAlgebra.exists_hyperbolic_pair_of_isotropic {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k 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 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 Formalization.GeometricAlgebra.restrict_orthogonal_nondegenerate {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBnd : B.Nondegenerate) (hBrefl : B.IsRefl) (P : Submodule k 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 Formalization.GeometricAlgebra.restrict_isSymm' {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hBsymm : B.IsSymm) (W : Submodule k V) : (B.restrict W).IsSymm

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

theorem Formalization.GeometricAlgebra.restrict_bot_nondegenerate' {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : (B.restrict ⊥).Nondegenerate

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

theorem Formalization.GeometricAlgebra.orthogonal_bot' {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : B.orthogonal ⊥ = ⊤

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

theorem Formalization.GeometricAlgebra.restrict_top_anisotropic {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hB : BilinForm.IsAnisotropicOn B ⊤) : BilinForm.IsAnisotropicOn (B.restrict ⊤) ⊤

If B is anisotropic on all of V, then its restriction to ⊤ is also anisotropic on ⊤ (as a subspace of the subtype ↥⊤).

theorem Formalization.GeometricAlgebra.orthogonal_sup_map_eq' {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (P Pperp : Submodule k V) (hPperp : Pperp = B.orthogonal P) (H' : Submodule k ↥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) coincides with the lift of (B|Pperp).orthogonal H'.

theorem Formalization.GeometricAlgebra.isCompl_lift_submodule' {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (P Pperp : Submodule k V) (hCompl : IsCompl P Pperp) (H' A' : Submodule k ↥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 Formalization.GeometricAlgebra.isAnisotropic_restrict_map {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (W : Submodule k V) (A : Submodule k ↥W) (hA : BilinForm.IsAnisotropicOn ((B.restrict W).restrict A) ⊤) : BilinForm.IsAnisotropicOn (B.restrict (Submodule.map W.subtype A)) ⊤

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

theorem Formalization.GeometricAlgebra.garrett_7_2_corollary {k : Type u_1} [Field k] [Invertible 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBnd : B.Nondegenerate) (hBsymm : B.IsSymm) : ∃ (H : Submodule k V), BilinForm.IsHyperbolicSubspace' B H ∧ (B.restrict H).Nondegenerate ∧ BilinForm.IsAnisotropicOn B (B.orthogonal H)

Garrett's Chapter 7 Corollary (Witt-decomposition corollary): every finite-dimensional nondegenerate symmetric formed space decomposes as H ⊕ H⊥, where H is a hyperbolic subspace on which B restricts nondegenerately and B is anisotropic on H⊥. Proved by strong induction on Module.finrank k V.