English
The composite of opProductIsoCoproduct' with its inverse for two colimits equals the opposite of the cocone-point-unique iso between hc and hc'.
Русский
Составление opProductIsoCoproduct' с его обратной для двух колимит дает противоположность единообразного изоморфизма точек коконов между hc и hc'.
LaTeX
$$$(opProductIsoCoproduct' hf hc).hom \circ (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv$$
Lean4
theorem opProductIsoCoproduct'_comp_self {f f' : Fan Z} {c : Cofan (op <| Z ·)} (hf : IsLimit f) (hf' : IsLimit f')
(hc : IsColimit c) :
(opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv :=
by
apply Quiver.Hom.unop_inj
apply hf.hom_ext
intro ⟨j⟩
change _ ≫ f.proj _ = _
simp only [unop_op, unop_comp, Category.assoc, Discrete.functor_obj, Iso.op_inv, Quiver.Hom.unop_op,
IsLimit.conePointUniqueUpToIso_inv_comp]
apply Quiver.Hom.op_inj
simp only [op_comp, op_unop, Quiver.Hom.op_unop, proj_comp_opProductIsoCoproduct'_hom]
rw [← proj_comp_opProductIsoCoproduct'_hom hf' hc]
simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id]
rfl
