NeronModelInfra.existsUnique_schemeHomOver_of_isProper_valuationSubring
The valuative criterion for a proper morphism, expressed as a unique morphism over the base.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace NeronModelInfraLean source · statement
theorem existsUnique_schemeHomOver_of_isProper_valuationSubring
{L : Type u} [Field L] (O : ValuationSubring L)
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f]
(s : Spec (CommRingCat.of ↥O) ⟶ Y) (x : Spec (CommRingCat.of L) ⟶ X)
(hx : x ≫ f = Spec.map (CommRingCat.ofHom O.subtype) ≫ s) :
∃! xt : SchemeHomOver s f, Spec.map (CommRingCat.ofHom O.subtype) ≫ xt.1 = x