instIsClosedImmersionInclusion — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance {I J : X.IdealSheafData} (h : I ≤ J) : IsClosedImmersion (I.inclusion h) :=
  by
  have : IsClosedImmersion (I.inclusion h ≫ I.subschemeι) :=
    by
    simp only [Scheme.IdealSheafData.inclusion_subschemeι]
    infer_instance
  exact .of_comp _ I.subschemeι

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