subschemeMap — Mathlib

English

If J ≤ I.map f, then there is a natural morphism between the closed subschemes I.subscheme and J.subscheme, i.e., the map restricts to a morphism on the closed subschemes compatible with f.

Русский

Если J ≤ I.map f, существует естественное отображение между замкнутыми подсхемами I.subscheme и J.subscheme, т.е. отображение ограничивается на подсхемы и совместимо с f.

LaTeX

$$$ subschemeMap\\; I\\; J\\; f\\; H : I.subscheme \\to J.subscheme $$$

Lean4

/-- If `J ≤ I.map f`, then `f` restricts to a map `I ⟶ J` between the closed subschemes. -/
def subschemeMap (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) :
    I.subscheme ⟶ J.subscheme :=
  IsClosedImmersion.lift J.subschemeι (I.subschemeι ≫ f) (by simpa using H)

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