English
If f is formally unramified and locally of finite type, then the diagonal morphism pullback diagonal f: X → X ×_S X is an open immersion.
Русский
Если f формально неразрывна и локально типа конечного, диагональная карта X → X ×_S X является открытым вложением.
LaTeX
$$$[\\text{FormallyUnramified}(f) \\land \\text{LocallyOfFiniteType}(f)] \\Rightarrow \\text{IsOpenImmersion}(\\text{pullback.diagonal } f)$$$
Lean4
/-- The diagonal of a formally unramified morphism of finite type is an open immersion. -/
instance isOpenImmersion_diagonal [FormallyUnramified f] [LocallyOfFiniteType f] :
IsOpenImmersion (pullback.diagonal f) :=
by
wlog hX : (∃ S, X = Spec S) ∧ ∃ R, Y = Spec R
· let 𝒰Y := Y.affineCover
let 𝒰X (j : (Y.affineCover.pullback₁ f).I₀) : ((Y.affineCover.pullback₁ f).X j).OpenCover := Scheme.affineCover _
apply
IsZariskiLocalAtTarget.of_range_subset_iSup _
(Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange f 𝒰Y 𝒰X)
intro ⟨i, j⟩
rw [arrow_mk_iso_iff (P := @IsOpenImmersion) (Scheme.Pullback.diagonalRestrictIsoDiagonal f 𝒰Y 𝒰X i j)]
have hu : FormallyUnramified ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
have hfin : LocallyOfFiniteType ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)) :=
comp_mem _ _ _ inferInstance (pullback_snd _ _ inferInstance)
exact this _ ⟨⟨_, rfl⟩, ⟨_, rfl⟩⟩
obtain ⟨⟨S, rfl⟩, R, rfl⟩ := hX
obtain ⟨f, rfl⟩ := Spec.map_surjective f
rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified),
HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at *
algebraize [f.hom]
rw [show f = CommRingCat.ofHom (algebraMap R S) from rfl, diagonal_Spec_map R S,
cancel_right_of_respectsIso (P := @IsOpenImmersion)]
infer_instance
