# 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, and zero morphisms and zero 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

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations