Commit 2025-02-03 16:47 71f75037
View on Github →feat(Topology/Category): concrete category refactor for topological spaces (#21302)
This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980
This PR updates the category definitions of TopCat
and some of its descendants to match the new ConcreteCategory
style:
- Package objects and homs into structures.
- Replace
HasForget
withConcreteCategory
. - Set up a good @[simp] set.
- Ensure constructors and projections are reducible. I found many places where proofs could be cleaned up, even without looking particularly hard. 🎉 Once all the concrete category instances are in we can get rid of even more workarounds.