Rel — Mathlib

English

The Clifford algebra of an R-module M equipped with a quadratic form Q is constructed as a suitable quotient of the tensor algebra on M, encoding the relation v^2 = Q(v)1 for all v ∈ M.

Русский

Клиффондова алгебра модуля M над R с квадратичной формой Q строится как подходящая фактор-алгебра тензорной алгебры на M, задающая отношение v^2 = Q(v)1 для всех v ∈ M.

LaTeX

$$CliffordAlgebra(Q) = T_R(M) / ⟨ v ⊗ v − Q(v)·1 ⟩$$

Lean4

/-- `Rel` relates each `ι m * ι m`, for `m : M`, with `Q m`.

The Clifford algebra of `M` is defined as the quotient modulo this relation.
-/
inductive Rel : TensorAlgebra R M → TensorAlgebra R M → Prop
  | of (m : M) : Rel (ι R m * ι R m) (algebraMap R _ (Q m))

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