Documentation

Mathlib.AlgebraicGeometry.ValuativeCriterion

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 : 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₁ : Spec (CommRingCat.of self.K) ⟶ X
The top map in a valuative commutative map.
i₂ : Spec (CommRingCat.of self.R) ⟶ Y
The bottom map in a valuative commutative map.
commSq : CategoryTheory.CommSq self.i₁ (Spec.map (CommRingCat.ofHom (algebraMap self.R self.K))) f self.i₂

def AlgebraicGeometry.ValuativeCriterion.Existence :

CategoryTheory.MorphismProperty 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 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 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 : Scheme} {f : X ⟶ Y} :

ValuativeCriterion f ↔ Existence f ∧ Uniqueness f

theorem AlgebraicGeometry.ValuativeCriterion.eq :

ValuativeCriterion = Existence ⊓ Uniqueness

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

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

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

SpecializingMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)

Stacks Tag 01KE

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

IsLocalHom (CommRingCat.Hom.hom e.hom)

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

instance AlgebraicGeometry.ValuativeCriterion.Existence.stableUnderBaseChange :

Existence.IsStableUnderBaseChange

theorem AlgebraicGeometry.ValuativeCriterion.Existence.eq :

Existence = (topologically @SpecializingMap).universally

Stacks Tag 01KE

theorem AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion :

@UniversallyClosed = ValuativeCriterion.Existence ⊓ @QuasiCompact

The valuative criterion for universally closed morphisms.

Stacks Tag 01KF

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

UniversallyClosed f

The valuative criterion for universally closed morphisms.

Stacks Tag 01KF

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

The valuative criterion for separated morphisms.

Stacks Tag 01L0

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

ValuativeCriterion.Uniqueness f

Stacks Tag 01KZ

theorem AlgebraicGeometry.IsSeparated.eq_valuativeCriterion :

@IsSeparated = ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated

The valuative criterion for separated morphisms.

theorem AlgebraicGeometry.IsProper.eq_valuativeCriterion :

@IsProper = ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType

The valuative criterion for proper morphisms.

Stacks Tag 0BX5

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

The valuative criterion for proper morphisms.

Stacks Tag 0BX5