Commit 2025-10-25 22:49 086483d5

View on Github →

feat(CategoryTheory/Sites): more API for zero hypercovers (#30906) We add constructors for isomorphisms of (pre)-0-hypercovers and operations relating Presieves and pre-0-hypercovers.

Estimated changes

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

added theorem CategoryTheory.PreZeroHypercover.Hom.ext'

added theorem CategoryTheory.PreZeroHypercover.Hom.ext'_iff

added def CategoryTheory.PreZeroHypercover.fromShrink

added theorem CategoryTheory.PreZeroHypercover.hom_inv_h₀

added theorem CategoryTheory.PreZeroHypercover.hom_inv_s₀_apply

added theorem CategoryTheory.PreZeroHypercover.inv_hom_h₀

added theorem CategoryTheory.PreZeroHypercover.inv_hom_s₀_apply

added def CategoryTheory.PreZeroHypercover.isoMk

added theorem CategoryTheory.PreZeroHypercover.presieve₀_eq_presieve₀_iff

added theorem CategoryTheory.PreZeroHypercover.presieve₀_shrink

added def CategoryTheory.PreZeroHypercover.shrink

added theorem CategoryTheory.PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀

added def CategoryTheory.PreZeroHypercover.toShrink

added def CategoryTheory.Precoverage.ZeroHypercover.isoMk

added theorem CategoryTheory.Precoverage.le_of_zeroHypercover

added theorem CategoryTheory.Presieve.exists_eq_preZeroHypercover

added def CategoryTheory.Presieve.preZeroHypercover

added theorem CategoryTheory.Presieve.presieve₀_preZeroHypercover