English
For a fixed F, Y, e, and a suitable p, the cofan built from the right unitor of the bifunctor is a colimit; moreover, the structure maps form the universal cocone with the left and right maps commuting appropriately.
Русский
Для заданного F, Y, e и подходящего p конус в правом униторе бифунктора является колимитным конусом; отображения образуют универcальный кокон с нужной совместимостью левых и правых отображений.
LaTeX
$$$\operatorname{IsColimit}(mapBifunctorRightUnitorCofan F Y e p hp X j)$$$
Lean4
/-- The cofan `mapBifunctorRightUnitorCofan F Y e p hp X j` is a colimit. -/
noncomputable def mapBifunctorRightUnitorCofanIsColimit (j : J) :
IsColimit (mapBifunctorRightUnitorCofan F Y e p hp X j) :=
mkCofanColimit _
(fun s => e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso (0 : I) Y).inv ≫ s.inj ⟨⟨j, 0⟩, hp j⟩)
(fun s => by
rintro ⟨⟨j', i⟩, h⟩
by_cases hi : i = 0
· subst hi
simp only [Set.mem_preimage, hp, Set.mem_singleton_iff] at h
subst h
dsimp
rw [mapBifunctorRightUnitorCofan_inj, assoc, Iso.hom_inv_id_app_assoc, ← Functor.map_comp_assoc, Iso.hom_inv_id,
Functor.map_id, id_comp]
· apply IsInitial.hom_ext
exact mapBifunctorObjObjSingle₀IsInitial _ _ _ _ hi)
(fun s m hm => by
dsimp
rw [← hm ⟨⟨j, 0⟩, hp j⟩, mapBifunctorRightUnitorCofan_inj, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id,
Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc])
