English
A specialized version of hom_ext for arrows in the presheaf IsSheaf setting, asserting equality from pointwise agreement on generating arrows.
Русский
Уточненная формулировка hom_ext для стрелок препрошки IsSheaf, дающая равенство по точечному совпадению на порождающих стрелках.
LaTeX
$$$\\text{hom\_ext}$$$
Lean4
/-- This is a wrapper around `Presieve.IsSheafFor.amalgamate` to be used below.
If `P`s a sheaf, `S` is a cover of `X`, and `x` is a collection of morphisms from `E`
to `P` evaluated at terms in the cover which are compatible, then we can amalgamate
the `x`s to obtain a single morphism `E ⟶ P.obj (op X)`. -/
def amalgamate {A : Type u₂} [Category.{v₂} A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A} (hP : Presheaf.IsSheaf J P) (S : J.Cover X)
(x : ∀ I : S.Arrow, E ⟶ P.obj (op I.Y))
(hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op) : E ⟶ P.obj (op X) :=
(hP _ _ S.condition).amalgamate (fun Y f hf => x ⟨Y, f, hf⟩) fun _ _ _ _ _ _ _ h₁ h₂ w =>
@hx { hf := h₁, .. } { hf := h₂, .. } { w := w, .. }
