finiteSubproductsCocone_π_app_eq_sum

English

A finite subproduct cocone projection π app evaluated on S equals the sum of projections onto components.

Русский

Проекция π, примененная к конечному подпроизведению, равна сумме проекций на компоненты.

LaTeX

$$$(finiteSubproductsCone f).\pi.app S = \sum a \in S.unop.attach, \Pi.π f a.1.as ≫ \Pi.ι (fun a => f a.1.as) a$$$

Lean4

theorem finiteSubproductsCocone_π_app_eq_sum {α : Type w} [DecidableEq α] (f : α → C) [HasProduct f]
    (S : (Finset (Discrete α))ᵒᵖ) :
    (finiteSubproductsCone f).π.app S = ∑ a ∈ S.unop.attach, Pi.π f a.1.as ≫ Pi.ι (fun a => f a.1.as) a :=
  by
  dsimp only [finiteSubproductsCone_pt, Functor.const_obj_obj, liftToFinsetObj_obj, Discrete.functor_obj_eq_as,
    finiteSubproductsCone_π_app]
  ext v
  simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Preadditive.sum_comp, Category.assoc]
  rw [Finset.sum_eq_single v]
  · simp
  · intro b hb hb₁
    rw [Pi.ι_π_of_ne _ hb₁, comp_zero]
  · simp

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