feat(AlgbraicGeometry), Hom(-, X) commutes with inverse limits for schemes of finite presentation

[erdOne]

---

• depends on: [Merged by Bors] - feat(AlgebraicGeometry): descending affine cover of an inverse limit #30988

[github-actions]

PR summary cb53e58ea4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Opens.IsBasis.isOpenCover
+ Opens.IsBasis.isOpenCover_mem_and_le
+ Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation
+ Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation_of_isAffine
+ wideCospan
+ wideSpan

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(AlgebraicGeometry): descending affine cover of an inverse limit #30988
  By Dependent Issues (🤖). Happy coding!

[dagurtomas]

I was trying to review this but got very confused until I finally scrolled to the top of the file and saw the comment "We refrain from considering diagrams in the over category since inverse limits in the over category is isomorphic to limits in Scheme. Instead we use D ⟶ (Functor.const I).obj S to say that the diagram is over the base scheme S".

Is this really a good idea? Why not just consider cones in the over category and provide proper API to move back and forth between limits in Scheme and limits in the over category?

In any case, don't you want to prove the result in the PR title, i.e. a result of the form PreservesLimit _ (yoneda.obj _)? Currently, your statement is only surjectivity of the comparison map (which is indeed the hard part). Also, it wouldn't hurt to add some documentation to these long proofs, and preferably split them up further.

[erdOne]

Is this really a good idea? Why not just consider cones in the over category and provide proper API to move back and forth between limits in Scheme and limits in the over category?

I wasn't sure at first, but since throughout the development I have never once hoped that I had a cone in Over X instead, I can quite confidently say that yes this is a good idea.

In any case, don't you want to prove the result in the PR title, i.e. a result of the form PreservesLimit _ (yoneda.obj _)?

Yes. It will come as a follow up. I don't expect it will be useful at all though. It is merely an aesthetically pleasing thing to have.

Currently, your statement is only surjectivity of the comparison map (which is indeed the hard part)

I'd say the injectivity is harder but it is already done earlier in the file.

Also, it wouldn't hurt to add some documentation to these long proofs, and preferably split them up further.

Sure I'll try to add some docstrings.

[chrisflav]

Thanks!
maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by chrisflav.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Build failed (retrying...):

• ci (staging) / Post-CI job

[mathlib-bors]

Build failed:

• ci (staging) / Post-Build Step

[riccardobrasca]

There are still a couple of errors, can you fix them? Thanks!

bors d+

[mathlib-bors]

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-merge-conflicts]

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