Theorems · Definition · category theory
Profinite.asLimitCone
(X : Profinite) → CategoryTheory.Limits.Cone X.diagram
A cone over X.diagram whose cone point is X.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopCat.carrierstatement and proof · cited by 3,184
- TopCatstatement and proof · cited by 1,889
- CategoryTheory.Limits.Conestatement · cited by 710
- TotallyDisconnectedSpacestatement and proof · cited by 295
- CompHausLike.toTopstatement and proof · cited by 258
- Profinitestatement and proof · cited by 75
- DiscreteQuotientstatement and proof · cited by 65
- DiscreteQuotient.projproof · cited by 23
- CompHausLike.ofHomproof · cited by 11
- Profinite.diagramstatement · cited by 8
Cited by17
Results whose statement or proof uses this declaration.
- Condensed.isColimitLocallyConstantPresheafDiagramstatement and proof · cited by 3
- Condensed.isoLocallyConstantOfIsColimitstatement and proof · cited by 2
- Condensed.lanPresheafNatIsostatement and proof · cited by 2
- CondensedSet.isDiscrete_tfaestatement and proof · cited by 1
- CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCoconestatement and proof · cited by 1
- Condensed.lanPresheafIsostatement and proof · cited by 1
- Condensed.lanPresheafIso_homstatement and proof · cited by 1
- Condensed.lanPresheafNatIso_hom_appstatement and proof · cited by 1
- LightProfinite.lightToProfinite_map_proj_eqstatement and proof · cited by 1
- Profinite.asLimitstatement · cited by 1
- Condensed.isColimitLocallyConstantPresheafDiagram_desc_applystatement and proof · cited by 0
- Condensed.isoLocallyConstantOfIsColimit_invstatement and proof · cited by 0