instSubschemeι

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsClosedImmersion.instSubschemeι

English

The subscheme immersion is a closed immersion for any ideal sheaf data range subscheme.

Русский

О immersed subscheme отношение к идеалу.

LaTeX

$$IsClosedImmersion I.subschemeι for any I ∈ X.IdealSheafData$$

Lean4

instance {X : Scheme} (I : X.IdealSheafData) : IsClosedImmersion I.subschemeι :=
  .of_isPreimmersion _ (I.range_subschemeι ▸ I.support.isClosed)

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

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

Разделы

Аффилиация

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