English
The amalgamateOfArrows is the morphism E → P(op S) obtained from the unique amalgamation guaranteed by the sheaf condition, given the arrows f_i and the compatible family x.
Русский
Амальгамирование стрел amalgamateOfArrows есть морфизм E → P(op S), полученный как уникальное амальгамирование, гарантируемое условием шейфа, при заданных стрелках f_i и совместимой семье x.
LaTeX
$$$\\text{amalgamateOfArrows} : E \\to P(\\mathrm{op} S) = (h_P.existsUnique_amalgamation_ofArrows \\, f \\, hf \\, x \\, hx).choose$$$
Lean4
/-- If `P : Cᵒᵖ ⥤ A` is a sheaf and `f i : X i ⟶ S` is a covering family, then
a morphism `E ⟶ P.obj (op S)` can be constructed from a compatible family of
morphisms `x : E ⟶ P.obj (op (X i))`. -/
def amalgamateOfArrows : E ⟶ P.obj (op S) :=
(hP.existsUnique_amalgamation_ofArrows f hf x hx).choose
