germ_stalkPullbackHom — Mathlib

English

The morphism germToPullbackStalk is defined from the pullback of a presheaf to the stalk: for each F: Y.Presheaf C, open U ⊆ X and x ∈ X with hx, it is the universal morphism from ((pullback C f).obj F).obj (op U) to F.stalk (f x).

Русский

Зародок к преобразованию к стэлу задаётся как универсальный морфизм от (pullback C f).obj F к F.stalk (f x).

Lean4

@[reassoc (attr := simp)]
theorem germ_stalkPullbackHom (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) (U : Opens Y) (hU : f x ∈ U) :
    F.germ U (f x) hU ≫ stalkPullbackHom C f F x =
      ((pushforwardPullbackAdjunction C f).unit.app F).app _ ≫ ((pullback C f).obj F).germ ((Opens.map f).obj U) x hU :=
  by simp [stalkPullbackHom, germ, stalkFunctor, stalkPushforward]

Похожие утверждения