Differential objects in a category.
A differential object in a category with zero morphisms and a shift is
an object X equipped with
a morphism d : X ⟶ X⟦1⟧, such that d^2 = 0.
We build the category of differential objects, and some basic constructions such as the forgetful functor, and zero morphisms and zero objects.
@[nolint]
structure
category_theory.differential_object
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
Type (max u v)
- X : C
- d : c.X ⟶ (category_theory.shift C ^ 1).functor.obj c.X
- d_squared' : c.d ≫ (category_theory.shift C ^ 1).functor.map c.d = 0 . "obviously"
A differential object in a category with zero morphisms and a shift is
an object X equipped with
a morphism d : X ⟶ X⟦1⟧, such that d^2 = 0.
@[nolint, ext]
structure
category_theory.differential_object.hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
A morphism of differential objects is a morphism commuting with the differentials.
theorem
category_theory.differential_object.hom.ext
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.limits.has_zero_morphisms C}
{_inst_3 : category_theory.has_shift C}
{X Y : category_theory.differential_object C}
(x y : X.hom Y) :
theorem
category_theory.differential_object.hom.ext_iff
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.limits.has_zero_morphisms C}
{_inst_3 : category_theory.has_shift C}
{X Y : category_theory.differential_object C}
(x y : X.hom Y) :
@[simp]
theorem
category_theory.differential_object.hom.id_f
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
(X : category_theory.differential_object C) :
def
category_theory.differential_object.hom.id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
(X : category_theory.differential_object C) :
X.hom X
The identity morphism of a differential object.
def
category_theory.differential_object.hom.comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
{X Y Z : category_theory.differential_object C} :
The composition of morphisms of differential objects.
@[simp]
theorem
category_theory.differential_object.hom.comp_f
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
{X Y Z : category_theory.differential_object C}
(f : X.hom Y)
(g : Y.hom Z) :
@[instance]
def
category_theory.differential_object.category_of_differential_objects
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
Equations
- category_theory.differential_object.category_of_differential_objects = {to_category_struct := {to_has_hom := {hom := category_theory.differential_object.hom _inst_3}, id := category_theory.differential_object.hom.id _inst_3, comp := λ (X Y Z : category_theory.differential_object C) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.differential_object.hom.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.differential_object.id_f
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
(X : category_theory.differential_object C) :
@[simp]
theorem
category_theory.differential_object.comp_f
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
{X Y Z : category_theory.differential_object C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
def
category_theory.differential_object.forget
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
The forgetful functor taking a differential object to its underlying object.
Equations
- category_theory.differential_object.forget C = {obj := λ (X : category_theory.differential_object C), X.X, map := λ (X Y : category_theory.differential_object C) (f : X ⟶ Y), f.f, map_id' := _, map_comp' := _}
@[instance]
def
category_theory.differential_object.forget_faithful
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
Equations
- _ = _
@[instance]
def
category_theory.differential_object.has_zero_morphisms
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
Equations
- category_theory.differential_object.has_zero_morphisms C = {has_zero := λ (X Y : category_theory.differential_object C), {zero := {f := 0, comm' := _}}, comp_zero' := _, zero_comp' := _}
@[simp]
theorem
category_theory.differential_object.zero_f
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C]
(P Q : category_theory.differential_object C) :
@[instance]
def
category_theory.differential_object.has_zero_object
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :
Equations
- category_theory.differential_object.has_zero_object C = {zero := {X := 0, d := 0, d_squared' := _}, unique_to := λ (X : category_theory.differential_object C), {to_inhabited := {default := {f := 0, comm' := _}}, uniq := _}, unique_from := λ (X : category_theory.differential_object C), {to_inhabited := {default := {f := 0, comm' := _}}, uniq := _}}
@[instance]
@[instance]
def
category_theory.differential_object.category_theory.has_forget₂
(C : Type (u+1))
[category_theory.large_category C]
[category_theory.concrete_category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.has_shift C] :