Theorems · Definition · algebraic topology
CategoryTheory.SimplicialObject.Splitting.IndexSet.pull
{Δ : SimplexCategoryᵒᵖ} →
CategoryTheory.SimplicialObject.Splitting.IndexSet Δ →
{Δ' : SimplexCategoryᵒᵖ} → (Δ ⟶ Δ') → CategoryTheory.SimplicialObject.Splitting.IndexSet Δ'When A : IndexSet Δ and θ : Δ → Δ' is a morphism in SimplexCategoryᵒᵖ,
an element in IndexSet Δ' can be defined by using the epi-mono factorisation
of θ.unop ≫ A.e.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- Oppositestatement and proof · cited by 8,081
- SimplexCategorystatement and proof · cited by 2,204
- Quiver.Hom.unopproof · cited by 903
- CategoryTheory.SimplicialObject.Splitting.IndexSetstatement and proof · cited by 65
- CategoryTheory.Limits.factorThruImageproof · cited by 55
- CategoryTheory.SimplicialObject.Splitting.IndexSet.eproof · cited by 28
- CategoryTheory.SimplicialObject.Splitting.IndexSet.mkproof · cited by 8
Cited by8
Results whose statement or proof uses this declaration.
- AlgebraicTopology.DoldKan.Γ₀.Obj.mapproof · cited by 9
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀proof · cited by 3
- CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pullstatement · cited by 2
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'statement · cited by 1
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'statement · cited by 1
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assocstatement and proof · cited by 0
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assocstatement and proof · cited by 0
- CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pull_assocstatement and proof · cited by 0