lof_coprodIsoDirectSum_inv — Mathlib

English

The inverse of the coproduct injection composed with coprodIsoDirectSum equals the directSum lof injection.

Русский

Обратный образ инъекции coproduct, композиция с coprodIsoDirectSum, равен инъекции DirectSum lof.

LaTeX

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

Lean4

@[simp, elementwise]
theorem lof_coprodIsoDirectSum_inv (i : ι) :
    ofHom (DirectSum.lof R ι (fun i ↦ Z i) i) ≫ (coprodIsoDirectSum Z).inv = Sigma.ι Z i :=
  (coproductCoconeIsColimit Z).comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) _

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