congr_app — Mathlib

English

If α = β, then their c-apps at U differ by composing with a transport given by the equality, i.e., α.c.app U = β.c.app U ∘ X.presheaf.map (eqToHom (by subst h; rfl)).

Русский

Если α = β, то их соответствующие карты на открытом U отличаются транспортом, задаваемым равенством.

LaTeX

$$$\forall X,Y:\mathrm{SheafedSpace}(C),\; \alpha,\beta:\, X\to Y,\; h:\alpha=\beta,\; U:\mathrm{Opens}\;Y,\; \alpha.c.app U = \beta.c.app U \;\circ\; X.presheaf.map(\mathrm{eqToHom}(by \text{ subst } h;\; rfl))$$$

Lean4

theorem congr_app {X Y : SheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U) :
    α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom (by subst h; rfl)) :=
  PresheafedSpace.congr_app h U

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