Commit 2025-09-14 16:34 07e43156

View on Github →

feat(CategoryTheory/Sites): functoriality of precoverages and 0-hypercovers (#29472)

Estimated changes

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

added def CategoryTheory.PreZeroHypercover.map

added theorem CategoryTheory.PreZeroHypercover.presieve₀_map

added def CategoryTheory.Precoverage.ZeroHypercover.map

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

added def CategoryTheory.Precoverage.comap

added theorem CategoryTheory.Precoverage.comap_inf

added theorem CategoryTheory.Precoverage.mem_comap_iff

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.map_map

added theorem CategoryTheory.Presieve.map_ofArrows

added theorem CategoryTheory.Presieve.map_singleton

added theorem CategoryTheory.Presieve.ofArrows.mk'