Commit 2024-06-17 14:29 402ae165

View on Github →

feat(CategoryTheory): characterise the covering sieves for the extensive topology (#13897)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

added def CategoryTheory.Limits.Cofan.isColimitTrans

added theorem CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

modified theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts

modified theorem CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts

Created Mathlib/CategoryTheory/Sites/Coherent/ExtensiveTopology.lean

added theorem CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan

Modified Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean

added def CategoryTheory.Presheaf.coherentExtensiveEquivalence

added theorem CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projective