ι_coprodIsoDirectSum_hom — Mathlib

English

Each injection Sigma.ι Z i followed by coprodIsoDirectSum.hom equals the direct sum inclusion lof.

Русский

Каждое вложение Sigma.ι Z_i после coprodIsoDirectSum.hom даёт прямую сумму инъекцию lof.

LaTeX

$$$ Sigma.ι Z i \; \; \; ≫ (coprodIsoDirectSum Z).hom = ofHom(DirectSum.lof R ι (fun i ↦ Z i) i) $$$

Lean4

@[simp, elementwise]
theorem ι_coprodIsoDirectSum_hom (i : ι) :
    Sigma.ι Z i ≫ (coprodIsoDirectSum Z).hom = ofHom (DirectSum.lof R ι (fun i ↦ Z i) i) :=
  colimit.isoColimitCocone_ι_hom _ _

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