Commit 2026-02-01 14:48 e3128c5d

View on Github →

chore(CategoryTheory/Sites): generalize universes in Sheaf.isSheaf_of_isRepresentable (#34234) For this we add some API on representable functors.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Ulift.lean

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

modified theorem CategoryTheory.Sheaf.isSheaf_of_isRepresentable

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

modified theorem CategoryTheory.Presieve.isSheaf_comp_uliftFunctor

added theorem CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.Functor.uliftCoyonedaCoreprXIso_hom_app

added theorem CategoryTheory.Functor.uliftYonedaReprXIso_hom_app