English
The germ after applying a morphism to the section corresponds to germ of the image section: (F.germ U x hx s) mapped under stalk is sent to G.germ U x hx (f.app (op U) s).
Русский
Зародок после применения морфизма к секции соответствует зародку образа секции: (F.germ U x hx s) переводится через стэла на G.germ U x hx (f.app (op U) s).
LaTeX
$$$ (F.germ\ U\ x\ hx\ s) \,\mapsto\, G.germ\ U\ x\ hx\ (f.app\ (op\ U)\ s) $$$
Lean4
theorem stalkFunctor_map_germ_apply [ConcreteCategory C FC] {F G : X.Presheaf C} (U : Opens X) (x : X) (hx : x ∈ U)
(f : F ⟶ G) (s) : (stalkFunctor C x).map f (F.germ U x hx s) = G.germ U x hx (f.app (op U) s) :=
by
rw [← ConcreteCategory.comp_apply, ← stalkFunctor_map_germ, ConcreteCategory.comp_apply]
rfl
-- a variant of `stalkFunctor_map_germ_apply` that makes simpNF happy.
