English
If for all opens U the map on F.obj (op U) to G.obj (op U) is injective, then the induced stalk map is injective for all x.
Русский
Если для каждого открытого U отображение F.obj(op U) → G.obj(op U) инъективно, то соответствующее отображение стэла инъективно для каждого x.
LaTeX
$$Injectivity of stalk map follows from injectivity on all opens.$$
Lean4
/-- The isomorphism `ℱ_{f(x)} ≅ (f⁻¹ℱ)ₓ`. -/
def stalkPullbackIso (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) : F.stalk (f x) ≅ ((pullback C f).obj F).stalk x
where
hom := stalkPullbackHom _ _ _ _
inv := stalkPullbackInv _ _ _ _
hom_inv_id := by
ext U hU
dsimp
rw [germ_stalkPullbackHom_assoc, germ_stalkPullbackInv, Category.comp_id,
pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk]
inv_hom_id := by
ext V hV
dsimp
rw [germ_stalkPullbackInv_assoc, Category.comp_id, germToPullbackStalk_stalkPullbackHom]
