sheafValGluedMk — Mathlib

English

Construction of glued section from compatible local sections on a glue datum.

Русский

Построение склеенной секции из совместимых локальных секций по данным склейки.

LaTeX

$$$$ \text{sheafValGluedMk} : F \to \text{glued} $$$$

Lean4

/-- Constructor for sections over `D.glued` of a sheaf of types on the big Zariski site. -/
noncomputable def sheafValGluedMk : F.val.obj (op D.glued) :=
  Multifork.IsLimit.sectionsEquiv (D.oneHypercover.isLimitMultifork F)
    { val := s
      property := fun _ ↦ h _ _ }

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