English
There is an equivalence between the sections of presheafHom F G and morphisms F → G, given by taking components at identity morphisms in each Over object.
Русский
Существует эквиваленция между секциями presheafHom F G и морфизмами F → G, получаемая из компонент на единичных морфизмах в каждом Over-объекте.
LaTeX
$$(presheafHom F G).sections ≃ (F ⟶ G)$$
Lean4
/-- Given two sheaves `F` and `G` on a site `(C, J)` with values in a category `A`,
this `sheafHom F G` is the sheaf of types which sends an object `X : C`
to the type of morphisms between the "restrictions" of `F` and `G` to the category `Over X`. -/
def sheafHom (F G : Sheaf J A) : Sheaf J (Type _)
where
val := sheafHom' F G
cond := (Presheaf.isSheaf_of_iso_iff (sheafHom'Iso F G)).2 (G.2.hom F.1)
