English
The inverse of the Coyoneda-Op Colimit iso satisfies a π-component identity with colimit injections: (coyonedaOpColimitIsoLimitCoyoneda').inv ≫ coyoneda.map (colimit.ι F ⟨i⟩).op = limit.π (F.rightOp ⋙ coyoneda) i.
Русский
Обратный к изоморфизму Coyoneda-OpColimit удовлетворяет тождеству π-компоненты с инъекциями колимита: (coyonedaOpColimitIsoLimitCoyoneda').inv ≫ coyoneda.map (colimit.ι F ⟨i⟩).op = limit.π (F.rightOp ⋙ coyoneda) i.
LaTeX
$$$\bigl(coyonedaOpColimitIsoLimitCoyoneda'\; F\bigr)^{\,-1} \;\circ\; (coyoneda.map (colimit.ι F \langle i \rangle).op) = \operatorname{limit.\,π}(F.rightOp \circ coyoneda) i$$$
Lean4
@[reassoc (attr := simp)]
theorem coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π (i : I) :
(coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i = coyoneda.map (colimit.ι F ⟨i⟩).op :=
by
simp only [coyonedaOpColimitIsoLimitCoyoneda', Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv,
Category.assoc, preservesLimitIso_hom_π, ← Functor.map_comp, limitRightOpIsoOpColimit_inv_comp_π]
