Dependent functions with finite support

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

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.

def DFinsupp.evalAddMonoidHom {ι : Type u} {β : ι → Type v} [(i : ι) → AddZeroClass (β i)] (i : ι) : (Π₀ (i : ι), β i) →+ β i

Evaluation at a point is an AddMonoidHom. This is the finitely-supported version of Pi.evalAddMonoidHom.

Equations

• DFinsupp.evalAddMonoidHom i = (Pi.evalAddMonoidHom β i).comp DFinsupp.coeFnAddMonoidHom

@[simp]

theorem DFinsupp.coe_finset_sum {ι : Type u} {β : ι → Type v} {α : Type u_1} [(i : ι) → AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ (i : ι), β i) : ⇑(∑ a ∈ s, g a) = ∑ a ∈ s, ⇑(g a)

@[simp]

theorem DFinsupp.finset_sum_apply {ι : Type u} {β : ι → Type v} {α : Type u_1} [(i : ι) → AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ (i : ι), β i) (i : ι) : (∑ a ∈ s, g a) i = ∑ a ∈ s, (g a) i

def DFinsupp.prod {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) : γ

DFinsupp.prod f g is the product of g i (f i) over the support of f.

Equations

• f.prod g = ∏ i ∈ f.support, g i (f i)

def DFinsupp.sum {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) : γ

sum f g is the sum of g i (f i) over the support of f.

Equations

• f.sum g = ∑ i ∈ f.support, g i (f i)

@[simp]

theorem map_dfinsuppProd {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} {H : Type u_3} [(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 : β a) => h (g a b)

@[simp]

theorem map_dfinsuppSum {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} {H : Type u_3} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid R] [AddCommMonoid S] [FunLike H R S] [AddMonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R) : h (f.sum g) = f.sum fun (a : ι) (b : β a) => h (g a b)

theorem DFinsupp.prod_mapRange_index {ι : Type u} {γ : Type w} [DecidableEq ι] {β₁ : ι → 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 : β₁ i) => h i (f i b)

theorem DFinsupp.sum_mapRange_index {ι : Type u} {γ : Type w} [DecidableEq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [(i : ι) → Zero (β₁ i)] [(i : ι) → Zero (β₂ i)] [(i : ι) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : (i : ι) → β₂ i → γ} (h0 : ∀ (i : ι), h i 0 = 0) : (mapRange f hf g).sum h = g.sum fun (i : ι) (b : β₁ i) => h i (f i b)

theorem DFinsupp.prod_zero_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {h : (i : ι) → β i → γ} : prod 0 h = 1

theorem DFinsupp.sum_zero_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {h : (i : ι) → β i → γ} : sum 0 h = 0

theorem DFinsupp.prod_single_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(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

theorem DFinsupp.sum_single_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {i : ι} {b : β i} {h : (i : ι) → β i → γ} (h_zero : h i 0 = 0) : (single i b).sum h = h i b

theorem DFinsupp.prod_neg_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(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 : β i) => h i (-b)

theorem DFinsupp.sum_neg_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {g : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h0 : ∀ (i : ι), h i 0 = 0) : (-g).sum h = g.sum fun (i : ι) (b : β i) => h i (-b)

theorem DFinsupp.prod_comm {γ : Type w} {ι₁ : Type u_3} {ι₂ : Type u_4} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} [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₁ : β₁ i₁) => f₂.prod fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = f₂.prod fun (i₂ : ι₂) (x₂ : β₂ i₂) => f₁.prod fun (i₁ : ι₁) (x₁ : β₁ i₁) => h i₁ x₁ i₂ x₂

theorem DFinsupp.sum_comm {γ : Type w} {ι₁ : Type u_3} {ι₂ : Type u_4} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} [DecidableEq ι₁] [DecidableEq ι₂] [(i : ι₁) → Zero (β₁ i)] [(i : ι₂) → Zero (β₂ i)] [(i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)] [(i : ι₂) → (x : β₂ i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (f₁ : Π₀ (i : ι₁), β₁ i) (f₂ : Π₀ (i : ι₂), β₂ i) (h : (i : ι₁) → β₁ i → (i : ι₂) → β₂ i → γ) : (f₁.sum fun (i₁ : ι₁) (x₁ : β₁ i₁) => f₂.sum fun (i₂ : ι₂) (x₂ : β₂ i₂) => h i₁ x₁ i₂ x₂) = f₂.sum fun (i₂ : ι₂) (x₂ : β₂ i₂) => f₁.sum fun (i₁ : ι₁) (x₁ : β₁ i₁) => h i₁ x₁ i₂ x₂

@[simp]

theorem DFinsupp.sum_apply {ι : Type u_1} {β : ι → 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 : β₁ i₁) => (g i₁ b) i₂

theorem DFinsupp.support_sum {ι : Type u} {β : ι → Type v} [DecidableEq ι] {ι₁ : 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

@[simp]

theorem DFinsupp.prod_one {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ (i : ι), β i} : (f.prod fun (x : ι) (x : β x) => 1) = 1

@[simp]

theorem DFinsupp.sum_zero {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : Π₀ (i : ι), β i} : (f.sum fun (x : ι) (x : β x) => 0) = 0

@[simp]

theorem DFinsupp.prod_mul {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ (i : ι), β i} {h₁ h₂ : (i : ι) → β i → γ} : (f.prod fun (i : ι) (b : β i) => h₁ i b * h₂ i b) = f.prod h₁ * f.prod h₂

@[simp]

theorem DFinsupp.sum_add {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : Π₀ (i : ι), β i} {h₁ h₂ : (i : ι) → β i → γ} : (f.sum fun (i : ι) (b : β i) => h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂

@[simp]

theorem DFinsupp.prod_inv {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [DivisionCommMonoid γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} : (f.prod fun (i : ι) (b : β i) => (h i b)⁻¹) = (f.prod h)⁻¹

@[simp]

theorem DFinsupp.sum_neg {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [SubtractionCommMonoid γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} : (f.sum fun (i : ι) (b : β i) => -h i b) = -f.sum h

theorem DFinsupp.prod_eq_one {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(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

theorem DFinsupp.sum_eq_zero {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (hyp : ∀ (i : ι), h i (f i) = 0) : f.sum h = 0

theorem DFinsupp.smul_sum {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] {α : Type u_1} [(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 : β a) => c • h a b

theorem DFinsupp.prod_add_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(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₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) : (f + g).prod h = f.prod h * g.prod h

theorem DFinsupp.sum_add_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {f g : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h_zero : ∀ (i : ι), h i 0 = 0) (h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) : (f + g).sum h = f.sum h + g.sum h

@[simp]

theorem DFinsupp.prod_eq_prod_fintype {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [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 (equivFunOnFintype v i)

@[simp]

theorem DFinsupp.sum_eq_sum_fintype {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (v : Π₀ (i : ι), β i) {f : (i : ι) → β i → γ} (hf : ∀ (i : ι), f i 0 = 0) : v.sum f = ∑ i : ι, f i (equivFunOnFintype v i)

@[simp]

theorem DFinsupp.prod_eq_zero_iff {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ} : f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0

theorem DFinsupp.prod_ne_zero_iff {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [(i : ι) → DecidableEq (β i)] {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ} : f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0

def DFinsupp.sumZeroHom {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [AddCommMonoid γ] (φ : (i : ι) → ZeroHom (β i) γ) : ZeroHom (Π₀ (i : ι), β i) γ

When summing over an ZeroHom, the decidability assumption is not needed, and the result is also an ZeroHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DFinsupp.sumZeroHom_single {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [AddCommMonoid γ] (φ : (i : ι) → ZeroHom (β i) γ) (i : ι) (x : β i) : (sumZeroHom φ) (single i x) = (φ i) x

@[simp]

theorem DFinsupp.sumZeroHom_piSingle {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [AddCommMonoid γ] (i : ι) (φ : ZeroHom (β i) γ) : sumZeroHom (Pi.single i φ) = φ.comp { toFun := fun (x : Π₀ (i : ι), β i) => x i, map_zero' := ⋯ }

theorem DFinsupp.sumZeroHom_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (φ : (i : ι) → ZeroHom (β i) γ) (f : Π₀ (i : ι), β i) : (sumZeroHom φ) f = f.sum fun (x : ι) => ⇑(φ x)

While we didn't need decidable instances to define it, we do to reduce it to a sum

def DFinsupp.sumAddHom {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) : (Π₀ (i : ι), β i) →+ γ

When summing over an AddMonoidHom, the decidability assumption is not needed, and the result is also an AddMonoidHom.

Equations

• DFinsupp.sumAddHom φ = { toZeroHom := DFinsupp.sumZeroHom fun (i : ι) => ↑(φ i), map_add' := ⋯ }

@[simp]

theorem DFinsupp.sumAddHom_toZeroHom {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) : ↑(sumAddHom φ) = sumZeroHom fun (i : ι) => ↑(φ i)

@[simp]

theorem DFinsupp.sumAddHom_single {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) : (sumAddHom φ) (single i x) = (φ i) x

@[simp]

theorem DFinsupp.sumAddHom_piSingle {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (i : ι) (φ : β i →+ γ) : sumAddHom (Pi.single i φ) = φ.comp (evalAddMonoidHom i)

@[simp]

theorem DFinsupp.sumAddHom_comp_single {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) : (sumAddHom f).comp (singleAddHom β i) = f i

theorem DFinsupp.sumAddHom_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (f : Π₀ (i : ι), β i) : (sumAddHom φ) f = f.sum fun (x : ι) => ⇑(φ x)

While we didn't need decidable instances to define it, we do to reduce it to a sum

theorem DFinsupp.sumAddHom_comm {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁ → Type u_1} {β₂ : ι₂ → Type u_2} {γ : Type u_3} [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₁

def DFinsupp.liftAddHom {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] : ((i : ι) → β i →+ γ) ≃+ ((Π₀ (i : ι), β i) →+ γ)

The DFinsupp version of Finsupp.liftAddHom

Equations

• DFinsupp.liftAddHom = { toFun := DFinsupp.sumAddHom, invFun := fun (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) => F.comp (DFinsupp.singleAddHom β i), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem DFinsupp.liftAddHom_symm_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (F : (Π₀ (i : ι), β i) →+ γ) (i : ι) : liftAddHom.symm F i = F.comp (singleAddHom β i)

@[simp]

theorem DFinsupp.liftAddHom_apply {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) : liftAddHom φ = sumAddHom φ

theorem DFinsupp.liftAddHom_singleAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] : liftAddHom (singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)

The DFinsupp version of Finsupp.liftAddHom_singleAddHom

theorem DFinsupp.liftAddHom_apply_single {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) (x : β i) : (liftAddHom f) (single i x) = (f i) x

The DFinsupp version of Finsupp.liftAddHom_apply_single

theorem DFinsupp.liftAddHom_comp_single {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) : (liftAddHom f).comp (singleAddHom β i) = f i

The DFinsupp version of Finsupp.liftAddHom_comp_single

theorem DFinsupp.comp_liftAddHom {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] {δ : Type u_1} [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ] (g : γ →+ δ) (f : (i : ι) → β i →+ γ) : g.comp (liftAddHom f) = liftAddHom fun (a : ι) => g.comp (f a)

The DFinsupp version of Finsupp.comp_liftAddHom

@[simp]

theorem DFinsupp.sumAddHom_zero {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] : (sumAddHom fun (i : ι) => 0) = 0

@[simp]

theorem DFinsupp.sumAddHom_add {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] (g h : (i : ι) → β i →+ γ) : (sumAddHom fun (i : ι) => g i + h i) = sumAddHom g + sumAddHom h

@[simp]

theorem DFinsupp.sumAddHom_singleAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] : sumAddHom (singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)

theorem DFinsupp.comp_sumAddHom {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] {δ : Type u_1} [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] [AddCommMonoid δ] (g : γ →+ δ) (f : (i : ι) → β i →+ γ) : g.comp (sumAddHom f) = sumAddHom fun (a : ι) => g.comp (f a)

theorem DFinsupp.sum_sub_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddGroup (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommGroup γ] {f g : Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂) : (f - g).sum h = f.sum h - g.sum h

theorem DFinsupp.prod_finset_sum_index {ι : Type u} {β : ι → Type v} [DecidableEq ι] {γ : 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₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h

theorem DFinsupp.sum_finset_sum_index {ι : Type u} {β : ι → Type v} [DecidableEq ι] {γ : Type w} {α : Type x} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ} (h_zero : ∀ (i : ι), h i 0 = 0) (h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) : ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h

theorem DFinsupp.prod_sum_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] {ι₁ : 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₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) : (f.sum g).prod h = f.prod fun (i : ι₁) (b : β₁ i) => (g i b).prod h

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

@[simp]

theorem DFinsupp.sum_single {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} : f.sum single = f

theorem DFinsupp.prod_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(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) : ((subtypeDomain p v).prod fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = v.prod h

theorem DFinsupp.sum_subtypeDomain_index {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {v : Π₀ (i : ι), β i} {p : ι → Prop} [DecidablePred p] {h : (i : ι) → β i → γ} (hp : ∀ x ∈ v.support, p x) : ((subtypeDomain p v).sum fun (i : Subtype p) (b : β ↑i) => h (↑i) b) = v.sum h

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

theorem DFinsupp.subtypeDomain_finsupp_sum {γ : Type w} {ι : Type u_1} {β : ι → 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} : subtypeDomain p (s.sum h) = s.sum fun (c : γ) (d : δ c) => subtypeDomain p (h c d)

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.

@[simp]

theorem MonoidHom.coe_dfinsuppProd {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [MulOneClass R] [CommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S) : ⇑(f.prod g) = f.prod fun (a : ι) (b : β a) => ⇑(g a b)

@[simp]

theorem AddMonoidHom.coe_dfinsuppSum {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddZeroClass R] [AddCommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S) : ⇑(f.sum g) = f.sum fun (a : ι) (b : β a) => ⇑(g a b)

@[deprecated AddMonoidHom.coe_dfinsuppSum (since := "2025-04-06")]

theorem AddMonoidHom.coe_dfinsupp_sum {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddZeroClass R] [AddCommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S) : ⇑(f.sum g) = f.sum fun (a : ι) (b : β a) => ⇑(g a b)

Alias of AddMonoidHom.coe_dfinsuppSum.

@[deprecated MonoidHom.coe_dfinsuppProd (since := "2025-04-06")]

theorem MonoidHom.coe_dfinsupp_prod {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [MulOneClass R] [CommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S) : ⇑(f.prod g) = f.prod fun (a : ι) (b : β a) => ⇑(g a b)

Alias of MonoidHom.coe_dfinsuppProd.

theorem MonoidHom.dfinsuppProd_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [MulOneClass R] [CommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S) (r : R) : (f.prod g) r = f.prod fun (a : ι) (b : β a) => (g a b) r

theorem AddMonoidHom.dfinsuppSum_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddZeroClass R] [AddCommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S) (r : R) : (f.sum g) r = f.sum fun (a : ι) (b : β a) => (g a b) r

@[deprecated AddMonoidHom.dfinsuppSum_apply (since := "2025-04-06")]

theorem AddMonoidHom.dfinsupp_sum_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddZeroClass R] [AddCommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S) (r : R) : (f.sum g) r = f.sum fun (a : ι) (b : β a) => (g a b) r

Alias of AddMonoidHom.dfinsuppSum_apply.

@[deprecated MonoidHom.dfinsuppProd_apply (since := "2025-04-06")]

theorem MonoidHom.dfinsupp_prod_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [MulOneClass R] [CommMonoid S] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →* S) (r : R) : (f.prod g) r = f.prod fun (a : ι) (b : β a) => (g a b) r

Alias of MonoidHom.dfinsuppProd_apply.

The above lemmas, repeated for DFinsupp.sumAddHom.

@[simp]

theorem AddMonoidHom.map_dfinsuppSumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddCommMonoid R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (h : R →+ S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) : h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => h.comp (g i)) f

@[deprecated AddMonoidHom.map_dfinsuppSumAddHom (since := "2025-04-06")]

theorem AddMonoidHom.map_dfinsupp_sumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddCommMonoid R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (h : R →+ S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) : h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => h.comp (g i)) f

Alias of AddMonoidHom.map_dfinsuppSumAddHom.

theorem AddMonoidHom.dfinsuppSumAddHom_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddZeroClass R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R →+ S) (r : R) : ((DFinsupp.sumAddHom g) f) r = (DFinsupp.sumAddHom fun (i : ι) => (eval r).comp (g i)) f

@[deprecated AddMonoidHom.dfinsuppSumAddHom_apply (since := "2025-04-06")]

theorem AddMonoidHom.dfinsupp_sumAddHom_apply {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddZeroClass R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R →+ S) (r : R) : ((DFinsupp.sumAddHom g) f) r = (DFinsupp.sumAddHom fun (i : ι) => (eval r).comp (g i)) f

Alias of AddMonoidHom.dfinsuppSumAddHom_apply.

@[simp]

theorem AddMonoidHom.coe_dfinsuppSumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddZeroClass R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R →+ S) : ⇑((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => (coeFn R S).comp (g i)) f

@[deprecated AddMonoidHom.coe_dfinsuppSumAddHom (since := "2025-04-06")]

theorem AddMonoidHom.coe_dfinsupp_sumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddZeroClass R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R →+ S) : ⇑((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => (coeFn R S).comp (g i)) f

Alias of AddMonoidHom.coe_dfinsuppSumAddHom.

@[simp]

theorem RingHom.map_dfinsuppSumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] [(i : ι) → AddZeroClass (β i)] (h : R →+* S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) : h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => h.toAddMonoidHom.comp (g i)) f

@[deprecated RingHom.map_dfinsuppSumAddHom (since := "2025-04-06")]

theorem RingHom.map_dfinsupp_sumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [NonAssocSemiring S] [(i : ι) → AddZeroClass (β i)] (h : R →+* S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) : h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => h.toAddMonoidHom.comp (g i)) f

Alias of RingHom.map_dfinsuppSumAddHom.

@[simp]

theorem AddEquiv.map_dfinsuppSumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddCommMonoid R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (h : R ≃+ S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) : h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => h.toAddMonoidHom.comp (g i)) f

@[deprecated AddEquiv.map_dfinsuppSumAddHom (since := "2025-04-06")]

theorem AddEquiv.map_dfinsupp_sumAddHom {ι : Type u} {β : ι → Type v} [DecidableEq ι] {R : Type u_1} {S : Type u_2} [AddCommMonoid R] [AddCommMonoid S] [(i : ι) → AddZeroClass (β i)] (h : R ≃+ S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ R) : h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun (i : ι) => h.toAddMonoidHom.comp (g i)) f

Alias of AddEquiv.map_dfinsuppSumAddHom.