Commit 2023-11-14 07:28 4b14c4ca

View on Github →

feat(CategoryTheory): a presheaf preserves certain products iff it IsSheafFor certain presieves (#7804) A presheaf preserving a particular product IsSheafFor the corresponding Presieve.ofArrows. Conversely, if a presheaf IsSheafFor a Presieve.ofArrows and the empty presive on an initial object, then it preserves the corresponding product.

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.Cofan.ext

added def CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc

Created Mathlib/CategoryTheory/Sites/Preserves.lean

added theorem CategoryTheory.Presieve.firstMap_eq_secondMap

added theorem CategoryTheory.Presieve.isSheafFor_iff_preservesProduct

added theorem CategoryTheory.Presieve.isSheafFor_of_preservesProduct

added def CategoryTheory.Presieve.isTerminal_of_isSheafFor_empty_presieve

added theorem CategoryTheory.Presieve.piComparison_fac

added def CategoryTheory.Presieve.preservesProductOfIsSheafFor

added def CategoryTheory.Presieve.preservesTerminalOfIsSheafForEmpty