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
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.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_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
    @[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
    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.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_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
      @[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_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_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
      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.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_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_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.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.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
          @[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
          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
            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
            @[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