English
There exists an affine property realization for quasi-separatedness: a morphism is quasi-separated iff its diagonal is quasi-compact when viewed with affine target.
Русский
Существует реализация свойства квазисепарабельности через афинность: морфизм квазисепарактен тогда и только тогда, когда диагональ квази-компактна в афинном контексте.
LaTeX
$$AffineProperty(diagonal) for QuasiSeparated ⇔ qc-diagonal$$
Lean4
instance : HasAffineProperty @QuasiSeparated (fun X _ _ _ ↦ QuasiSeparatedSpace X) where
__ :=
HasAffineProperty.copy quasiSeparated_eq_diagonal_is_quasiCompact.symm
(by ext; exact quasiCompact_affineProperty_iff_quasiSeparatedSpace _)
