of_isAffineHom — Mathlib

English

Lifted pullback along identity yields a closed immersion in the separated context.

Русский

Подъем по идентичности в линеаризованном контексте даёт замкнутое погружение.

LaTeX

$$$[IsSeparated g] \Rightarrow IsClosedImmersion( pullback.lift (\mathbf{1}) f (\mathrm{id}_{f} \circ g) ).$$$

Lean4

@[instance 100]
theorem of_isAffineHom [h : IsAffineHom f] : IsSeparated f :=
  by
  wlog hY : IsAffine Y
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsSeparated) _ (iSup_affineOpens_eq_top Y)]
    intro U
    have H : IsAffineHom (f ∣_ U) := IsZariskiLocalAtTarget.restrict h U
    exact this _ U.2
  have : IsAffine X := HasAffineProperty.iff_of_isAffine.mp h
  rw [MorphismProperty.arrow_mk_iso_iff @IsSeparated (arrowIsoSpecΓOfIsAffine f)]
  infer_instance

Похожие утверждения