Valuative criterion

Stream: mathlib4

[Andrew Yang]

I'd like to coordinate efforts to bring the valuative criterions into mathlib. My plan is to carry out this project in an experimental process in a branch of mathlib where I define all the defs and all the lemmas used would be sorried out but have its statement written out along with a list of lemmas used or a reference of the proof. People would then claim these sorries and have the responsibility of PRing it into mathlib.

Aside from the main goal of having the valuative criterions in mathlib, I'd like to see if this format is efficient, if it sparks interest, and if it lowers the skill threshold to contribute to mathlib.

I'll try to put out the branch soon if people are interested.

[Andrew Yang]

Following stacks, the roadmap I'm aiming for is

1. Show that a (quasi-compact) morphism is a closed map iff it is specialization lifts
   => : true for any topological space
   <= : reduce to f : X ⟶ Spec R, with X affine. For any closed Z ⊆ X, the image f '' Z is
   the range of the map Spec Π Rᵢ / Iᵢ ⟶ Spec R, where { Spec Rᵢ } is an affine cover of X
   and Iᵢ is an ideal corresponding to the closed set Z ∩ Spec Rᵢ.
   Then use stacks#00HY (second proof is easy in lean)

2. Deduce that for qc morphisms, universally closed <=> universally specializing

3. universally specializing <=> existence part of the valuative criterion (for general valuation rings)
   This is stacks#01KE. The prerequisites are

   • On the AG side: Description of morphisms of the form Spec K ⟶ X for fields K.
   • On the algebra side: The fact that valuation subring <=> maximal (wrt dominance) local subrings

4. If f is quasi separated
   separated <=> diagonal universally closed <=>
   diagonal satisfies existence part of valuative criterion <=>
   uniqueness part of the valuative criterion

5. If f is qcqs + finite type, then proper <=> valuative criteron

[Andrew Yang]

@Qi Ge have you had any progress in this direction?

[Qi Ge]

Unfortunately I did not start on this. Format sounds great and I’d happy to contribute though!

[Andrew Yang]

The branch is up at branch#valuativeCriterion or #14782.
To not ruin the cache, everything new should live in Mathlib/ValuativeCriterion.
There are 91 sorries in total, and in theory every sorry is independent of each other and should not require any prerequisites except those sorried out in the branch. Feel free to claim any of them by adding your name as a comment before the lemma in the lean file, and push directly to the branch when finished.
I'll keep an eye out for when a portion of it could be PR-ed and notify the author.

[Johan Commelin]

I fixed one sorry (-;

[Johan Commelin]

Good old sorry counter:

$ rg -l sorry Mathlib/ValuativeCriterion | while read file; do n=$(rg sorry $file | wc -l); echo "$n\t$file"; done | sort -rn
18      Mathlib/ValuativeCriterion/ValuativeCriterion.lean
15      Mathlib/ValuativeCriterion/PullbackCarrier.lean
13      Mathlib/ValuativeCriterion/Stalk.lean
11      Mathlib/ValuativeCriterion/ValuationRIng.lean
10      Mathlib/ValuativeCriterion/Immersion.lean
9       Mathlib/ValuativeCriterion/UniversallyClosed.lean
8       Mathlib/ValuativeCriterion/ResidueField.lean
4       Mathlib/ValuativeCriterion/ClosedImmersion.lean
1       Mathlib/ValuativeCriterion/Lemmas.lean
1       Mathlib/ValuativeCriterion/Fiber.lean

[Andrew Yang]

That's nice!

[Qi Ge]

Suppose I have f : A ->+* \top for A, \top subrings of some R, how do I get a ring map with correct typeclass?

[Qi Ge]

Should be obvious but really got myself confused...

[Ruben Van de Velde]

#mwe ?

[Adam Topaz]

Isn’t f a ring map? (And yeah, a #mwe would help)

[Adam Topaz]

do you want a ring map from A to R maybe?

[Qi Ge]

Yes

[Adam Topaz]

oh, I think it should just be RingHom.comp (Subring.subtype _) f or something like that

[Adam Topaz]

(untested, obviously)

[Adam Topaz]

docs#Subring.subtype <-- in general this gives you the inclusion of a subring into the ambient ring

[Adam Topaz]

Although if you ended up with some random morphism f between two subrings of the same ring, then this could be a #xy situation

[Qi Ge]

Yes, subtype is exactly what I need thanks!

[Qi Ge]

This isn't a precise question but why sometimes Spec.map (RingCat.ofHom ringmap) complains that application type mismatch at ringmap and I need to use Spec.map (CommRingCat.ofHom ringmap) but sometimes it works?

[Qi Ge]

Answering my own question, because ringmap is not actually a map between rings, there is some coercion mess going on...

[Qi Ge]

Is it possible to construct this function:

def mve (K : RingCat) (A : Subring K) : .of A ⟶ K := sorry

[Andrew Yang]

RingCat.ofHom A.subtype? Though you would probably want to work with CommRingCat.

[Qi Ge]

Right... That works... So my problem is elsewhere...

[Qi Ge]

Got specializingMap :grinning_face_with_smiling_eyes:

[Qi Ge]

Just to be sure is this mathematically correct? And how should I name it?

lemma domination_preserved_by_range {R : Type*} {S : Type*} {K : Type*}
    [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [CommRing K]
      (f : R →+* S) [IsLocalRingHom f] (g : S →+* K):
        (LocalSubring.range (g.comp f)) ≤ (LocalSubring.range g) := by
  sorry

[Qi Ge]

@Andrew Yang :smile:

[Kevin Buzzard]

The easiest way to check it's mathematically correct is just to prove it :-)

[Qi Ge]

It is 100% true in the case that matters. I'm getting the API's ready in the process getting another proof. It is distracting to work on this now :melting_face:

[Qi Ge]

What is the best way to deal with associativity of arrows?

[Andrew Yang]

Not sure what you are referring to but reassoc_of% might be useful.

[Qi Ge]

I meant situations like f \gg g \gg h \gg z = f \gg (g \gg h) \gg z

[Andrew Yang]

Usually you can get away with simp only [Category.assoc], and then use the _assoc lemmas (or reassoc_of%). slice_lhs and slice_rhs might also be usefule here but I can only be sure if you have a #mwe

[Qi Ge]

variable {X : TopCat} (f₁ f₂ f₃ f₄ : X ⟶ X)
lemma hyp : f₂ ≫ f₃ = 𝟙 _ := sorry
lemma mve : f₁ ≫ f₂ ≫ f₃ ≫ f₄ = f₁ ≫ f₄ := sorry

Say I have hyp and want to prove mve.

[Andrew Yang]

rw [reassoc_of% hyp, Category.id_comp] at mve

[Qi Ge]

When I rw [reassoc_of% hyp] I get the goal of f₃ ≫ f₄ = f₁ ≫ f₄

[Andrew Yang]

I think you got f₁ ≫ f₄ = f₁ ≫ f₄ instead. Category.id_comp is unnecessary.

[Qi Ge]

image.png
:exploding_head:

[Yaël Dillies]

That's because the variables don't have to match between hyp and mve in your code snippet

[Yaël Dillies]

Try

variable {X : TopCat} (f₁ f₂ f₃ f₄ : X ⟶ X)
lemma mve (hyp : f₂ ≫ f₃ = 𝟙 _) : f₁ ≫ f₂ ≫ f₃ ≫ f₄ = f₁ ≫ f₄ := sorry

instead

[Qi Ge]

Thanks! Thought I went crazy :grinning:

[Qi Ge]

How to deal with type mismatch:

variable (T : Type) (a b : T) (h : a = b) (α : T → Type) (x : α a)
lemma this : α a = α b := congrArg α h
#check (x : α b)

Do we have to define the arrow manually

def univalent_nightmare : α a → α b := sorry

If this is the case then more generally wouldn't every construction on α a need to be made functorial w.r.t. a?

I have two points that are equal and talking about their stalks is giving me nightmare...

[Andrew Yang]

You should use docs#TopCat.Presheaf.stalkCongr

[Qi Ge]

Yes, very painful...

[Andrew Yang]

I agree with you though. This is not easy to deal with.

[Adam Topaz]

What's the issue here?

[Qi Ge]

Take a scheme $X$ and "two points" $x, x'$ on it that are equal. In Lean their stalks as dependent type are not the same, so constructions for one does not work for the other. So in theory, any results about $\mathcal{O}_x$ need to be shown to be compatible with some identification with $\mathcal{O}_{x'}$. It's like there's a groupoid for each type $A$ involving $\mathcal{O}_x$, and now if there's another type $B$ that was constructed using $A$ there is like a morphism of groupoids?...

[Adam Topaz]

Well, no, the stalks are "the same", but the issue is that you are trying to deal with equality of types as opposed to equality of terms. You can always "cast", but this can lead to terms which are hard to deal with in practice:

variable (T : Type) (a b : T) (h : a = b) (α : T → Type) (x : α a)
#check (h ▸ x : α b)

[Andrew Yang]

And often you will need to show that the construction commutes with docs#TopCat.Presheaf.stalkSpecializes anyways.

[Adam Topaz]

You can think of it like this (I'm not suggesting this is what should be formalized): Consider the category of open immersions into $X$, say $T$. This is a category so don't talk about equality of objects in there! There's a functor from $T^{op}$ to rings given by taking the sections over the open set. Since CommRing has all (filtererd) colimits, we can extend this functor to $(Pro T)^{op} = Ind (T^{op}) \to CommRing$ using the universal property of Pro. Now, there's a functor from the discrete category associated to the underlying set of $X$ to Pro T which sends x to the nbhd filter of x (actually, as Andrew suggests, this actually gives a functor from $X$ with the specialization order). The composition of those two functors is what gives you the stalk.

[Qi Ge]

Can it be characterized which $(ProT)^{op}→CommRing$ comes from a scheme? (I meant $(ProT)$ as some unknown category)

[Qi Ge]

Well we have all the closed points, so all the open, so all the affine open, and they need to glue... Do they always glue?

[Qi Ge]

Well affines don't even have to cover...

[Qi Ge]

Would be interesting if valuative criterion holds in some sense for those functors... I see your point now!

[Kevin Buzzard]

Another issue with equality of types is that if $x=y$ then you might not even want to prove $\mathcal{O}_x=\mathcal{O}_y$, because equality of types doesn't imply that the addition and multiplication on these two equal types coincide! The typeclass inference system (which decides which multiplication you want) works up to syntactic equality, and the types are not syntactically equal. You want to deduce that they're isomorphic as rings, which is a completely different (and much more helpful) claim than the claim that they're equal as types.

[Adam Topaz]

But $\mathcal{O}_x$ should be a term of CommRingCat, so I think that point is ok.

[Qi Ge]

Sorry seems like I was not clear yesterday. The issue is that there is a "distinguish" point $\mathfrak{m}$ defined in docs#LocalRing.closedPoint that is convenient to use. However, once there is another point x that is equal to it, none of the existing types sees $\mathcal{O}_x$ as the same type as $\mathcal{O}_{\mathfrak{m}}$! My solution to this is defining a type class IsClosedPoint to record the equally $x = \mathfrak{m}$ and generalize needed results so that they takes in x as input. This is unpleasant in the sense that in theory, every construction/statement about $\mathcal{O}_{\mathfrak{m}}$ need be write down again with certain isomorphism in mind, but this solution is very functional for me right now.

[Andrew Yang]

Can you share where you are at now? I have a feeling that it might be easier to use stalkCongr instead.

[Qi Ge]

Setup is like this:

class IsClosedPoint {R : Type*} [CommSemiring R] [LocalRing R] (x : PrimeSpectrum R) where
  is_cls_pt : x = LocalRing.closedPoint R

lemma specialize_to_cls_pt {R : Type*} [CommSemiring R] [LocalRing R] (x : PrimeSpectrum R) [hx : IsClosedPoint x] :
  x ⤳ LocalRing.closedPoint R := Inseparable.specializes <| congrArg nhds hx.is_cls_pt

lemma cls_pt_specialize_to {R : Type*} [CommSemiring R] [LocalRing R] (x : PrimeSpectrum R) [hx : IsClosedPoint x] :
  LocalRing.closedPoint R ⤳ x := Inseparable.specializes <| congrArg nhds hx.is_cls_pt.symm

noncomputable def stalk_cls_pt_to {R : Type*} [CommRing R] [LocalRing R]
    (x : PrimeSpectrum R) [IsClosedPoint x] :
      (Spec <| CommRingCat.of R).stalk (LocalRing.closedPoint R) ⟶ (Spec <| CommRingCat.of R).stalk x :=
  TopCat.Presheaf.stalkSpecializes _ <| specialize_to_cls_pt x

noncomputable def to_stalk_cls_pt {R : Type*} [CommRing R] [LocalRing R]
    (x : PrimeSpectrum R) [IsClosedPoint x] :
      (Spec <| CommRingCat.of R).stalk x ⟶ (Spec <| CommRingCat.of R).stalk (LocalRing.closedPoint R) :=
  TopCat.Presheaf.stalkSpecializes _ <| cls_pt_specialize_to x

lemma stalk_cls_pt_to_fromSpecStalk {R : Type*} [CommRing R] [LocalRing R]
    (x : PrimeSpectrum R) [IsClosedPoint x] :
      Spec.map (stalk_cls_pt_to x) ≫ (Spec <| .of R).fromSpecStalk (LocalRing.closedPoint R) =
        (Spec <| .of R).fromSpecStalk x := sorry

lemma to_stalk_cls_pt_fromSpecStalk {R : Type*} [CommRing R] [LocalRing R]
    (x : PrimeSpectrum R) [IsClosedPoint x] :
      Spec.map (to_stalk_cls_pt x) ≫ (Spec <| .of R).fromSpecStalk x =
        (Spec <| .of R).fromSpecStalk (LocalRing.closedPoint R) := sorry

lemma same_image_cls_pt {R : Type*} [CommRing R] [LocalRing R]
    (x : PrimeSpectrum R) [hx : IsClosedPoint x]
      {X : Scheme} (f : Spec (.of R) ⟶ X) :
        f.1.base x = f.1.base (LocalRing.closedPoint R) :=
  congrArg (⇑f.val.base) hx.is_cls_pt

noncomputable def stalk_image_cls_pt_to {R : Type*} [CommRing R] [LocalRing R]
    {X : Scheme} (f : Spec (.of R) ⟶ X)
      (x : PrimeSpectrum R) [IsClosedPoint x]:
        X.presheaf.stalk (f.1.base (LocalRing.closedPoint R))
          ⟶ X.presheaf.stalk (f.1.base x) := sorry

noncomputable def to_stalk_image_cls_pt {R : Type*} [CommRing R] [LocalRing R]
    {X : Scheme} (f : Spec (.of R) ⟶ X)
      (x : PrimeSpectrum R) [IsClosedPoint x]:
        X.presheaf.stalk (f.1.base x)
          ⟶ X.presheaf.stalk (f.1.base (LocalRing.closedPoint R)) := sorry

For a construction like this

noncomputable
def Scheme.stalkClosedPointTo {R : CommRingCat} [LocalRing R] (f : Spec R ⟶ X) :
    X.presheaf.stalk (f.1.base (closedPoint R)) ⟶ R :=
  PresheafedSpace.stalkMap f.1 (closedPoint R) ≫ (stalkClosedPointIso R).hom

I will have

noncomputable
def Scheme.stalkClosedPointTo' {R : CommRingCat} [LocalRing R] (f : Spec R ⟶ X)
    (x : PrimeSpectrum R) [IsClosedPoint x] :
      X.presheaf.stalk (f.1.base x) ⟶ R :=
  to_stalk_image_cls_pt f x ≫ stalkClosedPointTo f

and you can imagine similar goes for lemmas etc.

[Qi Ge]

I'm very close to finishing of_specializingMap but there's some final annoying issue...

[Qi Ge]

of_specializingMap is finally done... But the diagram chasing is not done very elegantly... Also now there is quite some new sorrys in Stalk.lean and ValuativeCriterion.lean

[Qi Ge]

Complaint: for docs#CategoryTheory.MorphismProperty.StableUnderBaseChange the order of variable disagrees with those used in docs#CategoryTheory.CommSq and docs#CategoryTheory.IsPullback:

def StableUnderBaseChange (P : MorphismProperty C) : Prop :=
  ∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄ (_ : IsPullback f' g' g f)
    (_ : P g), P g'

[Qi Ge]

I need a recent commit (#14985) for our branch but I'm not sure what to do. Github seems to ask me to start a PR to merge the changes from master, that can't be the right way to do this?

[Ruben Van de Velde]

Where is your code?

[Qi Ge]

branch#valuativeCriterion

[Ruben Van de Velde]

While you're on that branch, run

git fetch origin
git merge origin/master
# address conflicts
git add [files with conflicts]
git merge --continue
git push origin valuativeCriterion

[Qi Ge]

Thank you!

[Qi Ge]

I want to show that two morphisms between affine schemes are equal when their pullbacks on global sections are the same. What is the right way to do this? (Is it in mathlib somewhere?) If I do the following and unfold Scheme.Γ it looks quite messy...

lemma mwe (R S : CommRingCat) (f g : Spec S ⟶ Spec R)
    (h : Scheme.Γ.map f.op = Scheme.Γ.map g.op) :
      f = g := sorry

[Adam Topaz]

We must know that taking global sections on affine schemes is faithful.

[Adam Topaz]

But you probably need to convert your schemes to terms of AffineScheme

[Adam Topaz]

docs#AlgebraicGeometry.AffineScheme

[Adam Topaz]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/AffineScheme.html#AlgebraicGeometry.AffineScheme.Spec_faithful

[Andrew Yang]

lemma hom_ext_of_isAffine [IsAffine Y] (f g : X ⟶ Y) (e : f.app ⊤ = g.app ⊤) : f = g := by
  rw [← cancel_mono Y.isoSpec.hom]
  simp only [Scheme.isoSpec, asIso_hom, ΓSpec.adjunction_unit_naturality, e]

[Andrew Yang]

By the way there are some results in #15240 and #15333 that I definitely should port over.

[Qi Ge]

I just got stalkClosedPointIso_fromSpecStalk, and with it some neat little results.

[Qi Ge]

In particular is identifying the counit map (Spec R).isoSpec.inv with Spec.map (StructureSheaf.toOpen R ⊤). It was a category theory argument on the adjuction.

[Qi Ge]

Note to myself: this is name_me.

[Qi Ge]

The PRs look Great! Is there anther file you are working on just so I don't crash into what you are working on?

[Qi Ge]

There's 2 things I'd happy to work on now:

1. Adapting the existence part of the code to use the new Stalk.lean
2. The explicit description of fibre product (in PullbackCarrier.lean), since I would need that to define jointly surjective topology.

I can work on 2 while waiting your code finalizes into the library. Do you think that would work? @Andrew Yang

[Andrew Yang]

I'm working on immersions and they came in the way so I finished them. Sorry, should've stated it here beforehand. But besides these two files and Immersion.lean (or maybe ClosedImmersion.lean), I don't have any immediate plans on working in this project.

[Andrew Yang]

I think 2 would be great. 1 would be helpful as well, but if you don't mind, I'd like to try it myself to see how to implement the IsClosedPoint class best.

[Qi Ge]

:tada: No problem at all!
I'm unsure on that so I'm looking forwards your opinion as well. If it turns out defining a new type class is superfluous I'm happy to change it, feel free to let me know.
Next I will work on 2 then.

[Qi Ge]

Why no automation works for this?

lemma mve (X Y : Type) (f g : X ⟶ Y) (h : f.op = g.op) : f = g := by
  exact congrArg Quiver.Hom.unop h

[Adam Topaz]

What do you want the automation to do?

[Qi Ge]

I meant simp or aesop don't solve the goal. And apply? would not suggest the proof as well.

[Adam Topaz]

docs#Quiver.Hom.op_injective

[Qi Ge]

:upside_down: 404 Not Found

[Adam Topaz]

Yeah…

[Qi Ge]

I have some notes experimenting with ΓSpec.adjunction. Currently the unit X.isoSpec.hom and counit (Scheme.ΓSpecIso R).inv are given quite confusing names. If there's a future refactor I would really like to see them renamed more consistently.

import Mathlib

open AlgebraicGeometry
open CategoryTheory

variables (R : CommRingCat) (X : Scheme)

-- When restricted to affine schemes, `Γ` is fully faithful, so unit `X ⟶ Spec Γ(X, ⊤)` is an isomorphism
variable [IsAffine X]
example : ΓSpec.adjunction.unit.app X = X.isoSpec.hom := rfl

-- `Spec` is fully faithful, so counit `R ⟶ Γ(Spec R, ⊤)` is an isomorphism
example : ΓSpec.adjunction.counit.app (Opposite.op R) = (Scheme.ΓSpecIso R).op.inv := rfl

-- triangle gives us the inverses of the unit/counit for images of the functors
lemma this : Scheme.Γ.map (X.isoSpec.hom).op
    = (Scheme.ΓSpecIso (Γ(X, ⊤))).hom := by
  apply congrArg Quiver.Hom.unop
  apply (Iso.comp_inv_eq_id (Scheme.ΓSpecIso (Scheme.Γ.obj (Opposite.op (X)))).op).mp
  exact ΓSpec.adjunction.left_triangle_components X

-- Just arrived in https://github.com/leanprover-community/mathlib4/blob/a2bc015603a75b40b4059d28b15f1b10fa524943/Mathlib/AlgebraicGeometry/AffineScheme.lean#L122
lemma that : Scheme.Spec.map (Scheme.ΓSpecIso R).op.inv
    = (Spec R).isoSpec.inv := by
  apply Iso.inv_ext'
  exact ΓSpec.adjunction.right_triangle_components (Opposite.op R)

[Andrew Yang]

docs#Quiver.Hom.op_inj

[Andrew Yang]

What do you suggest as better names? this is docs#AlgebraicGeometry.ΓSpec.adjunction_unit_app_app_top

[Andrew Yang]

I also have a PR #15082 wrapping the unit into a def.

[Qi Ge]

I think their names should be dual to each other, and their docstring should emphasize they are unit/counit.

[Qi Ge]

Andrew Yang said:

docs#Quiver.Hom.op_inj

Any reason this would not show up in apply?

[Andrew Yang]

Andrew Yang said:

I also have a PR #15082 wrapping the unit into a def.

Maybe Scheme.isoSpec -> Scheme.isoSpecΓ would help as well?

[Andrew Yang]

Qi Ge said:

Andrew Yang said:

docs#Quiver.Hom.op_inj

Any reason this would not show up in apply?

IIRC apply? does not work for goals about equalities

[Qi Ge]

Having both ΓSpecIso and isoSpecΓ sound both great and really bad :smiley: Maybe this is the best solution here

[Qi Ge]

I'm looking at docs#AlgebraicGeometry.IsPreimmersion and it claims that "preimmersions" (topological embedding + surjective on stalk) are stable under pullback. Is there a reference for this?

[Andrew Yang]

The key is docs#PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks. I'm waiting for the description of the underlying set of $X \times_S Y$ to promote this into a scheme-theoretic statement: If $f : X \to S$ is surjective on stalks (i.e. $\mathcal{O}_{S, f(x)} \to \mathcal{O}_{X, x}$ is surjective for all $x$) then the underlying space of $X \times_S Y$ is the set $\{ (x, y) \in X \times Y | f(x) = g(y) \}$ equipped with the product topology.

The claim then follows easily.

[Andrew Yang]

There isn't really a reference, but this statement can be seen in Corollary 11 of https://arxiv.org/pdf/1103.2139 (as a corollary of a big theorem and hence has a much more complex proof).

[Qi Ge]

Makes sense :+1: . But why is description of $X×_S​Y$ needed to globalize? Isn't $X×_S​Y$ already covered by such affines?

[Qi Ge]

Also I'm a bit confused where is this Preimmersion class going to be used?

[Andrew Yang]

You need to show that if $U_j \times_{S_i} V_k$ is an open cover of $X \times_S Y$, then $U_j \times V_k$ covers $\{ (x, y) \in X \times Y | f(x) = g(y) \}$.

[Andrew Yang]

An application is to show that the topology on the fiber $Y \times_X \kappa(x)$ is exactly the topology on $f^{-1}(\{x\})$. We can also show that closed immersions are stable under pullback via this route (as we are still missing the closed immersions = locally looks like $\operatorname{Spec}(A/I) \to \operatorname{Spec} A$ characterisation).

[Qi Ge]

Andrew Yang said:

You need to show that if $U_j \times_{S_i} V_k$ is an open cover of $X \times_S Y$, then $U_j \times V_k$ covers $\{ (x, y) \in X \times Y | f(x) = g(y) \}$.

But shouldn't the maps
$\{ (x,y) \in U_j \times V_k ∣ f(x)=g(y)\}\longrightarrow U_j \times_{S_i} V_k$
glue to a map
$\{ (x,y) \in X \times Y ∣ f(x)=g(y)\} \longrightarrow X\times_S​Y$?
Both LHS and RHS are covers that we know and need not depend on the description of the fibre product?

[Qi Ge]

I was trying to show that using (locally closed) immersions are stable under base change, the scheme theoretic fibers are set fibers, and consequently we get a description of the fibre products. Seems like this is the opposite direction of where things are set up?... If a description of the fibre product is the prerequisite it would need be an affine local argument that need to be glued this way anyhow I think? :octopus:

[Andrew Yang]

We do not have the map $\{ (x,y) \in U_j \times V_k ∣ f(x)=g(y)\}\longrightarrow U_j \times_{S_i} V_k$. We only know that the map $U_j \times_{S_i} V_k \to \{ (x,y) | x \in U_j, y \in V_k \}$ is a topological embedding. To get the described map requires the knowledge of the image.
Maybe you can get the description of the fibered products of affine schemes easier but that is extra work and we will need the description for general schemes anyways.
Plus, gluing morphisms is not that easy. I don't think it is completely trivial that the maps are compatible without some knowledge on how the underlying set of fibred product behaves.

[Andrew Yang]

Qi Ge said:

I was trying to show that using (locally closed) immersions are stable under base change, the scheme theoretic fibers are set fibers, and consequently we get a description of the fibre products. Seems like this is the opposite direction of where things are set up?... If a description of the fibre product is the prerequisite it would need be an affine local argument that need to be glued this way anyhow I think? :octopus:

Are you following https://github.com/leanprover-community/mathlib4/blob/valuativeCriterion/Mathlib/ValuativeCriterion/PullbackCarrier.lean? I think I have carefully thought it through to avoid circular arguments.

[Qi Ge]

I see the flow of argument now. Thanks for the context! :+1:

[Qi Ge]

I think I need the closed embedding of the residue field fromSpecResidueField is mono. Do we have this?

[Qi Ge]

(Or just left cancellation is enough)

[Andrew Yang]

No I didn't include that sorry because I thought we didn't need it. It is implied by the fact that fromSpecResidueField is a preimmersion, which in turn follows from $\operatorname{Spec} A_S \to \operatorname{Spec} A$ being a preimmersion (and other facts that are already in mathlib).

[Qi Ge]

So I can just use it, there is no circularity complication right?

[Andrew Yang]

Yes.

[Qi Ge]

:tada: Great

[Qi Ge]

Got a big chunk of PullbackCarrier.lean.
Two sorries so far:
1. I think we don't yet have fromSpecResidueField IsPreimmersion?
2. Need a lemma saying that Spec of pushout IsPullback, I haven't looked at the category theory API closely.

[Qi Ge]

Some diagrams chased for record d1 d2 d3

[Qi Ge]

Also I come to realize the congr lemma approach makes great sense. @Andrew Yang if you haven't touch my earlier code yet I'd like to go back to fix them up!

[Andrew Yang]

No I won't have time for lean for another week or two.

[Christian Merten]

@Qi Ge are you still working on the PullbackCarrier file? I need it for a different context and am happy to help finalize and get it into mathlib.

[Qi Ge]

Hi @Christian Merten! I was distracted by thesis work for a while now and I didn't have progress on that file. It'd be amazing if you want to work on it!

[Qi Ge]

I have not given up on the project, I think I will have time continue on it later this month. Sorry for the quietness!

[Christian Merten]

Oh, no worries. I'll work on finishing and cleaning it up then.

[Andrew Yang]

Thanks to the work by Qi and Christian, there are only four files containing sorries in branch#ValuativeCriterion

1. Mathlib/ValuativeCriterion/ClosedImmersion.lean: Closed immmersions are locally $\operatorname{Spec} A \to \operatorname{Spec}(A/I)$. Christian is working towards this independently IIRC.
2. Mathlib/ValuativeCriterion/Immersion.lean: The diagonal map is an immersion; and affine morphisms are separated. No-one is working on this AFAIK.
3. Mathlib/ValuativeCriterion/Stalk.lean: Basic yoga on stalks. Covered by #15240.
4. Mathlib/ValuativeCriterion/ValuationRing.lean: Valuative subrings are exactly the maximal local subrings wrt dominance. Is Christian working on this?

I strongly encourage people (like @Javier Lopez-Contreras :)) to go for 2 or 4; just indicate what sorry you are working on so that people don't step on your toes.
Other than that, probably we should start PRing stuff.

[Christian Merten]

1. is in #15038

[Andrew Yang]

The final two PRs of valuative criterion are now ready for review.

1. #19012 shows that valuative subrings of a field are exactly the maximal local subrings
2. #14782 the valuative criterion

[Andrew Yang]

#14782 The final PR proving the valuative criterion for universally closedness or separatedness or properness is ready for review.

[Johan Commelin]

How did you manage to get the new-contributor label on that PR?

[Andrew Yang]

I got some new contributor to solve some sorries for me and that seems to count.

[Johan Commelin]

This is a very nice milestone result. I think it can also be mentioned in the library overview.

[Yaël Dillies]

Thanks Andrew for the very generous co-authorship policy :folded_hands:

[Yaël Dillies]

/me definitely understands what the valuative criterion for properness is