quasiSeparatedOfMono

Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.quasiSeparatedOfMono

English

Every mono morphism of schemes is quasi-separated.

Русский

Любой моно-морфизм схем квазисепаратен.

LaTeX

$$$\\forall f:\\;\\text{Mono}(f)\\;\\Rightarrow\\; \\text{QuasiSeparated}(f)$$$

Lean4

instance (priority := 900) quasiSeparatedOfMono {X Y : Scheme} (f : X ⟶ Y) [Mono f] : QuasiSeparated f where

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru