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) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
Functor (ShortComplex (Functor J C)) (Functor J (ShortComplex C))

The obvious functor ShortComplex (J ⥤ C) ⥤ J ⥤ ShortComplex C.

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_obj (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (S : ShortComplex (Functor J C)) (j : J) :
      ((functor J C).obj S).obj j = S.map ((evaluation J C).obj j)
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.FunctorEquivalence.functor_map_app (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : ShortComplex (Functor J C)} (φ : X✝ ⟶ Y✝) (j : J) :
      ((functor J C).map φ).app j = ((evaluation J C).obj j).mapShortComplex.map φ
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_map (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) :
      ((functor J C).obj S).map f = S.mapNatTrans ((evaluation J C).map f)
      source
      def CategoryTheory.ShortComplex.FunctorEquivalence.inverse (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
      Functor (Functor J (ShortComplex C)) (ShortComplex (Functor J C))

      The obvious functor (J ⥤ ShortComplex C) ⥤ ShortComplex (J ⥤ C).

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₂ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) :
          ((inverse J C).obj F).X₂ = F.comp π₂
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₃ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) :
          ((inverse J C).obj F).X₃ = F.comp π₃
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_f (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) :
          ((inverse J C).obj F).f = F.whiskerLeft π₁Toπ₂
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_g (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) :
          ((inverse J C).obj F).g = F.whiskerLeft π₂Toπ₃
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₂ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : Functor J (ShortComplex C)} (φ : X✝ ⟶ Y✝) :
          ((inverse J C).map φ).τ₂ = Functor.whiskerRight φ π₂
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₁ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) :
          ((inverse J C).obj F).X₁ = F.comp π₁
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₃ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : Functor J (ShortComplex C)} (φ : X✝ ⟶ Y✝) :
          ((inverse J C).map φ).τ₃ = Functor.whiskerRight φ π₃
          source
          @[simp]
          theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₁ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : Functor J (ShortComplex C)} (φ : X✝ ⟶ Y✝) :
          ((inverse J C).map φ).τ₁ = Functor.whiskerRight φ π₁
          source
          def CategoryTheory.ShortComplex.FunctorEquivalence.unitIso (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
          Functor.id (ShortComplex (Functor J C)) ≅ (functor J C).comp (inverse J C)

          The unit isomorphism of the equivalence ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₃_app (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) :
              ((unitIso J C).inv.app X).τ₃.app X✝ = CategoryStruct.id (X.X₃.obj X✝)
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₃_app (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) :
              ((unitIso J C).hom.app X).τ₃.app X✝ = CategoryStruct.id (X.X₃.obj X✝)
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₁_app (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) :
              ((unitIso J C).inv.app X).τ₁.app X✝ = CategoryStruct.id (X.X₁.obj X✝)
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₂_app (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) :
              ((unitIso J C).hom.app X).τ₂.app X✝ = CategoryStruct.id (X.X₂.obj X✝)
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₂_app (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) :
              ((unitIso J C).inv.app X).τ₂.app X✝ = CategoryStruct.id (X.X₂.obj X✝)
              source
              @[simp]
              theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₁_app (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) :
              ((unitIso J C).hom.app X).τ₁.app X✝ = CategoryStruct.id (X.X₁.obj X✝)
              source
              def CategoryTheory.ShortComplex.FunctorEquivalence.counitIso (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
              (inverse J C).comp (functor J C) ≅ Functor.id (Functor J (ShortComplex C))

              The counit isomorphism of the equivalence ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₃ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) :
                  (((counitIso J C).hom.app X).app X✝).τ₃ = CategoryStruct.id (X.obj X✝).X₃
                  source
                  @[simp]
                  theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₂ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) :
                  (((counitIso J C).inv.app X).app X✝).τ₂ = CategoryStruct.id (X.obj X✝).X₂
                  source
                  @[simp]
                  theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₂ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) :
                  (((counitIso J C).hom.app X).app X✝).τ₂ = CategoryStruct.id (X.obj X✝).X₂
                  source
                  @[simp]
                  theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₃ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) :
                  (((counitIso J C).inv.app X).app X✝).τ₃ = CategoryStruct.id (X.obj X✝).X₃
                  source
                  @[simp]
                  theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₁ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) :
                  (((counitIso J C).inv.app X).app X✝).τ₁ = CategoryStruct.id (X.obj X✝).X₁
                  source
                  @[simp]
                  theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₁ (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) :
                  (((counitIso J C).hom.app X).app X✝).τ₁ = CategoryStruct.id (X.obj X✝).X₁
                  source
                  def CategoryTheory.ShortComplex.functorEquivalence (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
                  ShortComplex (Functor J C) ≌ Functor J (ShortComplex C)

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

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.ShortComplex.functorEquivalence_counitIso (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
                      (functorEquivalence J C).counitIso = FunctorEquivalence.counitIso J C
                      source
                      @[simp]
                      theorem CategoryTheory.ShortComplex.functorEquivalence_unitIso (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
                      (functorEquivalence J C).unitIso = FunctorEquivalence.unitIso J C
                      source
                      @[simp]
                      theorem CategoryTheory.ShortComplex.functorEquivalence_functor (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
                      (functorEquivalence J C).functor = FunctorEquivalence.functor J C
                      source
                      @[simp]
                      theorem CategoryTheory.ShortComplex.functorEquivalence_inverse (J : Type u_1) (C : Type u_2) [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] :
                      (functorEquivalence J C).inverse = FunctorEquivalence.inverse J C