base-change of localization

Stream: Is there code for X?

[Adam Topaz]

Dear algebraic geometers of mathlib,

I would be surprised if something like the following doesn't already exist. Can someone point me in the right direction?

import Mathlib

def IsBasicOpen {A B : CommRingCat.{u}} (e : A ⟶ B) (f : A) : Prop :=
  letI : Algebra A B := RingHom.toAlgebra e
  IsLocalization.Away f B

lemma IsBasicOpen.pushout
    {A A' B B' : CommRingCat.{u}}
    {e : A ⟶ B}
    {e' : A' ⟶ B'}
    (g' : B ⟶ B')
    {f : A}
    (h : IsBasicOpen e f)
    (g : A ⟶ A')
    (hh : CategoryTheory.IsPushout e g g' e') :
    IsBasicOpen e' (g f) :=
  sorry

[Adam Topaz]

.... sigh I can't even find the assertion that the base change of a localization is a localization. Do we really not have this?!

[Kevin Buzzard]

That's the kind of question which makes me wish I was better at loogling.

[Kevin Buzzard]

@loogle Localization, TensorProduct

[Michael Stoll]

@loogle Localization, TensorProduct

[loogle]

:shrug: nothing found

[Michael Stoll]

@loogle Localization

[loogle]

:search: Localization, Localization.one, and 172 more

[Adam Topaz]

@loogle IsLocalization, TensorProduct

[loogle]

:shrug: nothing found

[Kevin Buzzard]

So what do those responses mean? No theorems with both those functions in the conclusion? No theorems which mention both those functions anywhere at all? etc etc

[Michael Stoll]

No theorems that mention both of these anywhere.

[Kevin Buzzard]

Do we have IsTensorProduct? :-)

[Ruben Van de Velde]

@loogle IsTensorProduct

[loogle]

:search: TensorProduct.isTensorProduct, IsTensorProduct, and 9 more

[Ruben Van de Velde]

(deleted)

[Ruben Van de Velde]

@loogle IsTensorProduct, IsLocalization

[loogle]

:shrug: nothing found

[Adam Topaz]

:sad:

[Kevin Buzzard]

@loogle IsTensorProduct, Localization

[Michael Stoll]

(Type "@loo" and then select @loogle from the pop-up...)

[Kevin Buzzard]

Oh yeah, on mobile so didn't spot I'd got it wrong. What are the chances? :-)

[Kevin Buzzard]

@loogle IsTensorProduct Localization

[loogle]

:search: TensorProduct.isTensorProduct, IsTensorProduct.equiv, and 8 more

[Kevin Buzzard]

What does that output mean? Either/or, anywhere?

[Kevin Buzzard]

@loogle IsTensorProduct, Localization

[loogle]

:shrug: nothing found

[Kevin Buzzard]

Oh, like it means "I ignored Localization"? My loogle-fu is still so weak

[Adam Topaz]

In case anyone is wondering, this is the last thing I need to show that the functor of points of a scheme is a sheaf on the Zariski site on CommRingCat^op. It feels so silly that we don't have this!

[Kevin Buzzard]

Post the statement, finish the functor job and see if someone's nerdsniped into doing it :-)

[Adam Topaz]

it's in branch#AT-functor-of-points-zariski-descent

[Joël Riou]

I wonder whether your code could be adapted in order to obtain slightly more general results:

1. the Zariski topology on Scheme.{u} is subcanonical: this is the glueing of morphisms of schemes;
2. the inclusion of your Zariski affine site in the big Zariski site Scheme.{u} is a continuous functor;
3. the direct image functor for this continuous functor is fully faithful (and it would be an equivalence if we could replace Type u by Type (u + 1)...).

Then, 1. and 2. give that X.functorOfPointsis a sheaf. Then, I think that your API X.affineOpenCover could be used to prove 3. similarly as you prove the special case that schemeToFunctor is fully faithful.

[Adam Topaz]

Thanks! I’ll think more carefully about these points. For point 3, I took special care to choose Type u. Eventually I want to characterize which sheaves on CommRingCat^op arise from schemes in terms of open subfunctors etc. and define a convenient category equivalent to Scheme. It would be really cool to define, say, the Hilbert scheme in terms of its functor of points in this way :). More generally I’m interested in developing an API for doing scheme theory with just rings which is why so far I’ve mostly ignored the big Zariski site on Scheme.

[Kevin Buzzard]

At Imperial we have been taking some first tenative steps to making an API for doing the theory of affine algebraic groups with just Hopf algebras (see Amelia's 10 recent PRs; reviews of #11961 welcome); this reminds me a bit of how mathlib does elliptic curves over fields with plane cubics rather than smooth proper morphisms (note that the Frey curve is a plane cubic so this is fine for FLT).

I think that at some point we're going to have to come up with some kind of framework for representability of functors parametrising things of interest to algebraic geometers and I'd be very happy if the Hilbert scheme were the test case. For FLT I'll need moduli spaces of abelian varieties but first things first. Note that Jujian Zhang is pushing on with his work on Proj (reviews of #11920 welcome) and the Hilbert scheme was one of the applications I had in mind.

[Andrew Yang]

There is
@loogle IsLocalizedModule IsBaseChange

[Andrew Yang]

docs#isLocalizedModule_iff_isBaseChange

[Joël Riou]

For a starter, I would think that the construction of the algebraic Grassmannians (or more generally flag bundles) could be first nice applications of representability theorems based on a Zariski sheaf that is equipped with suitable representable "open subfunctors". I am not completely sure that restricting to rings is always better, but for finite flat group schemes I definitely agree (long ago, I very much enjoyed reading Tate's article in the yellow book on FLT!).

[Adam Topaz]

In any case, proving that big Zariski is subcanonical was so easy with the very nice gluing api that @Andrew Yang developed that now I think we should have all the approaches :)

[Adam Topaz]

Andrew Yang said:

There is
loogle IsLocalizedModule IsBaseChange

I can make this work. BTW, why doesn't docs#isLocalizedModule_iff_isLocalization' use docs#Algebra.linearMap ?

[Andrew Yang]

Good point. It should use that instead.

[Adam Topaz]

Ok I'll try to remember to PR a fix at somet point.

[Andrew Yang]

@Kevin Buzzard I think the approach above suggested by Adam (or Joël) above on grassmannians is the one mentioned by @Calle Sönne yesterday.