Commit 2025-02-11 09:10 ff73b3ec

View on Github →

refactor(Topology): colimits in TopCat (#20369) The API is slighly improved for colimits in the category of topological spaces. General lemmas characterizing the topology on the colimit are moved from TopCat.Limits.Pullbacks to TopCat.Limits.Basic.

Estimated changes

Modified Mathlib/Topology/Category/TopCat/EffectiveEpi.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

added def TopCat.coconeOfCoconeForget

added def TopCat.coconePtOfCoconeForget

added theorem TopCat.coinduced_of_isColimit

deleted def TopCat.colimitCocone

deleted def TopCat.colimitCoconeIsColimit

added theorem TopCat.colimit_isOpen_iff

added theorem TopCat.colimit_topology

added theorem TopCat.continuous_iff_of_isColimit

added theorem TopCat.hasColimit_iff_small_quot

added theorem TopCat.isClosed_iff_of_isColimit

added def TopCat.isColimitCoconeOfForget

added theorem TopCat.isOpen_iff_of_isColimit

Modified Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

modified theorem TopCat.coequalizer_isOpen_iff

deleted theorem TopCat.coinduced_of_isColimit

deleted theorem TopCat.colimit_isOpen_iff

deleted theorem TopCat.colimit_topology

added theorem TopCat.isOpen_iff_of_isColimit_cofork

added theorem TopCat.isQuotientMap_of_isColimit_cofork