theorem isometry_extension_lemma {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φ : Garrett.IsSubspaceIsometry B U W φ) : ∃ (Φ : V ≃ₗ[k] V), (∀ (v₁ v₂ : V), (B (Φ v₁)) (Φ v₂) = (B v₁) v₂) ∧ ∀ (u : ↥U), Φ ↑u = ↑(φ u)

Isometry extension lemma (Witt's theorem, extension form): every subspace isometry $\varphi : U \to W$ of a non-degenerate symmetric bilinear space $(V, B)$ extends to a global isometry $\Phi : V \to V$ with $B(\Phi v_1, \Phi v_2) = B(v_1, v_2)$ and $\Phi|_U = \varphi$.

theorem witt_cancellation {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₁ U₂ : Submodule k V) (φ : ↥U₁ ≃ₗ[k] ↥U₂) (hφ : Garrett.IsSubspaceIsometry B U₁ U₂ φ) : ∃ (ψ : ↥(B.orthogonal U₁) ≃ₗ[k] ↥(B.orthogonal U₂)), Garrett.IsSubspaceIsometry B (B.orthogonal U₁) (B.orthogonal U₂) ψ

Witt cancellation: any subspace isometry $\varphi : U_1 \to U_2$ of a non-degenerate symmetric bilinear space induces an isometry between the orthogonal complements $U_1^{\perp}$ and $U_2^{\perp}$.

theorem witt_theorem_section_7_3 {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), Garrett.IsSubspaceIsometry B U W φ → ∃ (Φ : V ≃ₗ[k] V), (∀ (v₁ v₂ : V), (B (Φ v₁)) (Φ v₂) = (B v₁) v₂) ∧ ∀ (u : ↥U), Φ ↑u = ↑(φ u)) ∧ ∀ (U₁ U₂ : Submodule k V) (φ : ↥U₁ ≃ₗ[k] ↥U₂), Garrett.IsSubspaceIsometry B U₁ U₂ φ → ∃ (ψ : ↥(B.orthogonal U₁) ≃ₗ[k] ↥(B.orthogonal U₂)), Garrett.IsSubspaceIsometry B (B.orthogonal U₁) (B.orthogonal U₂) ψ

Witt's theorem (Section 7.3): for non-degenerate symmetric bilinear spaces, both the extension lemma and Witt cancellation hold simultaneously.