Short complexes in functor categories #
In this file, it is shown that if J
and C
are two categories (such
that C
has zero morphisms), then there is an equivalence of categories
ShortComplex.functorEquivalence J C : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C
.
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_map
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
:
∀ {X Y : J} (f : X ⟶ Y),
((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).obj S).map f = S.mapNatTrans ((CategoryTheory.evaluation J C).map f)
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.functor_map_app
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
∀ {X Y : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)} (φ : X ⟶ Y) (j : J),
((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).map φ).app j = ((CategoryTheory.evaluation J C).obj j).mapShortComplex.map φ
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_obj
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
(j : J)
:
((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).obj S).obj j = S.map ((CategoryTheory.evaluation J C).obj j)
def
CategoryTheory.ShortComplex.FunctorEquivalence.functor
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
The obvious functor ShortComplex (J ⥤ C) ⥤ J ⥤ ShortComplex C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₂
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
∀ {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y),
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₂ = CategoryTheory.whiskerRight φ CategoryTheory.ShortComplex.π₂
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₁
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
∀ {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y),
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₁ = CategoryTheory.whiskerRight φ CategoryTheory.ShortComplex.π₁
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₃
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
∀ {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y),
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₃ = CategoryTheory.whiskerRight φ CategoryTheory.ShortComplex.π₃
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₃
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
:
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₃ = F.comp CategoryTheory.ShortComplex.π₃
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₂
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
:
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₂ = F.comp CategoryTheory.ShortComplex.π₂
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_g
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
:
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).g = CategoryTheory.whiskerLeft F CategoryTheory.ShortComplex.π₂Toπ₃
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₁
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
:
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₁ = F.comp CategoryTheory.ShortComplex.π₁
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_f
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
:
((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).f = CategoryTheory.whiskerLeft F CategoryTheory.ShortComplex.π₁Toπ₂
def
CategoryTheory.ShortComplex.FunctorEquivalence.inverse
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
The obvious functor (J ⥤ ShortComplex C) ⥤ ShortComplex (J ⥤ C)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₁_app
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
(X : J)
:
((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X✝).τ₁.app X = CategoryTheory.CategoryStruct.id (X✝.X₁.obj X)
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₃_app
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
(X : J)
:
((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X✝).τ₃.app X = CategoryTheory.CategoryStruct.id (X✝.X₃.obj X)
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₁_app
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
(X : J)
:
((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X✝).τ₁.app X = CategoryTheory.CategoryStruct.id (X✝.X₁.obj X)
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₃_app
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
(X : J)
:
((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X✝).τ₃.app X = CategoryTheory.CategoryStruct.id (X✝.X₃.obj X)
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₂_app
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
(X : J)
:
((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X✝).τ₂.app X = CategoryTheory.CategoryStruct.id (X✝.X₂.obj X)
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₂_app
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
(X : J)
:
((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X✝).τ₂.app X = CategoryTheory.CategoryStruct.id (X✝.X₂.obj X)
def
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
The unit isomorphism of the equivalence
ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₃
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
(X : J)
:
(((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X✝).app X).τ₃ = CategoryTheory.CategoryStruct.id (X✝.obj X).X₃
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₃
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
(X : J)
:
(((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X✝).app X).τ₃ = CategoryTheory.CategoryStruct.id (X✝.obj X).X₃
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₁
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
(X : J)
:
(((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X✝).app X).τ₁ = CategoryTheory.CategoryStruct.id (X✝.obj X).X₁
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₂
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
(X : J)
:
(((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X✝).app X).τ₂ = CategoryTheory.CategoryStruct.id (X✝.obj X).X₂
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₁
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
(X : J)
:
(((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X✝).app X).τ₁ = CategoryTheory.CategoryStruct.id (X✝.obj X).X₁
@[simp]
theorem
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₂
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
(X : J)
:
(((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X✝).app X).τ₂ = CategoryTheory.CategoryStruct.id (X✝.obj X).X₂
def
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
The counit isomorphism of the equivalence
ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.functorEquivalence_inverse
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
@[simp]
theorem
CategoryTheory.ShortComplex.functorEquivalence_functor
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
@[simp]
theorem
CategoryTheory.ShortComplex.functorEquivalence_counitIso
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
@[simp]
theorem
CategoryTheory.ShortComplex.functorEquivalence_unitIso
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
def
CategoryTheory.ShortComplex.functorEquivalence
(J : Type u_1)
(C : Type u_2)
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
The obvious equivalence ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C
.
Equations
- One or more equations did not get rendered due to their size.