Commit 2026-02-09 14:35 43178d5f

View on Github →

feat(Topology/Category): the standard Grothendieck topology on TopCat (#34979) We define the Grothendieck topology generated by families of jointly surjective open embeddings on TopCat and show it is subcanonical. This will be used to show that for a topological space T, the presheaf U ↦ C(U, T) on Scheme is a Zariski-sheaf. Co-authored by: Edward van de Meent edwardvdmeent@gmail.com From Proetale.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_forall_exists_isPullback

added theorem CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_forall_exists_isPullback

Modified Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

added theorem CategoryTheory.Precoverage.Small.inf

Modified Mathlib/CategoryTheory/Sites/JointlySurjective.lean

Created Mathlib/Topology/Category/TopCat/GrothendieckTopology.lean

added theorem TopCat.exists_mem_zeroHypercover_range

added def TopCat.isOpenEmbedding

added theorem TopCat.isOpenEmbedding_f_zeroHypercover

added theorem TopCat.isOpenEmbedding_iff

added def TopCat.precoverage

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

added theorem Topology.IsClosedEmbedding.uliftMap

added theorem Topology.IsEmbedding.toHomeomorph_symm_apply

added theorem Topology.IsEmbedding.uliftMap

added theorem Topology.IsOpenEmbedding.uliftMap