English
Compatibility of germToPullbackStalk with left Kan extension unit: the component at V after applying unit equals the germ map on V.
Русский
Совместимость germToPullbackStalk с единицей левостороннего Kan-расширения: компонент на V совпадает с зародком.
LaTeX
$$Compatibility statement for germToPullbackStalk with unit of Kan extension.$$
Lean4
/-- The morphism `(f⁻¹ℱ)(U) ⟶ ℱ_{f(x)}` for some `U ∋ x`. -/
def germToPullbackStalk (f : X ⟶ Y) (F : Y.Presheaf C) (U : Opens X) (x : X) (hx : x ∈ U) :
((pullback C f).obj F).obj (op U) ⟶ F.stalk (f x) :=
((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F (op U)).desc
{ pt := F.stalk ((f : X → Y) (x : X))
ι :=
{ app := fun V => F.germ _ (f x) (V.hom.unop.le hx)
naturality := fun _ _ i => by simp } }
