Commit 2026-04-23 19:41 99adb0aa

View on Github →

feat(CategoryTheory/Sites): Over.post F preserves one-hypercovers if F does (#38181)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Continuous.lean

added theorem CategoryTheory.PreOneHypercover.map_comp

added theorem CategoryTheory.PreOneHypercover.map_id

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

added theorem CategoryTheory.PreZeroHypercover.sieve₀_map

Modified Mathlib/CategoryTheory/Sites/Over.lean

added theorem CategoryTheory.Sieve.overEquiv_ofArrows

added theorem CategoryTheory.Sieve.overEquiv_preOneHypercover_sieve₁

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Sieve.functorPushforward_ofArrows