English
Global sections of a sheaf of types correspond to morphisms from a terminal constant sheaf to the sheaf.
Русский
Глобальные секции шейфа типа соответствуют морфизмам из терминального константного шейфа к данному шейфу.
LaTeX
$$$\text{(HasWeakSheafify } J\ (\text{Type } w)) \Rightarrow \text{(HasGlobalSectionsFunctor } J\ (\text{Type } w))} \,\Rightarrow\; (\Gamma J (\text{Type } w)).\mathrm{obj} F \simeq (\text{constantSheaf } J (\text{Type } w)).\mathrm{obj} X \to F$$$
Lean4
theorem ΓRes_naturality [HasGlobalSectionsFunctor J A] {F G : Sheaf J A} (f : F ⟶ G) (U : Cᵒᵖ) :
(Γ J A).map f ≫ ΓRes G U = ΓRes F U ≫ f.val.app U :=
by
refine .trans ?_ <| congr_app (ΓHomEquiv_naturality_right_symm _ _) U
exact (congr_app (ΓHomEquiv_naturality_left_symm ((Γ J A).map f) (𝟙 _)) U).symm.trans (by simp)
