colimitHomIsoLimitYoneda_inv_comp_π

English

The limit functor lim: [J → C] → C has a right adjoint given by the constant diagram functor Δ; i.e., lim is a left adjoint to Δ in the presence of HasLimitsOfShape J C.

Русский

Функтор предела lim: [J → C] → C имеет правого адъюнкта, заданного константной диаграммой Δ; то есть lim является левым адъунктом к Δ при существовании пределов формы J в C.

LaTeX

$$$\operatorname{HasLimitsOfShape}(J, C) \Rightarrow \lim \dashv \Delta$$$

Lean4

@[reassoc (attr := simp)]
theorem colimitHomIsoLimitYoneda_inv_comp_π [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) :
    (colimitHomIsoLimitYoneda F A).inv ≫ (coyoneda.map (colimit.ι F i).op).app A = limit.π (F.op ⋙ yoneda.obj A) ⟨i⟩ :=
  by rw [← colimitHomIsoLimitYoneda_hom_comp_π, ← Category.assoc, Iso.inv_hom_id, Category.id_comp]

Похожие утверждения