subschemeMap_subschemeι — Mathlib

English

The composition of the subscheme map with the inclusion of J into its ambient scheme equals the inclusion of I via f; i.e., the diagram commutes.

Русский

Сжатие отображения подсхем согласуется с вложением J в Y через f; диаграмма коммутирует.

LaTeX

$$$ (I.subschemeMap J f H) \\; ≫\\; J.subschemeι = I.subschemeι \\; ≫\\; f $$$

Lean4

@[reassoc (attr := simp)]
theorem subschemeMap_subschemeι (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) :
    subschemeMap I J f H ≫ J.subschemeι = I.subschemeι ≫ f :=
  IsClosedImmersion.lift_fac _ _ _

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