Commit 2026-04-01 14:12 278e559f

View on Github →

refactor(Topology): redefine Topology.IsQuotientMap with Topology.IsCoinducing (#36957) Currently, varying formulations for f : X -> Y is coinducing are used: Examples are an equality of TopologicalSpace.coinduced or an explicit characterization of open sets. We add a predicate Topology.IsCoinducing and redefine Topology.IsQuotientMap in terms of it.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/Topology/Algebra/Module/ModuleTopology.lean

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

Modified Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean

Modified Mathlib/Topology/Connected/Clopen.lean

added theorem Topology.IsCoinducing.image_connectedComponent

added theorem Topology.IsCoinducing.preimage_connectedComponent

deleted theorem Topology.IsQuotientMap.image_connectedComponent

deleted theorem Topology.IsQuotientMap.preimage_connectedComponent

Modified Mathlib/Topology/Connected/LocPathConnected.lean

Modified Mathlib/Topology/Constructions.lean

added theorem Topology.IsCoinducing.restrictPreimage_of_isOpen

Modified Mathlib/Topology/Defs/Induced.lean

added structure Topology.IsCoinducing

modified structure Topology.IsQuotientMap

Modified Mathlib/Topology/Homeomorph/Defs.lean

Modified Mathlib/Topology/Maps/Basic.lean

deleted theorem Topology.IsInducing.IsQuotientMap.of_comp_of_eq_coinduced

added theorem Topology.IsInducing.IsQuotientMap.of_comp_of_isCoinducing

added theorem Topology.IsInducing.isCoinducing_iff

added theorem Topology.IsInducing.isCoinducing_iff_isClosed

deleted theorem Topology.IsInducing.isQuotientMap_iff

Modified Mathlib/Topology/Maps/OpenQuotient.lean

Modified Mathlib/Topology/Order/ProjIcc.lean

modified theorem isQuotientMap_projIcc

Modified Mathlib/Topology/Sequences.lean