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
  • 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) [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
    • 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) [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 = whiskerLeft F π₁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 = whiskerLeft F π₂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 φ).τ₂ = 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 φ).τ₃ = 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 φ).τ₁ = 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
      • 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) [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
        • 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) [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
          • 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) [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