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.
- obj : C
The underlying object of a differential object.
- d : s.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj s.obj
The differential of a differential object.
- d_squared : CategoryTheory.CategoryStruct.comp s.d ((CategoryTheory.shiftFunctor C 1).map s.d) = 0
The differential
d
satisfies thatd² = 0
.
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
- f : X.obj ⟶ Y.obj
The morphism between underlying objects of the two differentiable objects.
- comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map s.f) = CategoryTheory.CategoryStruct.comp s.f Y.d
A morphism of differential objects is a morphism commuting with the differentials.
Instances For
The identity morphism of a differential object.
Instances For
The composition of morphisms of differential objects.
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
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
.
Instances For
The category of differential objects itself has a shift functor.
The shift functor on DifferentialObject S C
.
Instances For
The shift functor on DifferentialObject S C
is additive.
Instances For
The shift by zero is naturally isomorphic to the identity.