feat(CategoryTheory/Sites): the fiber functor associated to Point.comap

[joelriou]

The definition Point.comap is moved to a separate file. Using results on skyscraper sheaves, we obtain that if F : C ⥤ D is a representably flat continuous functor between sites (C, J) and (D, K), Φ is a point of (D, K), then the fiber functor attached to the point Φ.comap F hF of the site (C, J) (where hF : CoverPreserving J K F) identifies to the composition of the pullback functor for F followed by the fiber functor attached to the point Φ. This is a generalization to arbitrary sites of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Sheaves/Stalks.html#TopCat.Presheaf.stalkPullbackIso

Co-authored-by: Christian Merten

---

• depends on: feat(CategoryTheory/Sites): skyscraper sheaves #35719

[github-actions]

PR summary 360d94e7b3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Sites.Point.Skyscraper (new file)	1145
Mathlib.CategoryTheory.Sites.Point.Comap (new file)	1147

---

Declarations diff

+ isSheaf_skyscraperPresheaf
+ isSheaf_skyscraperPresheaf_aux
+ piFunctor
+ sheafFiberComapIso
+ sigmaFunctor
+ skyscraperPresheaf
+ skyscraperPresheafAdjunction
+ skyscraperPresheafFunctor
+ skyscraperPresheafHomEquiv
+ skyscraperPresheafHomEquiv_app_π
+ skyscraperPresheafHomEquiv_naturality_left_symm
+ skyscraperPresheafHomEquiv_naturality_right
+ skyscraperSheaf
+ skyscraperSheafAdjunction
+ skyscraperSheafFunctor
+ skyscraperSheafFunctorCompSheafPushforwardContinuous
+ toPresheafFiber_skyscraperPresheafHomEquiv_symm

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/Sites): skyscraper sheaves #35719
  By Dependent Issues (🤖). Happy coding!