English
There exists an explicit companion in the polar construction that coincides with the bilinear form polarBilin Q.
Русский
Существуют явный компаньон в полярной конструкции, совпадающий с билинейной формой polarBilin Q.
LaTeX
$$Q.exists_companion.choose = polarBilin Q$$
Lean4
/-- An alternative constructor to `QuadraticMap.mk`, for rings where `polar` can be used. -/
@[simps]
def ofPolar (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
(polar_add_left : ∀ x x' y : M, polar toFun (x + x') y = polar toFun x y + polar toFun x' y)
(polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y) : QuadraticMap R M N :=
{ toFun
toFun_smul
exists_companion' :=
⟨LinearMap.mk₂ R (polar toFun) (polar_add_left) (polar_smul_left)
(fun x _ _ ↦ by simp_rw [polar_comm _ x, polar_add_left])
(fun _ _ _ ↦ by rw [polar_comm, polar_smul_left, polar_comm]),
fun _ _ ↦ by
simp only [LinearMap.mk₂_apply]
rw [polar, sub_sub, add_sub_cancel]⟩ }
