English
Let f: X → S be a morphism of schemes. If the pullback of the diagonal Δ_f: X → X ×_S X is an open immersion, then f is formally unramified. In particular, monomorphisms (e.g., immersions) are formally unramified. Conversely, the converse holds if f is locally of finite type.
Русский
Пусть f: X → S — морфизм схем. Если диагональ Δ_f: X → X ×_S X является открытым вложением, то f формально неразрывный. В частности, монооморфизмы (например, вложения) формально неразрывны. Обратное верно, если f локально конечного типа.
LaTeX
$$$\\big[\\text{IsOpenImmersion}(\\text{pullback.diagonal } f)\\big] \\Rightarrow \\text{FormallyUnramified}(f)$$$
Lean4
/-- `f : X ⟶ S` is formally unramified if `X ⟶ X ×ₛ X` is an open immersion.
In particular, monomorphisms (e.g. immersions) are formally unramified.
The converse is true if `f` is locally of finite type. -/
instance (priority := 900) [IsOpenImmersion (pullback.diagonal f)] : FormallyUnramified f :=
by
wlog hY : ∃ R, Y = Spec R
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @FormallyUnramified) Y.affineCover]
intro i
have inst : IsOpenImmersion (pullback.diagonal (pullback.snd f (Y.affineCover.f i))) :=
MorphismProperty.pullback_snd (P := .diagonal @IsOpenImmersion) _ _ ‹_›
exact this (pullback.snd _ _) ⟨_, rfl⟩
obtain ⟨R, rfl⟩ := hY
wlog hX : ∃ S, X = Spec S generalizing X
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := @FormallyUnramified) X.affineCover]
intro i
have inst : IsOpenImmersion (pullback.diagonal (X.affineCover.f i ≫ f)) :=
MorphismProperty.comp_mem (.diagonal @IsOpenImmersion) _ _ (inferInstanceAs (IsOpenImmersion _)) ‹_›
exact this (_ ≫ _) ⟨_, rfl⟩
obtain ⟨S, rfl⟩ := hX
obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f
rw [HasRingHomProperty.Spec_iff (P := @FormallyUnramified)]
algebraize [φ.hom]
let F := (Algebra.TensorProduct.lmul' R (S := S)).toRingHom
have hF : Function.Surjective F := fun x ↦ ⟨.mk _ _ _ x 1, by simp [F]⟩
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom F)) := by
rwa [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _ (pullbackSpecIso R S S).inv, ←
AlgebraicGeometry.diagonal_Spec_map R S]
obtain ⟨e, he, he'⟩ := (isOpenImmersion_SpecMap_iff_of_surjective _ hF).mp this
refine ⟨subsingleton_of_forall_eq 0 fun x ↦ ?_⟩
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
obtain ⟨x, rfl⟩ := Ideal.mem_span_singleton.mp (he'.le hx)
refine (Ideal.toCotangent_eq_zero _ _).mpr ?_
rw [pow_two, Subtype.coe_mk, ← he, mul_assoc]
exact Ideal.mul_mem_mul (he'.ge (Ideal.mem_span_singleton_self e)) hx
