ι — Mathlib · SciLib

English

There is a version of the embedding ι that lands directly in the graded direct sum, mapping M into ⨁ i∈Z/2 evenOdd(Q,i).

Русский

Существует вариант отображения ι, который напрямую целится в разложение по градации, отображая M в прямую сумму по степени 0 и 1.

LaTeX

$$$\\iota: M \\to \\bigoplus_{i \\in \\mathbb{Z}_2} \\mathrm{evenOdd}(Q,i)$$$

Lean4

/-- A version of `CliffordAlgebra.ι` that maps directly into the graded structure. This is
primarily an auxiliary construction used to provide `CliffordAlgebra.gradedAlgebra`. -/
protected def ι : M →ₗ[R] ⨁ i : ZMod 2, evenOdd Q i :=
  DirectSum.lof R (ZMod 2) (fun i => ↥(evenOdd Q i)) 1 ∘ₗ (ι Q).codRestrict _ (ι_mem_evenOdd_one Q)

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