English
If a basis B for opens is given, then there is an equivalence between Hom-sets of restricted presheaves and the Hom-set of the original presheaves.
Русский
Дано основание B для открытых множеств, существует эквивалентность между множествами гомоморфизмов ограниченных пресшей и гомоморфизмов исходных пресшефов.
LaTeX
$$$\text{restrictHomEquivHom}(F,F',h) : \big((\operatorname{inducedFunctor} B)^{\mathrm{op}} \circ F \to (\operatorname{inducedFunctor} B)^{\mathrm{op}} \circ F'\!\!\!\!\!\!\!\!\!\!\!\!\!\!\right) \simeq (F \to F'.1)$$$
Lean4
/-- If a family `B` of open sets forms a basis of the topology on `X`, and if `F'`
is a sheaf on `X`, then a homomorphism between a presheaf `F` on `X` and `F'`
is equivalent to a homomorphism between their restrictions to the indexing type
`ι` of `B`, with the induced category structure on `ι`. -/
def restrictHomEquivHom (h : Opens.IsBasis (Set.range B)) :
((inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.1) ≃ (F ⟶ F'.1) :=
@Functor.IsCoverDense.restrictHomEquivHom _ _ _ _ _ _ _ _ (Opens.coverDense_inducedFunctor h) _ F F'
