Functors from a category to a category with a shift

Given a category C, and a category D equipped with a shift by a monoid A, we define a structure SingleFunctors C D A which contains the data of functors functor a : C ⥤ D for all a : A and isomorphisms shiftIso n a a' h : functor a' ⋙ shiftFunctor D n ≅ functor a whenever n + a = a'. These isomorphisms should satisfy certain compatibilities with respect to the shift on D.

This notion is similar to Functor.ShiftSequence which can be used in order to attach shifted versions of a homological functor D ⥤ C with D a triangulated category and C an abelian category. However, the definition SingleFunctors is for functors in the other direction: it is meant to ease the formalization of the compatibilities with shifts of the functors C ⥤ CochainComplex C ℤ (or C ⥤ DerivedCategory C (TODO)) which sends an object X : C to a complex where X sits in a single degree.

structure CategoryTheory.SingleFunctors (C : Type u_1) (D : Type u_2) [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] (A : Type u_5) [AddMonoid A] [HasShift D A] : Type (max (max (max (max u_1 u_2) u_5) u_6) u_7)

The type of families of functors A → C ⥤ D which are compatible with the shift by A on the category D.

• functor (a : A) : Functor C D

  a family of functors C ⥤ D indexed by the elements of the additive monoid A

• shiftIso (n a a' : A) (ha' : n + a = a') : (self.functor a').comp (shiftFunctor D n) ≅ self.functor a

  the isomorphism functor a' ⋙ shiftFunctor D n ≅ functor a when n + a = a'

• shiftIso_zero (a : A) : self.shiftIso 0 a a ⋯ = isoWhiskerLeft (self.functor a) (shiftFunctorZero D A)

  shiftIso 0 is the obvious isomorphism.

• shiftIso_add (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') : self.shiftIso (m + n) a a'' ⋯ = isoWhiskerLeft (self.functor a'') (shiftFunctorAdd D m n) ≪≫ ((self.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫ isoWhiskerRight (self.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ self.shiftIso n a a' ha'

  shiftIso (m + n) is determined by shiftIso m and shiftIso n.

theorem CategoryTheory.SingleFunctors.shiftIso_add_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' ⋯).hom.app X = CategoryStruct.comp ((shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X)) (CategoryStruct.comp ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ((F.shiftIso n a a' ha').hom.app X))

theorem CategoryTheory.SingleFunctors.shiftIso_add_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' ⋯).inv.app X = CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryStruct.comp ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X)) ((shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)))

theorem CategoryTheory.SingleFunctors.shiftIso_add' {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (n m mn : A) (hnm : m + n = mn) (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') : F.shiftIso mn a a'' ⋯ = isoWhiskerLeft (F.functor a'') (shiftFunctorAdd' D m n mn hnm) ≪≫ ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫ isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'

theorem CategoryTheory.SingleFunctors.shiftIso_add'_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (n m mn : A) (hnm : m + n = mn) (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso mn a a'' ⋯).hom.app X = CategoryStruct.comp ((shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X)) (CategoryStruct.comp ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ((F.shiftIso n a a' ha').hom.app X))

theorem CategoryTheory.SingleFunctors.shiftIso_add'_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (n m mn : A) (hnm : m + n = mn) (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso mn a a'' ⋯).inv.app X = CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryStruct.comp ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X)) ((shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X)))

@[simp]

theorem CategoryTheory.SingleFunctors.shiftIso_zero_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (a : A) (X : C) : (F.shiftIso 0 a a ⋯).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)

@[simp]

theorem CategoryTheory.SingleFunctors.shiftIso_zero_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (a : A) (X : C) : (F.shiftIso 0 a a ⋯).inv.app X = (shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)

structure CategoryTheory.SingleFunctors.Hom {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F G : SingleFunctors C D A) : Type (max (max u_1 u_5) u_7)

The morphisms in the category SingleFunctors C D A

• hom (a : A) : F.functor a ⟶ G.functor a

  a family of natural transformations F.functor a ⟶ G.functor a

• comm (n a a' : A) (ha' : n + a = a') : CategoryStruct.comp (F.shiftIso n a a' ha').hom (self.hom a) = CategoryStruct.comp (whiskerRight (self.hom a') (shiftFunctor D n)) (G.shiftIso n a a' ha').hom

theorem CategoryTheory.SingleFunctors.Hom.ext {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_6, u_1} C} {inst✝¹ : Category.{u_7, u_2} D} {A : Type u_5} {inst✝² : AddMonoid A} {inst✝³ : HasShift D A} {F G : SingleFunctors C D A} {x y : F.Hom G} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.SingleFunctors.Hom.comm_assoc {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (self : F.Hom G) (n a a' : A) (ha' : n + a = a') {Z : Functor C D} (h : G.functor a ⟶ Z) : CategoryStruct.comp (F.shiftIso n a a' ha').hom (CategoryStruct.comp (self.hom a) h) = CategoryStruct.comp (whiskerRight (self.hom a') (shiftFunctor D n)) (CategoryStruct.comp (G.shiftIso n a a' ha').hom h)

def CategoryTheory.SingleFunctors.Hom.id {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) : F.Hom F

The identity morphism in SingleFunctors C D A.

Equations

• CategoryTheory.SingleFunctors.Hom.id F = { hom := fun (x : A) => CategoryTheory.CategoryStruct.id (F.functor x), comm := ⋯ }

@[simp]

theorem CategoryTheory.SingleFunctors.Hom.id_hom {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (x✝ : A) : (id F).hom x✝ = CategoryStruct.id (F.functor x✝)

def CategoryTheory.SingleFunctors.Hom.comp {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G H : SingleFunctors C D A} (α : F.Hom G) (β : G.Hom H) : F.Hom H

The composition of morphisms in SingleFunctors C D A.

Equations

• α.comp β = { hom := fun (a : A) => CategoryTheory.CategoryStruct.comp (α.hom a) (β.hom a), comm := ⋯ }

@[simp]

theorem CategoryTheory.SingleFunctors.Hom.comp_hom {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G H : SingleFunctors C D A} (α : F.Hom G) (β : G.Hom H) (a : A) : (α.comp β).hom a = CategoryStruct.comp (α.hom a) (β.hom a)

instance CategoryTheory.SingleFunctors.instCategory {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] : Category.{max (max u_1 u_5) u_7, max (max (max (max u_7 u_6) u_5) u_2) u_1} (SingleFunctors C D A)

Equations

• CategoryTheory.SingleFunctors.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.SingleFunctors.id_hom {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (F : SingleFunctors C D A) (a : A) : (CategoryStruct.id F).hom a = CategoryStruct.id (F.functor a)

@[simp]

theorem CategoryTheory.SingleFunctors.comp_hom {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G H : SingleFunctors C D A} (f : F ⟶ G) (g : G ⟶ H) (a : A) : (CategoryStruct.comp f g).hom a = CategoryStruct.comp (f.hom a) (g.hom a)

theorem CategoryTheory.SingleFunctors.comp_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G H : SingleFunctors C D A} (f : F ⟶ G) (g : G ⟶ H) (a : A) {Z : Functor C D} (h : H.functor a ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp f g).hom a) h = CategoryStruct.comp (f.hom a) (CategoryStruct.comp (g.hom a) h)

theorem CategoryTheory.SingleFunctors.hom_ext {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (f g : F ⟶ G) (h : f.hom = g.hom) : f = g

def CategoryTheory.SingleFunctors.isoMk {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (iso : (a : A) → F.functor a ≅ G.functor a) (comm : ∀ (n a a' : A) (ha' : n + a = a'), CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom = CategoryStruct.comp (whiskerRight (iso a').hom (shiftFunctor D n)) (G.shiftIso n a a' ha').hom) : F ≅ G

Construct an isomorphism in SingleFunctors C D A by giving level-wise isomorphisms and checking compatibility only in the forward direction.

Equations

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

@[simp]

theorem CategoryTheory.SingleFunctors.isoMk_hom_hom {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (iso : (a : A) → F.functor a ≅ G.functor a) (comm : ∀ (n a a' : A) (ha' : n + a = a'), CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom = CategoryStruct.comp (whiskerRight (iso a').hom (shiftFunctor D n)) (G.shiftIso n a a' ha').hom) (a : A) : (isoMk iso comm).hom.hom a = (iso a).hom

@[simp]

theorem CategoryTheory.SingleFunctors.isoMk_inv_hom {C : Type u_1} {D : Type u_2} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (iso : (a : A) → F.functor a ≅ G.functor a) (comm : ∀ (n a a' : A) (ha' : n + a = a'), CategoryStruct.comp (F.shiftIso n a a' ha').hom (iso a).hom = CategoryStruct.comp (whiskerRight (iso a').hom (shiftFunctor D n)) (G.shiftIso n a a' ha').hom) (a : A) : (isoMk iso comm).inv.hom a = (iso a).inv

def CategoryTheory.SingleFunctors.evaluation (C : Type u_1) (D : Type u_2) [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (a : A) : Functor (SingleFunctors C D A) (Functor C D)

The evaluation SingleFunctors C D A ⥤ C ⥤ D for some a : A.

Equations

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

@[simp]

theorem CategoryTheory.SingleFunctors.evaluation_obj (C : Type u_1) (D : Type u_2) [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (a : A) (F : SingleFunctors C D A) : (evaluation C D a).obj F = F.functor a

@[simp]

theorem CategoryTheory.SingleFunctors.evaluation_map (C : Type u_1) (D : Type u_2) [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] (a : A) {x✝ x✝¹ : SingleFunctors C D A} (φ : x✝ ⟶ x✝¹) : (evaluation C D a).map φ = φ.hom a

@[simp]

theorem CategoryTheory.SingleFunctors.hom_inv_id_hom {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) : CategoryStruct.comp (e.hom.hom n) (e.inv.hom n) = CategoryStruct.id (F.functor n)

@[simp]

theorem CategoryTheory.SingleFunctors.hom_inv_id_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) {Z : Functor C D} (h : F.functor n ⟶ Z) : CategoryStruct.comp (e.hom.hom n) (CategoryStruct.comp (e.inv.hom n) h) = h

@[simp]

theorem CategoryTheory.SingleFunctors.inv_hom_id_hom {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) : CategoryStruct.comp (e.inv.hom n) (e.hom.hom n) = CategoryStruct.id (G.functor n)

@[simp]

theorem CategoryTheory.SingleFunctors.inv_hom_id_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) {Z : Functor C D} (h : G.functor n ⟶ Z) : CategoryStruct.comp (e.inv.hom n) (CategoryStruct.comp (e.hom.hom n) h) = h

@[simp]

theorem CategoryTheory.SingleFunctors.hom_inv_id_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) : CategoryStruct.comp ((e.hom.hom n).app X) ((e.inv.hom n).app X) = CategoryStruct.id ((F.functor n).obj X)

@[simp]

theorem CategoryTheory.SingleFunctors.hom_inv_id_hom_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) {Z : D} (h : (F.functor n).obj X ⟶ Z) : CategoryStruct.comp ((e.hom.hom n).app X) (CategoryStruct.comp ((e.inv.hom n).app X) h) = h

@[simp]

theorem CategoryTheory.SingleFunctors.inv_hom_id_hom_app {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) : CategoryStruct.comp ((e.inv.hom n).app X) ((e.hom.hom n).app X) = CategoryStruct.id ((G.functor n).obj X)

@[simp]

theorem CategoryTheory.SingleFunctors.inv_hom_id_hom_app_assoc {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) {Z : D} (h : (G.functor n).obj X ⟶ Z) : CategoryStruct.comp ((e.inv.hom n).app X) (CategoryStruct.comp ((e.hom.hom n).app X) h) = h

instance CategoryTheory.SingleFunctors.instIsIsoFunctorHom {C : Type u_1} {D : Type u_2} [Category.{u_7, u_1} C] [Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [HasShift D A] {F G : SingleFunctors C D A} (f : F ⟶ G) [IsIso f] (n : A) : IsIso (f.hom n)

def CategoryTheory.SingleFunctors.postcomp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C D A) (G : Functor D E) [G.CommShift A] : SingleFunctors C E A

Given F : SingleFunctors C D A, and a functor G : D ⥤ E which commutes with the shift by A, this is the "composition" of F and G in SingleFunctors C E A.

Equations

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

@[simp]

theorem CategoryTheory.SingleFunctors.postcomp_functor {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C D A) (G : Functor D E) [G.CommShift A] (a : A) : (F.postcomp G).functor a = (F.functor a).comp G

@[simp]

theorem CategoryTheory.SingleFunctors.postcomp_shiftIso_inv_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C D A) (G : Functor D E) [G.CommShift A] (n a a' : A) (ha' : n + a = a') (X : C) : ((F.postcomp G).shiftIso n a a' ha').inv.app X = CategoryStruct.comp (G.map ((F.shiftIso n a a' ha').inv.app X)) ((G.commShiftIso n).hom.app ((F.functor a').obj X))

@[simp]

theorem CategoryTheory.SingleFunctors.postcomp_shiftIso_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C D A) (G : Functor D E) [G.CommShift A] (n a a' : A) (ha' : n + a = a') (X : C) : ((F.postcomp G).shiftIso n a a' ha').hom.app X = CategoryStruct.comp ((G.commShiftIso n).inv.app ((F.functor a').obj X)) (G.map ((F.shiftIso n a a' ha').hom.app X))

def CategoryTheory.SingleFunctors.postcompFunctor (C : Type u_1) {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] (A : Type u_5) [AddMonoid A] [HasShift D A] [HasShift E A] (G : Functor D E) [G.CommShift A] : Functor (SingleFunctors C D A) (SingleFunctors C E A)

The functor SingleFunctors C D A ⥤ SingleFunctors C E A given by the postcomposition by a functor G : D ⥤ E which commutes with the shift.

Equations

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

def CategoryTheory.SingleFunctors.postcompPostcompIso {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] [Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] [HasShift E' A] (F : SingleFunctors C D A) (G : Functor D E) (G' : Functor E E') [G.CommShift A] [G'.CommShift A] : (F.postcomp G).postcomp G' ≅ F.postcomp (G.comp G')

The canonical isomorphism (F.postcomp G).postcomp G' ≅ F.postcomp (G ⋙ G').

Equations

• F.postcompPostcompIso G G' = CategoryTheory.SingleFunctors.isoMk (fun (x : A) => (F.functor x).associator G G') ⋯

@[simp]

theorem CategoryTheory.SingleFunctors.postcompPostcompIso_hom_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] [Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] [HasShift E' A] (F : SingleFunctors C D A) (G : Functor D E) (G' : Functor E E') [G.CommShift A] [G'.CommShift A] (a : A) (x✝ : C) : ((F.postcompPostcompIso G G').hom.hom a).app x✝ = CategoryStruct.id (G'.obj (G.obj ((F.functor a).obj x✝)))

@[simp]

theorem CategoryTheory.SingleFunctors.postcompPostcompIso_inv_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] [Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] [HasShift E' A] (F : SingleFunctors C D A) (G : Functor D E) (G' : Functor E E') [G.CommShift A] [G'.CommShift A] (a : A) (x✝ : C) : ((F.postcompPostcompIso G G').inv.hom a).app x✝ = CategoryStruct.id (G'.obj (G.obj ((F.functor a).obj x✝)))

def CategoryTheory.SingleFunctors.postcompIsoOfIso {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C D A) {G G' : Functor D E} (e : G ≅ G') [G.CommShift A] [G'.CommShift A] [NatTrans.CommShift e.hom A] : F.postcomp G ≅ F.postcomp G'

The isomorphism F.postcomp G ≅ F.postcomp G' induced by an isomorphism e : G ≅ G' which commutes with the shift.

Equations

• F.postcompIsoOfIso e = CategoryTheory.SingleFunctors.isoMk (fun (a : A) => CategoryTheory.isoWhiskerLeft (F.functor a) e) ⋯

@[simp]

theorem CategoryTheory.SingleFunctors.postcompIsoOfIso_hom_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C D A) {G G' : Functor D E} (e : G ≅ G') [G.CommShift A] [G'.CommShift A] [NatTrans.CommShift e.hom A] (a : A) (X : C) : ((F.postcompIsoOfIso e).hom.hom a).app X = e.hom.app ((F.functor a).obj X)

@[simp]

theorem CategoryTheory.SingleFunctors.postcompIsoOfIso_inv_hom_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{u_6, u_1} C] [Category.{u_7, u_2} D] [Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [HasShift D A] [HasShift E A] (F : SingleFunctors C D A) {G G' : Functor D E} (e : G ≅ G') [G.CommShift A] [G'.CommShift A] [NatTrans.CommShift e.hom A] (a : A) (X : C) : ((F.postcompIsoOfIso e).inv.hom a).app X = e.inv.app ((F.functor a).obj X)