English
If M is a free R-module, then every quadratic map Q: M → N arises from some bilinear form; equivalently, the map BilinMap.toQuadraticMap is surjective.
Русский
Если M свободный модуль над R, то любое квадратичное отображение Q: M → N arises from some bilinear form; эквивалентно отображение BilinMap.toQuadraticMap сюрьективно.
LaTeX
$$$\\text{Module.Free } R M \\; \\Rightarrow\\; \\text{Surjective}(\\text{LinearMap.BilinMap.toQuadraticMap} : \\mathrm{BilinMap}\\ R M N \\to \\mathrm{QuadraticMap}\\ R M N) $$$
Lean4
/-- From a free module, every quadratic map can be built from a bilinear form.
See `BilinMap.not_forall_toQuadraticMap_surjective` for a counterexample when the module is
not free. -/
theorem _root_.LinearMap.BilinMap.toQuadraticMap_surjective [Module.Free R M] :
Function.Surjective (LinearMap.BilinMap.toQuadraticMap : LinearMap.BilinMap R M N → _) :=
by
intro Q
obtain ⟨ι, b⟩ := Module.Free.exists_basis (R := R) (M := M)
letI : LinearOrder ι := IsWellOrder.linearOrder WellOrderingRel
exact ⟨_, toQuadraticMap_toBilin _ b⟩
