comp_c_app — Mathlib

English

If two presheafed space morphisms are equal, then their c-components apply suitably with the presheaf map.

Русский

Если два морфизма прешефдов пространства равны, то их компоненты c согласованы через отображение прешефа.

LaTeX

$$$\forall X,Y, \alpha = \beta \Rightarrow \alpha.c.app(U) = \beta.c.app(U) \circ X.presheaf.map(\text{eqToHom}())$$$

Lean4

/-- Sometimes rewriting with `comp_c_app` doesn't work because of dependent type issues.
In that case, `erw comp_c_app_assoc` might make progress.
The lemma `comp_c_app_assoc` is also better suited for rewrites in the opposite direction. -/
@[reassoc, simp]
theorem comp_c_app {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
    (α ≫ β).c.app U = β.c.app U ≫ α.c.app (op ((Opens.map β.base).obj (unop U))) :=
  rfl

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