closed immersions

Stream: LftCM22

[Sam van G]

@Sina, @Jake Levinson, and I (with the support of @Johan Commelin) started looking at the closed immersion project and were able to write a definition of closed immersion for schemes. A goal could be to eventually prove (2) <=> (4) in this theorem. As a first step, I would like to show that when I is an ideal in a commutative ring R, then applying Spec to the quotient map R ↠ R/I gives a closed embedding between the Zariski spectra.
I just committed some more code towards proving this first step - to be continued tomorrow.

[Sam van G]

Some very similar and useful existing stuff is in this mathlib file.
For now I opted for the least fancy possible proof, going directly to the definitions. There may be a way to do it in a slicker way using properties of the functor Spec.

[Sam van G]

@Jake Levinson and I managed to prove the first step today and just made a first pull request

[Anatole Dedecker]

This is really nice, I didn't expect a PR to come out of these projects so quickly !

[Anatole Dedecker]

It's not a big deal at all if you've got something wrong for a first PR, but you may want to read https://leanprover-community.github.io/contribute/index.html if you didn't already

[Sam van G]

Thanks Anatole! I'm finding that sitting right next to some experts in person is a great help...
I will update the commit message format

[Andrew Yang]

Great work!
For the project itself, I think it would be easier (and sufficient) to deal with the case where the target is affine.
There are some code here that contains an untidied proof that a closed embedding into an affine scheme is affine, which should be useful.
Also, I just opened a PR about surjective morphisms of (pre)sheaves (#15283), and it would be great if we could somehow link the two definitions.

[Jake Levinson]

Andrew, do you mean it would be an easier goal for the time frame of LFTCM this week? Or that the eventual global definition should be set up that way (i.e. closed immersion := morphism covered by closed immersions with affine targets)?

[Jake Levinson]

I think the global definition of closed immersion won't be too bad, it just needs your is_surjective definition for maps of sheaves.

[Jake Levinson]

There is also code written by @Jujian Zhang on another branch: https://github.com/leanprover-community/mathlib/compare/jjaassoonn/closed_immersion. I think it defines closed immersion via maps of sheaves that are surjective on stalks.

[Andrew Yang]

Yeah I also think that the global definition would be better.
I meant that to show the equivalence, I think it would be sufficient (and easier?) to show that
is_closed_immersion f ↔ ∀ (U : Y.affine_opens), is_closed_immersion (f ∣_ U) (The ∣_ part requires #14972)
and to show that for a [is_affine Y] (f : X ⟶ Y),
is_closed_immersion f ↔ is_affine X ∧ function.surjective (Scheme.Γ.map f.op)

[Jake Levinson]

Oh I see, that makes sense.

[Jake Levinson]

Following your PR #15283, it would be nice to add the equivalence between your definition of is_surjective via local coverings of sections, vs. surjectivity on stalks.

[Jake Levinson]

(I don't know how easy or hard that would be)

[Andrew Yang]

That PR is about sheaves on sites, and we do not yet have stalks on sites.
I'll definitely add that equivalence in the case of sheaves on spaces, but probably in the later PR.

[Jake Levinson]

Oh I see. Should we use your #15283 definition (of surjectivity) or write one independently for sheaves on spaces? I don't know much about sites.

[Andrew Yang]

I think using the definition in Jujian's code is fine for now? Is there any other property of surjectivity that you will need?
We could change it once we have surjective iff surjective on stalks.

[Kevin Buzzard]

If you are looking for a project after closed embeddings, we would love proper morphisms. We nearly have projective morphisms because of my PhD student Jujian Zhang, and it would be great to prove projective morphisms were proper.

[Andrew Yang]

It is definitely on the way. But it will probably take a while until it gets into mathlib because of the thousands of lines before it.

[Nikolas Kuhn]

I have also been working towards some properties of schemes, maybe we could coordinate as to what's going on and how to divide up tasks @Andrew Yang @Jake Levinson @Sam van G ? If you guys are already coordinated, I'd be happy to get roped in :)

For example, I thought about how to deal with local properties and have written up that finite-typeness is local on the source.

[Nikolas Kuhn]

Generally, is there some central place to track ongoing projects like this? I seem to only always seem vague references to things.

[Andrew Yang]

Oh, I didn't know that! I have these code that I did earlier this year and I am slowly pushing them into master. #15379 is also relavant. Maybe we could figure out a way to merge our efforts?

[Andrew Yang]

Ideally, a good place to gather and discuss is this topic, but it kind of died down in part because there isn't much people working on it now. To my knowledge, there is only Jujian who is working on sheaves of modules and Proj, and me who is working on morphism classes. Most of the other people interested in pushing algebraic geometry library are in the LTE hype.

[Nikolas Kuhn]

Ok, neat! Having a look there.

[Kevin Buzzard]

LTE hype is so last year, we need new hype

[Kevin Buzzard]

Maybe algebraic geometry can be the new hype

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

Maybe algebraic geometry can be the new hype

I can believe that :-) Btw, will you also post your slides from yesterday's lecture?

[Kevin Buzzard]

talk.pdf My slides

[Flo (Florent Schaffhauser)]

Thanks!