AlgebraicGeometry.PresheafedSpace.stalkMap.congr

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.congr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : AlgebraicGeometry.PresheafedSpace C} (α β : X ⟶ Y) (h₁ : α = β) (x x' : ↑↑X) (h₂ : x = x'), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap α x) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.stalkMap β x')

The theorem `AlgebraicGeometry.PresheafedSpace.stalkMap.congr` states that if we have two morphisms `α` and `β` from presheafed space `X` to `Y`, and two points `x` and `x'` in `X`, such that `α` equals `β` and `x` equals `x'`, then the stalk map of `α` at `x` followed by the morphism defined by the equality of the images of `x` under `α` and `β`, is the same as the morphism defined by the equality of `x` and `x'` followed by the stalk map of `β` at `x'`. This is a congruence theorem, which means it deals with equality up to isomorphism, and it's important in algebraic geometry because it shows how the stalk map depends on the morphism and the point, but only up to isomorphism. It uses `eqToHom` arrows to handle the equality of the morphisms and points, because their types are not the same by definition, and thus we can't just say that they are equal.

More concisely: Given presheafed spaces X and morphisms α, β: X -> Y, and points x, x' in X with α(x) = β(x) and x = x', the stalk maps [α]_x and [β]_x' are isomorphic.