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 with ConcreteCategory.
  • 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.

Estimated changes

added structure TopCat.Hom
modified theorem TopCat.coe_of
added theorem TopCat.ext
modified theorem TopCat.hom_apply
added theorem TopCat.hom_comp
added theorem TopCat.hom_ext
added theorem TopCat.hom_id
added theorem TopCat.hom_ofHom
deleted def TopCat.of
added theorem TopCat.ofHom_apply
added theorem TopCat.ofHom_comp
added theorem TopCat.ofHom_hom
added theorem TopCat.ofHom_id
added theorem TopCat.of_carrier
added structure TopCat
deleted def TopCat