Commit 2025-09-09 23:34 a862963e

View on Github →

feat(CategoryTheory/Sites): more constructions for ZeroHypercover (#29467) They are mostly "upstreamed" constructions from AlgebraicGeometry.Scheme.Cover.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

Modified Mathlib/CategoryTheory/Sites/ZeroHypercover.lean

added def CategoryTheory.PreZeroHypercover.add

added theorem CategoryTheory.PreZeroHypercover.add_X_none

added theorem CategoryTheory.PreZeroHypercover.add_X_some

added theorem CategoryTheory.PreZeroHypercover.add_f_nome

added theorem CategoryTheory.PreZeroHypercover.add_f_some

added def CategoryTheory.PreZeroHypercover.inter

added theorem CategoryTheory.PreZeroHypercover.inter_def

added theorem CategoryTheory.PreZeroHypercover.presieve₀_add

added theorem CategoryTheory.PreZeroHypercover.presieve₀_f

modified theorem CategoryTheory.PreZeroHypercover.presieve₀_pullback₁

added theorem CategoryTheory.PreZeroHypercover.presieve₀_reindex

added theorem CategoryTheory.PreZeroHypercover.presieve₀_singleton

added theorem CategoryTheory.PreZeroHypercover.presieve₀_sum

added def CategoryTheory.PreZeroHypercover.reindex

added theorem CategoryTheory.PreZeroHypercover.sieve₀_f

added def CategoryTheory.PreZeroHypercover.sum

added def CategoryTheory.PreZeroHypercover.sumInl

added def CategoryTheory.PreZeroHypercover.sumInr

added def CategoryTheory.PreZeroHypercover.sumLift

added theorem CategoryTheory.PreZeroHypercover.sum_X_inl

added theorem CategoryTheory.PreZeroHypercover.sum_X_inr

added theorem CategoryTheory.PreZeroHypercover.sum_f_inl

added theorem CategoryTheory.PreZeroHypercover.sum_f_inr

added def CategoryTheory.Precoverage.ZeroHypercover.add

added def CategoryTheory.Precoverage.ZeroHypercover.inter

modified def CategoryTheory.Precoverage.ZeroHypercover.pullback₁

modified def CategoryTheory.Precoverage.ZeroHypercover.pullback₂

added def CategoryTheory.Precoverage.ZeroHypercover.reindex

added def CategoryTheory.Precoverage.ZeroHypercover.sum

modified structure CategoryTheory.Precoverage.ZeroHypercover

added theorem CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover