mathlib documentation

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]

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]

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

The composition of morphisms of differential objects.

Equations

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

Equations

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

The category of differential objects itself has a shift functor.