desc_op_comp_opCoproductIsoProduct'_hom

English

If c' is any cocone on Z, the op of its description composed with opCoproductIsoProduct' hf hc gives hf.lift c'.op.

Русский

Если c' — любой кокон над Z, то преобразование_desc c'.op после.opCoproductIsoProduct' hf hc совпадает с hf.lift c'.op.

LaTeX

$$$(hc.desc c').op \circ (\mathrm{opCoproductIsoProduct}'(hc, hf).hom) = hf.lift(c'.op)$$$

Lean4

theorem desc_op_comp_opCoproductIsoProduct'_hom {c : Cofan Z} {f : Fan (op <| Z ·)} (hc : IsColimit c) (hf : IsLimit f)
    (c' : Cofan Z) : (hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op :=
  by
  refine (Iso.eq_comp_inv _).mp (Quiver.Hom.unop_inj (hc.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))
  simp only [unop_op, Discrete.functor_obj, const_obj_obj, Quiver.Hom.unop_op, IsColimit.fac, Cofan.op, unop_comp,
    op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc]
  erw [opCoproductIsoProduct'_inv_comp_inj, IsLimit.fac]
  rfl

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