stalkToFiber_germ — Mathlib

English

If every fiber point has a local sector passing through it, then stalkToFiber map is surjective.

Русский

Если каждый элемент волокна имеет локальную секцию, проходящую через него, то отображение stalkToFiber сюръективно.

LaTeX

$$$\\forall t, \\exists U,f,h, f\\_{|U} = t \\Rightarrow stalkToFiber\\ P\\ x \\text{ surjective}. $$$

Lean4

theorem stalkToFiber_germ (P : LocalPredicate T) (U : Opens X) (x : X) (hx : x ∈ U) (f) :
    stalkToFiber P x ((subsheafToTypes P).presheaf.germ U x hx f) = f.1 ⟨x, hx⟩ := by simp [Presheaf.germ, stalkToFiber]

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