feat(CategoryTheory/Sites): local sites

[peabrainiac]

A local site is a site with a terminal object whose only covering sieve is the trivial one. We define local sites, construct a functor coconstantSheaf on them that is right-adjoint to the global sections functor, prove that this functor and hence also the constant sheaf functor are fully faithful, and give several further characterisations of local sites.

---

A previous iteration of this was in #22817 already, but never got merged; this PR is based not directly on that version but on https://peabrainiac.github.io/lean-catdg/docs/CatDG/ForMathlib/LocalSite.html which I had developed a bit more since. Not all features from that file are included here to keep the PR small (in particular, I've left out the construction of the localTopology and proof that a site is local iff it is contained in that), but I did include some naming changes and IsLocalSite.tfae which was not in the previous PR.

Another difference is that Presheaf.coconst is now constructed explicitly instead of as a composition of several standard functors. @chrisflav I briefly asked you about this earlier, and you said that you preferred the construction as a composition, but after trying both approaches I came to the conclusion that the explicit approach is a lot more workable - the reason for this is that Presheaf.coconst.obj A sends each object X of the site to the type of functions (⊤_ C ⟶ X) → A, and it is important to be able to work with these functions explicitly. Defining Presheaf.coconst in terms of yoneda and coyoneda previously worked for this because morphism types in Type were defeq to function types, but since a recent refactor they aren't anymore, which adds yet another source of friction in addition to the two ULifts that that definition inserts. I think even though that definition was elegant/nice, it is more important that Presheaf.coconst evaluates up to defeq to types of functions and not morphism types involving two ULifts.

[github-actions]

PR summary 48772b84fa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Sites.LocalSite (new file)	1038

---

Declarations diff (regex)

+ GrothendieckTopology.IsLocalSite
+ GrothendieckTopology.IsLocalSite.tfae
+ IsLocalSite.coconstantSheaf
+ IsLocalSite.ΓCoconstantSheafAdj
+ LocalSite.from_terminal_mem_of_mem
+ Presheaf.coconst
+ Presheaf.coconst_isSheaf
+ coconstantSheafΓNatIsoId
+ fullyFaithfulCoconstantSheaf
+ fullyFaithfulConstantSheaf
+ instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v w} J).IsRightAdjoint
+ instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v} J).Faithful
+ instance [J.IsLocalSite] : (IsLocalSite.coconstantSheaf.{max u v} J).Full
+ instance {C : Type u} [Category.{v} C] [HasTerminal C] : (trivial C).IsLocalSite
++ instance [HasWeakSheafify J (Type max u v w)] [J.IsLocalSite] :

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

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

Current number	Change	Type (strong)
5664	2	backward.isDefEq.respectTransparency

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

Current number	Change	Type (weak)
4966	1	exposed public sections

Current commit 48772b84fa
Reference commit 8b62164d80

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).