Theorems · Theorem · algebraic topology

TopPair.HomologyPretheory.Hom.w_app_assoc

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i j : ι) (X : TopPair)
  {Z : C} (h : (HP'.H j).obj X.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HP.δ i j).app X) (CategoryTheory.CategoryStruct.comp ((f.hom j).app X.left) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app X) ((HP'.δ i j).app X)) h

Defined in

Mathlib.AlgebraicTopology.EilenbergSteenrod

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms