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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.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).toPrefunctor.obj self.obj

  The differential of a differential object.

• d_squared : CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).toPrefunctor.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).toPrefunctor.obj ((CategoryTheory.shiftFunctor C 1).toPrefunctor.obj self.obj) ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).toPrefunctor.map self.d) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.DifferentialObject.Hom.ext {S : Type u_1} : ∀ {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} (x y : CategoryTheory.DifferentialObject.Hom X Y), x.f = y.f → x = y

theorem CategoryTheory.DifferentialObject.Hom.ext_iff {S : Type u_1} : ∀ {inst : AddMonoidWithOne S} {C : Type u} {inst_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} (x y : CategoryTheory.DifferentialObject.Hom X Y), x = y ↔ x.f = y.f

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

@[simp]

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

@[simp]

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

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

The identity morphism of a differential object.

Equations

• CategoryTheory.DifferentialObject.Hom.id X = CategoryTheory.DifferentialObject.Hom.mk (CategoryTheory.CategoryStruct.id X.obj)

@[simp]

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

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

The composition of morphisms of differential objects.

Equations

• CategoryTheory.DifferentialObject.Hom.comp f g = CategoryTheory.DifferentialObject.Hom.mk (CategoryTheory.CategoryStruct.comp f.f g.f)

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

Equations

• CategoryTheory.DifferentialObject.categoryOfDifferentialObjects = CategoryTheory.Category.mk

theorem CategoryTheory.DifferentialObject.ext {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {A : CategoryTheory.DifferentialObject S C} {B : CategoryTheory.DifferentialObject S C} {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} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.obj

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : CategoryTheory.Faithful (CategoryTheory.DifferentialObject.forget S C)) = (_ : CategoryTheory.Faithful (CategoryTheory.DifferentialObject.forget S C))

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

Equations

• CategoryTheory.DifferentialObject.instZeroHomDifferentialObjectToQuiverToCategoryStructCategoryOfDifferentialObjects S C = { zero := CategoryTheory.DifferentialObject.Hom.mk 0 }

@[simp]

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

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

Equations

• CategoryTheory.DifferentialObject.hasZeroMorphisms = CategoryTheory.Limits.HasZeroMorphisms.mk

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.DifferentialObject.isoApp f = CategoryTheory.Iso.mk f.hom.f f.inv.f

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.DifferentialObject.mkIso f hf = CategoryTheory.Iso.mk (CategoryTheory.DifferentialObject.Hom.mk f.hom) (CategoryTheory.DifferentialObject.Hom.mk f.inv)

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C)) = (_ : CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C))

instance CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.ConcreteCategory (CategoryTheory.DifferentialObject S C)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.DifferentialObject.instHasForget₂DifferentialObjectCategoryOfDifferentialObjectsConcreteCategoryOfDifferentialObjects (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.HasForget₂ (CategoryTheory.DifferentialObject S C) C

Equations

• One or more equations did not get rendered due to their size.

The category of differential objects itself has a shift functor.

@[simp]

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

@[simp]

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

@[simp]

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

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

The shift functor on DifferentialObject S C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m : S) (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m : S) (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj

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

The shift functor on DifferentialObject S C is additive.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

The shift by zero is naturally isomorphic to the identity.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.