inclusion_subschemeι — Mathlib

English

The composition inclusion h ≫ I.subschemeι equals J.subschemeι when h corresponds to I ≤ J.

Русский

Составление включения h ≫ I.subschemeι равно J.subschemeι при соответствующем I ≤ J.

LaTeX

$$$inclusion(h) \circ I.subschemeι = J.subschemeι$$$

Lean4

@[reassoc (attr := simp)]
theorem inclusion_subschemeι {I J : IdealSheafData X} (h : I ≤ J) : inclusion h ≫ I.subschemeι = J.subschemeι :=
  J.subschemeCover.openCover.hom_ext _ _ fun _ ↦ by simp

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