English
For X, Y presheafed spaces and α, β : X ⟶ Y with h₁ : α = β and x, x' : X with h₂ : x = x', one has an equality up to transports: α.stalkMap x ≫ eqToHom (X.presheaf.stalk x = X.presheaf.stalk x') = eqToHom (Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (β.base x')) ≫ β.stalkMap x'.
Русский
Для X, Y и стрелок α, β: X ⟶ Y с h₁ : α = β и точек x, x' с h₂ : x = x' выполняется равенство с переносами: α.stalkMap x ≫ eqToHom (X.presheaf.stalk x = X.presheaf.stalk x') = eqToHom (Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (β.base x')) ≫ β.stalkMap x'.
LaTeX
$$$$\\alpha.stalkMap x \\;\\;\\; \\; \\; = \\;\\; \\mathrm{eqToHom}\\Big( X.presheaf.stalk x = X.presheaf.stalk x' \\Big) \\; \\; ≫ \\;\\; \\beta.stalkMap x' $$$$
Lean4
theorem congr_point {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (x x' : X) (h : x = x') :
α.stalkMap x ≫ eqToHom (show X.presheaf.stalk x = X.presheaf.stalk x' by rw [h]) =
eqToHom (show Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (α.base x') by rw [h]) ≫ α.stalkMap x' :=
by rw [stalkMap.congr α α rfl x x' h]
