mathlib3 documentation


Differential objects in a category. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, ext]

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

Instances for category_theory.differential_object.hom
  • category_theory.differential_object.hom.has_sizeof_inst

The composition of morphisms of differential objects.


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

Instances for category_theory.differential_object.forget

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


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


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.


The category of differential objects itself has a shift functor.