comp_ι_sq_scalar — Mathlib

English

If g is an R-algebra homomorphism from the Clifford algebra Clifford(Q) to some algebra A, then g respects the canonical relation that ι_Q(m) squares to Q(m) for all m in M; equivalently, the lift of g composed with ι_Q matches the induced quadratic relation in A.

Русский

Если g есть алгебра-гомоморфизм из Clifford(Q) в A, то он сохраняет отношение ι_Q(m)^2 = Q(m) для всех m ∈ M; эквивалентно тому, что подъем g через ι_Q сохраняет квадратичное отношение в A.

LaTeX

$$$g(\\iota_Q(m)) \\cdot g(\\iota_Q(m)) = \\mathrm{algebraMap}_{R \\to A}(Q(m))$ for all m ∈ M.$$

Lean4

@[simp]
theorem comp_ι_sq_scalar (g : CliffordAlgebra Q →ₐ[R] A) (m : M) : g (ι Q m) * g (ι Q m) = algebraMap _ _ (Q m) := by
  rw [← map_mul, ι_sq_scalar, AlgHom.commutes]

Похожие утверждения