limitIsoOfIsRightKanExtension_hom_π

English

The hom component of the right extension isomorphism satisfies a compatibility with the limit projections: (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i.

Русский

Компонент гомоморфизма изоморфности правого расширения совместим с проекциями предела: (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i.

LaTeX

$$$(F'.limitIsoOfIsRightKanExtension\\ α).hom \\;\\circ\\; \\text{limit.π}_F i = \\text{limit.π}_{F'}(L.obj i) \\circ α.app i$$$

Lean4

@[reassoc (attr := simp)]
theorem limitIsoOfIsRightKanExtension_hom_π (i : C) :
    (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i := by
  rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]

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