English
Natural transformations from a constant presheaf into a sheaf correspond to morphisms to its global sections; i.e., Hom(const X, F) ≅ Hom(X, Γ J A(F)).
Русский
Натуральные преобразования от константной префешиба к шейфу соответствуют морфизмам в его глобальные секции; тождество Hom(const X, F) ≅ Hom(X, Γ J A(F)).
LaTeX
$$$((\mathrm{Functor}.const _).\mathrm{obj} X \longrightarrow F.\mathrm{val}) \cong (X \longrightarrow (\Gamma J A).\mathrm{obj} F)$$$
Lean4
/-- Natural transformations from a constant presheaf into a sheaf correspond to morphisms to its
global sections. -/
noncomputable def ΓHomEquiv [HasGlobalSectionsFunctor J A] {X : A} {F : Sheaf J A} :
((Functor.const _).obj X ⟶ F.val) ≃ (X ⟶ (Γ J A).obj F) :=
((sheafificationAdjunction J A).homEquiv _ _).symm.trans ((constantSheafΓAdj J A).homEquiv _ _)
