English
If a bilinear map B: M×N→R is symmetric in its appropriate sense (i.e., B.flip = B when treated as a map M×M→R), then B can be lifted to a quadratic map Q: M→N with the associated map equal to B.
Русский
Если билинная форма B: M×M→R симметрична (B.flip = B), то B можно представить как ассоциированную квадратичную форму Q: M→N, так что ассоциированная форма Q равна B.
LaTeX
$$$\\forall B:\\mathrm{BilinMap}(R,M,N),\\; B^{\\mathrm{flip}}=B \\implies \\exists Q:\\mathrm{QuadraticMap}(R,M,N),\\; \\mathrm{associatedHom}(Q)=B.$$$
Lean4
/-- Symmetric bilinear maps can be lifted to quadratic maps -/
instance canLift' : CanLift (BilinMap R M N) (QuadraticMap R M N) (associatedHom ℕ) fun B ↦ B.flip = B where
prf B hB := ⟨B.toQuadraticMap, associated_left_inverse' _ hB⟩
