Theorems · Definition · category theory

HomologicalComplex.mapBifunctorAssociatorX

{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₁₂ : Type u_3} →
      {C₂₃ : Type u_4} →
        {C₃ : Type u_5} →
          {C₄ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃] →
                        [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                          [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                            [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] →
                              [inst_9 : CategoryTheory.Preadditive C₁₂] →
                                [inst_10 : CategoryTheory.Preadditive C₂₃] →
                                  [inst_11 : CategoryTheory.Preadditive C₄] →
                                    {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} →
                                      {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} →
                                        {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} →
                                          {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} →
                                            [inst_12 : F₁₂.PreservesZeroMorphisms] →
                                              [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] →
                                                [inst_14 : G.Additive] →
                                                  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] →
                                                    [inst_16 : G₂₃.PreservesZeroMorphisms] →
                                                      [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] →
                                                        [inst_18 : F.PreservesZeroMorphisms] →
                                                          [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                                                            (CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅
                                                                CategoryTheory.bifunctorComp₂₃ F G₂₃) →
                                                              {ι₁ : Type u_7} →
                                                                {ι₂ : Type u_8} →
                                                                  {ι₃ : Type u_9} →
                                                                    {ι₁₂ : Type u_10} →
                                                                      {ι₂₃ : Type u_11} →
                                                                        {ι₄ : Type u_12} →
                                                                          [inst_20 : DecidableEq ι₄] →
                                                                            {c₁ : ComplexShape ι₁} →
                                                                              {c₂ : ComplexShape ι₂} →
                                                                                {c₃ : ComplexShape ι₃} →
                                                                                  (K₁ : HomologicalComplex C₁ c₁) →
                                                                                    (K₂ : HomologicalComplex C₂ c₂) →
                                                                                      (K₃ : HomologicalComplex C₃ c₃) →
                                                                                        (c₁₂ : ComplexShape ι₁₂) →
                                                                                          (c₂₃ : ComplexShape ι₂₃) →
                                                                                            (c₄ : ComplexShape ι₄) →
                                                                                              [inst_21 :
                                                                                                  TotalComplexShape c₁
                                                                                                    c₂ c₁₂] →
                                                                                                [inst_22 :
                                                                                                    TotalComplexShape
                                                                                                      c₁₂ c₃ c₄] →
                                                                                                  [inst_23 :
                                                                                                      TotalComplexShape
                                                                                                        c₂ c₃ c₂₃] →
                                                                                                    [inst_24 :
                                                                                                        TotalComplexShape
                                                                                                          c₁ c₂₃ c₄] →
                                                                                                      ⋯

The associator isomorphism for the action of bifunctors on homological complexes, in each degree.

Defined in

Mathlib.Algebra.Homology.BifunctorAssociator

Cited by

11 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.AdditiveCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.AdditiveDecidableEqTotalComplexShapeTotalComplexShapeTotalComplexShapeTotalComplexShapeHomologicalComplex.HasMapBifunctorHomologicalComplex.HasMapBifunctorComplexShape.AssociativeDecidableEqDecidableEqHomologicalComplex.HasMapBifunctorHomologicalComplex.HasMapBifunctorHomologicalComplex.HasGoodTrifunctor₁₂ObjHomologicalComplex.HasGoodTrifunctor₂₃Obj