English
If α : X ⟶ Y is an isomorphism, then for every x ∈ X the stalk map α.stalkMap x is an isomorphism (i.e., invertible).
Русский
Если α : X ⟶ Y — изоморфизм, тогда для каждой точки x ∈ X отображение stalkMap x является изоморфизмом (обратимо).
LaTeX
$$$$ \\forall x,\\; IsIso(\\alpha.stalkMap x). $$$$
Lean4
@[reassoc (attr := simp), elementwise (attr := simp)]
theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C} (f : X ⟶ Y) {x y : X} (h : x ⤳ y) :
Y.presheaf.stalkSpecializes (f.base.hom.map_specializes h) ≫ f.stalkMap x =
f.stalkMap y ≫ X.presheaf.stalkSpecializes h :=
by
-- Porting note: the original one liner `dsimp [stalkMap]; simp [stalkMap]` doesn't work,
-- I had to uglify this
dsimp [stalkSpecializes, Hom.stalkMap, stalkFunctor, stalkPushforward]
-- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
refine colimit.hom_ext fun j => ?_
induction j with
| op j => ?_
dsimp
simp only [colimit.ι_desc_assoc, ι_colimMap_assoc, whiskerLeft_app, whiskerRight_app, NatTrans.id_app, colimit.ι_pre,
assoc, colimit.pre_desc, colimit.map_desc, colimit.ι_desc, Cocones.precompose_obj_ι, Cocone.whisker_ι,
NatTrans.comp_app]
tauto
