def Garrett.IsTotallyIsotropic {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (U : Submodule k V) : Prop

A submodule U is totally isotropic for B when B vanishes on all pairs of elements of U.

def Garrett.IsSubspaceIsometry {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (U W : Submodule k V) (φ : ↥U ≃ₗ[k] ↥W) : Prop

A linear isomorphism φ : U ≃ₗ W between two submodules is a subspace isometry for B when it preserves the values of B.

def Garrett.WittExtensionProp {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Prop

Witt extension property for B: when B is nondegenerate, every subspace isometry between two submodules extends to a global isometry of V.

def Garrett.WittCancellationProp {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Prop

Witt cancellation property for B: when B is nondegenerate, every isometry between two submodules induces an isometry between their orthogonal complements.

theorem Garrett.LinearEquiv.ofEq_coe {R : Type u_3} [Semiring R] {M : Type u_4} [AddCommMonoid M] [Module R M] {p q : Submodule R M} (h : p = q) (x : ↥p) : ↑((LinearEquiv.ofEq p q h) x) = ↑x

The underlying value of LinearEquiv.ofEq p q h x agrees with that of x since both submodules are equal.

theorem Garrett.orth_cross_zero {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hB_ref : ∀ (x y : V), (B x) y = 0 → (B y) x = 0) (U : Submodule k V) (u : ↥U) (v : ↥(B.orthogonal U)) : (B ↑u) ↑v = 0 ∧ (B ↑v) ↑u = 0

For a reflexive bilinear form B, any pair (u, v) with u ∈ U and v in the orthogonal complement of U satisfies B u v = 0 and B v u = 0.

theorem Garrett.bilinForm_decomp {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hB_ref : ∀ (x y : V), (B x) y = 0 → (B y) x = 0) (U : Submodule k V) (a b : ↥U) (c d : ↥(B.orthogonal U)) : (B (↑a + ↑c)) (↑b + ↑d) = (B ↑a) ↑b + (B ↑c) ↑d

For a reflexive form B, the bilinear values on sums a + c and b + d (with a, b ∈ U and c, d in the orthogonal complement of U) split into B a b + B c d because the cross terms vanish.

theorem Garrett.WittCancellation {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hWE : WittExtensionProp B) : WittCancellationProp B

Witt extension implies Witt cancellation: if every subspace isometry of B extends globally, then any isometry between two submodules also induces an isometry between their orthogonal complements.

theorem Garrett.WittExtension {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hWC : WittCancellationProp B) (hB_ref : ∀ (x y : V), (B x) y = 0 → (B y) x = 0) (hCompl : ∀ (S : Submodule k V), IsCompl S (B.orthogonal S)) : WittExtensionProp B

Witt cancellation implies Witt extension, given that B is reflexive and each subspace is complemented by its orthogonal complement: any subspace isometry of B then extends to a global isometry.