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
    theorem CategoryTheory.DifferentialObject.Hom.ext {S : Type u_1} :
    ∀ {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} (x y : X.Hom Y), x.f = y.fx = y

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

    Instances For

      The composition of morphisms of differential objects.

      Equations
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

          Equations
          Instances For

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

            Equations
            Instances For

              A functor F : C ⥤ D which commutes with shift functors on C and D and preserves zero morphisms can be lifted to a functor DifferentialObject S C ⥤ DifferentialObject S D.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The category of differential objects itself has a shift functor.

                The shift by zero is naturally isomorphic to the identity.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For