of_valuativeCriterion — Mathlib

English

If f is quasi-compact, quasi-separated, locally of finite type and ValuativeCriterion f holds, then f is proper.

Русский

Если f квазиквазитируем и квазоссепаратен, локально конечного типа и выполняется Валюативный критерий, то f является правильным.

LaTeX

$$$\mathrm{ValuativeCriterion}(f) \wedge \mathrm{QuasiCompact}(f) \wedge \mathrm{QuasiSeparated}(f) \wedge \mathrm{LocallyOfFiniteType}(f) \Rightarrow \mathrm{IsProper}(f)$$$

Lean4

/-- The **valuative criterion** for proper morphisms. -/
@[stacks 0BX5]
theorem of_valuativeCriterion [QuasiCompact f] [QuasiSeparated f] [LocallyOfFiniteType f] (H : ValuativeCriterion f) :
    IsProper f := by
  rw [eq_valuativeCriterion]
  exact ⟨⟨⟨‹_›, ‹_›⟩, ‹_›⟩, ‹_›⟩

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