stalkPullbackInv — Mathlib

English

If at every open U the map on sections is injective, then the induced stalk map is injective for all x.

Русский

Если на каждом открытом U отображение на секции инъективно, то индуцированное отображение на стэлах инъективно для всех x.

LaTeX

$$Injectivity of stalk map given injective maps on all opens.$$

Lean4

/-- The morphism `(f⁻¹ℱ)ₓ ⟶ ℱ_{f(x)}`. -/
def stalkPullbackInv (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) : ((pullback C f).obj F).stalk x ⟶ F.stalk (f x) :=
  colimit.desc ((OpenNhds.inclusion x).op ⋙ (Presheaf.pullback C f).obj F)
    { pt := F.stalk (f x)
      ι :=
        { app := fun U => F.germToPullbackStalk _ f (unop U).1 x (unop U).2
          naturality := fun U V i => by
            dsimp
            ext W hW
            dsimp [OpenNhds.inclusion]
            rw [Category.comp_id, ← Functor.map_comp_assoc,
              pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk]
            erw [pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk] } }

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