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).obj self.obj

  The differential of a differential object.

• d_squared : CategoryTheory.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 {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) : CategoryTheory.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} [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).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).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 : X.Hom 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 : X.Hom 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).map self.f) = CategoryTheory.CategoryStruct.comp self.f Y.d

@[simp]

theorem CategoryTheory.DifferentialObject.Hom.comm {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 : X.Hom Y) : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).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 : X.Hom Y) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj Y.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp X.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).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) : X.Hom X

The identity morphism of a differential object.

Equations

• CategoryTheory.DifferentialObject.Hom.id X = { f := CategoryTheory.CategoryStruct.id X.obj, comm := ⋯ }

@[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 : X.Hom Y) (g : Y.Hom Z) : (f.comp 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 : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

The composition of morphisms of differential objects.

Equations

• f.comp g = { f := CategoryTheory.CategoryStruct.comp f.f g.f, comm := ⋯ }

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 ⋯

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.DifferentialObject.forget S C).Faithful

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.DifferentialObject.instZeroHom S C = { zero := { f := 0, comm := ⋯ } }

@[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.shiftFunctor C 1).PreservesZeroMorphisms] (P : CategoryTheory.DifferentialObject S C) (Q : CategoryTheory.DifferentialObject S C) : CategoryTheory.DifferentialObject.Hom.f 0 = 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.shiftFunctor C 1).PreservesZeroMorphisms] : 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 = { hom := f.hom.f, inv := f.inv.f, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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_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).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).inv.f = f.inv

@[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).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).hom.f = f.hom

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).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 = { hom := { f := f.hom, comm := hf }, inv := { f := f.inv, comm := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[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.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).d = CategoryTheory.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} [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.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) : ∀ {X Y : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y), ((CategoryTheory.Functor.mapDifferentialObject D F η hF).map f).f = F.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.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).obj = F.obj 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.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.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.shiftFunctor C 1).PreservesZeroMorphisms] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C)

Equations

• ⋯ = ⋯

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

• CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects S C = CategoryTheory.ConcreteCategory.mk ((CategoryTheory.DifferentialObject.forget S C).comp (CategoryTheory.forget C))

instance CategoryTheory.DifferentialObject.instHasForget₂ (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

• CategoryTheory.DifferentialObject.instHasForget₂ S C = { forget₂ := CategoryTheory.DifferentialObject.forget S C, forget_comp := ⋯ }

The category of differential objects itself has a shift functor.

@[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).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj

@[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).map f).f = (CategoryTheory.shiftFunctor C n).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).obj X).d = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (CategoryTheory.shiftComm X.obj 1 n).hom

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.DifferentialObject.shiftFunctor C m).comp (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_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

@[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

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.instHasShift {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.