English
For any quadratic map Q and basis bm, the composition (Q.toBilin bm).toQuadraticMap equals Q. That is, one can recover Q from its associated bilinear form relative to the basis.
Русский
Для квадратичного отображения Q и базы bm композиция (Q.toBilin bm).toQuadraticMap равна Q: квадратичная форма восстанавливается по своей ассоциированной билинейной форме через базис.
LaTeX
$$$ (Q.toBilin bm).toQuadraticMap = Q $$$
Lean4
theorem toQuadraticMap_toBilin (Q : QuadraticMap R M N) (bm : Basis ι R M) : (Q.toBilin bm).toQuadraticMap = Q :=
by
ext x
rw [← bm.linearCombination_repr x, LinearMap.BilinMap.toQuadraticMap_apply, Finsupp.linearCombination_apply,
Finsupp.sum]
simp_rw [LinearMap.map_sum₂, map_sum, LinearMap.map_smul₂, map_smul, toBilin_apply, smul_ite, smul_zero, ←
Finset.sum_product', ← Finset.diag_union_offDiag, Finset.sum_union (Finset.disjoint_diag_offDiag _),
Finset.sum_diag, if_true]
rw [Finset.sum_ite_of_false, QuadraticMap.map_sum, ← Finset.sum_filter]
· simp_rw [← polar_smul_right _ (bm.repr x <| Prod.snd _), ← polar_smul_left _ (bm.repr x <| Prod.fst _)]
simp_rw [QuadraticMap.map_smul, mul_smul, Finset.sum_sym2_filter_not_isDiag]
rfl
· intro x hx
rw [Finset.mem_offDiag] at hx
simpa using hx.2.2
