English
The product of two linear maps into an R-algebra is a quadratic map; the value is given by (f x)(g x) with a symmetric companion built from f and g.
Русский
Произведение двух линейных отображений в R-алгебру образует квадратичное отображение; значение равно произведению изображений на векторе, с симметричным сопровождающим биллинейным отображением.
LaTeX
$$$Q(x) = f(x)\,g(x)$ defines a QuadraticMap R M A with companion given by $B(x,y) = f(x)g(y) + f(y)g(x)$.$$
Lean4
/-- The product of linear maps into an `R`-algebra is a quadratic map. -/
def linMulLin (f g : M →ₗ[R] A) : QuadraticMap R M A
where
toFun := f * g
toFun_smul a
x := by
rw [Pi.mul_apply, Pi.mul_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.map_smulₛₗ, RingHom.id_apply,
smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]
exists_companion' :=
⟨(LinearMap.mul R A).compl₁₂ f g + (LinearMap.mul R A).flip.compl₁₂ g f, fun x y =>
by
simp only [Pi.mul_apply, map_add, left_distrib, right_distrib, LinearMap.add_apply, LinearMap.compl₁₂_apply,
LinearMap.mul_apply', LinearMap.flip_apply]
abel_nf⟩
