# mathlibdocumentation

category_theory.differential_object

# 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, zero morphisms and zero objects, and the shift functor on differential objects.

@[nolint]
structure category_theory.differential_object (C : Type u)  :
Type (max u v)

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.

@[simp]
theorem category_theory.differential_object.d_squared {C : Type u}  :
c.d c.d = 0
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 : X.hom Y) (h : x.f = y.f) :
x = y
@[nolint, ext]
structure category_theory.differential_object.hom {C : Type u}  :
Type v

A morphism of differential objects is a morphism commuting with the differentials.

@[simp]
theorem category_theory.differential_object.hom.comm {C : Type u} (c : X.hom Y) :
X.d c.f = c.f Y.d
@[simp]
theorem category_theory.differential_object.hom.comm_assoc {C : Type u} (c : X.hom Y) {X' : C} (f' : Y.X X') :
X.d c.f f' = c.f Y.d f'
@[simp]

The identity morphism of a differential object.

Equations
def category_theory.differential_object.hom.comp {C : Type u} {X Y Z : category_theory.differential_object C} (f : X.hom Y) (g : Y.hom Z) :
X.hom Z

The composition of morphisms of differential objects.

Equations
@[simp]
theorem category_theory.differential_object.hom.comp_f {C : Type u} {X Y Z : category_theory.differential_object C} (f : X.hom Y) (g : Y.hom Z) :
(f.comp g).f = f.f g.f
@[instance]
Equations
@[simp]
theorem category_theory.differential_object.id_f {C : Type u}  :
(𝟙 X).f = 𝟙 X.X
@[simp]
theorem category_theory.differential_object.comp_f {C : Type u} {X Y Z : category_theory.differential_object C} (f : X Y) (g : Y Z) :
(f g).f = f.f g.f

The forgetful functor taking a differential object to its underlying object.

Equations
@[instance]
@[instance]
Equations
@[simp]
theorem category_theory.differential_object.zero_f {C : Type u}  :
0.f = 0
def category_theory.differential_object.iso_app {C : Type u} (f : X Y) :
X.X Y.X

An isomorphism of differential objects gives an isomorphism of the underlying objects.

Equations
@[simp]
theorem category_theory.differential_object.iso_app_inv {C : Type u} (f : X Y) :
@[simp]
theorem category_theory.differential_object.iso_app_hom {C : Type u} (f : X Y) :
@[simp]
@[simp]
@[simp]
theorem category_theory.differential_object.iso_app_trans {C : Type u} {X Y Z : category_theory.differential_object C} (f : X Y) (g : Y Z) :
@[simp]
theorem category_theory.functor.map_differential_object_obj_d {C : Type u} (D : Type u') (F : C D) (η : ) (hF : ∀ (c c' : C), F.map 0 = 0)  :
.obj X).d = F.map X.d η.app X.X
@[simp]
theorem category_theory.functor.map_differential_object_map_f {C : Type u} (D : Type u') (F : C D) (η : ) (hF : ∀ (c c' : C), F.map 0 = 0) (f : X Y) :
.map f).f = F.map f.f
def category_theory.functor.map_differential_object {C : Type u} (D : Type u') (F : C D) (η : ) (hF : ∀ (c c' : C), F.map 0 = 0) :

A functor F : C ⥤ D which commutes with shift functors on C and D and preserves zero morphisms can be lifted to a functor differential_object C ⥤ differential_object D.

Equations
@[simp]
theorem category_theory.functor.map_differential_object_obj_X {C : Type u} (D : Type u') (F : C D) (η : ) (hF : ∀ (c c' : C), F.map 0 = 0)  :
.obj X).X = F.obj X.X
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations

The category of differential objects itself has a shift functor.

@[simp]
@[simp]
@[simp]

The shift functor on differential_object C.

Equations
@[simp]
@[simp]

The inverse shift functor on differential C, at the level of objects.

Equations

The inverse shift functor on differential C.

Equations
@[simp]
theorem category_theory.differential_object.shift_inverse_map_f (C : Type u) (f : X Y) :
= ^ -1).functor.map f.f
@[simp]
@[simp]

The unit for the shift functor on differential_object C.

Equations

The inverse of the unit for the shift functor on differential_object C.

Equations
@[simp]
@[simp]

The unit isomorphism for the shift functor on differential_object C.

Equations
@[simp]

The counit for the shift functor on differential_object C.

Equations
@[simp]
@[simp]

The inverse of the counit for the shift functor on differential_object C.

Equations
@[simp]

The counit isomorphism for the shift functor on differential_object C.

Equations
@[simp]
@[instance]

The category of differential objects in C itself has a shift functor.

Equations