quasiSeparated_over_affine_iff — Mathlib

English

Let f: X → Y be a morphism of schemes with Y affine. Then f is quasi-separated if and only if the underlying topological space of X is quasi-separated.

Русский

Пусть f: X → Y — отображение схем с афинной целевой схемой Y. Тогда f квазиразделимо тогда и только тогда, когда пространство X в основании топологий квазиразделимо.

LaTeX

$$$\\mathrm{QuasiSeparated}(f) \\;\\iff\\; \\mathrm{QuasiSeparatedSpace}(X)$, \\qquad [\\text{IsAffine } Y],$$$

Lean4

theorem quasiSeparated_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
    QuasiSeparated f ↔ QuasiSeparatedSpace X := by rw [HasAffineProperty.iff_of_isAffine (P := @QuasiSeparated)]

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