ι_isoColimit_hom — Mathlib

English

For each j, the inclusion ι_j composed with the iso from Sigma to Colimit corresponds to the canonical colimit injection.

Русский

Для каждого j вложение ι_j композиция с изоморфизмом между Sigma и Colimit соответствует каноническому внедрению в копроизведение.

LaTeX

$$$\\text{ι}_{(\\dots)} \\circ (\\Sigma.\\text{isoColimit})_{\\text{hom}} = \\text{colimit.ι}$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_isoColimit_hom (j : α) : Sigma.ι _ j ≫ (Sigma.isoColimit X).hom = colimit.ι _ (Discrete.mk j) :=
  IsColimit.comp_coconePointUniqueUpToIso_hom (coproductIsCoproduct' X) _ _

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