cliffordAlgebra

Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory

URI: https://scilib.ai/kg/mathlib#QuadraticModuleCat.cliffordAlgebra

Lean4

/-- The "clifford algebra" functor, sending a quadratic `R`-module `V` to the clifford algebra on
`V`.

This is `CliffordAlgebra.map` through the lens of category theory. -/
@[simps]
def cliffordAlgebra : QuadraticModuleCat.{u} R ⥤ AlgCat.{u} R
    where
  obj M := AlgCat.of R (CliffordAlgebra M.form)
  map {_M _N} f := AlgCat.ofHom <| CliffordAlgebra.map f.toIsometry
  map_id _M := by simp
  map_comp {_M _N _P} f g := by ext; simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru