germ — Mathlib

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⟩)

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