Documentation

Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

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.

source
@[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)
source
@[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)
source
@[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 φ
source
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] :
CategoryTheory.Functor (CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (CategoryTheory.Functor J (CategoryTheory.ShortComplex 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
    source
    @[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.π₁
    source
    @[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.π₁
    source
    @[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π₃
    source
    @[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.π₃
    source
    @[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.π₃
    source
    @[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.π₂
    source
    @[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.π₂
    source
    @[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π₂
    source
    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] :
    CategoryTheory.Functor (CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (CategoryTheory.ShortComplex (CategoryTheory.Functor J 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
      source
      @[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)
      source
      @[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)
      source
      @[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)
      source
      @[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)
      source
      @[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)
      source
      @[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)
      source
      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] :
      CategoryTheory.Functor.id (CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) ≅ (CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).comp (CategoryTheory.ShortComplex.FunctorEquivalence.inverse J 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
        source
        @[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₁
        source
        @[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₂
        source
        @[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₃
        source
        @[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₂
        source
        @[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₁
        source
        @[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₃
        source
        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] :
        (CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).comp (CategoryTheory.ShortComplex.FunctorEquivalence.functor J C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor J (CategoryTheory.ShortComplex 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
          source
          @[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] :
          (CategoryTheory.ShortComplex.functorEquivalence J C).inverse = CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C
          source
          @[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] :
          (CategoryTheory.ShortComplex.functorEquivalence J C).counitIso = CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C
          source
          @[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] :
          (CategoryTheory.ShortComplex.functorEquivalence J C).unitIso = CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C
          source
          @[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] :
          (CategoryTheory.ShortComplex.functorEquivalence J C).functor = CategoryTheory.ShortComplex.FunctorEquivalence.functor J C
          source
          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] :
          CategoryTheory.ShortComplex (CategoryTheory.Functor J C) ≌ CategoryTheory.Functor J (CategoryTheory.ShortComplex C)

          The obvious equivalence ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

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