coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π

English

The inverse of the iso Coyoneda-OpColimit satisfies the π-identity: (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'_inv_comp_π (i : I) :
    (coyonedaOpColimitIsoLimitCoyoneda' F).inv ≫ coyoneda.map (colimit.ι F ⟨i⟩).op = limit.π (F.rightOp ⋙ coyoneda) i :=
  by rw [← coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, ← Category.assoc, Iso.inv_hom_id, Category.id_comp]

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