ι_comp_coproductIsoCofanPt — Mathlib

English

For each i in 𝒜, the i-th coproduct injection composed with the canonical iso coproductIsoCofanPt gives exactly the cofan injection at i. This expresses compatibility of the coproduct iso with the cofan injections.

Русский

Для каждого i из 𝒜 композиция инъекции i-го копроизведения с каноническим изоморфизмом coproductIsoCofanPt равна инъекции кофана i.

LaTeX

$$$\\Sigma.\\iota f i \\;\\gg\\; (coproductIsoCofanPt \\ 𝒜 f).hom = (cofan 𝒜 f).inj i$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_comp_coproductIsoCofanPt (i) : Sigma.ι f i ≫ (coproductIsoCofanPt 𝒜 f).hom = (cofan 𝒜 f).inj i :=
  colimit.isoColimitCocone_ι_hom _ _

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