Commit 2021-07-15 05:43 e42af8da

View on Github →

refactor(topology/category/Profinite): define Profinite as a subcategory of CompHaus (#8314) This adjusts the definition of Profinite to explicitly be a subcategory of CompHaus rather than a subcategory of Top which embeds into CompHaus. Essentially this means it's easier to construct an element of Profinite from an element of CompHaus.

Estimated changes

Modified src/topology/category/Profinite/cofiltered_limit.lean

Modified src/topology/category/Profinite/default.lean

added theorem Profinite.coe_to_CompHaus

deleted theorem Profinite.coe_to_Top

deleted def Profinite.to_CompHaus

modified def Profinite.to_Profinite_adj_to_CompHaus

added def Profinite.to_Top

added def Profinite_to_CompHaus

deleted def Profinite_to_Top