English
There is an additive monoid hom from BilinMap R M N to QuadraticMap R M N, preserving zero and addition.
Русский
Существует гомоморфизм аддитивных моноидов BilinMap R M N → QuadraticMap R M N, сохраняющий ноль и сложение.
LaTeX
$$$\text{toQuadraticMapAddMonoidHom} : (BilinMap\ R\ M\ N) \to+ QuadraticMap\ R\ M\ N$ with $toQuadraticMapAddMonoidHom(B_1+B_2) = toQuadraticMapAddMonoidHom(B_1) + toQuadraticMapAddMonoidHom(B_2)$ and $toQuadraticMapAddMonoidHom(0) = 0$.$$
Lean4
/-- A bilinear map gives a quadratic map by applying the argument twice. -/
def toQuadraticMap (B : BilinMap R M N) : QuadraticMap R M N
where
toFun x := B x x
toFun_smul a x := by simp only [map_smul, LinearMap.smul_apply, smul_smul]
exists_companion' := ⟨B + LinearMap.flip B, fun x y => by simp [add_add_add_comm, add_comm]⟩
