opCoproductIsoProduct'_inv_comp_inj

English

For each index b, the inverse of opCoproductIsoProduct' composed with the b-th opposite injection of c equals the b-th projection of f.

Русский

Для каждого индекса b обратное opCoproductIsoProduct' после b-й противоположной инъекции кокона равняется b-й проекции f.

LaTeX

$$$(\mathrm{opCoproductIsoProduct}'(hc, hf))^{-1} \circ (c_{\mathrm{inj}}(b))^{\mathrm{op}} = f_{\mathrm{proj}}(b)$$$

Lean4

theorem opCoproductIsoProduct'_inv_comp_inj {c : Cofan Z} {f : Fan (op <| Z ·)} (hc : IsColimit c) (hf : IsLimit f)
    (b : α) : (opCoproductIsoProduct' hc hf).inv ≫ (c.inj b).op = f.proj b :=
  IsLimit.conePointUniqueUpToIso_inv_comp (Cofan.IsColimit.op hc) hf ⟨b⟩

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