English
If two algebra homomorphisms from Clifford(Q) to A agree on the canonical map ι_Q, then they are equal as maps.
Русский
Если два алгебра-гомоморфизма от Clifford(Q) в A совпадают при ограничении на ι_Q, то они равны как отображения.
LaTeX
$$$f.toLinearMap \\circ (ι_Q) = g.toLinearMap \\circ (ι_Q) \\implies f = g$ for $f,g: Clifford(Q) → A$.$$
Lean4
/-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible.
To show a function squares to the quadratic form, it suffices to show that
`f x * f y + f y * f x = algebraMap _ _ (polar Q x y)` -/
theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (2 : A)) (f : M →ₗ[R] A) :
(∀ x, f x * f x = algebraMap _ _ (Q x)) ↔
(LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
Q.polarBilin.compr₂ (Algebra.linearMap R A) :=
by
simp_rw [DFunLike.ext_iff]
refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩
change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticMap.polar Q x y) at h
apply h2.mul_left_cancel
rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]
