English
The germ map on a pullback along f composed with stalkPullbackHom equals a canonical unit map composed with germ on the pullback: F.germ U (f x) hx ≫ stalkPullbackHom C f F x = ((pushforwardPullbackAdjunction C f).unit.app F).app _ ≫ ((pullback C f).obj F).germ ((Opens.map f).obj U) x hx.
Русский
Зародок вдоль f совместим с stalkPullbackHom через единичный морфизм кардинальных канонических карт; эквивалентно формуле.
LaTeX
$$$F.germ U (f x) hx ≫ stalkPullbackHom C f F x = ((pushforwardPullbackAdjunction C f).unit.app F).app _ ≫ ((pullback C f).obj F).germ ((Opens.map f).obj U) x hx$$$
Lean4
/-- The morphism `ℱ_{f x} ⟶ (f⁻¹ℱ)ₓ` that factors through `(f_*f⁻¹ℱ)_{f x}`. -/
def stalkPullbackHom (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) : F.stalk (f x) ⟶ ((pullback C f).obj F).stalk x :=
(stalkFunctor _ (f x)).map ((pushforwardPullbackAdjunction C f).unit.app F) ≫ stalkPushforward _ _ _ x
