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 ⥤ Dindexed by the elements of the additive monoidA - shiftIso : (n a a' : A) → n + a = a' → ((self.functor a').comp (CategoryTheory.shiftFunctor D n) ≅ self.functor a)
- shiftIso_zero : ∀ (a : A), self.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerLeft (self.functor a) (CategoryTheory.shiftFunctorZero D A)
shiftIso 0is 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'
Instances For
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)
theorem
CategoryTheory.SingleFunctors.Hom.ext_iff
{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 = y ↔ x.hom = y.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
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
- 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
Instances For
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)
@[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)
(a : A)
:
(CategoryTheory.SingleFunctors.Hom.id F).hom a = CategoryTheory.CategoryStruct.id (F.functor a)
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 (a : A) => CategoryTheory.CategoryStruct.id (F.functor a), comm := ⋯ }
Instances For
@[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)
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 := ⋯ }
Instances For
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]
:
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)
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)
@[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.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
@[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.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.
Instances For
@[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)
{F : CategoryTheory.SingleFunctors C D A}
{G : CategoryTheory.SingleFunctors C D A}
(φ : F ⟶ G)
:
(CategoryTheory.SingleFunctors.evaluation C D a).map φ = φ.hom a
@[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
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)
:
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.
Instances For
@[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.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.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.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.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.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.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
@[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)
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
- ⋯ = ⋯
@[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.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]
:
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.
Instances For
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]
:
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.
Instances For
@[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)))
@[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)))
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 (a : A) => (F.functor a).associator G G') ⋯
Instances For
@[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)
@[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)
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) ⋯