English
If C is adhesive and has pullbacks and pushouts, then the functor category D ⥤ C is adhesive.
Русский
Если C адгезивна и в ней существуют ограниченные/универсальные объекты, то категория функторов D ⥤ C также адгезивна.
LaTeX
$$$\operatorname{Adhesive}(D \to C)$$$
Lean4
instance adhesive_functor [Adhesive C] [HasPullbacks C] [HasPushouts C] : Adhesive (D ⥤ C) :=
by
constructor
intro W X Y Z f g h i hf H
rw [IsPushout.isVanKampen_iff]
apply isVanKampenColimit_of_evaluation
intro x
refine (IsVanKampenColimit.precompose_isIso_iff (diagramIsoSpan _).inv).mp ?_
refine IsVanKampenColimit.of_iso ?_ (PushoutCocone.isoMk _).symm
refine (IsPushout.isVanKampen_iff (H.map ((evaluation _ _).obj x))).mp ?_
apply Adhesive.van_kampen
