pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk

English

Under mild forgetful-preserves-filtered-colimits conditions, every stalk element comes from a germ of a section: there exist U m s with F.germ U x m s = t.

Русский

При подходящих условиях существования совместимых колимитов, каждый элемент стэла является зародком секции: существуют U, m, s такие, что F.germ U x m s = t.

LaTeX

$$germ_exist (F : X.Presheaf C) (x : X) (t) : ∃ U m s, F.germ U x m s = t$$

Lean4

@[reassoc (attr := simp)]
theorem pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk (f : X ⟶ Y) (F : Y.Presheaf C) (V : (Opens Y)ᵒᵖ)
    (x : X) (hx : f x ∈ V.unop) :
    ((pushforwardPullbackAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F _ x hx = F.germ _ (f x) hx := by
  simpa using
    pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk C f F ((Opens.map f).obj V.unop) x hx V.unop
      (by rfl)

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