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

An isomorphism of differential objects can be constructed from an isomorphism of the underlying objects that commutes with the differentials.

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.