feat(AlgebraicGeometry/Sites): characterization of sheaves for the P-qc topology

[chrisflav]

From Proetale.

---

• depends on: [Merged by Bors] - feat(AlgebraicGeometry): a quasi-compact cover of a quasi-compact scheme can be refined by a finite affine cover #34923
• depends on: [Merged by Bors] - feat(CategoryTheory/Sites): various API additions for #34917 #34921
• depends on: [Merged by Bors] - chore(AlgebraicGeometry/Sites): use Precoverage.toGrothendieck instead of Pretopology.toGrothendieck #34995
• depends on: feat(AlgebraicGeometry): Zariski sheaves preserve products #35508
• depends on: feat(AlgebraicGeometry): P-qc precoverage #35509

[github-actions]

PR summary 8ca4eacd8c

Import changes exceeding 2%

%	File
+35.81%	Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct	444	603	+159 (+35.81%)

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	1
Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct	159
Mathlib.AlgebraicGeometry.Sites.Fpqc (new file)	2252

---

Declarations diff

+ CoproductDisjoint.isPullback_of_isInitial
+ Cover.forgetQc
+ Cover.mem_propqcTopology
+ Cover.ofQuasiCompactCover
+ Cover.qculift
+ Hom.generate_singleton_mem_propqcTopology
+ Hom.singleton_mem_propqcPrecoverage
+ Hom.singleton_mem_qcPrecoverage
+ Presieve.IsSheafFor.of_isSheafFor_pullback
+ Presieve.IsSheafFor.of_isSheafFor_pullback'
+ Presieve.isSheafFor_sigmaDesc_iff
+ Scheme.Cover.Hom.isSheafFor
+ Scheme.Cover.isSheafFor_sigma_iff
+ Scheme.Hom.presieve₀_cover
+ instance : Precoverage.Small.{u} (propqcPrecoverage P)
+ instance {S : Scheme.{u}} (𝒰 : S.AffineCover P) (i : 𝒰.I₀) : IsAffine (𝒰.cover.X i)
+ instance {S : Scheme.{u}} (𝒰 : S.Cover (precoverage P)) [QuasiCompactCover 𝒰.1] :
+ instance {S : Scheme.{u}} [IsAffine S] (𝒰 : S.AffineCover P) [Finite 𝒰.I₀] :
+ isSheaf_propqcTopology_iff
+ mem_propqcPrecoverage_iff_exists_quasiCompactCover
+ ofArrows_ι_mem_zariskiTopology_of_isColimit
+ preservesLimitsOfShape_discrete_of_isSheaf_zariskiTopology
+ presieve₀_sigma
+ propqcPrecoverage
+ propqcPrecoverage_le_precoverage
+ propqcTopology
+ zariskiTopology_le_propqcTopology
++ instance {S : Scheme.{u}} (𝒰 : Scheme.Cover (propqcPrecoverage P) S) :

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-merge-conflicts]

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

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(AlgebraicGeometry): a quasi-compact cover of a quasi-compact scheme can be refined by a finite affine cover #34923
• [Merged by Bors] - feat(CategoryTheory/Sites): various API additions for #34917 #34921
• [Merged by Bors] - chore(AlgebraicGeometry/Sites): use Precoverage.toGrothendieck instead of Pretopology.toGrothendieck #34995
• feat(AlgebraicGeometry): Zariski sheaves preserve products #35508
• feat(AlgebraicGeometry): P-qc precoverage #35509
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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