Theorems · Definition · category theory
QuadraticModuleCat.cliffordAlgebra
{R : Type u} → [inst : CommRing R] → CategoryTheory.Functor (QuadraticModuleCat R) (AlgCat R)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.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functorstatement · cited by 16,252
- CliffordAlgebraproof · cited by 309
- AlgCatstatement · cited by 75
- QuadraticModuleCatstatement and proof · cited by 40
- QuadraticModuleCat.formproof · cited by 30
- AlgCat.ofproof · cited by 23
- QuadraticModuleCat.Hom.toIsometryproof · cited by 18
- AlgCat.ofHomproof · cited by 16
- CliffordAlgebra.mapproof · cited by 15
Cited by2
Results whose statement or proof uses this declaration.
- QuadraticModuleCat.cliffordAlgebra_mapstatement and proof · cited by 0
- QuadraticModuleCat.cliffordAlgebra_obj_carrierstatement and proof · cited by 0