English
For hx and g with Z and p, hp, the equation app hG x hx g ≫ G.map p.op = F.map p.op ≫ (x(p ≫ g) hp).app ⟨Over.mk(𝟙 Z)⟩ holds.
Русский
Для hx и g с Z и p, hp верно равенство app hG x hx g ≫ G.map p.op = F.map p.op ≫ (x(p ≫ g) hp).app(Over.mk(id_Z)).
LaTeX
$$app hG x hx g ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app(Over.mk(id_Z))$$
Lean4
/-- The underlying presheaf of `sheafHom F G`. It is isomorphic to `presheafHom F.1 G.1`
(see `sheafHom'Iso`), but has better definitional properties. -/
def sheafHom' (F G : Sheaf J A) : Cᵒᵖ ⥤ Type _
where
obj X := (J.overPullback A X.unop).obj F ⟶ (J.overPullback A X.unop).obj G
map f := fun φ => (J.overMapPullback A f.unop).map φ
map_id
X := by
ext φ : 2
exact congr_fun ((presheafHom F.1 G.1).map_id X) φ.1
map_comp f
g := by
ext φ : 2
exact congr_fun ((presheafHom F.1 G.1).map_comp f g) φ.1
