English
Let Z be a family of objects in a category, and let c be a colimit cocone on Z, with f a limit cone on the opposite of Z. Then the canonical isomorphism between op of the cocone and the cocone, when composed with the f-projection at position i, equals the opposite of the i-th injection of c.
Русский
Пусть Z — семейство объектов в некоторой категории, c — колимитный кокон над Z, а f — предел-коник на противоположном отношении Z. Тогда каноническое изоморфизм между противоположностью кокона и коконом, по композиции с проекцией f в позиции i, совпадает с противоположностью i-й инъекции кокона c.
LaTeX
$$$\big(\mathrm{opCoproductIsoProduct}'(hc, hf)\big)^{\mathrm{hom}} \circ f_{\mathrm{proj}}(i) = \big( c_{\mathrm{inj}}(i) \big)^{\mathrm{op}}$$$
Lean4
@[reassoc (attr := simp)]
theorem opCoproductIsoProduct'_hom_comp_proj {c : Cofan Z} {f : Fan (op <| Z ·)} (hc : IsColimit c) (hf : IsLimit f)
(i : α) : (opCoproductIsoProduct' hc hf).hom ≫ f.proj i = (c.inj i).op := by simp [opCoproductIsoProduct', Fan.proj]
