English
Let P be a presheaf on a category C, R a presieve on X, and x a compatible family of elements of P indexed by R. An element t ∈ P(op X) is called an amalgamation for x if restricting t along every arrow in R lands at the corresponding component of x; i.e., for every Y and every morphism f: Y → X with f ∈ R, P.map f^{op}(t) = x_f.
Русский
Пусть P — предшкепа над категорией C, R — предрассыпь на X, и x — совместная совокупность элементов P, индексированная по R. Элемент t ∈ P(op X) называется амальгаммой для x, если при ограничении t вдоль каждого стрелки f: Y → X с f ∈ R получаем соответствующий компонент x_f; то есть P.map f^{op}(t) = x_f для всех Y, f, h.
LaTeX
$$$IsAmalgamation(x,R,t) \equiv \forall Y \left( f:Y\to X \right) \left( h:R f \right),\; P.map f^{op} t = x f h$$$
Lean4
/-- The given element `t` of `P.obj (op X)` is an *amalgamation* for the family of elements `x` if every
restriction `P.map f.op t = x_f` for every arrow `f` in the presieve `R`.
This is the definition given in https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents,
and https://ncatlab.org/nlab/show/matching+family, as well as [MM92], Chapter III, Section 4,
equation (2).
-/
def IsAmalgamation (x : FamilyOfElements P R) (t : P.obj (op X)) : Prop :=
∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : R f), P.map f.op t = x f h
