Commit 2025-02-05 23:58 191c189e

View on Github →

refactor(Topology/Category): clean up remaining uses of HasForget (#21458) This PR upgrades the remaining usage of HasForget in the folder Mathlib/Topology/Category, upgrading to ConcreteCategory. I made a Hom structure for UniformSpaceCat but not for the other concrete categories, since it was the only category to actually need some disambiguating between categorical homs and uniformly continuous maps.

Estimated changes

Modified Mathlib/Topology/Category/Born.lean

deleted def Born.of

added structure Born

deleted def Born

Modified Mathlib/Topology/Category/CompactlyGenerated.lean

Modified Mathlib/Topology/Category/Compactum.lean

Modified Mathlib/Topology/Category/LightProfinite/Extend.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Category/TopCommRingCat.lean

deleted def TopCommRingCat.of

Modified Mathlib/Topology/Category/UniformSpace.lean

added theorem CpltSepUniformSpace.hom_comp

added theorem CpltSepUniformSpace.hom_id

added theorem CpltSepUniformSpace.hom_ofHom

added structure UniformSpaceCat.Hom

added theorem UniformSpaceCat.hom_comp

modified theorem UniformSpaceCat.hom_ext

added theorem UniformSpaceCat.hom_id

added theorem UniformSpaceCat.hom_ofHom

deleted def UniformSpaceCat.of

added structure UniformSpaceCat

deleted def UniformSpaceCat