comp_c_app — Mathlib

English

The structural map of the composite morphism equals the composition of the corresponding structural maps with the appropriate transport of opens.

Русский

Структурная карта композиции равна композиции соответствующих структурных карт с корректной переноской открытых множеств.

LaTeX

$$$\forall X,Y,Z:\mathrm{SheafedSpace}(C),\; \alpha:X\to Y,\ \beta:Y\to Z,\ U,\; (\alpha\circ\beta).c.app\;U = \beta.c.app\;U\;\circ\;\alpha.c.app\left(\mathrm{op}\left(\mathrm{Opens.map}\;\beta.base\;.obj\; (\mathrm{unop}\;U)\right)\right)$$$

Lean4

@[simp]
theorem comp_c_app {X Y Z : SheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
    (α ≫ β).c.app U = β.c.app U ≫ α.c.app (op ((Opens.map β.base).obj (unop U))) :=
  rfl

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