English
The amalgamation criterion for presheafHom is stated with the same shape as for a generic presheaf, specialized to the presheafHom case.
Русский
Критерий amalgamation для presheafHom имеет ту же форму, что и для общего presheaf, специализированного к случаю presheafHom.
LaTeX
$$x.IsAmalgamation(y) \iff \forall Y,g,hg: y(app(Over.mk g)) = (x g hg).app(Over.mk(id_Y))$$
Lean4
/-- The sections of the presheaf `presheafHom F G` identify to morphisms `F ⟶ G`. -/
def presheafHomSectionsEquiv : (presheafHom F G).sections ≃ (F ⟶ G)
where
toFun
s :=
{ app := fun X => (s.1 X).app ⟨Over.mk (𝟙 _)⟩
naturality := by
rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f : X₂ ⟶ X₁⟩
dsimp
refine Eq.trans ?_ ((s.1 ⟨X₁⟩).naturality (Over.homMk f : Over.mk f ⟶ Over.mk (𝟙 X₁)).op)
rw [← s.2 f.op, presheafHom_map_app_op_mk_id]
rfl }
invFun f := ⟨fun _ => Functor.whiskerLeft _ f, fun _ => rfl⟩
left_inv
s := by
dsimp
ext ⟨X⟩ ⟨Y : Over X⟩
have H := s.2 Y.hom.op
dsimp at H ⊢
rw [← H]
apply presheafHom_map_app_op_mk_id
