Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-15 08:05 60bc370d

View on Github →

feat(category_theory/sites/limits): Sheaf_to_presheaf creates limits (#10328) As a consequence, we obtain that sheaves have limits (of a given shape) when the target category does, and that these limit sheaves are computed on each object of the site "pointwise".

Estimated changes