finiteSubcoproductsCocone_ι_app_eq_sum

English

A finite subcoproduct cocone evaluated at a Finset S gives a sum of projections composed with injections; a standard finset identity.

Русский

Для конечного подкопродукта кокон-индексирование по финсету S даёт сумму проекций, композированных с инъекциями.

LaTeX

$$$(finiteSubcoproductsCocone f).\ι.app S = \sum a \in S.attach, Σ.a.π ≫ Σ.a$$

Lean4

theorem finiteSubcoproductsCocone_ι_app_eq_sum {α : Type w} [DecidableEq α] (f : α → C) [HasCoproduct f]
    (S : Finset (Discrete α)) :
    (finiteSubcoproductsCocone f).ι.app S = ∑ a ∈ S.attach, Sigma.π _ a ≫ Sigma.ι _ a.1.as :=
  by
  dsimp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt, Functor.const_obj_obj,
    finiteSubcoproductsCocone_ι_app]
  ext v
  simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, Preadditive.comp_sum]
  rw [Finset.sum_eq_single v]
  · simp
  · intro b hb hb₁
    rw [Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁), zero_comp]
  · simp

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