subSchemeCover_map_inclusion — Mathlib

English

Compatibility of the inclusion with the open cover gluing maps.

Русский

Совместимость включения с величинами склейки открытого покрытия.

LaTeX

$$$subSchemeCover(Map(inclusion)) = glueDataObjHom$$$

Lean4

@[reassoc (attr := simp)]
theorem subSchemeCover_map_inclusion {I J : IdealSheafData X} (h : I ≤ J) (U) :
    J.subschemeCover.f U ≫ inclusion h = glueDataObjHom h U ≫ I.subschemeCover.f U :=
  J.subschemeCover.openCover.ι_glueMorphisms _ _ _

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