feat(AlgebraicGeometry): restriction of quasi-coherent sheaf is quasi-coherent

[chrisflav]

---

• depends on: [Merged by Bors] - chore(Algebra/Category): add ModuleCat.restrictScalarsIsoOfEquiv #37773
• depends on: [Merged by Bors] - feat(CategoryTheory/Sites): Over.post F preserves covers if F does #37775
• depends on: [Merged by Bors] - feat(CategoryTheory/Sites): Over.post F preserves one-hypercovers if F does #38181
• depends on: [Merged by Bors] - feat(CategoryTheory/Sites): a cover preserving functor that preserves pullbacks preserves 1-hypercovers #39592
• depends on: [Merged by Bors] - chore(CategoryTheory/Limits): some API for binary (co)products #39594
• depends on: [Merged by Bors] - chore(CategoryTheory/Limits): preservation of pullbacks in terms of IsPullback #39595
• depends on: feat(Algebra/Category): pushforward of quasi-coherent sheafs #40231

[github-actions]

PR summary b2b31c9fec

Import changes exceeding 2%

%	File
+14.65%	Mathlib.CategoryTheory.Discrete.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Discrete.Basic	314	360	+46 (+14.65%)
Mathlib.CategoryTheory.Limits.Preorder	453	454	+1 (+0.22%)
Mathlib.AlgebraicGeometry.Modules.Tilde	2375	2380	+5 (+0.21%)

Import changes for all files

Files	Import difference
7 files Mathlib.CategoryTheory.Limits.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape Mathlib.CategoryTheory.SmallObject.Iteration.Basic Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty	1
Mathlib.AlgebraicGeometry.Modules.Tilde	5
Mathlib.CategoryTheory.PUnit	35
17 files Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.Comma.CatCommSq Mathlib.CategoryTheory.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HasFibers Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Square	46

---

Declarations diff (regex)

+ CoverPreserving.of_comp_of_isCocontinuous
+ Discrete.as_bijective
+ QuasicoherentData.pushforward
+ Scheme.Modules.isQuasicoherent_restrictFunctor
+ TopologicalSpace.Opens.coe_iInf
+ _root_.CategoryTheory.Limits.isLimitEquivFanOfIsThin
+ _root_.CategoryTheory.Limits.preservesLimit_walkingParallelPair_of_eq
+ _root_.CategoryTheory.isPullback_iff_isLimit_binaryFan_of_isThin
+ appIso_hom_naturality
+ coverPreserving_opensFunctor
+ instance (priority := low) {C D : Type*} [Category* C] [Category* D] [Quiver.IsThin C]
+ instance (priority := low) {C D : Type*} [Category* C] [Category* D] [Quiver.IsThin C] (F : C ⥤ D) :
+ instance : f.opensFunctor.Full
+ instance : f.opensFunctor.IsCocontinuous (Opens.grothendieckTopology _)
+ instance : f.opensFunctor.IsLeftAdjoint
+ instance {C D : Type*} [Category* C] [Category* D] (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) :
+ instance {D : Type*} [Category* D] {J : GrothendieckTopology C} {K : GrothendieckTopology D}
+ instance {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : (Over.map f).IsLeftAdjoint
+ instance {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : (Over.pullback f).IsRightAdjoint
+ instance {X Y : TopCat.{u}} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding f) :
+ instance {X Y : TopCat.{u}} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding f) {ι : Type*} [Nonempty ι]
+ isColimitISup
+ isLeftAdjoint_pushforward_of_isIso
+ isLimitIInf
+ isQuasicoherent_over
+ isQuasicoherent_pushforward
+ isQuasicoherent_pushforward_of_isLeftAdjoint
+ opensFunctorAdjunction
+ range_functor
+ sieve₀_map
++ instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit b2b31c9fec
Reference commit 185c8cd930

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

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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

[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] - chore(Algebra/Category): add ModuleCat.restrictScalarsIsoOfEquiv #37773
• [Merged by Bors] - feat(CategoryTheory/Sites): Over.post F preserves covers if F does #37775
• [Merged by Bors] - feat(CategoryTheory/Sites): Over.post F preserves one-hypercovers if F does #38181
• [Merged by Bors] - feat(CategoryTheory/Sites): a cover preserving functor that preserves pullbacks preserves 1-hypercovers #39592
• [Merged by Bors] - chore(CategoryTheory/Limits): some API for binary (co)products #39594
• [Merged by Bors] - chore(CategoryTheory/Limits): preservation of pullbacks in terms of IsPullback #39595
• feat(Algebra/Category): pushforward of quasi-coherent sheafs #40231
  By Dependent Issues (🤖). Happy coding!