Commit 2026-03-07 20:02 1b6e7d48

View on Github →

chore(CategoryTheory/Sites): API for the trivial sieve and the trivial topology (#36325)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Closed.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

added theorem CategoryTheory.GrothendieckTopology.bot_eq_top_iff_isEmpty

added theorem CategoryTheory.GrothendieckTopology.bot_lt_top_iff_nonempty

added theorem CategoryTheory.GrothendieckTopology.eq_top_iff

added theorem CategoryTheory.GrothendieckTopology.eq_top_of_isEmpty

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

added def CategoryTheory.PreZeroHypercover.empty

added theorem CategoryTheory.PreZeroHypercover.presieve₀_empty

Modified Mathlib/CategoryTheory/Sites/Over.lean

added theorem CategoryTheory.Sieve.overEquiv_bot

added theorem CategoryTheory.Sieve.overEquiv_symm_bot

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.ofArrows_of_isEmpty

added theorem CategoryTheory.Sieve.arrows_bot

added theorem CategoryTheory.Sieve.arrows_eq_bot_iff

added theorem CategoryTheory.Sieve.bot_apply

added theorem CategoryTheory.Sieve.generate_eq_bot_iff

added theorem CategoryTheory.Sieve.pullback_bot

added theorem CategoryTheory.Sieve.pushforward_bot

added theorem CategoryTheory.Sieve.pushforward_eq_bot_iff

added theorem CategoryTheory.bot_apply