noncomputable def Garrett.bilinReflect {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (a : V) (_ha : (B a) a ≠ 0) (v : V) : V

Bilinear reflection of v through the hyperplane orthogonal to a non-isotropic vector a: subtracts off twice the a-component measured by B.

noncomputable def Garrett.bilinReflectLM {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (a : V) (ha : (B a) a ≠ 0) : V →ₗ[k] V

The bilinear reflection through a packaged as a linear map V →ₗ[k] V.

theorem Garrett.bilinReflect_invol {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (a : V) (ha : (B a) a ≠ 0) (v : V) : bilinReflect B a ha (bilinReflect B a ha v) = v

The bilinear reflection is an involution: applying it twice returns the original vector.

theorem Garrett.bilinReflect_preserves {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (a : V) (ha : (B a) a ≠ 0) (v₁ v₂ : V) : (B (bilinReflect B a ha v₁)) (bilinReflect B a ha v₂) = (B v₁) v₂

The bilinear reflection through a non-isotropic vector preserves a symmetric bilinear form: B (Refl v₁) (Refl v₂) = B v₁ v₂.

noncomputable def Garrett.bilinReflectEquiv {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (a : V) (ha : (B a) a ≠ 0) : V ≃ₗ[k] V

The bilinear reflection through a, packaged as a linear equivalence V ≃ₗ[k] V (using its involutive property).

theorem Garrett.bilinReflect_maps {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (x y : V) (hxy : (B (x - y)) (x - y) ≠ 0) (hBxy : (B x) x = (B y) y) : bilinReflect B (x - y) hxy x = y

If x and y have the same B-norm and their difference is non-isotropic, the bilinear reflection through x - y sends x to y.

theorem Garrett.exists_noniso_difference {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (x y : V) (hBxx : (B x) x ≠ 0) (hBxy : (B x) x = (B y) y) : (B (x - y)) (x - y) ≠ 0 ∨ (B (x + y)) (x + y) ≠ 0

If x is non-isotropic and B x x = B y y, then at least one of x - y or x + y is also non-isotropic.

theorem Garrett.bilinReflectEquiv_apply {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (a : V) (ha : (B a) a ≠ 0) (v : V) : (bilinReflectEquiv B a ha) v = bilinReflect B a ha v

The action of the bilinReflectEquiv linear equivalence agrees with the underlying bilinReflect function.

theorem Garrett.bilinReflect_neg_self {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (a : V) (ha : (B a) a ≠ 0) : bilinReflect B a ha (-a) = a

The bilinear reflection through a sends -a back to a.

theorem Garrett.bilinReflectEquiv_preserves {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (a : V) (ha : (B a) a ≠ 0) (v₁ v₂ : V) : (B ((bilinReflectEquiv B a ha) v₁)) ((bilinReflectEquiv B a ha) v₂) = (B v₁) v₂

The bilinear reflection linear equivalence preserves the symmetric bilinear form B.

theorem Garrett.bilinReflect_of_ortho {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (a : V) (ha : (B a) a ≠ 0) (v : V) (hv : (B v) a = 0) : bilinReflect B a ha v = v

Vectors orthogonal to a are fixed by the bilinear reflection through a.

theorem Garrett.wittExtension_noniso_step {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (_hnd : B.orthogonal ⊤ = ⊥) (U W : Submodule k V) (φ : ↥U ≃ₗ[k] ↥W) (hφ : IsSubspaceIsometry B U W φ) {x : V} (hxU : x ∈ U) (hx_noniso : (B x) x ≠ 0) (ih : ∀ (U' W' : Submodule k V) (φ' : ↥U' ≃ₗ[k] ↥W'), IsSubspaceIsometry B U' W' φ' → Module.finrank k ↥U' < Module.finrank k ↥U → ∃ (Φ : V ≃ₗ[k] V), (∀ (v₁ v₂ : V), (B (Φ v₁)) (Φ v₂) = (B v₁) v₂) ∧ ∀ (u : ↥U'), Φ ↑u = ↑(φ' u)) : ∃ (Φ : V ≃ₗ[k] V), (∀ (v₁ v₂ : V), (B (Φ v₁)) (Φ v₂) = (B v₁) v₂) ∧ ∀ (u : ↥U), Φ ↑u = ↑(φ u)

Inductive step in Witt's extension theorem when U contains a non-isotropic vector x: assuming the inductive hypothesis for smaller subspaces, the isometry φ : U ≃ W extends to an isometry of the whole space V.

theorem Garrett.wittExtension_isotropic_step {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (hnd : B.orthogonal ⊤ = ⊥) (U W : Submodule k V) (φ : ↥U ≃ₗ[k] ↥W) (hφ : IsSubspaceIsometry B U W φ) {u : V} (huU : u ∈ U) (hu_ne : u ≠ 0) (hu_iso : (B u) u = 0) (ih : ∀ (U' W' : Submodule k V) (φ' : ↥U' ≃ₗ[k] ↥W'), IsSubspaceIsometry B U' W' φ' → Module.finrank k ↥U' < Module.finrank k ↥U → ∃ (Φ : V ≃ₗ[k] V), (∀ (v₁ v₂ : V), (B (Φ v₁)) (Φ v₂) = (B v₁) v₂) ∧ ∀ (u : ↥U'), Φ ↑u = ↑(φ' u)) : ∃ (Φ : V ≃ₗ[k] V), (∀ (v₁ v₂ : V), (B (Φ v₁)) (Φ v₂) = (B v₁) v₂) ∧ ∀ (u : ↥U), Φ ↑u = ↑(φ u)

Inductive step in Witt's extension theorem when U contains a nonzero isotropic vector u: reduces to the non-isotropic step (or handles the case where U is totally isotropic) to extend φ : U ≃ W to an isometry of all of V.

theorem Garrett.wittExtensionProp_of_symmetric {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (hnd : B.orthogonal ⊤ = ⊥) : WittExtensionProp B

Witt's Extension Theorem for symmetric nondegenerate bilinear forms in characteristic not two: any isometry between subspaces extends to an isometry of the whole space. Proved by strong induction on Module.finrank k U, dispatching to wittExtension_noniso_step or wittExtension_isotropic_step as appropriate.

theorem Garrett.wittCancellationProp_of_symmetric {k : Type u_1} [Field k] [NeZero 2] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (B : LinearMap.BilinForm k V) (hBsymm : ∀ (x y : V), (B x) y = (B y) x) (hnd : B.orthogonal ⊤ = ⊥) : WittCancellationProp B

Witt's Cancellation Theorem for symmetric nondegenerate bilinear forms, obtained as a corollary of the extension theorem wittExtensionProp_of_symmetric.