instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated

Mathlib.AlgebraicGeometry.Morphisms.Separated

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.instQuasiSeparatedSpaceCarrierCarrierCommRingCatOfIsSeparated

English

For any I ≤ J, the inclusion I.inclusion h is a closed immersion.

Русский

Для любых I ≤ J включение I.inclusion h является замкнутым вложением.

LaTeX

$$IsClosedImmersion\left(I.inclusion h\right)$$

Lean4

instance (priority := low) {X : Scheme.{u}} [X.IsSeparated] : QuasiSeparatedSpace X :=
  quasiSeparatedSpace_of_quasiSeparated (terminal.from X)

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

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

Разделы

Аффилиация

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