Theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι

Modification history

2026-08-23 14:46

Mathlib/CategoryTheory/Sites/Sieves.lean

refactor(CategoryTheory/Sites): split long file Sieves.lean (#43014) …

Modified CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι View on Github →

2026-03-13 23:21

Mathlib/CategoryTheory/Sites/Sieves.lean

chore(CategoryTheory/Sites): generalize universes in `Presieve.isSheafFor_iff_yonedaSheafCondition` (#36461) …

Added CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι View on Github →