# mathlib3documentation

category_theory.differential_object

# 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]
structure category_theory.differential_object (C : Type u)  :
Type (max u v)
• X : C
• d : self.X self.X
• d_squared' : self.d self.d = 0 . "obviously"

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.

Instances for category_theory.differential_object
theorem category_theory.differential_object.hom.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_zero_morphisms C} {_inst_3 : } (x y : X.hom Y) :
x = y x.f = y.f
theorem category_theory.differential_object.hom.ext {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_zero_morphisms C} {_inst_3 : } (x y : X.hom Y) (h : x.f = y.f) :
x = y
@[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
@[simp]
theorem category_theory.differential_object.hom.comm {C : Type u} (self : X.hom Y) :
X.d self.f = self.f Y.d
@[simp]
theorem category_theory.differential_object.hom.comm_assoc {C : Type u} (self : X.hom Y) {X' : C} (f' : Y.X X') :
X.d self.f f' = self.f Y.d f'
@[simp]

The identity morphism of a differential object.

Equations

The composition of morphisms of differential objects.

Equations
@[simp]
theorem category_theory.differential_object.hom.comp_f {C : Type u} {X Y Z : category_theory.differential_object C} (f : X.hom Y) (g : Y.hom Z) :
(f.comp g).f = f.f g.f
@[protected, instance]
Equations
@[simp]
@[simp]
theorem category_theory.differential_object.comp_f {C : Type u} {X Y Z : category_theory.differential_object C} (f : X Y) (g : Y Z) :
(f g).f = f.f g.f
@[simp]

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

Equations
Instances for category_theory.differential_object.forget
@[protected, instance]
@[protected, instance]
Equations
@[simp]

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

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem category_theory.differential_object.mk_iso_hom_f {C : Type u} (f : X.X Y.X) (hf : X.d f.hom = f.hom Y.d) :
@[simp]
theorem category_theory.differential_object.mk_iso_inv_f {C : Type u} (f : X.X Y.X) (hf : X.d f.hom = f.hom Y.d) :
def category_theory.differential_object.mk_iso {C : Type u} (f : X.X Y.X) (hf : X.d f.hom = f.hom Y.d) :
X Y

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

Equations
@[simp]
theorem category_theory.functor.map_differential_object_obj_d {C : Type u} (D : Type u') (F : C D) (η : ) (hF : (c c' : C), F.map 0 = 0)  :
.obj X).d = F.map X.d η.app X.X
@[simp]
theorem category_theory.functor.map_differential_object_map_f {C : Type u} (D : Type u') (F : C D) (η : ) (hF : (c c' : C), F.map 0 = 0) (f : X Y) :
.map f).f = F.map f.f
def category_theory.functor.map_differential_object {C : Type u} (D : Type u') (F : C D) (η : ) (hF : (c c' : C), F.map 0 = 0) :

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
@[simp]
theorem category_theory.functor.map_differential_object_obj_X {C : Type u} (D : Type u') (F : C D) (η : ) (hF : (c c' : C), F.map 0 = 0)  :
.obj X).X = F.obj X.X
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations

The category of differential objects itself has a shift functor.

@[simp]
@[simp]

The shift functor on differential_object C.

Equations

The shift functor on differential_object C is additive.

Equations
@[simp]

The shift by zero is naturally isomorphic to the identity.

Equations
@[simp]
@[protected, instance]
Equations