Theorems · Theorem · algebraic topology

CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pull_assoc

∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {Δ' : SimplexCategoryᵒᵖ}
  (θ : Δ ⟶ Δ') {Z : SimplexCategory} (h : Opposite.unop A.fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.pull θ).e
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)) h) =
    CategoryTheory.CategoryStruct.comp θ.unop (CategoryTheory.CategoryStruct.comp A.e h)

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Split

Cited by

0 results in Mathlib

Foundations

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