feat(AlgebraicGeometry): category of schemes affine over a base

[erdOne]

---

[github-actions]

PR summary c5134ef9dc

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.Morphisms.Affine	2240	2246	+6 (+0.27%)

Import changes for all files

Files	Import difference
5 files Mathlib.AlgebraicTopology.ModelCategory.Over Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits	1
Mathlib.AlgebraicGeometry.Sites.Etale	4
Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono	5
30 files Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.ValuativeCriterion	6
Mathlib.AlgebraicGeometry.AffineOver (new file)	2278

---

Declarations diff

+ CoequifiberedAlgCat
+ CoequifiberedAlgCat.gluingData
+ CoequifiberedAlgCat.ι_gluingData_toBase
+ CoequifiberedAlgCatEquivOver
+ CoequifiberedAlgCatEquivOver_inverse_map_unop_hom_right_app
+ CoequifiberedAlgCatEquivOver_inverse_obj_unop_obj_hom_app
+ CoequifiberedAlgCatEquivOver_inverse_obj_unop_obj_right_map
+ CoequifiberedAlgCatEquivOver_inverse_obj_unop_obj_right_obj
+ CoequifiberedAlgCatEquivOver_unitIso_hom_app_unop_hom_right_app
+ CoequifiberedAlgCatForget
+ CoequifiberedAlgCatOfOver
+ CoequifiberedAlgCatRestrict
+ CoequifiberedAlgCatToOver
+ IsOpenImmersion.presheafIso
+ Scheme.AffineZariskiSite.preimage
+ image
+ instance : CreatesColimits X.CoequifiberedAlgCatForget
+ instance : HasColimits X.CoequifiberedAlgCat
+ instance : HasLimits (MorphismProperty.Over @IsAffineHom ⊤ X)
+ instance : PreservesLimits (MorphismProperty.Over.forget @IsAffineHom ⊤ X) := by
+ instance : PreservesLimits (MorphismProperty.Over.pullback @IsAffineHom ⊤ f) := by
+ instance : ReflectsLimits (MorphismProperty.Over.forget @IsAffineHom ⊤ X)
+ instance [IsConnected J] {B : C} : PreservesColimitsOfShape J (Under.forget B) := by
+ instance [IsConnected J] {B : C} : ReflectsColimitsOfShape J (Under.forget B) := by
+ instance [IsOpenImmersion f] :
+ instance {F : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat}
+ instance {X : Scheme.{u}} (F : X.CoequifiberedAlgCat) (U : X.AffineZariskiSite) :
+ instance {f : MorphismProperty.Over @IsAffineHom ⊤ X} : IsAffineHom f.hom := f.prop
+ isLimitOverOfOpenCover
+ relativeGluingData_toBase_preimage

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

[mathlib4-merge-conflict-bot]

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

[dagurtomas]

This erw, the two noted defeq abuses earlier in the proof, and the length of the proof, suggest to me that we should try to build some small custom API and break it down into smaller pieces. Do you think this is feasible?

[erdOne]

I have removed this proof.

[dagurtomas]

"essentially" -- is this the official mathlib definition of the category of quasi-coherent 𝒪ₓ-algebras, or does that definition exist elsewhere, or are there plans to add it?

[erdOne]

We are quite far from the "official mathlib definition" so we can only make do with this ad-hoc definition for the time being. I think this is fine because once we have the "official definition" we would still want to show that it is isomorphic to this category and then use the API here.

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