DG functors

A dg functor is an object map together with a degree-preserving additive map on Hom-complexes that commutes with the differential and respects the identity and the graded composition.

The map is required to commute with the differential degreewise rather than to be packaged as a chain map: the composition of DGCategoryStruct is already stated degreewise, and mixing the two styles is what makes later simp sets fight each other.

structure CategoryTheory.DGFunctor (C : Type u) (D : Type u') [DGCategory C] [DGCategory D] : Type (max (max u u') v)

A dg functor between dg categories.

• obj : C → D

  The map on objects.

• map {X Y : C} (p : ℤ) : ↑((DGCategoryStruct.dgHom X Y).X p) →+ ↑((DGCategoryStruct.dgHom (self.obj X) (self.obj Y)).X p)

  The degree-preserving additive map on Hom-complexes.

• map_d {X Y : C} (p q : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (self.map q) ((AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d p q)) f) = (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom (self.obj X) (self.obj Y)).d p q)) ((self.map p) f)

  A dg functor commutes with the differential.

• map_id (X : C) : (self.map 0) (DGCategoryStruct.dgId X) = DGCategoryStruct.dgId (self.obj X)

  A dg functor preserves the identity.

• map_comp {X Y Z : C} (p q r : ℤ) (h : p + q = r) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (g : ↑((DGCategoryStruct.dgHom Y Z).X q)) : (self.map r) (((DGCategoryStruct.dgComp p q r h) f) g) = ((DGCategoryStruct.dgComp p q r h) ((self.map p) f)) ((self.map q) g)

  A dg functor preserves the graded composition.

def CategoryTheory.DGFunctor.id (C : Type u) [DGCategory C] : DGFunctor C C

The identity dg functor.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.id_map (C : Type u) [DGCategory C] {X✝ Y✝ : C} (x✝ : ℤ) : (id C).map x✝ = AddMonoidHom.id ↑((DGCategoryStruct.dgHom X✝ Y✝).X x✝)

@[simp]

theorem CategoryTheory.DGFunctor.id_obj (C : Type u) [DGCategory C] (X : C) : (id C).obj X = X

def CategoryTheory.DGFunctor.comp {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G : DGFunctor D E) : DGFunctor C E

Composition of dg functors.

Equations

• F.comp G = { obj := fun (X : C) => G.obj (F.obj X), map := fun {X Y : C} (p : ℤ) => (G.map p).comp (F.map p), map_d := ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.DGFunctor.comp_obj {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G : DGFunctor D E) (X : C) : (F.comp G).obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.DGFunctor.comp_map {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G : DGFunctor D E) {X✝ Y✝ : C} (p : ℤ) : (F.comp G).map p = (G.map p).comp (F.map p)

Strictness

Composition of dg functors is strictly associative and strictly unital: all three laws hold by rfl, because comp composes the object maps and the AddMonoidHoms directly and the remaining fields are proofs. Stating them is what lets a law about horizontally composed dg natural transformations be written down at all, since the two sides then have definitionally equal types.

@[simp]

theorem CategoryTheory.DGFunctor.id_comp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : (id C).comp F = F

@[simp]

theorem CategoryTheory.DGFunctor.comp_id {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : F.comp (id D) = F

theorem CategoryTheory.DGFunctor.comp_assoc {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {B : Type u'''} [DGCategory B] (F : DGFunctor C D) (G : DGFunctor D E) (H : DGFunctor E B) : (F.comp G).comp H = F.comp (G.comp H)