inclusion — Mathlib

English

The inclusion of ideal sheaf data induces a morphism of schemes when I ≤ J.

Русский

Включение данных идеала шейфа индуцирует морфизм подсхем при I ≤ J.

LaTeX

$$$\text{inclusion}: I \le J \Rightarrow J.subscheme \to I.subscheme$$$

Lean4

/-- The inclusion of ideal sheaf induces an inclusion of subschemes -/
noncomputable def inclusion {I J : IdealSheafData X} (h : I ≤ J) : J.subscheme ⟶ I.subscheme :=
  J.subschemeCover.openCover.glueMorphisms (fun U ↦ glueDataObjHom h U ≫ I.subschemeCover.f U)
    (by
      intro U V
      simp only [← cancel_mono I.subschemeι, AffineOpenCover.openCover_X, glueDataObjHom_ι_assoc,
        AffineOpenCover.openCover_f, Category.assoc, subschemeCover_map_subschemeι]
      rw [← subschemeCover_map_subschemeι, pullback.condition_assoc, subschemeCover_map_subschemeι])

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