English
For IsSeparated morphisms, ValuativeCriterion.Uniqueness(f) holds.
Русский
Для Морфизмов с отделимостью выполняется ValuativeCriterion.Uniqueness.
LaTeX
$$$\mathrm{ValuativeCriterion.Uniqueness}(f)$$$
Lean4
@[stacks 01KZ]
theorem valuativeCriterion [IsSeparated f] : ValuativeCriterion.Uniqueness f :=
by
intro S
constructor
rintro ⟨l₁, hl₁, hl₁'⟩ ⟨l₂, hl₂, hl₂'⟩
ext : 1
dsimp at *
have h := hl₁'.trans hl₂'.symm
let Z := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
let g : Z ⟶ Spec (.of S.R) := pullback.snd _ _
have : IsClosedImmersion g := MorphismProperty.pullback_snd _ _ inferInstance
have hZ : IsAffine Z := by
rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
exact this.left
suffices IsIso g by
rw [← cancel_epi g]
conv_lhs => rw [← pullback.lift_fst l₁ l₂ h, ← pullback.condition_assoc]
conv_rhs => rw [← pullback.lift_snd l₁ l₂ h, ← pullback.condition_assoc]
simp
suffices h : Function.Bijective (g.appTop)
by
refine (HasAffineProperty.iff_of_isAffine (P := MorphismProperty.isomorphisms Scheme)).mpr ?_
exact ⟨hZ, (ConcreteCategory.isIso_iff_bijective _).mpr h⟩
constructor
· let l : Spec (.of S.K) ⟶ Z :=
pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))
(by
apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)
· simpa using hl₁.symm
· simpa using hl₂.symm)
have hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) := pullback.lift_snd _ _ _
have : Function.Injective ((l ≫ g).appTop) := by
rw [hg]
let e := arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom <| algebraMap S.R S.K)
let P : MorphismProperty CommRingCat := RingHom.toMorphismProperty <| fun f ↦ Function.Injective f
have : (RingHom.toMorphismProperty <| fun f ↦ Function.Injective f).RespectsIso :=
RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.injective_respectsIso
change P _
rw [← MorphismProperty.arrow_mk_iso_iff (P := P) e]
exact FaithfulSMul.algebraMap_injective S.R S.K
rw [Scheme.comp_appTop] at this
exact Function.Injective.of_comp this
· rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
exact this.right