English
Let f: X → Y and F: X.Presheaf C. For open U ⊆ Y and x ∈ X with hx: f(x) ∈ U, the germ of the pushforward along f corresponds to the germ of F on a suitable open: (f_*F).germ U (f x) hx ≫ stalkPushforward C f x = F.germ ((Opens.map f).obj U) x hx.
Русский
Пусть f: X → Y и F: X.Presheaf. Для открытого U ⊆ Y и x ∈ X с hx: f(x) ∈ U, зародок вытеснения вдоль f соответствует зародку F на подходящем открытом: (f_*F).germ U (f x) hx ≫ stalkPushforward C f x = F.germ ((Opens.map f).obj U) x hx.
LaTeX
$$$(f_*F).germ\ U\ (f x)\ hx\; ≫\ stalkPushforward\ C\ f\ x = F.germ\ ((Opens.map f).obj U)\ x\ hx$$$
Lean4
@[reassoc (attr := simp), elementwise (attr := simp)]
theorem stalkPushforward_germ (f : X ⟶ Y) (F : X.Presheaf C) (U : Opens Y) (x : X) (hx : f x ∈ U) :
(f _* F).germ U (f x) hx ≫ F.stalkPushforward C f x = F.germ ((Opens.map f).obj U) x hx := by
simp [germ, stalkPushforward]
-- Here are two other potential solutions, suggested by @fpvandoorn at
-- <https://github.com/leanprover-community/mathlib/pull/1018#discussion_r283978240>
-- However, I can't get the subsequent two proofs to work with either one.
-- def stalkPushforward'' (f : X ⟶ Y) (ℱ : X.Presheaf C) (x : X) :
-- (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x :=
-- colim.map ((Functor.associator _ _ _).inv ≫
-- whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) ℱ) ≫
-- colimit.pre ((OpenNhds.inclusion x).op ⋙ ℱ) (OpenNhds.map f x).op
-- def stalkPushforward''' (f : X ⟶ Y) (ℱ : X.Presheaf C) (x : X) :
-- (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x :=
-- (colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) ℱ) :
-- colim.obj ((OpenNhds.inclusion (f x) ⋙ Opens.map f).op ⋙ ℱ) ⟶ _) ≫
-- colimit.pre ((OpenNhds.inclusion x).op ⋙ ℱ) (OpenNhds.map f x).op
