sumAddHom_comm — Mathlib

English

A commutativity relation: sumAddHom with a nested sum can be rearranged; the double sum equals the other order of summation with a flip.

Русский

Коммутативное свойство: сумма двойная перестраивается, меняется порядок суммирования с соответствующим перекрёстным пересчетом.

LaTeX

$$$ \\text{sumAddHom} (\\lambda i_2, \\text{sumAddHom}(\\lambda i_1, h(i_1,i_2)) f_1) \\, f_2 = \\text{sumAddHom} (\\lambda i_1, \\text{sumAddHom}(\\lambda i_2, (h(i_1,i_2)).\\text{flip}) f_2) f_1. $$$

Lean4

theorem sumAddHom_comm {ι₁ ι₂ : Sort _} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} {γ : Type*} [DecidableEq ι₁]
    [DecidableEq ι₂] [∀ i, AddZeroClass (β₁ i)] [∀ i, AddZeroClass (β₂ i)] [AddCommMonoid γ] (f₁ : Π₀ i, β₁ i)
    (f₂ : Π₀ i, β₂ i) (h : ∀ i j, β₁ i →+ β₂ j →+ γ) :
    sumAddHom (fun i₂ => sumAddHom (fun i₁ => h i₁ i₂) f₁) f₂ =
      sumAddHom (fun i₁ => sumAddHom (fun i₂ => (h i₁ i₂).flip) f₂) f₁ :=
  by
  obtain ⟨⟨f₁, s₁, h₁⟩, ⟨f₂, s₂, h₂⟩⟩ := f₁, f₂
  simpa [sumAddHom, sumZeroHom, AddMonoidHom.finset_sum_apply, AddMonoidHom.coe_mk, AddMonoidHom.flip_apply, Trunc.lift,
    toFun_eq_coe, ZeroHom.coe_mk, coe_mk'] using Finset.sum_comm

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