Schemes over fields and base change

Stream: maths

[Bryan Wang]

Are there idiomatic ways to state the following:

• scheme over a field k
• base change of this scheme to a field extension L of k

From what I can see, getting a statement is not the problem, I'm just wondering if there is a standard or if one should maybe make a definition.

[Christian Merten]

It depends on the context: The options we use are:

import Mathlib

universe u
open AlgebraicGeometry CategoryTheory Limits
noncomputable section

variable (X : Scheme.{u}) (k L : Type u) [Field k] [Field L] [Algebra k L]

-- should be the default option
example (f : X ⟶ Spec(k)) :
    pullback f (Spec.map (CommRingCat.ofHom <| algebraMap k L)) ⟶ Spec(L) :=
  pullback.snd _ _

-- sometimes a good choice
example [X.Over Spec(k)] :
    (pullback (X ↘ Spec(k))
      (Spec.map (CommRingCat.ofHom <| algebraMap k L))).Over Spec(L) :=
  ⟨pullback.snd _ _⟩

-- only if really needed
example (X : Over Spec(k)) : Over Spec(L) :=
  (Over.pullback (Spec.map (CommRingCat.ofHom <| algebraMap k L))).obj X

I admit this does not look great, but the main problem here is the Spec.map (CommRingCat.ofHom <| algebraMap k L))). There are two ways to fix this:

• rename CommRingCat.ofHom to CommRingCat.Hom.of, this would turn this into Spec.map (.of <| algebraMap k L).
• add a notation Spec.map(f) elaborating to Spec.map (CommRingCat.ofHom f).

[Christian Merten]

If you give me a more concrete setting, I can also give a more explicit recommendation.

[Kim Morrison]

Christian Merten said:

• rename CommRingCat.ofHom to CommRingCat.Hom.of

:+1:

[Bryan Wang]

Thank you very much! I was thinking along the lines of e.g. for elliptic curves there is docs#WeierstrassCurve.baseChange, so perhaps we could have something similar for k-schemes

[Antoine Chambert-Loir]

@Christian Merten , would you insert these lines in the docstring of the relevant mathlib file? (probably the one definining schemes)

[Christian Merten]

I can do that, but I am wondering about the right place. Should we use the theory documentation section of the website for that? I.e. add a section "AlgebraicGeometry" here: https://leanprover-community.github.io/theories?

[Antoine Chambert-Loir]

That would be great but doesn't forbid the other way. For example, is there a way to link files in the mathlib library to a companion page for the relevant theory?

[Christian Merten]

We can just put a link to the website in the module docstring.