English
For presheafHom, the same identity-lifting condition characterizes amalgamations across pullbacks.
Русский
Для presheafHom то же условие на подстановку в виде тяготения определяется через тяготение на обратных произведениях.
LaTeX
$$x.IsAmalgamation(y) \iff \forall Y,g,hg:\; y.app(Over.mk g) = (x g hg).app(Over.mk(id_Y))$$
Lean4
theorem isAmalgamation_iff {X : C} (S : Sieve X) (x : Presieve.FamilyOfElements (presheafHom F G) S.arrows)
(hx : x.Compatible) (y : (presheafHom F G).obj (op X)) :
x.IsAmalgamation y ↔ ∀ (Y : C) (g : Y ⟶ X) (hg : S g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y))) :=
by
constructor
· intro h Y g hg
rw [← h g hg, presheafHom_map_app_op_mk_id]
· intro h Y g hg
dsimp
ext ⟨W : Over Y⟩
refine (h W.left (W.hom ≫ g) (S.downward_closed hg _)).trans ?_
have H := hx (𝟙 _) W.hom (S.downward_closed hg W.hom) hg (by simp)
dsimp at H
simp only [FunctorToTypes.map_id_apply] at H
rw [H, presheafHom_map_app_op_mk_id]
rfl
