glueDataObjHom_comp — Mathlib

English

Simplified equality of functorial actions in subscheme context.

Русский

Упрощённое равенство действий функторов в контексте подсхемы.

LaTeX

$$$(I.subschemeι.app U) = \text{simplified form}$$$

Lean4

@[reassoc (attr := simp)]
theorem glueDataObjHom_comp {I J K : IdealSheafData X} (hIJ : I ≤ J) (hJK : J ≤ K) (U) :
    glueDataObjHom hJK U ≫ glueDataObjHom hIJ U = glueDataObjHom (hIJ.trans hJK) U :=
  by
  rw [← cancel_mono (I.glueDataObjι U)]
  simp

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