Theorems · Definition · algebraic topology

CategoryTheory.SimplicialObject.Splitting.cofan

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.Limits.Cofan (CategoryTheory.SimplicialObject.Splitting.summand s.N Δ)

The cofan for summand s.N Δ induced by a splitting of a simplicial object.

Defined in: Mathlib.AlgebraicTopology.SimplicialObject.Split
Cited by: 46 results in Mathlib
Foundations: Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites18

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.objproof · cited by 19,642
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.Functor.mapproof · cited by 8,698
Oppositestatement and proof · cited by 8,081
Opposite.unopproof · cited by 2,231
SimplexCategorystatement and proof · cited by 2,204
Quiver.Hom.opproof · cited by 1,948
CategoryTheory.SimplicialObjectstatement and proof · cited by 548
SimplexCategory.lenproof · cited by 542
CategoryTheory.Limits.Cofanstatement · cited by 124
CategoryTheory.Limits.Cofan.mkproof · cited by 105

Cited by51

Results whose statement or proof uses this declaration.

CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁proof · cited by 16
CategoryTheory.SimplicialObject.Splitting.hom_ext'statement and proof · cited by 5
CategoryTheory.SimplicialObject.Splitting.ι_descstatement · cited by 5
CategoryTheory.SimplicialObject.Splitting.cofan_inj_eqstatement · cited by 4
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summandstatement · cited by 4
AlgebraicTopology.DoldKan.Γ₀.mapproof · cited by 2
CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zerostatement and proof · cited by 2
CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_appstatement · cited by 2
CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zerostatement · cited by 2
CategoryTheory.SimplicialObject.Splitting.comp_PInfty_eq_zero_iffproof · cited by 2
CategoryTheory.SimplicialObject.Splitting.decomposition_idstatement and proof · cited by 2
AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_selfstatement and proof · cited by 2