English
The composition of opCoproductIsoProduct' hc hf with its inverse for c' matches the cocone-point-unique iso between hc and hc'.op, inverted.
Русский
Составление opCoproductIsoProduct' hc hf с его обратным отображает единообразие конусного указателя hc и hc'.op, в инверсии.
LaTeX
$$$(\mathrm{opCoproductIsoProduct}'(hc, hf))^{\mathrm{hom}} \circ (\mathrm{opCoproductIsoProduct}'(hc', hf))^{-1} = (hc.coconePointUniqueUpToIso hc').\mathrm{op}.\mathrm{inv}$$$
Lean4
theorem opCoproductIsoProduct'_comp_self {c c' : Cofan Z} {f : Fan (op <| Z ·)} (hc : IsColimit c) (hc' : IsColimit c')
(hf : IsLimit f) :
(opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv =
(hc.coconePointUniqueUpToIso hc').op.inv :=
by
apply Quiver.Hom.unop_inj
apply hc'.hom_ext
intro ⟨j⟩
change c'.inj _ ≫ _ = _
simp only [unop_op, unop_comp, Discrete.functor_obj, const_obj_obj, Iso.op_inv, Quiver.Hom.unop_op,
IsColimit.comp_coconePointUniqueUpToIso_inv]
apply Quiver.Hom.op_inj
simp only [op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc, opCoproductIsoProduct'_inv_comp_inj]
rw [← opCoproductIsoProduct'_inv_comp_inj hc hf]
simp only [Iso.hom_inv_id_assoc]
rfl
