English
If R is a diagram with colimit and left adjoint objects defined at each R.obj(j), then left adjoint object is defined for the colimit, i.e., F.leftAdjointObjIsDefined (colimit R).
Русский
Если R — диаграмма с колимитом и для каждого j функция F.leftAdjointObjIsDefined(R.obj(j)) верна, то левый элемент сопряжённости определён и для colimit R.
LaTeX
$$$\bigwedge_{j} F.leftAdjointObjIsDefined (R.obj j) \Rightarrow F.leftAdjointObjIsDefined (\mathrm{colimit}\;R)$$$
Lean4
/-- Auxiliary definition for `leftAdjointObjIsDefined_of_isColimit`. -/
noncomputable def corepresentableByCompCoyonedaObjOfIsColimit {J : Type*} [Category J]
{R : J ⥤ F.PartialLeftAdjointSource} {c : Cocone (R ⋙ ObjectProperty.ι _)} (hc : IsColimit c)
{c' : Cocone (R ⋙ F.partialLeftAdjoint)} (hc' : IsColimit c') : (F ⋙ coyoneda.obj (op c.pt)).CorepresentableBy c'.pt
where
homEquiv
{Y} :=
{ toFun := fun f ↦
hc.desc
(Cocone.mk _
{ app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f)
naturality := fun j j' φ ↦ by
dsimp
rw [comp_id, ← c'.w φ, ← partialLeftAdjointHomEquiv_map_comp, assoc]
dsimp })
invFun := fun g ↦
hc'.desc
(Cocone.mk _
{ app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g)
naturality := fun j j' φ ↦ by
apply F.partialLeftAdjointHomEquiv.injective
have := c.w φ
dsimp at this ⊢
rw [comp_id, Equiv.apply_symm_apply, partialLeftAdjointHomEquiv_map_comp, Equiv.apply_symm_apply,
reassoc_of% this] })
left_inv := fun f ↦ hc'.hom_ext (fun j ↦ by simp)
right_inv := fun g ↦ hc.hom_ext (fun j ↦ by simp) }
homEquiv_comp {Y Y'} g
f :=
hc.hom_ext
(fun j ↦ by
dsimp
simp only [IsColimit.fac, IsColimit.fac_assoc, partialLeftAdjointHomEquiv_comp, F.map_comp, assoc])
