Residue field of locally ringed space and evaluation

Stream: Is there code for X?

[Christian Merten]

I am surprised, I can't find the following:

import Mathlib

open CategoryTheory Opposite

namespace AlgebraicGeometry

namespace LocallyRingedSpace

noncomputable def residueField (X : LocallyRingedSpace) (x : X) : CommRingCat :=
  CommRingCat.of <| LocalRing.ResidueField (X.stalk x)

noncomputable def evaluation (X : LocallyRingedSpace) (x : X) :
    LocallyRingedSpace.Γ.obj (op X) ⟶ X.residueField x :=
  X.ΓToStalk x ≫ LocalRing.residue _

noncomputable def evaluationMap {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : X) :
    Y.residueField (f.val.base x) ⟶ X.residueField x :=
  LocalRing.ResidueField.map (LocallyRingedSpace.stalkMap f x)

Is it somewhere?

[Andrew Yang]

I'm fairly certain that we don't have it. What do you plan to use it for? (Just curious)

[Christian Merten]

I am proving that closed immersions with affine target have affine source and are induced by quotient maps for which this language is very convenient.
Also I think we should have a RingedSpace.zeroLocus of a set of global sections. Then for a locally ringed space, we get the characterisation that a point $x$ is in the zero locus of a set $S$ of global sections if and only if all elements of $S$ "vanish" (i.e. evaluate to zero) in $x$.

[Christian Merten]

I guess, the above evaluation should be called LocallyRingedSpace.Γevaluation which is a special case of evaluating sections over an U : Opens X?

[Andrew Yang]

Ooh sounds nice.
Do you have

example {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y]
    (hf : ClosedEmbedding f.1.base) : IsAffine X := sorry

yet?

[Andrew Yang]

Christian Merten said:

Also I think we should have a RingedSpace.zeroLocus of a set of global sections.

That sounds useful. We have docs#AlgebraicGeometry.RingedSpace.mem_basicOpen which might help?

[Christian Merten]

Andrew Yang said:

Ooh sounds nice.
Do you have

example {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y]
    (hf : ClosedEmbedding f.1.base) : IsAffine X := sorry

yet?

No, I reduced to showing that if $X \to Y$ is a homeomorphism with $Y$ affine and the induced map on global sections is injective, then the map on stalks is injective.
(If $X \to Y$ is now a closed immersion, the map on stalks is an iso and we are done).

[Christian Merten]

Andrew Yang said:

Ooh sounds nice.
Do you have

example {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y]
    (hf : ClosedEmbedding f.1.base) : IsAffine X := sorry

yet?

Does this really hold without the surjectivity on stalks assumption?

[Christian Merten]

Andrew Yang said:

Christian Merten said:

Also I think we should have a RingedSpace.zeroLocus of a set of global sections.

That sounds useful. We have docs#AlgebraicGeometry.RingedSpace.mem_basicOpen which might help?

Yes, I am using that. My definition is:

def AlgebraicGeometry.RingedSpace.zeroLocus {X : RingedSpace}
    (s : Set (X.presheaf.obj (op ⊤))) : Set X :=
  sInf { (X.basicOpen f : Set X)ᶜ | (f ∈ s) }

(I don't know if we should introduce a RingedSpace.basicClosed? I don't need it, but might be useful?)

[Andrew Yang]

You don't even need injectivity. Only inducing + $X$ quasi-compact.
(For X affine. To show that it comes from a quotient ring hom still needs injectivity and stalk conditions)

1. For any $x \in U \subseteq X$, $U$ is the preimage of some open $V \subseteq Y$ (by inducing),
   And $V$ is the union of basic opens in $Y$. That is, $U$ is the union of the form $X_{f_\ast s_i}$ for a family $\{s_i\} \subseteq \mathcal{O}_Y(Y)$.

2. Now, if $U$ is affine, then the $X_{f_\ast s_i}$ from earlier is also affine, because it is also a basic open of $U$. (docs#AlgebraicGeometry.IsAffine.basicOpen_isAffine)

3. Since $X$ can be covered by affine opens, it can be covered by (finite) affine opens of the form $X_{t_i}$.
4. In particular $X$ is qcqs and by the qcqs lemma (docs#AlgebraicGeometry.is_localization_basicOpen_of_qcqs) $X$ is (zariski-locally) isomorphic to $\operatorname{Spec}\mathcal{O}_X(X)$.

[Andrew Yang]

We use Inter instead of Inf for sets. That is

def AlgebraicGeometry.RingedSpace.zeroLocus {X : RingedSpace}
    (s : Set (X.presheaf.obj (op ⊤))) : Set X :=
  ⋃ f ∈ s, (X.basicOpen f)ᶜ

[Kevin Buzzard]

@FMLJohn were you working on this recently?

[Fangming Li (John)]

Kevin Buzzard said:

FMLJohn were you working on this recently?

Yeah I think so. Things discussed here have some connections with what I am doing recently.

[Fangming Li (John)]

Christian Merten said:

I am surprised, I can't find the following:

import Mathlib

open CategoryTheory Opposite

namespace AlgebraicGeometry

namespace LocallyRingedSpace

noncomputable def residueField (X : LocallyRingedSpace) (x : X) : CommRingCat :=
  CommRingCat.of <| LocalRing.ResidueField (X.stalk x)

noncomputable def evaluation (X : LocallyRingedSpace) (x : X) :
    LocallyRingedSpace.Γ.obj (op X) ⟶ X.residueField x :=
  X.ΓToStalk x ≫ LocalRing.residue _

noncomputable def evaluationMap {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : X) :
    Y.residueField (f.val.base x) ⟶ X.residueField x :=
  LocalRing.ResidueField.map (LocallyRingedSpace.stalkMap f x)

Is it somewhere?

I have constructed something which I think is broader than the evaluation you have mentioned. For a scheme X and a point x : X.toTopCat, I have formalised the canonical scheme morphism from the spectrum of the residue field of x to X. The contents are available in this pull request:
Feat(AlgebraicGeometry/Curve): defining a curve. by FMLJohn · Pull Request #13857 · leanprover-community/mathlib4 (github.com)