English
Let X, Y be presheafed spaces and α : X ⟶ Y. For x, x' ∈ X with h : x = x', one has α.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. Для точек x, 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) \\; \\; ≫ \\;\\; \\alpha.stalkMap x' $$$$
Lean4
instance isIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) [IsIso α] (x : X) : IsIso (α.stalkMap x) where
out := by
let β : Y ⟶ X := CategoryTheory.inv α
have h_eq : (α ≫ β).base x = x := by
rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
-- Intuitively, the inverse of the stalk map of `α` at `x` should just be the stalk map of `β`
-- at `α x`. Unfortunately, we have a problem with dependent type theory here: Because `x`
-- is not *definitionally* equal to `β (α x)`, the map `stalk_map β (α x)` has not the correct
-- type for an inverse.
-- To get a proper inverse, we need to compose with the `eqToHom` arrow
-- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`.
refine
⟨eqToHom (show X.presheaf.stalk x = X.presheaf.stalk ((α ≫ β).base x) by rw [h_eq]) ≫ (β.stalkMap (α.base x) :),
?_, ?_⟩
· rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]
erw [← stalkMap.comp β α (α.base x)]
rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]
·
rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id, eqToHom_trans_assoc,
eqToHom_refl, Category.id_comp]