congr_hom — Mathlib

English

If α = β, then the stalk map at x is equal to the appropriate transport plus the stalk map β: α.stalkMap x = eqToHom (...) ≫ β.stalkMap x.

Русский

Если α = β, то отображение stalkMap в точке x равно соответствующему переносу плюс stalkMap β: α.stalkMap x = eqToHom (...) ≫ β.stalkMap x.

LaTeX

$$$$\\alpha.stalkMap x = \\; \\; \\mathrm{eqToHom}\\Big( Y.presheaf.stalk (\\alpha.base x) = Y.presheaf.stalk (\\beta.base x) \\Big) \\;\\; \\ggg\\; \\beta.stalkMap x$$$$

Lean4

theorem congr_hom {X Y : PresheafedSpace.{_, _, v} C} (α β : X ⟶ Y) (h : α = β) (x : X) :
    α.stalkMap x = eqToHom (show Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (β.base x) by rw [h]) ≫ β.stalkMap x :=
  by rw [← stalkMap.congr α β h x x rfl, eqToHom_refl, Category.comp_id]

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