quasiSeparatedSpace_iff_quasiCompact_prod_lift

English

A space X is quasi-separated if and only if the diagonal morphism X → X × X is quasi-compact (equivalently, the product map X → X × X is quasi-compact).

Русский

Пространство X квазиразделимо тогда и только тогда, когда диагональ X → X × X квазиуплотна.

LaTeX

$$$\\mathrm{QuasiSeparatedSpace}(X) \\iff \\mathrm{QuasiCompact}(\\mathrm{prod.lift}(\\mathrm{id}_X, \\mathrm{id}_X)).$$$

Lean4

theorem quasiSeparatedSpace_iff_quasiCompact_prod_lift : QuasiSeparatedSpace X ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X)) :=
  by
  rw [← MorphismProperty.cancel_right_of_respectsIso @QuasiCompact _ (prodIsoPullback X X).hom, ←
    HasAffineProperty.iff_of_isAffine (f := terminal.from X) (P := @QuasiSeparated), quasiSeparated_iff]
  congr!
  ext : 1 <;> simp

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