feat(CategoryTheory): presheaves of types which preserve a limit

[joelriou]

Let F : J ⥤ Cᵒᵖ be a functor. We show that a presheaf P : Cᵒᵖ ⥤ Type w preserves the limit of F iff P is a local object with respect to a suitable family of morphisms in Cᵒᵖ ⥤ Type w (this family contains 1 or 0 morphism depending on whether the limit of F exists or not).

---

• depends on: feat(CategoryTheory): MorphismProperty.single #38257

[github-actions]

PR summary 42a89fc2b9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.Presheaf (new file)	870

---

Declarations diff

+ coconeCompShrinkYonedaHomEquiv
+ coconePtToShrinkYoneda
+ coconePtToShrinkYoneda_comp
+ iSup_ofHoms
+ instance {α : Type t} [Small.{w} α] (W : α → MorphismProperty C) [∀ i, IsSmall.{w} (W i)] :
+ isColocal_iSup
+ isColocal_single_iff_bijective
+ isLocal_iSup
+ isLocal_single_iff_bijective
+ nonempty_isLimit_mapCone_iff
+ preservesLimitHomFamily
+ preservesLimitHomFamilySrc
+ preservesLimitHomFamilyTgt
+ preservesLimit_eq_isLocal
+ preservesLimit_eq_isLocal_single
+ preservesLimitsOfShape_eq_isLocal
+ single

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
6538	3	backward.isDefEq.respectTransparency

Current commit d666851284
Reference commit 42a89fc2b9

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[robin-carlier]

a few questions/suggestions for this one

• This definition should be in an other file: I think CategoryTheory.Limits.Types.Yoneda is a good target (because it contains the similar construction I link below).
• This is essentially (a variation on) the LocallySmall + shrinkYoneda version of the existing CategoryTheory.Limits.compCoyonedaSectionsEquiv, so the docstring should at least reference this? (Though it is not the exact same construction).
• To mimic the pattern from CategoryTheory.Limits.compCoyonedaSectionsEquiv, perhaps this should instead first be stated as an equivalence with natural transformations from the constant functor (dropping c' from the parameters) to a composition with shrinkYoneda, and then maybe for the result in this file you can work with composing this with an equivalence between morphisms out of c'.pt and natural transformations out of a constant functor in that case?

[joelriou]

Thanks for the suggestion, but I do not see any relation with compCoyonedaSectionsEquiv. As IsColimit appears in all the definitions, I do not think it would make sense to break the cocone c' into two variables.

[robin-carlier]

Okay, but can you still move that part (say up to l. 83) to the file CategoryTheory.Limits.Types.Yoneda (or a new file under CategoryTheory/Limits/Types if there are import increase issues)? It has pretty low discoverability within ObjectProperty/.

[robin-carlier]

I still have a nitpick about the location of the result relating sections and morphisms from the cocone point, but otherwise LGTM.

[robin-carlier]

Okay, but can you still move that part (say up to l. 83) to the file CategoryTheory.Limits.Types.Yoneda (or a new file under CategoryTheory/Limits/Types if there are import increase issues)? It has pretty low discoverability within ObjectProperty/.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory): MorphismProperty.single #38257
  By Dependent Issues (🤖). Happy coding!