Theorems · Definition · algebraic topology
SSet.toTop
CategoryTheory.Functor SSet TopCat
The geometric realization functor is
the left Kan extension of SimplexCategory.toTop along the Yoneda embedding.
It is left adjoint to TopCat.toSSet, as witnessed by sSetTopAdj.
- Defined in
- Mathlib.AlgebraicTopology.SingularSet
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement · cited by 8,081
- SimplexCategorystatement · cited by 2,204
- TopCatstatement · cited by 1,889
- SSetstatement · cited by 1,283
- SSet.stdSimplexproof · cited by 499
- CategoryTheory.Functor.leftKanExtensionproof · cited by 29
- SimplexCategory.toTopproof · cited by 6
Cited by15
Results whose statement or proof uses this declaration.
- sSetTopAdjstatement · cited by 7
- SSet.toTopSimplexstatement · cited by 6
- SimplexCategory.toTopHomeostatement · cited by 6
- sSetTopAdj_homEquiv_stdSimplex_zerostatement and proof · cited by 2
- SimplexCategory.toTopHomeo_naturality_applystatement and proof · cited by 2
- sSetTopAdj_unit_app_app_downstatement · cited by 1
- SimplexCategory.toTopHomeo_naturalitystatement and proof · cited by 1
- SimplexCategory.toTopHomeo_symm_naturalitystatement · cited by 1
- SSet.stdSimplex.δ_one_toSSetObjIproof · cited by 1
- SSet.stdSimplex.δ_zero_toSSetObjIproof · cited by 1
- AlgebraicTopology.singularChainComplexFunctorAdjunction_unit_appproof · cited by 0
- SSet.stdSimplexToTop_app_app_hom_apply_down_hom_applystatement · cited by 0