English
The specialization relation on stalks is compatible with composition of specializations; associativity holds.
Русский
Связь специализации на стэлах совместима с композициями специализаций; ассоциативность соблюдается.
LaTeX
$$F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes (h.trans h')$$
Lean4
/-- If `x` specializes to `y`, then there is a natural map `F.stalk y ⟶ F.stalk x`. -/
noncomputable def stalkSpecializes (F : X.Presheaf C) {x y : X} (h : x ⤳ y) : F.stalk y ⟶ F.stalk x :=
by
refine colimit.desc _ ⟨_, fun U => ?_, ?_⟩
·
exact
colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
(op ⟨(unop U).1, (specializes_iff_forall_open.mp h _ (unop U).1.2 (unop U).2 :)⟩)
· intro U V i
dsimp
rw [Category.comp_id]
let U' : OpenNhds x := ⟨_, (specializes_iff_forall_open.mp h _ (unop U).1.2 (unop U).2 :)⟩
let V' : OpenNhds x := ⟨_, (specializes_iff_forall_open.mp h _ (unop V).1.2 (unop V).2 :)⟩
exact colimit.w ((OpenNhds.inclusion x).op ⋙ F) (show V' ⟶ U' from i.unop).op
