[Merged by Bors] - feat(AlgebraicGeometry): directed covers

[chrisflav]

Directed covers are covers, where every intersection can be covered by a component of the cover. For open covers this is equivalent to the images forming a basis of the topology.

If a cover is directed, the compatibility conditions for gluing become easier, because only compatibility with the transition maps needs to be checked. In particular, the covered scheme naturally is the colimit of the components
of the cover.

---

[github-actions]

PR summary d1e01e284e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Cover.Directed (new file)	2192

---

Declarations diff

+ Cover.LocallyDirected.ofIsBasisOpensRange
+ Cover.LocallyDirected.ofIsBasisOpensRange_le_iff
+ Cover.LocallyDirected.ofIsBasisOpensRange_trans
+ LocallyDirected
+ coconeOfLocallyDirected
+ directedAffineCover
+ directedAffineCover_trans
+ exists_lift_trans_eq
+ functorOfLocallyDirected
+ glueMorphismsOfLocallyDirected
+ glueMorphismsOverOfLocallyDirected
+ instance : (𝒰.functorOfLocallyDirected ⋙ Scheme.forget).IsLocallyDirected
+ instance : Category (𝒰.pullbackCover f).J := inferInstanceAs <| Category 𝒰.J
+ instance : Preorder X.directedAffineCover.J := inferInstanceAs <| Preorder X.affineOpens
+ instance : Scheme.Cover.LocallyDirected X.directedAffineCover
+ instance {i j : 𝒰.J} (f : i ⟶ j) : IsOpenImmersion (𝒰.functorOfLocallyDirected.map f)
+ instance {i j : 𝒰.J} (f : i ⟶ j) : IsOpenImmersion (𝒰.trans f)
+ intersectionOfLocallyDirected
+ isColimitCoconeOfLocallyDirected
+ locallyDirectedPullbackCover
+ map_glueMorphismsOfLocallyDirected
+ map_glueMorphismsOverOfLocallyDirected_left
+ property_trans
+ trans
+ trans_comp
+ trans_id
+ trans_map

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

[joelriou]

Is this notion used somewhere in the literature?

[chrisflav]

I don't know, but it will be used to simplify the proof of the relative gluing lemma #18284 (which is stacks tag https://stacks.math.columbia.edu/tag/01LH). This lemma I need to construct colimits in over categories by gluing the affine pieces, which is used to obtain existence of colimits of shape J in Affine S from existence of limits of shape Jᵒᵖ in Under R.

Working with directed covers makes gluing much easier, because no intersections need to be considered.

[leanprover-community-bot-assistant]

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

[mattrobball]

I see unresolved conversations so I am tagging as awaiting-author.

[mattrobball]

I don't love that we jump to a general Category instance instead of working with a Preorder or something similar for the indexing type.

[mattrobball]

Could you comment on this design choice? Thanks.

[chrisflav]

I don't love that we jump to a general Category instance instead of working with a Preorder or something similar for the indexing type.

The first version of this PR indeed assumed a Preorder instance and in my application, this is the only case I need. But @erdOne raised (via DM) the suggestion to generalize it to Category, because it might be useful for gluing morphisms out of X in cases like J = WalkingCospan which is equivalent to a preorder, but not equal (possible use case: a scheme obtained from gluing two schemes along an open, e.g. projective line).

We could postpone this generalization to the point we actually need it, but the cost of having Category instead of Preorder is quite low, so I decided against it.

[mattrobball]

I think the overhead is not terrible for a Category and wanted to make sure there was a plausible use case for the generality. Seems ok.

bors merge

[chrisflav]

Thanks for the reviews!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success