English
If B is a symmetric bilinear form on a module, then there exists a quadratic form Q whose associated bilinear form equals B (i.e., B is the 'polarization' of Q). This requires that 2 is invertible in the base ring.
Русский
Пусть B — симметричная билинейная форма на модуле; тогда существует квадратичная форма Q такая, что связанная с Q билинейная форма равна B (то есть B является поляризацией Q). Требуется, чтобы 2 было обратимо в основанной кольцевой структуре.
LaTeX
$$$\\forall B:\\mathrm{BilinMap}(R,M,R),\\; B^{\\mathrm{flip}}=B \\implies \\exists Q:\\mathrm{QuadraticForm}(R,M),\\; \\mathrm{associated}(Q)=B.$$$
Lean4
/-- Symmetric bilinear forms can be lifted to quadratic forms -/
instance canLift [Invertible (2 : R)] : CanLift (BilinMap R M R) (QuadraticForm R M) (associatedHom ℕ) LinearMap.IsSymm
where prf B := fun ⟨hB⟩ ↦ ⟨B.toQuadraticMap, associated_left_inverse _ hB⟩
