Commit 2026-03-13 23:21 1efa5b0e

View on Github →

chore(CategoryTheory/Sites): generalize universes in Presieve.isSheafFor_iff_yonedaSheafCondition (#36461) We add a shrinkYoneda version and deduce the existing one from that.

Estimated changes

Modified Mathlib/CategoryTheory/ShrinkYoneda.lean

added def CategoryTheory.shrinkYonedaIsoYoneda

added theorem CategoryTheory.shrinkYonedaObjObjEquiv_map_app

added theorem CategoryTheory.shrinkYonedaObjObjEquiv_obj_map

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

deleted theorem CategoryTheory.Presieve.extension_iff_amalgamation

added theorem CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp

deleted def CategoryTheory.Presieve.natTransEquivCompatibleFamily

added theorem CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added def CategoryTheory.Sieve.shrinkFunctor

added def CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso

added theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι