ι_sq_scalar — Mathlib

English

For every m in M, the image ι_Q(m) in the Clifford algebra squares to the scalar Q(m) when viewed in the base ring R via the algebra map.

Русский

Для каждого вектора m из M образ ι_Q(m) в клиффордовой алгебре имеет квадрат, равный скаляру Q(m), получаемому через алгебраическое отображение.

LaTeX

$$$\\iota_Q(m) \\cdot \\iota_Q(m) = \\mathrm{algebraMap}_{R \\to Clifford(Q)}(Q(m))$$$

Lean4

/-- As well as being linear, `ι Q` squares to the quadratic form -/
@[simp]
theorem ι_sq_scalar (m : M) : ι Q m * ι Q m = algebraMap R _ (Q m) :=
  by
  rw [ι]
  erw [LinearMap.comp_apply]
  rw [AlgHom.toLinearMap_apply, ← map_mul (RingQuot.mkAlgHom R (Rel Q)), RingQuot.mkAlgHom_rel R (Rel.of m),
    AlgHom.commutes]
  rfl

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