Commit 2025-11-27 10:43 1ad1c36c

View on Github →

feat(CategoryTheory/Sites): cover of pullback from cover of left or right component (#31336) To construct this, we also add a typeclass Precoverage.RespectsIso that asserts that a pre-0-hypercover being covering for a precoverage J implies being covering for every isomorphic pre-0-hypercover.

Estimated changes

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

added theorem CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f

added theorem CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f

added theorem CategoryTheory.PreZeroHypercover.presieve₀_mem_iff_of_iso

added theorem CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso

added def CategoryTheory.PreZeroHypercover.pullbackCoverOfLeftIsoPullback₁

added def CategoryTheory.PreZeroHypercover.pullbackCoverOfRightIsoPullback₂

added theorem CategoryTheory.Precoverage.RespectsIso.of_forall_exists_iso

added theorem CategoryTheory.Precoverage.ZeroHypercover.presieve₀_mem_of_iso

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.ofArrows_comp_eq_of_surjective

added theorem CategoryTheory.Presieve.ofArrows_comp_le