English
The Yoneda variant of the limit-π identities gives a π-map equality for the op-wards constructions: colimitYonedaHomIsoLimitOp_π_apply.
Русский
Версия для Yoneda пределов дает тождество π для операций, строящихся с помощью обратной операции: colimitYonedaHomIsoLimitOp_π_apply.
LaTeX
$$$\text{colimitYonedaHomIsoLimitOp}_\pi\_\text{apply}$$$
Lean4
@[simp]
theorem colimitYonedaHomIsoLimit'_π_apply (f : colimit (D.leftOp ⋙ yoneda) ⟶ F) (i : I) :
limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i ((colimitYonedaHomIsoLimit' D F).hom f) =
⟨f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i) (𝟙 (D.obj i).unop))⟩ :=
by
change ((colimitYonedaHomIsoLimit' D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _
simp only [colimitYonedaHomIsoLimit', Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]
rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]
dsimp [yonedaLemma]
rfl
