English
Definition of the germ of a presheaf section at a point within an open set.
Русский
Определение герма секции предперешафа в точке внутри открытого множества.
LaTeX
$$$\text{germ}(F, U, x, hx): F.obj(op U) \to F.stalk x$$$
Lean4
/-- The germ of a section of a presheaf over an open at a point of that open.
-/
def germ (F : X.Presheaf C) (U : Opens X) (x : X) (hx : x ∈ U) : F.obj (op U) ⟶ stalk F x :=
colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨U, hx⟩)