Witt's extension theorem

An isometry between two regular subspaces of a finite-dimensional quadratic space extends to an isometry of the whole space. The construction splits the ambient space as each subspace orthogonally summed with its orthogonal complement. Witt cancellation identifies the two complements, and the two isometries then combine across these decompositions. In fact the ambient form itself need not be regular; regularity of the two subspaces is exactly what the proof uses.

This is Witt's extension theorem in the form used by the local classification and transfer theory of quadratic forms. The subspaces are required to be regular: without that hypothesis they need not split off as orthogonal summands.

Main results

• QuadraticMap.IsometryEquiv.exists_extension: Witt's extension theorem.
• QuadraticMap.IsometryEquiv.extension: a chosen extension, with the simplification theorem QuadraticMap.IsometryEquiv.extension_apply on the original subspace.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter I, Theorem 4.9.

theorem QuadraticMap.IsometryEquiv.exists_extension {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (f : (restrict Q W).IsometryEquiv (restrict Q W')) (hW : Nondegenerate) : ∃ (e : IsometryEquiv Q Q), ∀ (x : ↥W), e ↑x = ↑(f x)

Witt's extension theorem (Lam I.4.9). An isometry between regular subspaces of a finite-dimensional quadratic space extends to an isometry of the whole space. No regularity hypothesis on the ambient form is needed.

noncomputable def QuadraticMap.IsometryEquiv.extension {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (f : (restrict Q W).IsometryEquiv (restrict Q W')) (hW : Nondegenerate) : IsometryEquiv Q Q

A chosen ambient isometry extending an isometry between two regular subspaces.

@[simp]

theorem QuadraticMap.IsometryEquiv.extension_apply {K : Type u} [Field K] [Invertible 2] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (f : (restrict Q W).IsometryEquiv (restrict Q W')) (hW : Nondegenerate) (x : ↥W) : (f.extension hW) ↑x = ↑(f x)

Witt's chosen extension agrees with the original isometry on its source subspace.