Theorems · Definition · algebraic topology
FundamentalGroupoid.fundamentalGroupoidFunctor
CategoryTheory.Functor TopCat CategoryTheory.Grpd
The functor sending a topological space X to its fundamental groupoid.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 139 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.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- TopCat.carrierproof · cited by 3,184
- TopCatstatement and proof · cited by 1,889
- TopCat.Hom.homproof · cited by 169
- FundamentalGroupoidproof · cited by 60
- CategoryTheory.Grpdstatement · cited by 30
- FundamentalGroupoid.mapproof · cited by 6
Cited by39
Results whose statement or proof uses this declaration.
- FundamentalGroupoidFunctor.prodToProdTopstatement and proof · cited by 7
- FundamentalGroupoid.fromTopstatement · cited by 6
- ContinuousMap.Homotopy.hcaststatement · cited by 6
- ContinuousMap.Homotopy.prodToProdTopIstatement · cited by 4
- FundamentalGroupoidFunctor.piToPiTopstatement and proof · cited by 3
- FundamentalGroupoidFunctor.projstatement and proof · cited by 3
- ContinuousMap.Homotopy.eq_path_of_eq_imagestatement and proof · cited by 2
- FundamentalGroupoidFunctor.coneDiscreteCompstatement and proof · cited by 2
- FundamentalGroupoidFunctor.piIsostatement · cited by 2
- FundamentalGroupoidFunctor.prodIsostatement · cited by 2
- FundamentalGroupoidFunctor.projLeftstatement · cited by 2
- FundamentalGroupoidFunctor.projRightstatement · cited by 2