quasiSeparatedSpace_of_quasiSeparated

English

If Y is quasi-separated and f: X → Y is quasi-separated, then X has a quasi-separated underlying topological space.

Русский

Если Y квазиразделим и f: X → Y квазиразделимо, то пространство X как топологическое пространство квазиразделимо.

LaTeX

$$$[\\mathrm{QuasiSeparatedSpace}(Y)] , \\mathrm{QuasiSeparated}(f) \\Rightarrow \\mathrm{QuasiSeparatedSpace}(X).$$$

Lean4

theorem quasiSeparatedSpace_of_quasiSeparated {X Y : Scheme} (f : X ⟶ Y) [hY : QuasiSeparatedSpace Y]
    [QuasiSeparated f] : QuasiSeparatedSpace X :=
  by
  rw [quasiSeparatedSpace_iff_quasiSeparated] at hY ⊢
  rw [← terminalIsTerminal.hom_ext (f ≫ terminal.from Y) (terminal.from X)]
  infer_instance

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