Mathlib.Data.DFinsupp.BigOperators

Module docstring

{"# Dependent functions with finite support

For a non-dependent version see Mathlib.Data.Finsupp.Defs.

Notation

This file introduces the notation Π₀ a, β a as notation for DFinsupp β, mirroring the α →₀ β notation used for Finsupp. This works for nested binders too, with Π₀ a b, γ a b as notation for DFinsupp (fun a ↦ DFinsupp (γ a)).

Implementation notes

The support is internally represented (in the primed DFinsupp.support') as a Multiset that represents a superset of the true support of the function, quotiented by the always-true relation so that this does not impact equality. This approach has computational benefits over storing a Finset; it allows us to add together two finitely-supported functions without having to evaluate the resulting function to recompute its support (which would required decidability of b = 0 for b : β i).

The true support of the function can still be recovered with DFinsupp.support; but these decidability obligations are now postponed to when the support is actually needed. As a consequence, there are two ways to sum a DFinsupp: with DFinsupp.sum which works over an arbitrary function but requires recomputation of the support and therefore a Decidable argument; and with DFinsupp.sumAddHom which requires an additive morphism, using its properties to show that summing over a superset of the support is sufficient.

Finsupp takes an altogether different approach here; it uses Classical.Decidable and declares the Add instance as noncomputable. This design difference is independent of the fact that DFinsupp is dependently-typed and Finsupp is not; in future, we may want to align these two definitions, or introduce two more definitions for the other combinations of decisions. ","### Product and sum lemmas for bundled morphisms.

In this section, we provide analogues of AddMonoidHom.map_sum, AddMonoidHom.coe_finset_sum, and AddMonoidHom.finset_sum_apply for DFinsupp.sum and DFinsupp.sumAddHom instead of Finset.sum.

We provide these for AddMonoidHom, MonoidHom, RingHom, AddEquiv, and MulEquiv.

Lemmas for LinearMap and LinearEquiv are in another file. ","The above lemmas, repeated for DFinsupp.sumAddHom. "}

DFinsupp.evalAddMonoidHom definition

[∀ i, AddZeroClass (β i)] (i : ι) : (Π₀ i, β i) →+ β i

Full source

/-- Evaluation at a point is an `AddMonoidHom`. This is the finitely-supported version of
`Pi.evalAddMonoidHom`. -/
def evalAddMonoidHom [∀ i, AddZeroClass (β i)] (i : ι) : (Π₀ i, β i) →+ β i :=
  (Pi.evalAddMonoidHom β i).comp coeFnAddMonoidHom

Evaluation homomorphism for finitely supported dependent functions

Informal description

For each index $i$ in a family of types $\beta_i$ equipped with an additive zero class structure, the evaluation map at $i$ is an additive monoid homomorphism from the type of finitely supported dependent functions $\Pi_{i} \beta_i$ to $\beta_i$. This is the finitely supported version of the evaluation homomorphism for ordinary dependent functions.

DFinsupp.coe_finset_sum theorem

 {α} [∀ i, AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ i, β i) : ⇑(∑ a ∈ s, g a) = ∑ a ∈ s, ⇑(g a)

Full source

@[simp, norm_cast]
theorem coe_finset_sum {α} [∀ i, AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ i, β i) :
    ⇑(∑ a ∈ s, g a) = ∑ a ∈ s, ⇑(g a) :=
  map_sum coeFnAddMonoidHom g s

Sum of Finitely Supported Dependent Functions Commutes with Evaluation

Informal description

Let $\beta_i$ be a family of additive commutative monoids indexed by $i \in \iota$. Given a finite set $s$ of elements of type $\alpha$ and a function $g \colon \alpha \to \Pi_{i} \beta_i$ (where $\Pi_{i} \beta_i$ denotes the type of finitely supported dependent functions), the underlying function of the sum of $g$ over $s$ is equal to the sum over $s$ of the underlying functions of $g$. In other words, \[ \left( \sum_{a \in s} g(a) \right) = \sum_{a \in s} g(a). \]

DFinsupp.finset_sum_apply theorem

 {α} [∀ i, AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ i, β i) (i : ι) : (∑ a ∈ s, g a) i = ∑ a ∈ s, g a i

Full source

@[simp]
theorem finset_sum_apply {α} [∀ i, AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ i, β i) (i : ι) :
    (∑ a ∈ s, g a) i = ∑ a ∈ s, g a i :=
  map_sum (evalAddMonoidHom i) g s

Evaluation of Finite Sum of Finitely Supported Dependent Functions

Informal description

Let $\beta_i$ be a family of types indexed by $i \in \iota$, each equipped with an additive commutative monoid structure. Given a finite set $s$ of elements of type $\alpha$ and a function $g \colon \alpha \to \Pi_{i} \beta_i$ (where $\Pi_{i} \beta_i$ denotes the type of finitely supported dependent functions), the evaluation at any index $i$ of the sum of $g$ over $s$ is equal to the sum over $s$ of the evaluations of $g$ at $i$. In other words, for any $i \in \iota$, \[ \left( \sum_{a \in s} g(a) \right)(i) = \sum_{a \in s} g(a)(i). \]

DFinsupp.prod definition

 [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] (f : Π₀ i, β i) (g : ∀ i, β i → γ) : γ

Full source

/-- `DFinsupp.prod f g` is the product of `g i (f i)` over the support of `f`. -/
@[to_additive "`sum f g` is the sum of `g i (f i)` over the support of `f`."]
def prod [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] (f : Π₀ i, β i)
    (g : ∀ i, β i → γ) : γ :=
  ∏ i ∈ f.support, g i (f i)

Product over support of a finitely supported dependent function

Informal description

Given a family of types $\beta_i$ indexed by $i \in \iota$ each with a zero element and a decidable equality on non-zero elements, and a commutative monoid $\gamma$, the product $\prod_{i \in \text{supp}(f)} g_i(f_i)$ is defined for a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of functions $g_i \colon \beta_i \to \gamma$. Here $\text{supp}(f)$ denotes the support of $f$, i.e., the set of indices where $f_i \neq 0$.

map_dfinsuppProd theorem

 {R S H : Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid R] [CommMonoid S] [FunLike H R S]
  [MonoidHomClass H R S] (h : H) (f : Π₀ i, β i) (g : ∀ i, β i → R) : h (f.prod g) = f.prod fun a b => h (g a b)

Full source

@[to_additive (attr := simp)]
theorem _root_.map_dfinsuppProd
    {R S H : Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [CommMonoid R] [CommMonoid S] [FunLike H R S] [MonoidHomClass H R S] (h : H) (f : Π₀ i, β i)
    (g : ∀ i, β i → R) : h (f.prod g) = f.prod fun a b => h (g a b) :=
  map_prod _ _ _

Monoid Homomorphism Preserves Product of Finitely Supported Dependent Function

Informal description

Let $R$, $S$, and $H$ be types, and let $\beta_i$ be a family of types indexed by $i \in \iota$, each with a zero element and a decidable condition for being non-zero. Suppose $R$ and $S$ are commutative monoids, and $H$ is a function-like type with a monoid homomorphism structure from $R$ to $S$. For any monoid homomorphism $h \colon H$, any finitely supported dependent function $f \colon \Pi_{i} \beta_i$, and any family of functions $g_i \colon \beta_i \to R$, we have \[ h \left( \prod_{i \in \text{supp}(f)} g_i(f_i) \right) = \prod_{i \in \text{supp}(f)} h(g_i(f_i)). \]

DFinsupp.prod_mapRange_index theorem

 {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [∀ i, Zero (β₁ i)] [∀ i, Zero (β₂ i)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)]
  [∀ (i) (x : β₂ i), Decidable (x ≠ 0)] [CommMonoid γ] {f : ∀ i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i}
  {h : ∀ i, β₂ i → γ} (h0 : ∀ i, h i 0 = 1) : (mapRange f hf g).prod h = g.prod fun i b => h i (f i b)

Full source

@[to_additive]
theorem prod_mapRange_index {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [∀ i, Zero (β₁ i)]
    [∀ i, Zero (β₂ i)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ (i) (x : β₂ i), Decidable (x ≠ 0)]
    [CommMonoid γ] {f : ∀ i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} {h : ∀ i, β₂ i → γ}
    (h0 : ∀ i, h i 0 = 1) : (mapRange f hf g).prod h = g.prod fun i b => h i (f i b) := by
  rw [mapRange_def]
  refine (Finset.prod_subset support_mk_subset ?_).trans ?_
  · intro i h1 h2
    simp only [mem_support_toFun, ne_eq] at h1
    simp only [Finset.coe_sort_coe, mem_support_toFun, mk_apply, ne_eq, h1, not_false_iff,
      dite_eq_ite, ite_true, not_not] at h2
    simp [h2, h0]
  · refine Finset.prod_congr rfl ?_
    intro i h1
    simp only [mem_support_toFun, ne_eq] at h1
    simp [h1]

Product Preservation under Component-wise Mapping of Finitely Supported Dependent Functions

Informal description

Let $\beta_1$ and $\beta_2$ be families of types indexed by $i \in \iota$, each with a zero element and a decidable condition for being non-zero. Let $\gamma$ be a commutative monoid. Given a family of functions $f_i \colon \beta_1 i \to \beta_2 i$ such that $f_i(0) = 0$ for all $i$, a finitely supported dependent function $g \colon \Pi_{i} \beta_1 i$, and a family of functions $h_i \colon \beta_2 i \to \gamma$ such that $h_i(0) = 1$ for all $i$, we have \[ \prod_{i \in \text{supp}(g)} h_i(f_i(g_i)) = \prod_{i \in \text{supp}(g)} (h_i \circ f_i)(g_i). \]

DFinsupp.prod_zero_index theorem

 [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {h : ∀ i, β i → γ} :
  (0 : Π₀ i, β i).prod h = 1

Full source

@[to_additive]
theorem prod_zero_index [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [CommMonoid γ] {h : ∀ i, β i → γ} : (0 : Π₀ i, β i).prod h = 1 :=
  rfl

Product over Support of Zero Function is One

Informal description

Let $\beta_i$ be a family of types indexed by $i \in \iota$, each with an additive commutative monoid structure and a decidable predicate for non-zero elements, and let $\gamma$ be a commutative monoid. For any family of functions $h_i \colon \beta_i \to \gamma$, the product over the support of the zero function $0 \colon \Pi_{i} \beta_i$ satisfies: \[ \prod_{i \in \text{supp}(0)} h_i(0_i) = 1. \]

DFinsupp.prod_single_index theorem

 [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {i : ι} {b : β i} {h : ∀ i, β i → γ}
  (h_zero : h i 0 = 1) : (single i b).prod h = h i b

Full source

@[to_additive]
theorem prod_single_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
    {i : ι} {b : β i} {h : ∀ i, β i → γ} (h_zero : h i 0 = 1) : (single i b).prod h = h i b := by
  by_cases h : b ≠ 0
  · simp [DFinsupp.prod, support_single_ne_zero h]
  · rw [not_not] at h
    simp [h, prod_zero_index, h_zero]
    rfl

Product of a Single-Entry Dependent Function Equals Its Value

Informal description

Let $\beta_i$ be a family of types indexed by $i \in \iota$, each with a zero element and a decidable predicate for non-zero elements, and let $\gamma$ be a commutative monoid. For a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ of the form $f = \text{single}_i b$ (where $\text{single}_i b$ is the function that is $b$ at index $i$ and zero elsewhere), and a family of functions $h \colon \forall i, \beta_i \to \gamma$ such that $h_i(0) = 1$, the product over the support of $f$ satisfies: \[ \prod_{j \in \text{supp}(f)} h_j(f_j) = h_i(b). \]

DFinsupp.prod_neg_index theorem

 [∀ i, AddGroup (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {g : Π₀ i, β i} {h : ∀ i, β i → γ}
  (h0 : ∀ i, h i 0 = 1) : (-g).prod h = g.prod fun i b => h i (-b)

Full source

@[to_additive]
theorem prod_neg_index [∀ i, AddGroup (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
    {g : Π₀ i, β i} {h : ∀ i, β i → γ} (h0 : ∀ i, h i 0 = 1) :
    (-g).prod h = g.prod fun i b => h i (-b) :=
  prod_mapRange_index h0

Product over Support of Negated Dependent Function Equals Product of Negated Components

Informal description

Let $\beta_i$ be a family of types indexed by $i \in \iota$, each with an additive group structure and a decidable predicate for non-zero elements, and let $\gamma$ be a commutative monoid. For any finitely supported dependent function $g \colon \Pi_{i} \beta_i$ and any family of functions $h \colon \forall i, \beta_i \to \gamma$ such that $h_i(0) = 1$ for all $i$, the product over the support of $-g$ satisfies: \[ \prod_{i \in \text{supp}(-g)} h_i((-g)_i) = \prod_{i \in \text{supp}(g)} h_i(-g_i). \]

DFinsupp.prod_comm theorem

 {ι₁ ι₂ : Sort _} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} [DecidableEq ι₁] [DecidableEq ι₂] [∀ i, Zero (β₁ i)]
  [∀ i, Zero (β₂ i)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ (i) (x : β₂ i), Decidable (x ≠ 0)] [CommMonoid γ]
  (f₁ : Π₀ i, β₁ i) (f₂ : Π₀ i, β₂ i) (h : ∀ i, β₁ i → ∀ i, β₂ i → γ) :
  (f₁.prod fun i₁ x₁ => f₂.prod fun i₂ x₂ => h i₁ x₁ i₂ x₂) = f₂.prod fun i₂ x₂ => f₁.prod fun i₁ x₁ => h i₁ x₁ i₂ x₂

Full source

@[to_additive]
theorem prod_comm {ι₁ ι₂ : Sort _} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} [DecidableEq ι₁]
    [DecidableEq ι₂] [∀ i, Zero (β₁ i)] [∀ i, Zero (β₂ i)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)]
    [∀ (i) (x : β₂ i), Decidable (x ≠ 0)] [CommMonoid γ] (f₁ : Π₀ i, β₁ i) (f₂ : Π₀ i, β₂ i)
    (h : ∀ i, β₁ i → ∀ i, β₂ i → γ) :
    (f₁.prod fun i₁ x₁ => f₂.prod fun i₂ x₂ => h i₁ x₁ i₂ x₂) =
      f₂.prod fun i₂ x₂ => f₁.prod fun i₁ x₁ => h i₁ x₁ i₂ x₂ :=
  Finset.prod_comm

Commutativity of Double Product over Finitely Supported Dependent Functions

Informal description

Let $\iota_1$ and $\iota_2$ be types with decidable equality, and let $\beta_1 \colon \iota_1 \to \Type$ and $\beta_2 \colon \iota_2 \to \Type$ be families of types each equipped with a zero element and a decidable predicate for non-zero elements. Let $\gamma$ be a commutative monoid. Given two finitely supported dependent functions $f_1 \colon \Pi_{i_1} \beta_1(i_1)$ and $f_2 \colon \Pi_{i_2} \beta_2(i_2)$, and a family of functions $h \colon \forall i_1, \beta_1(i_1) \to \forall i_2, \beta_2(i_2) \to \gamma$, the following equality holds: \[ \prod_{i_1 \in \text{supp}(f_1)} \left( \prod_{i_2 \in \text{supp}(f_2)} h(i_1, f_1(i_1), i_2, f_2(i_2)) \right) = \prod_{i_2 \in \text{supp}(f_2)} \left( \prod_{i_1 \in \text{supp}(f_1)} h(i_1, f_1(i_1), i_2, f_2(i_2)) \right). \]

DFinsupp.sum_apply theorem

 {ι} {β : ι → Type v} {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
  [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)] {f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i}
  {i₂ : ι} : (f.sum g) i₂ = f.sum fun i₁ b => g i₁ b i₂

Full source

@[simp]
theorem sum_apply {ι} {β : ι → Type v} {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁}
    [∀ i₁, Zero (β₁ i₁)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)]
    {f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} {i₂ : ι} :
    (f.sum g) i₂ = f.sum fun i₁ b => g i₁ b i₂ :=
  map_sum (evalAddMonoidHom i₂) _ f.support

Evaluation of Sum of Finitely Supported Dependent Functions

Informal description

Let $\iota$ and $\iota_1$ be types with $\iota_1$ having decidable equality. Let $\beta \colon \iota \to \Type$ and $\beta_1 \colon \iota_1 \to \Type$ be families of types where each $\beta_1(i_1)$ has a zero element and a decidable predicate for non-zero elements, and each $\beta(i)$ is an additive commutative monoid. Given a finitely supported dependent function $f \colon \Pi_{i_1} \beta_1(i_1)$ and a family of functions $g \colon \forall i_1, \beta_1(i_1) \to \Pi_{i} \beta(i)$, the evaluation of the sum $\sum_{i_1} g(i_1, f(i_1))$ at any index $i_2 \in \iota$ is equal to the sum $\sum_{i_1} (g(i_1, f(i_1)))(i_2)$. In symbols: \[ \left(\sum_{i_1} g(i_1, f(i_1))\right)(i_2) = \sum_{i_1} \left(g(i_1, f(i_1))(i_2)\right). \]

DFinsupp.support_sum theorem

 {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)]
  [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} :
  (f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support

Full source

theorem support_sum {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
    [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)]
    [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i₁, β₁ i₁} {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} :
    (f.sum g).support ⊆ f.support.biUnion fun i => (g i (f i)).support := by
  have :
    ∀ i₁ : ι,
      (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
    fun i₁ h =>
    let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨i, mem_support_iff.1 hi, Ne⟩
  simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this

Support of Sum of Finitely Supported Dependent Functions is Contained in Union of Supports

Informal description

Let $\iota_1$ be a type with decidable equality, and let $\beta_1 \colon \iota_1 \to \Type$ be a family of types where each $\beta_1(i_1)$ has a zero element and a decidable predicate for non-zero elements. Let $\beta$ be another family of types where each $\beta(i)$ is an additive commutative monoid with decidable equality on non-zero elements. Given a finitely supported dependent function $f \colon \Pi_{i_1} \beta_1(i_1)$ and a family of functions $g \colon \forall i_1, \beta_1(i_1) \to \Pi_{i} \beta(i)$, the support of the sum $\sum_{i_1} g(i_1, f(i_1))$ is contained in the union over the support of $f$ of the supports of $g(i_1, f(i_1))$. In symbols: \[ \text{supp}\left(\sum_{i_1} g(i_1, f(i_1))\right) \subseteq \bigcup_{i_1 \in \text{supp}(f)} \text{supp}(g(i_1, f(i_1))). \]

DFinsupp.prod_one theorem

 [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i, β i} :
  (f.prod fun _ _ => (1 : γ)) = 1

Full source

@[to_additive (attr := simp)]
theorem prod_one [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
    {f : Π₀ i, β i} : (f.prod fun _ _ => (1 : γ)) = 1 :=
  Finset.prod_const_one

Product of Ones over Support Equals One

Informal description

DFinsupp.prod_mul theorem

 [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i, β i} {h₁ h₂ : ∀ i, β i → γ} :
  (f.prod fun i b => h₁ i b * h₂ i b) = f.prod h₁ * f.prod h₂

Full source

@[to_additive (attr := simp)]
theorem prod_mul [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
    {f : Π₀ i, β i} {h₁ h₂ : ∀ i, β i → γ} :
    (f.prod fun i b => h₁ i b * h₂ i b) = f.prod h₁ * f.prod h₂ :=
  Finset.prod_mul_distrib

Product Splitting for Finitely Supported Dependent Functions

Informal description

Let $\{β_i\}_{i \in \iota}$ be a family of additively commutative monoids, each with a zero element and decidable equality on non-zero elements, and let $\gamma$ be a commutative monoid. For any finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and two families of functions $h_1, h_2 \colon \beta_i \to \gamma$, the product $\prod_{i \in \text{supp}(f)} (h_1(i, f_i) \cdot h_2(i, f_i))$ equals the product of the individual products $\left(\prod_{i \in \text{supp}(f)} h_1(i, f_i)\right) \cdot \left(\prod_{i \in \text{supp}(f)} h_2(i, f_i)\right)$.

DFinsupp.prod_inv theorem

 [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [DivisionCommMonoid γ] {f : Π₀ i, β i}
  {h : ∀ i, β i → γ} : (f.prod fun i b => (h i b)⁻¹) = (f.prod h)⁻¹

Full source

@[to_additive (attr := simp)]
theorem prod_inv [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [DivisionCommMonoid γ] {f : Π₀ i, β i} {h : ∀ i, β i → γ} :
    (f.prod fun i b => (h i b)⁻¹) = (f.prod h)⁻¹ :=
  (map_prod (invMonoidHom : γ →* γ) _ f.support).symm

Inverse of Product Equals Product of Inverses for Finitely Supported Dependent Functions

Informal description

Let $\{β_i\}_{i \in \iota}$ be a family of additively commutative monoids, each with a zero element and decidable equality on non-zero elements, and let $\gamma$ be a division commutative monoid. For any finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of functions $h_i \colon \beta_i \to \gamma$, the product of the inverses $\prod_{i \in \text{supp}(f)} (h_i(f_i))^{-1}$ is equal to the inverse of the product $(\prod_{i \in \text{supp}(f)} h_i(f_i))^{-1}$.

DFinsupp.prod_eq_one theorem

 [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i, β i} {h : ∀ i, β i → γ}
  (hyp : ∀ i, h i (f i) = 1) : f.prod h = 1

Full source

@[to_additive]
theorem prod_eq_one [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
    {f : Π₀ i, β i} {h : ∀ i, β i → γ} (hyp : ∀ i, h i (f i) = 1) : f.prod h = 1 :=
  Finset.prod_eq_one fun i _ => hyp i

Product of Trivial Factors Equals One for Finitely Supported Dependent Functions

Informal description

Let $\{\beta_i\}_{i \in \iota}$ be a family of types each with a zero element and decidable equality on non-zero elements, and let $\gamma$ be a commutative monoid. Given a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of functions $h_i \colon \beta_i \to \gamma$ such that $h_i(f_i) = 1$ for all $i$, then the product $\prod_{i \in \text{supp}(f)} h_i(f_i)$ equals $1$.

DFinsupp.smul_sum theorem

 {α : Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommMonoid γ] [DistribSMul α γ] {f : Π₀ i, β i}
  {h : ∀ i, β i → γ} {c : α} : c • f.sum h = f.sum fun a b => c • h a b

Full source

theorem smul_sum {α : Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [AddCommMonoid γ] [DistribSMul α γ] {f : Π₀ i, β i} {h : ∀ i, β i → γ} {c : α} :
    c • f.sum h = f.sum fun a b => c • h a b :=
  Finset.smul_sum

Distributivity of Scalar Multiplication over Sum for Finitely Supported Dependent Functions

Informal description

Let $\alpha$ be a type, $\{\beta_i\}_{i \in \iota}$ a family of types each with a zero element and decidable equality on non-zero elements, and $\gamma$ an additively commutative monoid with a distributive scalar multiplication by $\alpha$. For any finitely supported dependent function $f \colon \Pi_{i} \beta_i$, a family of functions $h_i \colon \beta_i \to \gamma$, and a scalar $c \in \alpha$, we have: \[ c \cdot \left(\sum_{i \in \text{supp}(f)} h_i(f_i)\right) = \sum_{i \in \text{supp}(f)} c \cdot h_i(f_i). \]

DFinsupp.prod_add_index theorem

 [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f g : Π₀ i, β i} {h : ∀ i, β i → γ}
  (h_zero : ∀ i, h i 0 = 1) (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) : (f + g).prod h = f.prod h * g.prod h

Full source

@[to_additive]
theorem prod_add_index [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [CommMonoid γ] {f g : Π₀ i, β i} {h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1)
    (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) : (f + g).prod h = f.prod h * g.prod h :=
  have f_eq : (∏ i ∈ f.support ∪ g.support, h i (f i)) = f.prod h :=
    (Finset.prod_subset Finset.subset_union_left <| by
        simp +contextual [mem_support_iff, h_zero]).symm
  have g_eq : (∏ i ∈ f.support ∪ g.support, h i (g i)) = g.prod h :=
    (Finset.prod_subset Finset.subset_union_right <| by
        simp +contextual [mem_support_iff, h_zero]).symm
  calc
    (∏ i ∈ (f + g).support, h i ((f + g) i)) = ∏ i ∈ f.support ∪ g.support, h i ((f + g) i) :=
      Finset.prod_subset support_add <| by
        simp +contextual [mem_support_iff, h_zero]
    _ = (∏ i ∈ f.support ∪ g.support, h i (f i)) * ∏ i ∈ f.support ∪ g.support, h i (g i) := by
      { simp [h_add, Finset.prod_mul_distrib] }
    _ = _ := by rw [f_eq, g_eq]

Product over Support Preserves Addition for Finitely Supported Dependent Functions

Informal description

Let $\{\beta_i\}_{i \in \iota}$ be a family of additively commutative monoids, $\gamma$ a commutative monoid, and $f, g \colon \Pi_{i} \beta_i$ finitely supported dependent functions. For a family of functions $h_i \colon \beta_i \to \gamma$ satisfying $h_i(0) = 1$ and $h_i(b_1 + b_2) = h_i(b_1) \cdot h_i(b_2)$ for all $i \in \iota$ and $b_1, b_2 \in \beta_i$, we have: \[ \prod_{i \in \text{supp}(f + g)} h_i((f + g)_i) = \left(\prod_{i \in \text{supp}(f)} h_i(f_i)\right) \cdot \left(\prod_{i \in \text{supp}(g)} h_i(g_i)\right). \]

DFinsupp.prod_eq_prod_fintype theorem

 [Fintype ι] [∀ i, Zero (β i)] [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] (v : Π₀ i, β i)
  {f : ∀ i, β i → γ} (hf : ∀ i, f i 0 = 1) : v.prod f = ∏ i, f i (DFinsupp.equivFunOnFintype v i)

Full source

@[to_additive (attr := simp)]
theorem prod_eq_prod_fintype [Fintype ι] [∀ i, Zero (β i)] [∀ (i : ι) (x : β i), Decidable (x ≠ 0)]
    [CommMonoid γ] (v : Π₀ i, β i) {f : ∀ i, β i → γ} (hf : ∀ i, f i 0 = 1) :
    v.prod f = ∏ i, f i (DFinsupp.equivFunOnFintype v i) := by
  suffices (∏ i ∈ v.support, f i (v i)) = ∏ i, f i (v i) by simp [DFinsupp.prod, this]
  apply Finset.prod_subset v.support.subset_univ
  intro i _ hi
  rw [mem_support_iff, not_not] at hi
  rw [hi, hf]

Product over Support Equals Product over Finite Index Set for Finitely Supported Dependent Functions

Informal description

Let $\iota$ be a finite type, $\{\beta_i\}_{i \in \iota}$ a family of types each with a zero element and decidable equality on non-zero elements, and $\gamma$ a commutative monoid. For any finitely supported dependent function $v \colon \Pi_{i} \beta_i$ and a family of functions $f_i \colon \beta_i \to \gamma$ satisfying $f_i(0) = 1$ for all $i \in \iota$, we have: \[ \prod_{i \in \text{supp}(v)} f_i(v_i) = \prod_{i \in \iota} f_i(v_i), \] where $v_i$ denotes the value of $v$ at index $i$ via the equivalence `DFinsupp.equivFunOnFintype`.

DFinsupp.prod_eq_zero_iff theorem

: f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0

Full source

@[simp]
lemma prod_eq_zero_iff : f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0 := Finset.prod_eq_zero_iff

Zero Product Criterion for Finitely Supported Dependent Functions

Informal description

For a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of functions $g_i \colon \beta_i \to \gamma$ into a commutative monoid $\gamma$, the product $\prod_{i \in \text{supp}(f)} g_i(f_i)$ equals zero if and only if there exists an index $i$ in the support of $f$ such that $g_i(f_i) = 0$.

DFinsupp.prod_ne_zero_iff theorem

: f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0

Full source

lemma prod_ne_zero_iff : f.prod g ≠ 0f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0 := Finset.prod_ne_zero_iff

Nonzero Product Criterion for Finitely Supported Dependent Functions

Informal description

For a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of functions $g_i \colon \beta_i \to \gamma$ into a commutative monoid $\gamma$, the product $\prod_{i \in \text{supp}(f)} g_i(f_i)$ is nonzero if and only if for every index $i$ in the support of $f$, the value $g_i(f_i)$ is nonzero.

DFinsupp.sumAddHom definition

[∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) : (Π₀ i, β i) →+ γ

Full source

/--
When summing over an `AddMonoidHom`, the decidability assumption is not needed, and the result is
also an `AddMonoidHom`.
-/
def sumAddHom [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) :
    (Π₀ i, β i) →+ γ where
  toFun f :=
    (f.support'.lift fun s => ∑ i ∈ Multiset.toFinset s.1, φ i (f i)) <| by
      rintro ⟨sx, hx⟩ ⟨sy, hy⟩
      dsimp only [Subtype.coe_mk, toFun_eq_coe] at *
      have H1 : sx.toFinset ∩ sy.toFinsetsx.toFinset ∩ sy.toFinset ⊆ sx.toFinset := Finset.inter_subset_left
      have H2 : sx.toFinset ∩ sy.toFinsetsx.toFinset ∩ sy.toFinset ⊆ sy.toFinset := Finset.inter_subset_right
      refine
        (Finset.sum_subset H1 ?_).symm.trans
          ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))
      · intro i H1 H2
        rw [Finset.mem_inter] at H2
        simp only [Multiset.mem_toFinset] at H1 H2
        convert AddMonoidHom.map_zero (φ i)
        exact (hy i).resolve_left (mt (And.intro H1) H2)
      · intro i _
        rfl
      · intro i H1 H2
        rw [Finset.mem_inter] at H2
        simp only [Multiset.mem_toFinset] at H1 H2
        convert AddMonoidHom.map_zero (φ i)
        exact (hx i).resolve_left (mt (fun H3 => And.intro H3 H1) H2)
  map_add' := by
    rintro ⟨f, sf, hf⟩ ⟨g, sg, hg⟩
    change (∑ i ∈ _, _) = (∑ i ∈ _, _) + ∑ i ∈ _, _
    simp only [coe_add, coe_mk', Subtype.coe_mk, Pi.add_apply, map_add, Finset.sum_add_distrib]
    congr 1
    · refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inl
      · intro i _ H2
        simp only [Multiset.mem_toFinset, Multiset.mem_add] at H2
        rw [(hf i).resolve_left H2, AddMonoidHom.map_zero]
    · refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inr
      · intro i _ H2
        simp only [Multiset.mem_toFinset, Multiset.mem_add] at H2
        rw [(hg i).resolve_left H2, AddMonoidHom.map_zero]
  map_zero' := by
    simp only [toFun_eq_coe, coe_zero, Pi.zero_apply, map_zero, Finset.sum_const_zero]; rfl

Summation of dependent functions with finite support via additive homomorphisms

Informal description

Given a family of additive monoid homomorphisms $\phi_i \colon \beta_i \to \gamma$ for each $i$ in some index set, where each $\beta_i$ is an additive zero class and $\gamma$ is an additive commutative monoid, the function `DFinsupp.sumAddHom` constructs an additive monoid homomorphism from the type of dependently-typed functions with finite support $\Pi_{i} \beta_i$ to $\gamma$. This homomorphism sums the results of applying each $\phi_i$ to the corresponding component of the input function.

DFinsupp.sumAddHom_single theorem

 [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) (i) (x : β i) : sumAddHom φ (single i x) = φ i x

Full source

@[simp]
theorem sumAddHom_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) (i)
    (x : β i) : sumAddHom φ (single i x) = φ i x := by
  dsimp [sumAddHom, single, Trunc.lift_mk]
  rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]

Evaluation of Sum Homomorphism on Single-Element Function

Informal description

Let $\{\beta_i\}_{i \in I}$ be a family of additive zero classes, $\gamma$ an additive commutative monoid, and $\phi_i \colon \beta_i \to \gamma$ a family of additive monoid homomorphisms. For any index $i$ and element $x \in \beta_i$, the sum of homomorphisms $\operatorname{sumAddHom} \phi$ applied to the single-element function $\operatorname{single}_i(x)$ equals $\phi_i(x)$, i.e., \[ \operatorname{sumAddHom} \phi (\operatorname{single}_i(x)) = \phi_i(x). \]

DFinsupp.sumAddHom_comp_single theorem

 [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ) (i : ι) : (sumAddHom f).comp (singleAddHom β i) = f i

Full source

@[simp]
theorem sumAddHom_comp_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ)
    (i : ι) : (sumAddHom f).comp (singleAddHom β i) = f i :=
  AddMonoidHom.ext fun x => sumAddHom_single f i x

Composition of Summation Homomorphism with Single-Element Homomorphism

Informal description

Let $\{\beta_i\}_{i \in I}$ be a family of additive zero classes and $\gamma$ an additive commutative monoid. For any family of additive monoid homomorphisms $f_i \colon \beta_i \to \gamma$ and any index $i \in I$, the composition of the summation homomorphism $\operatorname{sumAddHom} f$ with the single-element homomorphism $\operatorname{singleAddHom}_i$ equals $f_i$, i.e., \[ (\operatorname{sumAddHom} f) \circ (\operatorname{singleAddHom}_i) = f_i. \]

DFinsupp.sumAddHom_apply theorem

 [∀ i, AddZeroClass (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) (f : Π₀ i, β i) :
  sumAddHom φ f = f.sum fun x => φ x

Full source

/-- While we didn't need decidable instances to define it, we do to reduce it to a sum -/
theorem sumAddHom_apply [∀ i, AddZeroClass (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) (f : Π₀ i, β i) : sumAddHom φ f = f.sum fun x => φ x := by
  rcases f with ⟨f, s, hf⟩
  change (∑ i ∈ _, _) = ∑ i ∈ _ with _, _
  rw [Finset.sum_filter, Finset.sum_congr rfl]
  intro i _
  dsimp only [coe_mk', Subtype.coe_mk] at *
  split_ifs with h
  · rfl
  · rw [not_not.mp h, AddMonoidHom.map_zero]

Summation of Additive Homomorphisms over Finite Support Functions

Informal description

Let $\{\beta_i\}_{i \in I}$ be a family of additive zero classes, $\gamma$ an additive commutative monoid, and $\phi_i \colon \beta_i \to \gamma$ a family of additive monoid homomorphisms. For any dependently-typed function with finite support $f \in \Pi_{i} \beta_i$ where the support is decidable, the sum of homomorphisms $\operatorname{sumAddHom} \phi$ applied to $f$ equals the sum over all $i$ of $\phi_i(f(i))$, i.e., \[ \operatorname{sumAddHom} \phi (f) = \sum_{i} \phi_i(f(i)). \]

DFinsupp.sumAddHom_comm theorem

 {ι₁ ι₂ : 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₁

Full source

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₂
  simp only [sumAddHom, AddMonoidHom.finset_sum_apply, Quotient.liftOn_mk, AddMonoidHom.coe_mk,
    AddMonoidHom.flip_apply, Trunc.lift, toFun_eq_coe, ZeroHom.coe_mk, coe_mk']
  exact Finset.sum_comm

Commutativity of Double Summation for Dependent Functions with Finite Support

Informal description

Let $\iota_1$ and $\iota_2$ be index types, and let $\beta_1 \colon \iota_1 \to \text{Type}^*$ and $\beta_2 \colon \iota_2 \to \text{Type}^*$ be families of types such that for each $i$, $\beta_1 i$ and $\beta_2 i$ are additive zero classes. Let $\gamma$ be an additive commutative monoid. Given two dependently-typed functions with finite support $f_1 \colon \Pi_{i_1} \beta_1 i_1$ and $f_2 \colon \Pi_{i_2} \beta_2 i_2$, and a family of additive monoid homomorphisms $h \colon \forall i_1 i_2, \beta_1 i_1 \to+ \beta_2 i_2 \to+ \gamma$, the following equality holds: \[ \sum_{i_2} \left( \sum_{i_1} h_{i_1 i_2} (f_1 i_1) \right) (f_2 i_2) = \sum_{i_1} \left( \sum_{i_2} h_{i_1 i_2}^\text{flip} (f_2 i_2) \right) (f_1 i_1) \] where $h_{i_1 i_2}^\text{flip}$ denotes the flipped version of $h_{i_1 i_2}$.

DFinsupp.liftAddHom definition

[∀ i, AddZeroClass (β i)] [AddCommMonoid γ] : (∀ i, β i →+ γ) ≃+ ((Π₀ i, β i) →+ γ)

Full source

/-- The `DFinsupp` version of `Finsupp.liftAddHom` -/
@[simps apply symm_apply]
def liftAddHom [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] :
    (∀ i, β i →+ γ) ≃+ ((Π₀ i, β i) →+ γ) where
  toFun := sumAddHom
  invFun F i := F.comp (singleAddHom β i)
  left_inv x := by ext; simp
  right_inv ψ := by ext; simp
  map_add' F G := by ext; simp

Lifting additive homomorphisms to dependent functions with finite support

Informal description

Given a family of additive monoid homomorphisms $\phi_i \colon \beta_i \to \gamma$ for each index $i$, where each $\beta_i$ is an additive zero class and $\gamma$ is an additive commutative monoid, the function `DFinsupp.liftAddHom` constructs an equivalence of additive monoid homomorphisms between the type of families $(\forall i, \beta_i \to+ \gamma)$ and the type of additive monoid homomorphisms $(\Pi_{i} \beta_i) \to+ \gamma$. Specifically, `liftAddHom` maps a family $\phi$ to the homomorphism that sums the results of applying each $\phi_i$ to the corresponding component of a dependently-typed function with finite support. The inverse operation takes a homomorphism $F \colon (\Pi_{i} \beta_i) \to+ \gamma$ and produces the family of homomorphisms obtained by composing $F$ with the canonical injection $\text{singleAddHom} \beta_i \colon \beta_i \to+ \Pi_{i} \beta_i$ for each $i$.

DFinsupp.liftAddHom_singleAddHom theorem

[∀ i, AddCommMonoid (β i)] : liftAddHom (singleAddHom β) = AddMonoidHom.id (Π₀ i, β i)

Full source

/-- The `DFinsupp` version of `Finsupp.liftAddHom_singleAddHom` -/
theorem liftAddHom_singleAddHom [∀ i, AddCommMonoid (β i)] :
    liftAddHom (singleAddHom β) = AddMonoidHom.id (Π₀ i, β i) :=
  liftAddHom.toEquiv.apply_eq_iff_eq_symm_apply.2 rfl

Lifted Single Homomorphism is Identity on Dependent Functions with Finite Support

Informal description

For any family of additive commutative monoids $\{\beta_i\}_{i \in I}$, the lifted additive homomorphism of the family of single-element homomorphisms $\operatorname{singleAddHom} \beta_i \colon \beta_i \to+ \Pi_{i} \beta_i$ is equal to the identity homomorphism on $\Pi_{i} \beta_i$, i.e., \[ \operatorname{liftAddHom} (\operatorname{singleAddHom} \beta) = \operatorname{id}_{\Pi_{i} \beta_i}. \]

DFinsupp.liftAddHom_apply_single theorem

 [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ) (i : ι) (x : β i) : liftAddHom f (single i x) = f i x

Full source

/-- The `DFinsupp` version of `Finsupp.liftAddHom_apply_single` -/
theorem liftAddHom_apply_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ)
    (i : ι) (x : β i) : liftAddHom f (single i x) = f i x := by simp

Evaluation of Lifted Additive Homomorphism on Single-Element Function

Informal description

Let $\{\beta_i\}_{i \in I}$ be a family of additive zero classes, $\gamma$ an additive commutative monoid, and $f_i \colon \beta_i \to \gamma$ a family of additive monoid homomorphisms. For any index $i$ and element $x \in \beta_i$, the lifted homomorphism $\operatorname{liftAddHom} f$ applied to the single-element function $\operatorname{single}_i(x)$ equals $f_i(x)$, i.e., \[ \operatorname{liftAddHom} f (\operatorname{single}_i(x)) = f_i(x). \]

DFinsupp.liftAddHom_comp_single theorem

 [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ) (i : ι) : (liftAddHom f).comp (singleAddHom β i) = f i

Full source

/-- The `DFinsupp` version of `Finsupp.liftAddHom_comp_single` -/
theorem liftAddHom_comp_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ)
    (i : ι) : (liftAddHom f).comp (singleAddHom β i) = f i := by simp

Composition of Lifted Homomorphism with Single-Element Homomorphism

Informal description

Let $\{\beta_i\}_{i \in I}$ be a family of additive zero classes and $\gamma$ an additive commutative monoid. For any family of additive monoid homomorphisms $f_i \colon \beta_i \to \gamma$ and any index $i \in I$, the composition of the lifted homomorphism $\operatorname{liftAddHom} f$ with the single-element homomorphism $\operatorname{singleAddHom}_i$ equals $f_i$, i.e., \[ (\operatorname{liftAddHom} f) \circ (\operatorname{singleAddHom}_i) = f_i. \]

DFinsupp.comp_liftAddHom theorem

 {δ : Type*} [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ] (g : γ →+ δ) (f : ∀ i, β i →+ γ) :
  g.comp (liftAddHom f) = liftAddHom fun a => g.comp (f a)

Full source

/-- The `DFinsupp` version of `Finsupp.comp_liftAddHom` -/
theorem comp_liftAddHom {δ : Type*} [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ]
    (g : γ →+ δ) (f : ∀ i, β i →+ γ) :
    g.comp (liftAddHom f) = liftAddHom fun a => g.comp (f a) :=
  liftAddHom.symm_apply_eq.1 <|
    funext fun a => by
      rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

Composition of Additive Homomorphism with Lifted Homomorphism in Dependent Finite Support Functions

Informal description

Let $\{\beta_i\}_{i}$ be a family of additive zero classes, and let $\gamma$ and $\delta$ be additive commutative monoids. For any additive monoid homomorphism $g \colon \gamma \to \delta$ and any family of additive monoid homomorphisms $f_i \colon \beta_i \to \gamma$, the composition of $g$ with the lifted homomorphism $\operatorname{liftAddHom} f$ equals the lifted homomorphism of the composed maps $g \circ f_i$, i.e., \[ g \circ (\operatorname{liftAddHom} f) = \operatorname{liftAddHom} (\lambda a, g \circ f_a). \]

DFinsupp.sumAddHom_zero theorem

[∀ i, AddZeroClass (β i)] [AddCommMonoid γ] : (sumAddHom fun i => (0 : β i →+ γ)) = 0

Full source

@[simp]
theorem sumAddHom_zero [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] :
    (sumAddHom fun i => (0 : β i →+ γ)) = 0 :=
  map_zero liftAddHom

Sum of Zero Homomorphisms is Zero in Dependent Finite Support Functions

Informal description

For any family of additive zero classes $\{\beta_i\}_{i}$ and any additive commutative monoid $\gamma$, the sum of the zero homomorphisms (where each $\beta_i \to+ \gamma$ is the zero homomorphism) is equal to the zero homomorphism on $\Pi_{i} \beta_i$. In other words, $\text{sumAddHom} (\lambda i, 0) = 0$.

DFinsupp.sumAddHom_add theorem

 [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (g : ∀ i, β i →+ γ) (h : ∀ i, β i →+ γ) :
  (sumAddHom fun i => g i + h i) = sumAddHom g + sumAddHom h

Full source

@[simp]
theorem sumAddHom_add [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (g : ∀ i, β i →+ γ)
    (h : ∀ i, β i →+ γ) : (sumAddHom fun i => g i + h i) = sumAddHom g + sumAddHom h :=
  map_add liftAddHom _ _

Additivity of sum over dependent functions with finite support

Informal description

Let $\{\beta_i\}_{i}$ be a family of additive zero classes and $\gamma$ be an additive commutative monoid. For any two families of additive monoid homomorphisms $g, h \colon \forall i, \beta_i \to+ \gamma$, the sum of the homomorphisms satisfies: \[ \text{sumAddHom} (\lambda i, g_i + h_i) = \text{sumAddHom}\, g + \text{sumAddHom}\, h \]

DFinsupp.sumAddHom_singleAddHom theorem

[∀ i, AddCommMonoid (β i)] : sumAddHom (singleAddHom β) = AddMonoidHom.id _

Full source

@[simp]
theorem sumAddHom_singleAddHom [∀ i, AddCommMonoid (β i)] :
    sumAddHom (singleAddHom β) = AddMonoidHom.id _ :=
  liftAddHom_singleAddHom

Sum of Single Homomorphisms is Identity on Dependent Functions with Finite Support

Informal description

For any family of additive commutative monoids $\{\beta_i\}_{i \in I}$, the sum of the single-element homomorphisms $\operatorname{singleAddHom} \beta_i \colon \beta_i \to+ \Pi_{i} \beta_i$ is equal to the identity homomorphism on $\Pi_{i} \beta_i$, i.e., \[ \operatorname{sumAddHom} (\operatorname{singleAddHom} \beta) = \operatorname{id}_{\Pi_{i} \beta_i}. \]

DFinsupp.comp_sumAddHom theorem

 {δ : Type*} [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ] (g : γ →+ δ) (f : ∀ i, β i →+ γ) :
  g.comp (sumAddHom f) = sumAddHom fun a => g.comp (f a)

Full source

theorem comp_sumAddHom {δ : Type*} [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ]
    (g : γ →+ δ) (f : ∀ i, β i →+ γ) : g.comp (sumAddHom f) = sumAddHom fun a => g.comp (f a) :=
  comp_liftAddHom _ _

Composition of Additive Homomorphism with Summation Homomorphism in Dependent Finite Support Functions

Informal description

Let $\{\beta_i\}_{i}$ be a family of additive zero classes, and let $\gamma$ and $\delta$ be additive commutative monoids. For any additive monoid homomorphism $g \colon \gamma \to \delta$ and any family of additive monoid homomorphisms $f_i \colon \beta_i \to \gamma$, the composition of $g$ with the summation homomorphism $\operatorname{sumAddHom} f$ equals the summation homomorphism of the composed maps $g \circ f_i$, i.e., \[ g \circ (\operatorname{sumAddHom} f) = \operatorname{sumAddHom} (\lambda a, g \circ f_a). \]

DFinsupp.sum_sub_index theorem

 [∀ i, AddGroup (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommGroup γ] {f g : Π₀ i, β i} {h : ∀ i, β i → γ}
  (h_sub : ∀ i b₁ b₂, h i (b₁ - b₂) = h i b₁ - h i b₂) : (f - g).sum h = f.sum h - g.sum h

Full source

theorem sum_sub_index [∀ i, AddGroup (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [AddCommGroup γ]
    {f g : Π₀ i, β i} {h : ∀ i, β i → γ} (h_sub : ∀ i b₁ b₂, h i (b₁ - b₂) = h i b₁ - h i b₂) :
    (f - g).sum h = f.sum h - g.sum h := by
  have := (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
  rw [liftAddHom_apply, sumAddHom_apply, sumAddHom_apply, sumAddHom_apply] at this
  exact this

Linearity of Summation over Difference of Finitely Supported Functions

Informal description

Let $\{\beta_i\}_{i \in I}$ be a family of additive groups, $\gamma$ an additive commutative group, and $f, g \colon \Pi_{i} \beta_i$ two dependently-typed functions with finite support. For any family of functions $h_i \colon \beta_i \to \gamma$ satisfying $h_i(b_1 - b_2) = h_i(b_1) - h_i(b_2)$ for all $i \in I$ and $b_1, b_2 \in \beta_i$, the sum of $h_i$ over the difference $f - g$ equals the difference of the sums of $h_i$ over $f$ and $g$ respectively, i.e., \[ \sum_{i} h_i((f - g)_i) = \left(\sum_{i} h_i(f_i)\right) - \left(\sum_{i} h_i(g_i)\right). \]

DFinsupp.prod_finset_sum_index theorem

 {γ : Type w} {α : Type x} [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {s : Finset α}
  {g : α → Π₀ i, β i} {h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1)
  (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) : (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h

Full source

@[to_additive]
theorem prod_finset_sum_index {γ : Type w} {α : Type x} [∀ i, AddCommMonoid (β i)]
    [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {s : Finset α} {g : α → Π₀ i, β i}
    {h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1)
    (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
    (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h := by
  classical
  exact Finset.induction_on s (by simp [prod_zero_index])
        (by simp +contextual [prod_add_index, h_zero, h_add])

Product over Support Commutes with Finite Sum of Finitely Supported Dependent Functions

Informal description

Let $\{\beta_i\}_{i \in \iota}$ be a family of additively commutative monoids, $\gamma$ a commutative monoid, and $s$ a finite set of indices. For a family of finitely supported dependent functions $g_a \colon \Pi_{i} \beta_i$ indexed by $a \in s$ and a family of functions $h_i \colon \beta_i \to \gamma$ satisfying $h_i(0) = 1$ and $h_i(b_1 + b_2) = h_i(b_1) \cdot h_i(b_2)$ for all $i \in \iota$ and $b_1, b_2 \in \beta_i$, we have: \[ \prod_{a \in s} \left(\prod_{i \in \text{supp}(g_a)} h_i((g_a)_i)\right) = \prod_{i \in \text{supp}(\sum_{a \in s} g_a)} h_i\left(\left(\sum_{a \in s} g_a\right)_i\right). \]

DFinsupp.prod_sum_index theorem

 {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)] [∀ (i) (x : β₁ i), Decidable (x ≠ 0)]
  [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i₁, β₁ i₁}
  {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} {h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1)
  (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) : (f.sum g).prod h = f.prod fun i b => (g i b).prod h

Full source

@[to_additive]
theorem prod_sum_index {ι₁ : Type u₁} [DecidableEq ι₁] {β₁ : ι₁ → Type v₁} [∀ i₁, Zero (β₁ i₁)]
    [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] [∀ i, AddCommMonoid (β i)]
    [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i₁, β₁ i₁}
    {g : ∀ i₁, β₁ i₁ → Π₀ i, β i} {h : ∀ i, β i → γ} (h_zero : ∀ i, h i 0 = 1)
    (h_add : ∀ i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
    (f.sum g).prod h = f.prod fun i b => (g i b).prod h :=
  (prod_finset_sum_index h_zero h_add).symm

Product-Sum Commutation for Finitely Supported Dependent Functions

Informal description

Let $\iota_1$ be a type with decidable equality, $\beta_1 \colon \iota_1 \to \text{Type}$ a family of types each with a zero element and decidable equality on non-zero elements, and $\beta \colon \iota \to \text{Type}$ a family of additively commutative monoids with decidable equality on non-zero elements. Let $\gamma$ be a commutative monoid. Given a finitely supported dependent function $f \colon \Pi_{i_1} \beta_1 i_1$, a family of functions $g_{i_1} \colon \beta_1 i_1 \to \Pi_i \beta i$, and a family of functions $h_i \colon \beta i \to \gamma$ satisfying $h_i(0) = 1$ and $h_i(b_1 + b_2) = h_i(b_1) \cdot h_i(b_2)$ for all $i \in \iota$ and $b_1, b_2 \in \beta i$, we have: \[ \prod_{i \in \text{supp}(f \sum g)} h_i\left(\left(\sum_{i_1} g_{i_1}(f_{i_1})\right)_i\right) = \prod_{i_1 \in \text{supp}(f)} \left(\prod_{i \in \text{supp}(g_{i_1}(f_{i_1}))} h_i((g_{i_1}(f_{i_1}))_i)\right). \]

DFinsupp.sum_single theorem

[∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i, β i} : f.sum single = f

Full source

@[simp]
theorem sum_single [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i, β i} :
    f.sum single = f := by
  have := DFunLike.congr_fun (liftAddHom_singleAddHom (β := β)) f
  rw [liftAddHom_apply, sumAddHom_apply] at this
  exact this

Sum of Single-Element Functions Recovers Original Function

Informal description

For any dependently-typed function $f$ with finite support, where each $\beta_i$ is an additive commutative monoid and the support is decidable, the sum of the single-element functions $\operatorname{single}$ over the support of $f$ equals $f$ itself, i.e., \[ \sum_{i \in \text{supp}(f)} \operatorname{single}_i (f(i)) = f. \]

DFinsupp.prod_subtypeDomain_index theorem

 [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {v : Π₀ i, β i} {p : ι → Prop} [DecidablePred p]
  {h : ∀ i, β i → γ} (hp : ∀ x ∈ v.support, p x) : (v.subtypeDomain p).prod (fun i b => h i b) = v.prod h

Full source

@[to_additive]
theorem prod_subtypeDomain_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [CommMonoid γ] {v : Π₀ i, β i} {p : ι → Prop} [DecidablePred p] {h : ∀ i, β i → γ}
    (hp : ∀ x ∈ v.support, p x) : (v.subtypeDomain p).prod (fun i b => h i b) = v.prod h := by
  refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop

Product Equality for Restricted Domain of Finitely Supported Dependent Function

Informal description

Let $\iota$ be a type, $\beta \colon \iota \to \text{Type}$ a family of types each with a zero element and decidable equality on non-zero elements, and $\gamma$ a commutative monoid. Given a finitely supported dependent function $v \colon \Pi_{i} \beta i$, a predicate $p \colon \iota \to \text{Prop}$ with decidable values, and a family of functions $h_i \colon \beta i \to \gamma$, if for every $x$ in the support of $v$ the predicate $p(x)$ holds, then the product over the restricted domain equals the product over the full domain: $$ \prod_{i \in \text{supp}(v \vert_p)} h_i(v_i) = \prod_{i \in \text{supp}(v)} h_i(v_i) $$ where $v \vert_p$ denotes the restriction of $v$ to the subtype where $p$ holds.

DFinsupp.subtypeDomain_sum theorem

 {ι} {β : ι → Type v} [∀ i, AddCommMonoid (β i)] {s : Finset γ} {h : γ → Π₀ i, β i} {p : ι → Prop} [DecidablePred p] :
  (∑ c ∈ s, h c).subtypeDomain p = ∑ c ∈ s, (h c).subtypeDomain p

Full source

theorem subtypeDomain_sum {ι} {β : ι → Type v} [∀ i, AddCommMonoid (β i)] {s : Finset γ}
    {h : γ → Π₀ i, β i} {p : ι → Prop} [DecidablePred p] :
    (∑ c ∈ s, h c).subtypeDomain p = ∑ c ∈ s, (h c).subtypeDomain p :=
  map_sum (subtypeDomainAddMonoidHom β p) _ s

Sum Commutes with Subtype Restriction for Dependent Functions with Finite Support

Informal description

Let $ι$ be a type, $\beta : ι \to \text{Type}_v$ a family of types with each $\beta i$ an additive commutative monoid. For a finite set $s$ of elements of type $\gamma$, a family of functions $h : \gamma \to \Pi_{i} \beta i$ with finite support, and a predicate $p : ι \to \text{Prop}$ with decidable values, we have: $$(\sum_{c \in s} h c).\text{subtypeDomain } p = \sum_{c \in s} (h c).\text{subtypeDomain } p$$ where $\text{subtypeDomain}$ restricts a function to the subset where $p$ holds.

DFinsupp.subtypeDomain_finsupp_sum theorem

 {ι} {β : ι → Type v} {δ : γ → Type x} [DecidableEq γ] [∀ c, Zero (δ c)] [∀ (c) (x : δ c), Decidable (x ≠ 0)]
  [∀ i, AddCommMonoid (β i)] {p : ι → Prop} [DecidablePred p] {s : Π₀ c, δ c} {h : ∀ c, δ c → Π₀ i, β i} :
  (s.sum h).subtypeDomain p = s.sum fun c d => (h c d).subtypeDomain p

Full source

theorem subtypeDomain_finsupp_sum {ι} {β : ι → Type v} {δ : γ → Type x} [DecidableEq γ]
    [∀ c, Zero (δ c)] [∀ (c) (x : δ c), Decidable (x ≠ 0)]
    [∀ i, AddCommMonoid (β i)] {p : ι → Prop} [DecidablePred p]
    {s : Π₀ c, δ c} {h : ∀ c, δ c → Π₀ i, β i} :
    (s.sum h).subtypeDomain p = s.sum fun c d => (h c d).subtypeDomain p :=
  subtypeDomain_sum

Sum Commutes with Subtype Restriction for Finitely Supported Dependent Functions

Informal description

Let $\iota$ and $\gamma$ be types, with $\beta \colon \iota \to \text{Type}$ and $\delta \colon \gamma \to \text{Type}$ families of types. Assume: - $\gamma$ has decidable equality, - Each $\delta c$ has a zero element and decidable equality on non-zero elements, - Each $\beta i$ is an additive commutative monoid, - $p \colon \iota \to \text{Prop}$ is a decidable predicate. Given a finitely supported dependent function $s \colon \Pi_{c} \delta c$ and a family of functions $h_c \colon \delta c \to \Pi_{i} \beta i$ with finite support, we have: $$(s.\text{sum } h).\text{subtypeDomain } p = s.\text{sum } \big(c \mapsto d \mapsto (h_c d).\text{subtypeDomain } p\big)$$ where $\text{subtypeDomain}$ restricts a function to the subset where $p$ holds, and $\text{sum}$ denotes the sum over the support of $s$.

MonoidHom.coe_dfinsuppProd theorem

 [MulOneClass R] [CommMonoid S] (f : Π₀ i, β i) (g : ∀ i, β i → R →* S) : ⇑(f.prod g) = f.prod fun a b => ⇑(g a b)

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_dfinsuppProd [MulOneClass R] [CommMonoid S] (f : Π₀ i, β i) (g : ∀ i, β i → R →* S) :
    ⇑(f.prod g) = f.prod fun a b => ⇑(g a b) :=
  coe_finset_prod _ _

Coefficient of Product Homomorphism over Finitely Supported Dependent Function

Informal description

Let $R$ be a type with a multiplicative monoid structure and $S$ a commutative monoid. Given a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of monoid homomorphisms $g_i \colon \beta_i \to R \to^* S$, the underlying function of the product homomorphism $f.\text{prod} \, g$ is equal to the product over the support of $f$ of the underlying functions $\text{coe}(g_i(b_i))$, where $b_i = f(i)$.

MonoidHom.dfinsuppProd_apply theorem

 [MulOneClass R] [CommMonoid S] (f : Π₀ i, β i) (g : ∀ i, β i → R →* S) (r : R) :
  (f.prod g) r = f.prod fun a b => (g a b) r

Full source

@[to_additive]
theorem dfinsuppProd_apply [MulOneClass R] [CommMonoid S] (f : Π₀ i, β i) (g : ∀ i, β i → R →* S)
    (r : R) : (f.prod g) r = f.prod fun a b => (g a b) r :=
  finset_prod_apply _ _ _

Evaluation of Product Homomorphism over Finitely Supported Dependent Function

Informal description

Let $R$ be a type with a multiplicative monoid structure, $S$ a commutative monoid, and $\beta_i$ a family of types indexed by $i$. Given a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of monoid homomorphisms $g_i \colon \beta_i \to R \to^* S$, the evaluation of the product homomorphism $(f.\text{prod} \, g)$ at an element $r \in R$ equals the product over the support of $f$ of the evaluations $(g_i(b_i))(r)$, where $b_i = f(i)$.

AddMonoidHom.map_dfinsuppSumAddHom theorem

 [AddCommMonoid R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)] (h : R →+ S) (f : Π₀ i, β i) (g : ∀ i, β i →+ R) :
  h (sumAddHom g f) = sumAddHom (fun i => h.comp (g i)) f

Full source

@[simp]
theorem map_dfinsuppSumAddHom [AddCommMonoid R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)]
    (h : R →+ S) (f : Π₀ i, β i) (g : ∀ i, β i →+ R) :
    h (sumAddHom g f) = sumAddHom (fun i => h.comp (g i)) f :=
  DFunLike.congr_fun (comp_liftAddHom h g) f

Additive Homomorphism Commutes with Summation of Finitely Supported Dependent Functions

Informal description

Let $R$ and $S$ be additive commutative monoids, and let $\{\beta_i\}_{i}$ be a family of additive zero classes. Given an additive monoid homomorphism $h \colon R \to S$, a finitely supported dependent function $f \colon \Pi_{i} \beta_i$, and a family of additive monoid homomorphisms $g_i \colon \beta_i \to R$, the following equality holds: \[ h\left(\sum_{i} g_i(f_i)\right) = \sum_{i} (h \circ g_i)(f_i). \] Here, $\sum$ denotes the summation via `DFinsupp.sumAddHom`, which sums over the support of $f$.

AddMonoidHom.dfinsuppSumAddHom_apply theorem

 [AddZeroClass R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i) (g : ∀ i, β i →+ R →+ S) (r : R) :
  (sumAddHom g f) r = sumAddHom (fun i => (eval r).comp (g i)) f

Full source

theorem dfinsuppSumAddHom_apply [AddZeroClass R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)]
    (f : Π₀ i, β i) (g : ∀ i, β i →+ R →+ S) (r : R) :
    (sumAddHom g f) r = sumAddHom (fun i => (eval r).comp (g i)) f :=
  map_dfinsuppSumAddHom (eval r) f g

Evaluation of Sum Homomorphism over Finitely Supported Dependent Function

Informal description

Let $R$ be an additive zero class, $S$ an additive commutative monoid, and $\{\beta_i\}_{i}$ a family of additive zero classes. Given a finitely supported dependent function $f \colon \Pi_{i} \beta_i$, a family of additive monoid homomorphisms $g_i \colon \beta_i \to R \to^+ S$, and an element $r \in R$, the evaluation of the sum homomorphism $\text{sumAddHom}\,g\,f$ at $r$ equals the sum over the support of $f$ of the evaluations $(g_i)(b_i)(r)$, where $b_i = f(i)$. In other words: \[ \left(\sum_{i} g_i(f_i)\right)(r) = \sum_{i} \left(g_i(f_i)(r)\right). \]

AddMonoidHom.coe_dfinsuppSumAddHom theorem

 [AddZeroClass R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)] (f : Π₀ i, β i) (g : ∀ i, β i →+ R →+ S) :
  ⇑(sumAddHom g f) = sumAddHom (fun i => (coeFn R S).comp (g i)) f

Full source

@[simp, norm_cast]
theorem coe_dfinsuppSumAddHom [AddZeroClass R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)]
    (f : Π₀ i, β i) (g : ∀ i, β i →+ R →+ S) :
    ⇑(sumAddHom g f) = sumAddHom (fun i => (coeFn R S).comp (g i)) f :=
  map_dfinsuppSumAddHom (coeFn R S) f g

Coefficient Function Commutes with Summation of Additive Homomorphisms over Finitely Supported Dependent Functions

Informal description

Let $R$ be an additive zero class, $S$ an additive commutative monoid, and $\{\beta_i\}_{i}$ a family of additive zero classes. Given a finitely supported dependent function $f \colon \Pi_{i} \beta_i$ and a family of additive monoid homomorphisms $g_i \colon \beta_i \to R \to^+ S$, the underlying function of the sum homomorphism $\operatorname{sumAddHom} g f$ equals the sum homomorphism of the family obtained by composing each $g_i$ with the canonical embedding $\operatorname{coeFn} \colon R \to S$. In other words: \[ \left(\sum_{i} g_i(f_i)\right) = \sum_{i} \left(\operatorname{coeFn} \circ g_i\right)(f_i). \]

RingHom.map_dfinsuppSumAddHom theorem

 [NonAssocSemiring R] [NonAssocSemiring S] [∀ i, AddZeroClass (β i)] (h : R →+* S) (f : Π₀ i, β i) (g : ∀ i, β i →+ R) :
  h (sumAddHom g f) = sumAddHom (fun i => h.toAddMonoidHom.comp (g i)) f

Full source

@[simp]
theorem map_dfinsuppSumAddHom [NonAssocSemiring R] [NonAssocSemiring S] [∀ i, AddZeroClass (β i)]
    (h : R →+* S) (f : Π₀ i, β i) (g : ∀ i, β i →+ R) :
    h (sumAddHom g f) = sumAddHom (fun i => h.toAddMonoidHom.comp (g i)) f :=
  DFunLike.congr_fun (comp_liftAddHom h.toAddMonoidHom g) f

Ring Homomorphism Commutes with Dependent Summation of Additive Homomorphisms

Informal description

Let $R$ and $S$ be non-associative semirings, and let $\{\beta_i\}_{i}$ be a family of additive zero classes. For any ring homomorphism $h \colon R \to S$, any dependently-typed function with finite support $f \colon \Pi_{i} \beta_i$, and any family of additive monoid homomorphisms $g_i \colon \beta_i \to R$, the following equality holds: \[ h\left(\sum_{i} g_i(f_i)\right) = \sum_{i} (h \circ g_i)(f_i). \] Here, $\sum$ denotes the summation via `DFinsupp.sumAddHom`.

AddEquiv.map_dfinsuppSumAddHom theorem

 [AddCommMonoid R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)] (h : R ≃+ S) (f : Π₀ i, β i) (g : ∀ i, β i →+ R) :
  h (sumAddHom g f) = sumAddHom (fun i => h.toAddMonoidHom.comp (g i)) f

Full source

@[simp]
theorem map_dfinsuppSumAddHom [AddCommMonoid R] [AddCommMonoid S] [∀ i, AddZeroClass (β i)]
    (h : R ≃+ S) (f : Π₀ i, β i) (g : ∀ i, β i →+ R) :
    h (sumAddHom g f) = sumAddHom (fun i => h.toAddMonoidHom.comp (g i)) f :=
  DFunLike.congr_fun (comp_liftAddHom h.toAddMonoidHom g) f

Additive Equivalence Commutes with Summation of Dependent Functions with Finite Support

Informal description

Let $R$ and $S$ be additive commutative monoids, and let $\{\beta_i\}_{i}$ be a family of additive zero classes. Given an additive equivalence $h \colon R \simeq S$, a dependently-typed function with finite support $f \colon \Pi_{i} \beta_i$, and a family of additive monoid homomorphisms $g_i \colon \beta_i \to R$, the image of the sum $\operatorname{sumAddHom} g f$ under $h$ equals the sum of the compositions $h \circ g_i$ applied to $f$, i.e., \[ h\left(\operatorname{sumAddHom} g f\right) = \operatorname{sumAddHom} (\lambda i, h \circ g_i) f. \]