English
If α = β and x = x', then the stalk maps agree up to transport along equalities. More precisely, α.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₁, h₂]) ≫ β.stalkMap x'.
Русский
Если α = β и x = x', то отображения stalkMap совпадают после переноса по равенствам. Точнее: α.stalkMap x ≫ eqToHom (покажите X.presheaf.stalk x = X.presheaf.stalk x' по rw [h₂]) = eqToHom (покажите Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (β.base x') по rw [h₁, h₂]) ≫ β.stalkMap x'.
LaTeX
$$$$\\alpha.stalkMap x \\;\\;\\; \\; = \\;\\;\\; \\mathrm{eqToHom}\\Big( X.presheaf.stalk x = X.presheaf.stalk x' \\Big) \\; \\circ \\; \\beta.stalkMap x'$$$$
Lean4
/-- If `α = β` and `x = x'`, we would like to say that `stalk_map α x = stalk_map β x'`.
Unfortunately, this equality is not well-formed, as their types are not _definitionally_ the same.
To get a proper congruence lemma, we therefore have to introduce these `eqToHom` arrows on
either side of the equality.
-/
theorem congr {X Y : PresheafedSpace.{_, _, v} C} (α β : X ⟶ Y) (h₁ : α = β) (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₁, h₂]) ≫ β.stalkMap x' :=
by
ext
substs h₁ h₂
simp
