Category-theoretic interpretations of clifford_algebra #
Main definitions #
QuadraticModule R: the category of quadratic modulesCliffordAlgebra: the functor from quadratic modules to algebrasclifford_algebra.is_initial: the clifford algebra is initial in the category of pairs(A, clifford_hom Q A).
- carrier : Type ?
- is_add_comm_group : add_comm_group self.carrier
- is_module : module R self.carrier
- form' : quadratic_form R self.carrier
Instances for QuadraticModule
- QuadraticModule.has_sizeof_inst
- QuadraticModule.has_coe_to_sort
- QuadraticModule.category
- QuadraticModule.concrete_category
- QuadraticModule.has_forget_to_Module
@[protected, instance]
def
QuadraticModule.has_coe_to_sort
{R : Type u}
[comm_ring R] :
has_coe_to_sort (QuadraticModule R) (Type v)
Equations
- QuadraticModule.has_coe_to_sort = {coe := QuadraticModule.carrier _inst_1}
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
- QuadraticModule.category = {to_category_struct := {to_quiver := {hom := λ (M N : QuadraticModule R), M.form.isometric_map N.form}, id := λ (M : QuadraticModule R), quadratic_form.isometric_map.id M.form, comp := λ (A B C : QuadraticModule R) (f : A ⟶ B) (g : B ⟶ C), quadratic_form.isometric_map.comp g f}, id_comp' := _, comp_id' := _, assoc' := _}
theorem
QuadraticModule.comp_def
{R : Type u}
[comm_ring R]
{M N U : QuadraticModule R}
(f : M ⟶ N)
(g : N ⟶ U) :
f ≫ g = quadratic_form.isometric_map.comp g f
@[protected, instance]
Equations
- QuadraticModule.concrete_category = category_theory.concrete_category.mk {obj := λ (R_1 : QuadraticModule R), ↥R_1, map := λ (R_1 S : QuadraticModule R) (f : R_1 ⟶ S), ⇑f, map_id' := _, map_comp' := _}
@[protected, instance]
Equations
- QuadraticModule.has_forget_to_Module = {forget₂ := {obj := λ (M : QuadraticModule R), Module.of R ↥M, map := λ (M₁ M₂ : QuadraticModule R), quadratic_form.isometric_map.to_linear_map, map_id' := _, map_comp' := _}, forget_comp := _}
@[protected, instance]
def
QuadraticModule.linear_map_class
{R : Type u}
[comm_ring R]
(M N : QuadraticModule R) :
linear_map_class (M ⟶ N) R ↥M ↥N
Equations
- M.linear_map_class N = {coe := λ (f : M ⟶ N), ⇑f, coe_injective' := _, map_add := _, map_smulₛₗ := _}
The "clifford algebra" functor, sending a quadratic R-module V to the clifford algebra on V.
Equations
- CliffordAlgebra = {obj := λ (M : QuadraticModule R), Algebra.mk (clifford_algebra M.form), map := λ (M N : QuadraticModule R) (f : M ⟶ N), clifford_algebra.map M.form N.form (quadratic_form.isometric_map.to_linear_map f) _, map_id' := _, map_comp' := _}
@[simp]
theorem
CliffordAlgebra_obj_carrier
{R : Type u}
[comm_ring R]
(M : QuadraticModule R) :
↥(CliffordAlgebra.obj M) = clifford_algebra M.form
@[simp]
@[simp]
@[simp]
structure
Cliff
{R : Type u}
[comm_ring R]
{M : Type w}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
Type (max u (v+1) w)
- alg : Algebra R
- hom : clifford_algebra.clifford_hom Q ↥(self.alg)
The category of pairs of algebras and clifford_homs to those algebras.
https://empg.maths.ed.ac.uk/Activities/Spin/Lecture1.pdf
Instances for Cliff
- Cliff.has_sizeof_inst
- Cliff.category_theory.category
- Cliff.concrete_category
- Cliff.has_forget_to_Algebra
def
Cliff.of
{R : Type u}
[comm_ring R]
{M : Type w}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{A : Type v}
[ring A]
[algebra R A]
(f : clifford_algebra.clifford_hom Q A) :
Cliff Q
Convert a clifford_hom Q A to an element of Cliff Q.
@[protected, instance]
def
Cliff.category_theory.category
{R : Type u}
[comm_ring R]
{M : Type w}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
Equations
- Cliff.category_theory.category Q = {to_category_struct := {to_quiver := {hom := λ (f g : Cliff Q), {h // (alg_hom.to_linear_map h).comp f.hom.val = g.hom.val}}, id := λ (f : Cliff Q), ⟨𝟙 f.alg, _⟩, comp := λ (x y z : Cliff Q) (f : x ⟶ y) (g : y ⟶ z), ⟨f.val ≫ g.val, _⟩}, id_comp' := _, comp_id' := _, assoc' := _}
@[protected, instance]
def
Cliff.concrete_category
{R : Type u}
[comm_ring R]
{M : Type w}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
@[protected, instance]
def
Cliff.has_forget_to_Algebra
{R : Type u}
[comm_ring R]
{M : Type w}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
category_theory.has_forget₂ (Cliff Q) (Algebra R)
@[protected, instance]
def
Cliff.quiver.hom.unique
{R : Type u}
[comm_ring R]
{M : Type w}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(Y : Cliff Q) :
unique (Cliff.of Q ⟨clifford_algebra.ι Q, _⟩ ⟶ Y)
Equations
- Cliff.quiver.hom.unique Q Y = {to_inhabited := {default := ⟨⇑(clifford_algebra.lift Q) Y.hom, _⟩}, uniq := _}
- _ = _
def
clifford_algebra.is_initial
{R : Type u}
[comm_ring R]
{M : Type w}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
The clifford algebra is the initial object in Cliff.