Valuative criterion

Main results

• AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion: A morphism is universally closed if and only if it is quasi-compact and satisfies the existence part of the valuative criterion.
• AlgebraicGeometry.IsSeparated.eq_valuativeCriterion: A morphism is separated if and only if it is quasi-separated and satisfies the uniqueness part of the valuative criterion.
• AlgebraicGeometry.IsProper.eq_valuativeCriterion: A morphism is proper if and only if it is qcqs and of fintite type and satisfies the valuative criterion.

Future projects

Show that it suffices to check discrete valuation rings when the base is noetherian.

structure AlgebraicGeometry.ValuativeCommSq {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Type (u + 1)

A valuative commutative square over a morphism f : X ⟶ Y is a square

Spec K ⟶ Y
  |       |
  ↓       ↓
Spec R ⟶ X

where R is a valuation ring, and K is its ring of fractions.

We are interested in finding lifts Spec R ⟶ Y of this diagram.

• R : Type u

  The valuation ring of a valuative commutative square.

• commRing : CommRing self.R
• domain : IsDomain self.R
• valuationRing : ValuationRing self.R
• K : Type u

  The field of fractions of a valuative commutative square.

• field : Field self.K
• algebra : Algebra self.R self.K
• isFractionRing : IsFractionRing self.R self.K
• i₁ : AlgebraicGeometry.Spec (CommRingCat.of self.K) ⟶ X

  The top map in a valuative commutative map.

• i₂ : AlgebraicGeometry.Spec (CommRingCat.of self.R) ⟶ Y

  The bottom map in a valuative commutative map.

• commSq : CategoryTheory.CommSq self.i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap self.R self.K))) f self.i₂

def AlgebraicGeometry.ValuativeCriterion.Existence : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

A morphism f : X ⟶ Y satisfies the existence part of the valuative criterion if every valuative commutative square over f has (at least) a lift.

Equations

• AlgebraicGeometry.ValuativeCriterion.Existence f = ∀ (S : AlgebraicGeometry.ValuativeCommSq f), ⋯.HasLift

def AlgebraicGeometry.ValuativeCriterion.Uniqueness : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

A morphism f : X ⟶ Y satisfies the uniqueness part of the valuative criterion if every valuative commutative square over f has at most one lift.

Equations

• AlgebraicGeometry.ValuativeCriterion.Uniqueness f = ∀ (S : AlgebraicGeometry.ValuativeCommSq f), Subsingleton ⋯.LiftStruct

def AlgebraicGeometry.ValuativeCriterion : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

A morphism f : X ⟶ Y satisfies the valuative criterion if every valuative commutative square over f has a unique lift.

Equations

• AlgebraicGeometry.ValuativeCriterion f = ∀ (S : AlgebraicGeometry.ValuativeCommSq f), Nonempty (Unique ⋯.LiftStruct)

theorem AlgebraicGeometry.ValuativeCriterion.iff {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} : AlgebraicGeometry.ValuativeCriterion f ↔ AlgebraicGeometry.ValuativeCriterion.Existence f ∧ AlgebraicGeometry.ValuativeCriterion.Uniqueness f

theorem AlgebraicGeometry.ValuativeCriterion.eq : AlgebraicGeometry.ValuativeCriterion = AlgebraicGeometry.ValuativeCriterion.Existence ⊓ AlgebraicGeometry.ValuativeCriterion.Uniqueness

theorem AlgebraicGeometry.ValuativeCriterion.existence {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (h : AlgebraicGeometry.ValuativeCriterion f) : AlgebraicGeometry.ValuativeCriterion.Existence f

theorem AlgebraicGeometry.ValuativeCriterion.uniqueness {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (h : AlgebraicGeometry.ValuativeCriterion f) : AlgebraicGeometry.ValuativeCriterion.Uniqueness f

theorem AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (H : AlgebraicGeometry.ValuativeCriterion.Existence f) : SpecializingMap ⇑f.base

Stacks Tag 01KE

instance AlgebraicGeometry.ValuativeCriterion.Existence.instIsLocalHomCarrierRingHomHomHomCommRingCat {R S : CommRingCat} (e : R ≅ S) : IsLocalHom e.hom.hom

theorem AlgebraicGeometry.ValuativeCriterion.Existence.of_specializingMap {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (H : (AlgebraicGeometry.topologically @SpecializingMap).universally f) : AlgebraicGeometry.ValuativeCriterion.Existence f

instance AlgebraicGeometry.ValuativeCriterion.Existence.stableUnderBaseChange : AlgebraicGeometry.ValuativeCriterion.Existence.IsStableUnderBaseChange

theorem AlgebraicGeometry.ValuativeCriterion.Existence.eq : AlgebraicGeometry.ValuativeCriterion.Existence = (AlgebraicGeometry.topologically @SpecializingMap).universally

Stacks Tag 01KE

theorem AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion : @AlgebraicGeometry.UniversallyClosed = AlgebraicGeometry.ValuativeCriterion.Existence ⊓ @AlgebraicGeometry.QuasiCompact

The valuative criterion for universally closed morphisms.

Stacks Tag 01KF

theorem AlgebraicGeometry.UniversallyClosed.of_valuativeCriterion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] (hf : AlgebraicGeometry.ValuativeCriterion.Existence f) : AlgebraicGeometry.UniversallyClosed f

The valuative criterion for universally closed morphisms.

Stacks Tag 01KF

theorem AlgebraicGeometry.IsSeparated.of_valuativeCriterion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiSeparated f] (hf : AlgebraicGeometry.ValuativeCriterion.Uniqueness f) : AlgebraicGeometry.IsSeparated f

The valuative criterion for separated morphisms.

Stacks Tag 01L0

theorem AlgebraicGeometry.IsSeparated.valuativeCriterion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsSeparated f] : AlgebraicGeometry.ValuativeCriterion.Uniqueness f

Stacks Tag 01KZ

theorem AlgebraicGeometry.IsSeparated.eq_valuativeCriterion : @AlgebraicGeometry.IsSeparated = AlgebraicGeometry.ValuativeCriterion.Uniqueness ⊓ @AlgebraicGeometry.QuasiSeparated

The valuative criterion for separated morphisms.

theorem AlgebraicGeometry.IsProper.eq_valuativeCriterion : @AlgebraicGeometry.IsProper = AlgebraicGeometry.ValuativeCriterion ⊓ @AlgebraicGeometry.QuasiCompact ⊓ @AlgebraicGeometry.QuasiSeparated ⊓ @AlgebraicGeometry.LocallyOfFiniteType

The valuative criterion for proper morphisms.

Stacks Tag 0BX5

theorem AlgebraicGeometry.IsProper.of_valuativeCriterion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f] [AlgebraicGeometry.LocallyOfFiniteType f] (H : AlgebraicGeometry.ValuativeCriterion f) : AlgebraicGeometry.IsProper f

The valuative criterion for proper morphisms.

Stacks Tag 0BX5