English
For a presheafHom between F and G, a comma-family x has an amalgamation y iff for all Y, g, and hg with S g, y on g equals the corresponding x-component on id_Y.
Русский
Для presheafHom между F и G, семейство x имеет amalgamation y тогда и только тогда, когда для каждого Y, g и hg с S g, часть y на g равна соответствующей компоненте x на id_Y.
LaTeX
$$x.IsAmalgamation(y) \iff \forall Y\, \forall g\, \forall hg,\; y.app(Over.mk g) = (x g hg).app(Over.mk(id_Y))$$
Lean4
/-- Equational lemma for the presheaf structure on `presheafHom`.
It is advisable to use this lemma rather than `dsimp [presheafHom]` which may result
in the need to prove equalities of objects in an `Over` category. -/
theorem presheafHom_map_app {X Y Z : C} (f : Z ⟶ Y) (g : Y ⟶ X) (h : Z ⟶ X) (w : f ≫ g = h)
(α : (presheafHom F G).obj (op X)) : ((presheafHom F G).map g.op α).app (op (Over.mk f)) = α.app (op (Over.mk h)) :=
by
subst w
rfl
