Commit 2025-09-22 17:31 eb10b353

View on Github →

feat(CategoryTheory/Sites): jointly surjective precoverage (#29883) We define the precoverage on Type u of jointly surjective families. This precoverage can be pulled-back along a (forgetful) functor from C to Type u to obtain a precoverage on C. We show that the obtained precoverage is stable under base change if the pullback comparison map is surjective. This will be used to define the jointly surjective precoverage on the category of schemes.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Types/Pullbacks.lean

added theorem CategoryTheory.Limits.Types.range_fst_of_isPullback

added theorem CategoryTheory.Limits.Types.range_pullbackFst

added theorem CategoryTheory.Limits.Types.range_pullbackSnd

added theorem CategoryTheory.Limits.Types.range_snd_of_isPullback

Created Mathlib/CategoryTheory/Sites/JointlySurjective.lean

added theorem CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff

added def CategoryTheory.Types.jointlySurjectivePrecoverage

added theorem CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iff

added theorem CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff

added theorem CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff

added theorem CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

added theorem CategoryTheory.Precoverage.comap_id

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Presieve.map_id