# 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.

structure CategoryTheory.DifferentialObject (S : Type u_1) [] (C : Type u) [] :
Type (max u v)
• obj : C

The underlying object of a differential object.

• d : s.obj ().obj s.obj

The differential of a differential object.

• d_squared : CategoryTheory.CategoryStruct.comp s.d (().map s.d) = 0

The differential d satisfies that d² = 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
@[simp]
theorem CategoryTheory.DifferentialObject.d_squared_assoc {S : Type u_1} [] {C : Type u} [] (self : ) {Z : C} (h : ().obj (().obj self.obj) Z) :
theorem CategoryTheory.DifferentialObject.Hom.ext {S : Type u_1} :
∀ {inst : } {C : Type u} {inst_1 : } {inst_2 : } {inst_3 : } {X Y : } (x y : ), x.f = y.fx = y
theorem CategoryTheory.DifferentialObject.Hom.ext_iff {S : Type u_1} :
∀ {inst : } {C : Type u} {inst_1 : } {inst_2 : } {inst_3 : } {X Y : } (x y : ), x = y x.f = y.f
structure CategoryTheory.DifferentialObject.Hom {S : Type u_1} [] {C : Type u} [] (X : ) (Y : ) :

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

Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.Hom.comm_assoc {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (self : ) {Z : C} (h : ().obj Y.obj Z) :
@[simp]
theorem CategoryTheory.DifferentialObject.Hom.id_f {S : Type u_1} [] {C : Type u} [] (X : ) :
def CategoryTheory.DifferentialObject.Hom.id {S : Type u_1} [] {C : Type u} [] (X : ) :

The identity morphism of a differential object.

Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.Hom.comp_f {S : Type u_1} [] {C : Type u} [] {X : } {Y : } {Z : } :
def CategoryTheory.DifferentialObject.Hom.comp {S : Type u_1} [] {C : Type u} [] {X : } {Y : } {Z : } :

The composition of morphisms of differential objects.

Instances For
theorem CategoryTheory.DifferentialObject.ext {S : Type u_1} [] {C : Type u} [] {A : } {B : } {f : A B} {g : A B} (w : autoParam (f.f = g.f) _auto✝) :
f = g
@[simp]
theorem CategoryTheory.DifferentialObject.id_f {S : Type u_1} [] {C : Type u} [] (X : ) :
@[simp]
theorem CategoryTheory.DifferentialObject.comp_f {S : Type u_1} [] {C : Type u} [] {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.DifferentialObject.eqToHom_f {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (h : X = Y) :
().f = CategoryTheory.eqToHom (_ : X.obj = Y.obj)

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

Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.zero_f {S : Type u_1} [] {C : Type u} [] (P : ) (Q : ) :
0.f = 0
@[simp]
theorem CategoryTheory.DifferentialObject.isoApp_inv {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X Y) :
= f.inv.f
@[simp]
theorem CategoryTheory.DifferentialObject.isoApp_hom {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X Y) :
= f.hom.f
def CategoryTheory.DifferentialObject.isoApp {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X Y) :
X.obj Y.obj

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

Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.isoApp_refl {S : Type u_1} [] {C : Type u} [] (X : ) :
@[simp]
theorem CategoryTheory.DifferentialObject.isoApp_symm {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X Y) :
@[simp]
theorem CategoryTheory.DifferentialObject.isoApp_trans {S : Type u_1} [] {C : Type u} [] {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.DifferentialObject.mkIso_hom_f {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X.obj Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d (().map f.hom) = ) :
().hom.f = f.hom
@[simp]
theorem CategoryTheory.DifferentialObject.mkIso_inv_f {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X.obj Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d (().map f.hom) = ) :
().inv.f = f.inv
def CategoryTheory.DifferentialObject.mkIso {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X.obj Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d (().map f.hom) = ) :
X Y

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

Instances For
@[simp]
theorem CategoryTheory.Functor.mapDifferentialObject_map_f {S : Type u_1} [] {C : Type u} [] (D : Type u') [] [] (F : ) (hF : ∀ (c c' : C), F.map 0 = 0) :
∀ {X Y : } (f : X Y), (().map f).f = F.map f.f
@[simp]
theorem CategoryTheory.Functor.mapDifferentialObject_obj_obj {S : Type u_1} [] {C : Type u} [] (D : Type u') [] [] (F : ) (hF : ∀ (c c' : C), F.map 0 = 0) (X : ) :
(().obj X).obj = F.obj X.obj
@[simp]
theorem CategoryTheory.Functor.mapDifferentialObject_obj_d {S : Type u_1} [] {C : Type u} [] (D : Type u') [] [] (F : ) (hF : ∀ (c c' : C), F.map 0 = 0) (X : ) :
(().obj X).d = CategoryTheory.CategoryStruct.comp (F.map X.d) (η.app X.obj)
def CategoryTheory.Functor.mapDifferentialObject {S : Type u_1} [] {C : Type u} [] (D : Type u') [] [] (F : ) (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 DifferentialObject S C ⥤ DifferentialObject S D.

Instances For

The category of differential objects itself has a shift functor.

@[simp]
theorem CategoryTheory.DifferentialObject.shiftFunctor_map_f {S : Type u_1} (C : Type u) [] (n : S) :
∀ {X Y : } (f : X Y), ().f = ().map f.f
@[simp]
theorem CategoryTheory.DifferentialObject.shiftFunctor_obj_d {S : Type u_1} (C : Type u) [] (n : S) (X : ) :
@[simp]
theorem CategoryTheory.DifferentialObject.shiftFunctor_obj_obj {S : Type u_1} (C : Type u) [] (n : S) (X : ) :
().obj = ().obj X.obj
def CategoryTheory.DifferentialObject.shiftFunctor {S : Type u_1} (C : Type u) [] (n : S) :

The shift functor on DifferentialObject S C.

Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f {S : Type u_1} (C : Type u) [] (m : S) (n : S) (X : ) :
(.app X).f = ().inv.app X.obj
@[simp]
theorem CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f {S : Type u_1} (C : Type u) [] (m : S) (n : S) (X : ) :
(.app X).f = ().hom.app X.obj
def CategoryTheory.DifferentialObject.shiftFunctorAdd {S : Type u_1} (C : Type u) [] (m : S) (n : S) :

The shift functor on DifferentialObject S C is additive.

Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.shiftZero_hom_app_f {S : Type u_1} (C : Type u) [] (X : ) :
(.app X).f = ().hom.app X.obj
@[simp]
theorem CategoryTheory.DifferentialObject.shiftZero_inv_app_f {S : Type u_1} (C : Type u) [] (X : ) :
(.app X).f = ().inv.app X.obj

The shift by zero is naturally isomorphic to the identity.

Instances For