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

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.

• obj : C

The underlying object of a differential object.

• d : self.obj .obj self.obj

The differential of a differential object.

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

The differential d satisfies that d² = 0.

Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.d_squared {S : Type u_1} [] {C : Type u} [] (self : ) :
CategoryTheory.CategoryStruct.comp self.d (.map self.d) = 0

The differential d satisfies that d² = 0.

@[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.Hom 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.Hom 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 {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (self : X.Hom Y) :
@[simp]
theorem CategoryTheory.DifferentialObject.Hom.comm_assoc {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (self : X.Hom Y) {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 : ) :
X.Hom X

The identity morphism of a differential object.

Equations
• = { f := , comm := }
Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.Hom.comp_f {S : Type u_1} [] {C : Type u} [] {X : } {Y : } {Z : } (f : X.Hom Y) (g : Y.Hom Z) :
(f.comp g).f =
def CategoryTheory.DifferentialObject.Hom.comp {S : Type u_1} [] {C : Type u} [] {X : } {Y : } {Z : } (f : X.Hom Y) (g : Y.Hom Z) :
X.Hom Z

The composition of morphisms of differential objects.

Equations
• f.comp g = { f := , comm := }
Instances For
Equations
• CategoryTheory.DifferentialObject.categoryOfDifferentialObjects =
theorem CategoryTheory.DifferentialObject.ext_iff {S : Type u_1} [] {C : Type u} [] {A : } {B : } {f : A B} {g : A B} :
f = g autoParam (f.f = g.f) _auto✝
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) :

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
instance CategoryTheory.DifferentialObject.forget_faithful (S : Type u_1) [] (C : Type u) [] :
.Faithful
Equations
• =
instance CategoryTheory.DifferentialObject.instZeroHom {S : Type u_1} [] {C : Type u} [] [.PreservesZeroMorphisms] {X : } {Y : } :
Zero (X Y)
Equations
• CategoryTheory.DifferentialObject.instZeroHom = { zero := { f := 0, comm := } }
@[simp]
theorem CategoryTheory.DifferentialObject.zero_f {S : Type u_1} [] {C : Type u} [] [.PreservesZeroMorphisms] (P : ) (Q : ) :
instance CategoryTheory.DifferentialObject.hasZeroMorphisms {S : Type u_1} [] {C : Type u} [] [.PreservesZeroMorphisms] :
Equations
• CategoryTheory.DifferentialObject.hasZeroMorphisms =
@[simp]
theorem CategoryTheory.DifferentialObject.isoApp_hom {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X Y) :
= f.hom.f
@[simp]
theorem CategoryTheory.DifferentialObject.isoApp_inv {S : Type u_1} [] {C : Type u} [] {X : } {Y : } (f : X Y) :
= f.inv.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.

Equations
• = { hom := f.hom.f, inv := f.inv.f, hom_inv_id := , inv_hom_id := }
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.

Equations
• = { hom := { f := f.hom, comm := hf }, inv := { f := f.inv, comm := }, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Functor.mapDifferentialObject_map_f {S : Type u_1} [] {C : Type u} [] (D : Type u') [] [] (F : ) (η : .comp F F.comp ) (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 : ) (η : .comp F F.comp ) (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 : ) (η : .comp F F.comp ) (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 : ) (η : .comp F F.comp ) (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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.DifferentialObject.hasZeroObject (S : Type u_1) [] (C : Type u) [] [.PreservesZeroMorphisms] :
Equations
• =
Equations
instance CategoryTheory.DifferentialObject.instHasForget₂ (S : Type u_1) [] (C : Type (u + 1)) [] :
Equations
• = { forget₂ := , forget_comp := }

The category of differential objects itself has a shift functor.

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

The shift functor on DifferentialObject S C.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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
@[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
def CategoryTheory.DifferentialObject.shiftFunctorAdd {S : Type u_1} (C : Type u) [] (m : S) (n : S) :

The shift functor on DifferentialObject S C is additive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.DifferentialObject.shiftZero_inv_app_f {S : Type u_1} (C : Type u) [] (X : ) :
(.app X).f = .inv.app X.obj
@[simp]
theorem CategoryTheory.DifferentialObject.shiftZero_hom_app_f {S : Type u_1} (C : Type u) [] (X : ) :
(.app X).f = .hom.app X.obj

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
Equations
• One or more equations did not get rendered due to their size.