instLocallyOfFiniteTypeOfIsClosedImmersion

English

Closed immersions are locally of finite type.

Русский

Замкнутые вложения локально конечного типа.

LaTeX

$$$LocallyOfFiniteType(f)$ for IsClosedImmersion f$$

Lean4

/-- Closed immersions are locally of finite type. -/
instance (priority := 900) {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsClosedImmersion f] : LocallyOfFiniteType f :=
  by
  wlog hY : IsAffine Y
  · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @LocallyOfFiniteType) _ (iSup_affineOpens_eq_top Y)]
    intro U
    have H : IsClosedImmersion (f ∣_ U) := IsZariskiLocalAtTarget.restrict h U
    exact this _ U.2
  obtain ⟨_, hf⟩ := h.isAffine_surjective_of_isAffine
  rw [HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)]
  exact RingHom.FiniteType.of_surjective (Scheme.Hom.app f ⊤).hom hf

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