English
If 2 is a unit in A, then the condition f(x)^2 = Q(x) for all x is equivalent to the cross-term identity f(x)f(y) + f(y)f(x) = polar(Q)(x,y) after suitable normalization.
Русский
Если 2 обратимо в A, то условие f(x)^2 = Q(x) эквивалентно тождеству cross-term: f(x)f(y) + f(y)f(x) = polar(Q)(x,y).
LaTeX
$$$\\text{2 is a unit in } A \\implies (\\forall f: M \\to A)\n(\\forall x, f(x)^2 = Q(x)) \\\\iff (f \\text{ satisfies } f(x)f(y) + f(y)f(x) = polar_Bilin(Q)(x,y))$$$
Lean4
theorem mul_add_swap_eq_polar_of_forall_mul_self_eq {A : Type*} [Ring A] [Algebra R A] (f : M →ₗ[R] A)
(hf : ∀ x, f x * f x = algebraMap _ _ (Q x)) (a b : M) :
f a * f b + f b * f a = algebraMap R _ (QuadraticMap.polar Q a b) :=
calc
f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b := by
rw [f.map_add, mul_add, add_mul, add_mul]; abel
_ = algebraMap R _ (Q (a + b)) - algebraMap R _ (Q a) - algebraMap R _ (Q b) := by rw [hf, hf, hf]
_ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub]
_ = algebraMap R _ (QuadraticMap.polar Q a b) := rfl
