Continuity of quadratic maps

A quadratic map on a finite module is continuous for the module topologies when two is invertible. This follows from Mathlib's continuity theorem for bilinear maps by evaluating the associated bilinear map on the diagonal. For any continuous quadratic map, its preserving endomorphisms form a closed set when the codomain is Hausdorff.

Over the reals, near a vector with nonzero quadratic value, the ratio to that value is a nonzero square. This is the neighborhood condition that allows weak approximation of vectors to preserve the square classes of their quadratic values.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §66.

theorem QuadraticMap.continuous {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [TopologicalSpace M] [IsModuleTopology R M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [IsModuleTopology R N] [Invertible 2] (Q : QuadraticMap R M N) : Continuous ⇑Q

A quadratic map on a finite module is continuous for the module topologies if two is invertible on its codomain.

theorem QuadraticMap.isClosed_setOfPred_forall_map_app {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsModuleTopology R M] [TopologicalSpace (Module.End R M)] [IsModuleTopology R (Module.End R M)] [AddCommGroup N] [Module R N] [TopologicalSpace N] [T2Space N] (Q : QuadraticMap R M N) (hQ : Continuous ⇑Q) : IsClosed {f : Module.End R M | ∀ (x : M), Q (f x) = Q x}

Endomorphisms preserving a continuous quadratic map form a closed subset of the endomorphism space when the codomain is Hausdorff.

theorem QuadraticForm.eventually_isSquare_div {V : Type u_1} [AddCommGroup V] [Module ℝ V] [Module.Finite ℝ V] [TopologicalSpace V] [IsModuleTopology ℝ V] (Q : QuadraticForm ℝ V) {x : V} (hx : Q x ≠ 0) : ∀ᶠ (z : V) in nhds x, Q z ≠ 0 ∧ IsSquare (Q z / Q x)

Near a vector where a real quadratic form is nonzero, its value remains nonzero and in the same square class. No nondegeneracy assumption on the form is needed.