English
Let G: C → D be a functor, ℱ a presheaf on D and ℱ' a sheaf on D with respect to a topology K; for a given morphism α: G^op ∘ ℱ → G^op ∘ ℱ'.val, the construction appHom_X(α) provides, for every X ∈ D, a morphism ℱ(op X) → ℱ'.val(op X) obtained by gluing the pushforward data.
Русский
Пусть G: C → D — функтор, ℱ — претопос на D, ℱ' — шейф на D по топологии K; дано морфизм α: G^op ∘ ℱ → G^op ∘ ℱ'.val; для каждого объекта X ∈ D существует естественный морфизм ℱ(op X) → ℱ'.val(op X), получаемый путём склейки данных pushforward.
LaTeX
$$$\mathrm{appHom}_X(\alpha): \mathcal{F}(\mathrm{op} X) \longrightarrow \mathcal{F}'(\mathrm{op} X).$$$
Lean4
/-- (Implementation). The morphism `ℱ(X) ⟶ ℱ'(X)` given by gluing the `pushforwardFamily`. -/
noncomputable def appHom (X : D) : ℱ.obj (op X) ⟶ ℱ'.val.obj (op X) := fun x =>
((isSheaf_iff_isSheaf_of_type _ _).1 ℱ'.cond _ (G.is_cover_of_isCoverDense _ X)).amalgamate (pushforwardFamily α x)
(pushforwardFamily_compatible α x)
