[Merged by Bors] - feat(AlgebraicGeometry): constant sheaf associated to a topological space

[chrisflav]

For a topological space (or topological abelian group) we define an associated constant sheaf by the rule U ↦ C(U, T). We show that this is a Zariski sheaf and a follow-up PR will show this is an fpqc sheaf.
When T is discrete, this recovers the constant sheaf.
This construction is from Lemma 4.2.12 in https://www.math.uni-bonn.de/people/scholze/proetale.pdf.

From Proetale.

---

[github-actions]

PR summary 474a9dd2e6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Category.TopCat.GrothendieckTopology	936	942	+6 (+0.64%)
Mathlib.AlgebraicGeometry.Sites.BigZariski	2250	2252	+2 (+0.09%)

Import changes for all files

Files	Import difference
4 files Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Representability	2
Mathlib.Topology.Category.TopCat.GrothendieckTopology	6
Mathlib.AlgebraicGeometry.Sites.ConstantSheaf (new file)	2253

---

Declarations diff

+ ContinuousMap.uliftEquiv
+ Hom.equivContinuousMap
+ continuousMapPresheaf
+ continuousMapPresheafAb
+ continuousMapPresheafAbForgetIso
+ continuousMapPresheafEquivOfTotallyDisconnectedSpace
+ continuousMapPresheafIsoUlift
+ forgetToTop_comp_forget
+ instance : Scheme.forgetToTop.{u}.IsContinuous zariskiTopology TopCat.grothendieckTopology := by
+ instance : uliftFunctor.IsContinuous grothendieckTopology grothendieckTopology := by
+ isSheaf_zariskiTopology_continuousMapPresheaf
+ op_comp_isSheaf_of_isSheaf
+ precoverage_le_comap_uliftFunctor

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

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Build