English
The existence part of the valuative criterion is stable under base change: pulling back f along any base change preserves existence.
Русский
Существование по критерию Валюативности сохраняется при базовом изменении: взятие обратной картины f по любой огибающей базовой схеме сохраняет существование.
LaTeX
$$$\text{ValuativeCriterion.Existence}$ is stable under base change$$
Lean4
instance stableUnderBaseChange : ValuativeCriterion.Existence.IsStableUnderBaseChange :=
by
constructor
intro Y' X X' Y Y'_to_Y f X'_to_X f' hP hf commSq
let commSq' : ValuativeCommSq f :=
{ R := commSq.R
K := commSq.K
i₁ := commSq.i₁ ≫ X'_to_X
i₂ := commSq.i₂ ≫ Y'_to_Y
commSq := ⟨by simp only [Category.assoc, hP.w, reassoc_of% commSq.commSq.w]⟩ }
obtain ⟨l₀, hl₁, hl₂⟩ := (hf commSq').exists_lift
refine ⟨⟨⟨hP.lift l₀ commSq.i₂ (by simp_all only [commSq']), ?_, hP.lift_snd _ _ _⟩⟩⟩
apply hP.hom_ext
· simpa
· simp only [Category.assoc]
rw [hP.lift_snd]
rw [commSq.commSq.w]
