Documentation

Mathlib.CategoryTheory.DifferentialObject

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 : obj ⟶ obj⟦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.

A differential object in a category with zero morphisms and a shift is an object obj equipped with a morphism d : obj ⟶ obj⟦1⟧, such that d^2 = 0.

Instances For

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

    Instances For

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

      Instances For

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

        Instances For

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

          Instances For

            The category of differential objects itself has a shift functor.