Commit 2021-05-07 22:54 dbcd4546

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.