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) [AddMonoidWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] : 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 ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj

  The differential of a differential object.

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

  The differential d satisfies that d² = 0.

@[simp]

theorem CategoryTheory.DifferentialObject.d_squared_assoc {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (self : DifferentialObject S C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) ⟶ Z) : CategoryStruct.comp self.d (CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.d) h) = CategoryStruct.comp 0 h

The differential d satisfies that d² = 0.

structure CategoryTheory.DifferentialObject.Hom {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (X Y : DifferentialObject S C) : Type v

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

• f : X.obj ⟶ Y.obj

  The morphism between underlying objects of the two differentiable objects.

• comm : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) = CategoryStruct.comp self.f Y.d

theorem CategoryTheory.DifferentialObject.Hom.ext {S : Type u_1} {inst✝ : AddMonoidWithOne S} {C : Type u} {inst✝¹ : Category.{v, u} C} {inst✝² : Limits.HasZeroMorphisms C} {inst✝³ : HasShift C S} {X Y : DifferentialObject S C} {x y : X.Hom Y} (f : x.f = y.f) : x = y

theorem CategoryTheory.DifferentialObject.Hom.ext_iff {S : Type u_1} {inst✝ : AddMonoidWithOne S} {C : Type u} {inst✝¹ : Category.{v, u} C} {inst✝² : Limits.HasZeroMorphisms C} {inst✝³ : HasShift C S} {X Y : DifferentialObject S C} {x y : X.Hom Y} : x = y ↔ x.f = y.f

@[simp]

theorem CategoryTheory.DifferentialObject.Hom.comm_assoc {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (self : X.Hom Y) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj Y.obj ⟶ Z) : CategoryStruct.comp X.d (CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.f) h) = CategoryStruct.comp self.f (CategoryStruct.comp Y.d h)

def CategoryTheory.DifferentialObject.Hom.id {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (X : DifferentialObject S C) : X.Hom X

The identity morphism of a differential object.

@[simp]

theorem CategoryTheory.DifferentialObject.Hom.id_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (X : DifferentialObject S C) : (id X).f = CategoryStruct.id X.obj

def CategoryTheory.DifferentialObject.Hom.comp {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y Z : DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

The composition of morphisms of differential objects.

@[simp]

theorem CategoryTheory.DifferentialObject.Hom.comp_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y Z : DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).f = CategoryStruct.comp f.f g.f

@[implicit_reducible]

instance CategoryTheory.DifferentialObject.categoryOfDifferentialObjects {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] : Category.{v, max u v} (DifferentialObject S C)

theorem CategoryTheory.DifferentialObject.ext {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {A B : DifferentialObject S C} {f g : A ⟶ B} (w : f.f = g.f := by cat_disch) : f = g

theorem CategoryTheory.DifferentialObject.ext_iff {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {A B : DifferentialObject S C} {f g : A ⟶ B} : f = g ↔ autoParam (f.f = g.f) ext._auto_1

@[simp]

theorem CategoryTheory.DifferentialObject.id_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (X : DifferentialObject S C) : (CategoryStruct.id X).f = CategoryStruct.id X.obj

@[simp]

theorem CategoryTheory.DifferentialObject.comp_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y Z : DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).f = CategoryStruct.comp f.f g.f

@[simp]

theorem CategoryTheory.DifferentialObject.eqToHom_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (h : X = Y) : (eqToHom h).f = eqToHom ⋯

def CategoryTheory.DifferentialObject.forget (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] : Functor (DifferentialObject S C) C

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

instance CategoryTheory.DifferentialObject.forget_faithful (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] : (forget S C).Faithful

@[implicit_reducible]

instance CategoryTheory.DifferentialObject.instZeroHom {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] {X Y : DifferentialObject S C} : Zero (X ⟶ Y)

@[simp]

theorem CategoryTheory.DifferentialObject.zero_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] (P Q : DifferentialObject S C) : Hom.f 0 = 0

@[implicit_reducible]

instance CategoryTheory.DifferentialObject.hasZeroMorphisms {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : Limits.HasZeroMorphisms (DifferentialObject S C)

def CategoryTheory.DifferentialObject.isoApp {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (f : X ≅ Y) : X.obj ≅ Y.obj

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

@[simp]

theorem CategoryTheory.DifferentialObject.isoApp_hom {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (f : X ≅ Y) : (isoApp f).hom = f.hom.f

@[simp]

theorem CategoryTheory.DifferentialObject.isoApp_inv {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (f : X ≅ Y) : (isoApp f).inv = f.inv.f

@[simp]

theorem CategoryTheory.DifferentialObject.isoApp_refl {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (X : DifferentialObject S C) : isoApp (Iso.refl X) = Iso.refl X.obj

@[simp]

theorem CategoryTheory.DifferentialObject.isoApp_symm {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (f : X ≅ Y) : isoApp f.symm = (isoApp f).symm

@[simp]

theorem CategoryTheory.DifferentialObject.isoApp_trans {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y Z : DifferentialObject S C} (f : X ≅ Y) (g : Y ≅ Z) : isoApp (f ≪≫ g) = isoApp f ≪≫ isoApp g

def CategoryTheory.DifferentialObject.mkIso {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryStruct.comp 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.

@[simp]

theorem CategoryTheory.DifferentialObject.mkIso_hom_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryStruct.comp f.hom Y.d) : (mkIso f hf).hom.f = f.hom

@[simp]

theorem CategoryTheory.DifferentialObject.mkIso_inv_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] {X Y : DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryStruct.comp f.hom Y.d) : (mkIso f hf).inv.f = f.inv

def CategoryTheory.Functor.mapDifferentialObject {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (D : Type u') [Category.{v', u'} D] [Limits.HasZeroMorphisms D] [HasShift D S] (F : Functor C D) (η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) : Functor (DifferentialObject S C) (DifferentialObject S D)

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.

@[simp]

theorem CategoryTheory.Functor.mapDifferentialObject_obj_obj {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (D : Type u') [Category.{v', u'} D] [Limits.HasZeroMorphisms D] [HasShift D S] (F : Functor C D) (η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : DifferentialObject S C) : ((mapDifferentialObject D F η hF).obj X).obj = F.obj X.obj

@[simp]

theorem CategoryTheory.Functor.mapDifferentialObject_obj_d {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (D : Type u') [Category.{v', u'} D] [Limits.HasZeroMorphisms D] [HasShift D S] (F : Functor C D) (η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : DifferentialObject S C) : ((mapDifferentialObject D F η hF).obj X).d = CategoryStruct.comp (F.map X.d) (η.app X.obj)

@[simp]

theorem CategoryTheory.Functor.mapDifferentialObject_map_f {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (D : Type u') [Category.{v', u'} D] [Limits.HasZeroMorphisms D] [HasShift D S] (F : Functor C D) (η : (shiftFunctor C 1).comp F ⟶ F.comp (shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) {X✝ Y✝ : DifferentialObject S C} (f : X✝ ⟶ Y✝) : ((mapDifferentialObject D F η hF).map f).f = F.map f.f

instance CategoryTheory.DifferentialObject.hasZeroObject (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [Limits.HasZeroMorphisms C] [HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : Limits.HasZeroObject (DifferentialObject S C)

@[reducible, inline]

abbrev CategoryTheory.DifferentialObject.HomSubtype (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [LargeCategory C] [Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [HasShift C S] (X Y : DifferentialObject S C) : Type u_2

The type of C-morphisms that can be lifted back to morphisms in the category DifferentialObject.

@[implicit_reducible]

instance CategoryTheory.DifferentialObject.instFunLikeHomSubtypeObj (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [LargeCategory C] [Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [HasShift C S] (X Y : DifferentialObject S C) : FunLike (HomSubtype S C X Y) (CC X.obj) (CC Y.obj)

@[implicit_reducible]

instance CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [LargeCategory C] [Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [HasShift C S] : ConcreteCategory (DifferentialObject S C) (HomSubtype S C)

@[implicit_reducible]

instance CategoryTheory.DifferentialObject.instHasForget₂HomSubtypeObj (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [LargeCategory C] [Limits.HasZeroMorphisms C] {FC : C → C → Type u_2} {CC : C → Type u_3} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [HasShift C S] : HasForget₂ (DifferentialObject S C) C

The category of differential objects itself has a shift functor.

def CategoryTheory.DifferentialObject.shiftFunctor {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (n : S) : Functor (DifferentialObject S C) (DifferentialObject S C)

The shift functor on DifferentialObject S C.

@[simp]

theorem CategoryTheory.DifferentialObject.shiftFunctor_obj_d {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (n : S) (X : DifferentialObject S C) : ((shiftFunctor C n).obj X).d = CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (shiftComm X.obj 1 n).hom

@[simp]

theorem CategoryTheory.DifferentialObject.shiftFunctor_map_f {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (n : S) {X✝ Y✝ : DifferentialObject S C} (f : X✝ ⟶ Y✝) : ((shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f

@[simp]

theorem CategoryTheory.DifferentialObject.shiftFunctor_obj_obj {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (n : S) (X : DifferentialObject S C) : ((shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj

def CategoryTheory.DifferentialObject.shiftFunctorAdd {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (m n : S) : shiftFunctor C (m + n) ≅ (shiftFunctor C m).comp (shiftFunctor C n)

The shift functor on DifferentialObject S C is additive.

@[simp]

theorem CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (m n : S) (X : DifferentialObject S C) : ((shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj

@[simp]

theorem CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (m n : S) (X : DifferentialObject S C) : ((shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj

def CategoryTheory.DifferentialObject.shiftZero {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] : shiftFunctor C 0 ≅ Functor.id (DifferentialObject S C)

The shift by zero is naturally isomorphic to the identity.

@[simp]

theorem CategoryTheory.DifferentialObject.shiftZero_hom_app_f {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (X : DifferentialObject S C) : ((shiftZero C).hom.app X).f = (shiftFunctorZero C S).hom.app X.obj

@[simp]

theorem CategoryTheory.DifferentialObject.shiftZero_inv_app_f {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] (X : DifferentialObject S C) : ((shiftZero C).inv.app X).f = (shiftFunctorZero C S).inv.app X.obj

@[implicit_reducible]

instance CategoryTheory.DifferentialObject.instHasShift {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [HasShift C S] : HasShift (DifferentialObject S C) S