Theorems · Definition · category theory
HomologicalComplex.mapBifunctorAssociator
{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.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 57 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
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Isostatement and proof · cited by 3,963
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- HomologicalComplexstatement and proof · cited by 1,691
- ComplexShapestatement and proof · cited by 1,684
- CategoryTheory.Functor.Additivestatement and proof · cited by 1,179
- CategoryTheory.Functor.PreservesZeroMorphismsstatement and proof · cited by 458
- TotalComplexShapestatement and proof · cited by 210
- HomologicalComplex.mapBifunctorstatement and proof · cited by 109
Cited by1
Results whose statement or proof uses this declaration.
- HomologicalComplex.associatorproof · cited by 0