proj_comp_opProductIsoCoproduct'_hom

English

For each i, the i-th projection of f, when composed with the opProductIsoCoproduct' hom, equals the corresponding element of the cocone.

Русский

Для каждого i проекция f, композицию с opProductIsoCoproduct' hom упорядочивает соответствующий элемент кокона.

LaTeX

$$$(f.proj i)^{op} \circ (opProductIsoCoproduct' hf hc).hom = c.inj i$$$

Lean4

theorem proj_comp_opProductIsoCoproduct'_hom {f : Fan Z} {c : Cofan (op <| Z ·)} (hf : IsLimit f) (hc : IsColimit c)
    (b : α) : (f.proj b).op ≫ (opProductIsoCoproduct' hf hc).hom = c.inj b :=
  IsColimit.comp_coconePointUniqueUpToIso_hom (Fan.IsLimit.op hf) hc ⟨b⟩

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