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) [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (A : Type u_5) [AddMonoid A] [CategoryTheory.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 → CategoryTheory.Functor C D

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

• shiftIso : (n a a' : A) → n + a = a' → ((self.functor a').comp (CategoryTheory.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 ⋯ = CategoryTheory.isoWhiskerLeft (self.functor a) (CategoryTheory.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'' ⋯ = CategoryTheory.isoWhiskerLeft (self.functor a'') (CategoryTheory.shiftFunctorAdd D m n) ≪≫ ((self.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫ CategoryTheory.isoWhiskerRight (self.shiftIso m a' a'' ha'') (CategoryTheory.shiftFunctor D n) ≪≫ self.shiftIso n a a' ha'

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

theorem CategoryTheory.SingleFunctors.shiftIso_zero {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (self : CategoryTheory.SingleFunctors C D A) (a : A) : self.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerLeft (self.functor a) (CategoryTheory.shiftFunctorZero D A)

shiftIso 0 is the obvious isomorphism.

theorem CategoryTheory.SingleFunctors.shiftIso_add {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (self : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') : self.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerLeft (self.functor a'') (CategoryTheory.shiftFunctorAdd D m n) ≪≫ ((self.functor a'').associator (CategoryTheory.shiftFunctor D m) (CategoryTheory.shiftFunctor D n)).symm ≪≫ CategoryTheory.isoWhiskerRight (self.shiftIso m a' a'' ha'') (CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso (m + n) a a'' ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X)) ((CategoryTheory.shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)))

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

theorem CategoryTheory.SingleFunctors.shiftIso_add'_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (mn : A) (hnm : m + n = mn) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso mn a a'' ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (n : A) (m : A) (mn : A) (hnm : m + n = mn) (a : A) (a' : A) (a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) : (F.shiftIso mn a a'' ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X)) ((CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A) (X : C) : (F.shiftIso 0 a a ⋯).hom.app X = (CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A) (X : C) : (F.shiftIso 0 a a ⋯).inv.app X = (CategoryTheory.shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)

structure CategoryTheory.SingleFunctors.Hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.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'), CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (self.hom a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (self.hom a') (CategoryTheory.shiftFunctor D n)) (G.shiftIso n a a' ha').hom

theorem CategoryTheory.SingleFunctors.Hom.ext {C : Type u_1} {D : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_6, u_1} C} {inst_1 : CategoryTheory.Category.{u_7, u_2} D} {A : Type u_5} {inst_2 : AddMonoid A} {inst_3 : CategoryTheory.HasShift D A} {F G : CategoryTheory.SingleFunctors C D A} {x y : F.Hom G}, x.hom = y.hom → x = y

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

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

def CategoryTheory.SingleFunctors.Hom.id {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) : ∀ (x : A), (CategoryTheory.SingleFunctors.Hom.id F).hom x = CategoryTheory.CategoryStruct.id (F.functor x)

def CategoryTheory.SingleFunctors.Hom.comp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} {H : CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} {H : CategoryTheory.SingleFunctors C D A} (α : F.Hom G) (β : G.Hom H) (a : A) : (α.comp β).hom a = CategoryTheory.CategoryStruct.comp (α.hom a) (β.hom a)

instance CategoryTheory.SingleFunctors.instCategory {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] : CategoryTheory.Category.{max (max u_1 u_5) u_7, max (max (max (max u_7 u_6) u_5) u_2) u_1} (CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (a : A) : (CategoryTheory.CategoryStruct.id F).hom a = CategoryTheory.CategoryStruct.id (F.functor a)

@[simp]

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

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

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

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

@[simp]

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

def CategoryTheory.SingleFunctors.evaluation (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (a : A) : CategoryTheory.Functor (CategoryTheory.SingleFunctors C D A) (CategoryTheory.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) [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] (a : A) (F : CategoryTheory.SingleFunctors C D A) : (CategoryTheory.SingleFunctors.evaluation C D a).obj F = F.functor a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.SingleFunctors.inv_hom_id_hom_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) {Z : CategoryTheory.Functor C D} (h : G.functor n ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inv.hom n) (CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) : CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X) ((e.inv.hom n).app X) = CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) {Z : D} (h : (F.functor n).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X) (CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) : CategoryTheory.CategoryStruct.comp ((e.inv.hom n).app X) ((e.hom.hom n).app X) = CategoryTheory.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} [CategoryTheory.Category.{u_7, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] {F : CategoryTheory.SingleFunctors C D A} {G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) {Z : D} (h : (G.functor n).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((e.inv.hom n).app X) (CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X) h) = h

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

Equations

• ⋯ = ⋯

def CategoryTheory.SingleFunctors.postcomp {C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [G.CommShift A] : CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [G.CommShift A] (n : A) (a : A) (a' : A) (ha' : n + a = a') (X : C) : ((F.postcomp G).shiftIso n a a' ha').inv.app X = CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [G.CommShift A] (n : A) (a : A) (a' : A) (ha' : n + a = a') (X : C) : ((F.postcomp G).shiftIso n a a' ha').hom.app X = CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (G : CategoryTheory.Functor D E) [G.CommShift A] : CategoryTheory.Functor (CategoryTheory.SingleFunctors C D A) (CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] [CategoryTheory.Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [CategoryTheory.HasShift E' A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) (G' : CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] [CategoryTheory.Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [CategoryTheory.HasShift E' A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) (G' : CategoryTheory.Functor E E') [G.CommShift A] [G'.CommShift A] (a : A) : ∀ (x : C), ((F.postcompPostcompIso G G').hom.hom a).app x = CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] [CategoryTheory.Category.{u_9, u_4} E'] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] [CategoryTheory.HasShift E' A] (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) (G' : CategoryTheory.Functor E E') [G.CommShift A] [G'.CommShift A] (a : A) : ∀ (x : C), ((F.postcompPostcompIso G G').inv.hom a).app x = CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) {G : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor D E} (e : G ≅ G') [G.CommShift A] [G'.CommShift A] [CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) {G : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor D E} (e : G ≅ G') [G.CommShift A] [G'.CommShift A] [CategoryTheory.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} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] [CategoryTheory.Category.{u_8, u_3} E] {A : Type u_5} [AddMonoid A] [CategoryTheory.HasShift D A] [CategoryTheory.HasShift E A] (F : CategoryTheory.SingleFunctors C D A) {G : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor D E} (e : G ≅ G') [G.CommShift A] [G'.CommShift A] [CategoryTheory.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)