stalkToFiber_surjective — Mathlib

English

For every point x ∈ X, every germ at x arises from some section over a neighborhood of x; i.e., the canonical stalk-to-germ map is surjective.

Русский

Для каждой точки x ∈ X каждый герм в стеке в точке x образуется гомоморфизмом некоторой секции над окрестностью x; то есть каноническое отображение стека на герм является сюръективным.

LaTeX

$$$\forall x, \operatorname{Im}(F.stalkToFiber x) = F_x.$$$

Lean4

theorem stalkToFiber_surjective (x : X) : Function.Surjective (F.stalkToFiber x) :=
  by
  apply TopCat.stalkToFiber_surjective
  intro t
  obtain ⟨U, m, s, rfl⟩ := F.germ_exist _ t
  use ⟨U, m⟩
  fconstructor
  · exact fun y => F.germ _ _ y.2 s
  · exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩

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