Commit 2021-05-07 22:54 dbcd4546
View on Github →feat(topology/category/*): Add alternative explicit limit cones for Top
, etc. and shows X : Profinite
is a limit of finite sets. (#7448)
This PR redefines Top.limit_cone
, and defines similar explicit limit cones for CompHaus
and Profinite
.
Using the definition with the subspace topology makes the proofs that the limit is compact, t2 and/or totally disconnected much easier.
This also expresses any X : Profinite
as a limit of its discrete quotients, which are all finite.