English
Let F be a presheaf on X valued in a category, x a point of X, and t a germ of F at x. Then there exists an open neighborhood U of x, an element m ∈ x ∈ U, a basis element U with U ∈ B, and a section s ∈ F(U) whose germ at x equals t.
Русский
Пусть F есть расслойка-пресеша над X, x — точка X, t — гёрм F в x. Тогда существует открытое окрестность U точки x с U ∈ B, точка m ∈ x ∈ U и секция s ∈ F(U), такая что Germ(F, U, x, m, s) = t.
LaTeX
$$$\forall F: X\text{-Presheaf}, \forall x \in X, \forall t:\ToType(F.stalk\,x),\exists U\in Opens(X),\exists m:\, x\in U\ (m\in x)\ (U\in B)\ (s:\ToType(F.obj(op\ U))),\ F.germ\,U\,x\,m\,s = t$$$
Lean4
theorem germ_exist_of_isBasis (F : X.Presheaf C) (x : X) (t : ToType (F.stalk x)) :
∃ (U : Opens X) (m : x ∈ U) (_ : U ∈ B) (s : ToType (F.obj (op U))), F.germ _ x m s = t :=
by
obtain ⟨U, hxU, s, rfl⟩ := F.germ_exist x t
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hB.exists_subset_of_mem_open hxU U.2
exact ⟨V, hxV, hV, F.map (homOfLE hVU).op s, by rw [← ConcreteCategory.comp_apply, F.germ_res']⟩
