glueDataObjHom_ι — Mathlib

English

A compatibility lemma for glueDataObjHom with theι.

Русский

Лемма совместимости glueDataObjHom с subschemeι.

LaTeX

$$$GlueDataObjHom(h,U) \circ I.glueDataObjι U = J.glueDataObjι U$$$

Lean4

@[reassoc (attr := simp)]
theorem glueDataObjHom_ι {I J : IdealSheafData X} (h : I ≤ J) (U) :
    glueDataObjHom h U ≫ I.glueDataObjι U = J.glueDataObjι U := by
  rw [glueDataObjHom, glueDataObjι, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.Quotient.factor_comp_mk]

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