If `s : X.stalk x`, it comes from some $$F(V)$$

Stream: Is there code for X?

[Jujian Zhang]

I think the following is true:

$(X, \mathcal F)$ is a presheafed space and $V\subseteq X$ open and $x \in V$, $s \in \mathcal F_x$, then for some $s'\in\mathcal F(V)$, $s'_x=s$.

If this is true, is there a way to prove this? An MWE is below.

import algebraic_geometry.sheafed_space
import algebraic_geometry.stalks
import algebra.category.CommRing.colimits

open algebraic_geometry
  algebraic_geometry.PresheafedSpace topological_space opposite
  Top.presheaf

variables (X : PresheafedSpace CommRing) (V : opens X) (x : X) (hx : x ∈ V)
  (s : X.stalk x)

example : ∃ s' : X.presheaf.obj (op V), germ X.2 ⟨x, hx⟩ s' = s := sorry

Thank you.

[Johan Commelin]

You might need to replace V by some smaller open V'. But otherwise, the statement is math-true.

[Johan Commelin]

Proving this in Lean means that you have to know that X.stalk x is equal to the concrete colimit construction, which should be in src/algebra/category/CommRing/colimits.lean. That will give you the V' ∋ x and s' almost automatically.

[Johan Commelin]

Of course "equal" means "canonically isomorphic".

[Justus Springer]

I think docs#Top.presheaf.germ_exist should be it. It is stated in a slightly more general way, namely for concrete categories in which the forgetful functor preserves filtered colimits. This is true for CommRing and type class inference will know about it, as soon as you import src/algebra/category/CommRing/filtered_colimits.lean

[Justus Springer]

And yes, you will only get a section on a neighbourhood contained in V.