# mathlibdocumentation

data.finsupp.to_dfinsupp

# Conversion between finsupp and homogenous dfinsupp#

This module provides conversions between finsupp and dfinsupp. It is in its own file since neither finsupp or dfinsupp depend on each other.

## Main definitions #

• "identity" maps between finsupp and dfinsupp:
• finsupp.to_dfinsupp : (ι →₀ M) → (Π₀ i : ι, M)
• dfinsupp.to_finsupp : (Π₀ i : ι, M) → (ι →₀ M)
• Bundled equiv versions of the above:
• finsupp_equiv_dfinsupp : (ι →₀ M) ≃ (Π₀ i : ι, M)
• finsupp_add_equiv_dfinsupp : (ι →₀ M) ≃+ (Π₀ i : ι, M)
• finsupp_lequiv_dfinsupp R : (ι →₀ M) ≃ₗ[R] (Π₀ i : ι, M)
• stronger versions of finsupp.split:
• sigma_finsupp_equiv_dfinsupp : ((Σ i, η i) →₀ N) ≃ (Π₀ i, (η i →₀ N))
• sigma_finsupp_add_equiv_dfinsupp : ((Σ i, η i) →₀ N) ≃+ (Π₀ i, (η i →₀ N))
• sigma_finsupp_lequiv_dfinsupp : ((Σ i, η i) →₀ N) ≃ₗ[R] (Π₀ i, (η i →₀ N))

## Theorems #

The defining features of these operations is that they preserve the function and support:

• finsupp.to_dfinsupp_coe
• finsupp.to_dfinsupp_support
• dfinsupp.to_finsupp_coe
• dfinsupp.to_finsupp_support

and therefore map finsupp.single to dfinsupp.single and vice versa:

• finsupp.to_dfinsupp_single
• dfinsupp.to_finsupp_single

as well as preserving arithmetic operations.

For the bundled equivalences, we provide lemmas that they reduce to finsupp.to_dfinsupp:

• finsupp_add_equiv_dfinsupp_apply
• finsupp_lequiv_dfinsupp_apply
• finsupp_add_equiv_dfinsupp_symm_apply
• finsupp_lequiv_dfinsupp_symm_apply

## Implementation notes #

We provide dfinsupp.to_finsupp and finsupp_equiv_dfinsupp computably by adding [decidable_eq ι] and [Π m : M, decidable (m ≠ 0)] arguments. To aid with definitional unfolding, these arguments are also present on the noncomputable equivs.

### Basic definitions and lemmas #

def finsupp.to_dfinsupp {ι : Type u_1} {M : Type u_3} [has_zero M] (f : ι →₀ M) :
Π₀ (i : ι), M

Interpret a finsupp as a homogenous dfinsupp.

Equations
@[simp]
theorem finsupp.to_dfinsupp_coe {ι : Type u_1} {M : Type u_3} [has_zero M] (f : ι →₀ M) :
@[simp]
theorem finsupp.to_dfinsupp_single {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] (i : ι) (m : M) :
@[simp]
theorem to_dfinsupp_support {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] (f : ι →₀ M) :
def dfinsupp.to_finsupp {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] (f : Π₀ (i : ι), M) :
ι →₀ M

Interpret a homogenous dfinsupp as a finsupp.

Note that the elaborator has a lot of trouble with this definition - it is often necessary to write (dfinsupp.to_finsupp f : ι →₀ M) instead of f.to_finsupp, as for some unknown reason using dot notation or omitting the type ascription prevents the type being resolved correctly.

Equations
@[simp]
theorem dfinsupp.to_finsupp_coe {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] (f : Π₀ (i : ι), M) :
@[simp]
theorem dfinsupp.to_finsupp_support {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] (f : Π₀ (i : ι), M) :
@[simp]
theorem dfinsupp.to_finsupp_single {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] (i : ι) (m : M) :
@[simp]
theorem finsupp.to_dfinsupp_to_finsupp {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] (f : ι →₀ M) :
@[simp]
theorem dfinsupp.to_finsupp_to_dfinsupp {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] (f : Π₀ (i : ι), M) :

### Lemmas about arithmetic operations #

@[simp]
theorem finsupp.to_dfinsupp_zero {ι : Type u_1} {M : Type u_3} [has_zero M] :
@[simp]
theorem finsupp.to_dfinsupp_add {ι : Type u_1} {M : Type u_3} (f g : ι →₀ M) :
(f + g).to_dfinsupp =
@[simp]
theorem finsupp.to_dfinsupp_neg {ι : Type u_1} {M : Type u_3} [add_group M] (f : ι →₀ M) :
@[simp]
theorem finsupp.to_dfinsupp_sub {ι : Type u_1} {M : Type u_3} [add_group M] (f g : ι →₀ M) :
(f - g).to_dfinsupp =
@[simp]
theorem finsupp.to_dfinsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [monoid R] [add_monoid M] [ M] (r : R) (f : ι →₀ M) :
@[simp]
theorem dfinsupp.to_finsupp_zero {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] :
@[simp]
theorem dfinsupp.to_finsupp_add {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [Π (m : M), decidable (m 0)] (f g : Π₀ (i : ι), M) :
(f + g).to_finsupp =
@[simp]
theorem dfinsupp.to_finsupp_neg {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_group M] [Π (m : M), decidable (m 0)] (f : Π₀ (i : ι), M) :
@[simp]
theorem dfinsupp.to_finsupp_sub {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_group M] [Π (m : M), decidable (m 0)] (f g : Π₀ (i : ι), M) :
(f - g).to_finsupp =
@[simp]
theorem dfinsupp.to_finsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [decidable_eq ι] [monoid R] [add_monoid M] [ M] [Π (m : M), decidable (m 0)] (r : R) (f : Π₀ (i : ι), M) :

### Bundled equivs #

@[simp]
theorem finsupp_equiv_dfinsupp_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] :
@[simp]
theorem finsupp_equiv_dfinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] :
def finsupp_equiv_dfinsupp {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m 0)] :
→₀ M) Π₀ (i : ι), M

finsupp.to_dfinsupp and dfinsupp.to_finsupp together form an equiv.

Equations
def finsupp_add_equiv_dfinsupp {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [Π (m : M), decidable (m 0)] :
→₀ M) ≃+ Π₀ (i : ι), M

The additive version of finsupp.to_finsupp. Note that this is noncomputable because finsupp.has_add is noncomputable.

Equations
@[simp]
theorem finsupp_add_equiv_dfinsupp_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [Π (m : M), decidable (m 0)] :
@[simp]
theorem finsupp_add_equiv_dfinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [Π (m : M), decidable (m 0)] :
def finsupp_lequiv_dfinsupp {ι : Type u_1} (R : Type u_2) {M : Type u_3} [decidable_eq ι] [semiring R] [Π (m : M), decidable (m 0)] [ M] :
→₀ M) ≃ₗ[R] Π₀ (i : ι), M

The additive version of finsupp.to_finsupp. Note that this is noncomputable because finsupp.has_add is noncomputable.

Equations
@[simp]
theorem finsupp_lequiv_dfinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [decidable_eq ι] [semiring R] [Π (m : M), decidable (m 0)] [ M] :
@[simp]
theorem finsupp_lequiv_dfinsupp_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [decidable_eq ι] [semiring R] [Π (m : M), decidable (m 0)] [ M] :
noncomputable def sigma_finsupp_equiv_dfinsupp {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [has_zero N] :
((Σ (i : ι), η i) →₀ N) Π₀ (i : ι), η i →₀ N

finsupp.split is an equivalence between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

Equations
@[simp]
theorem sigma_finsupp_equiv_dfinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [has_zero N] (f : (Σ (i : ι), η i) →₀ N) :
@[simp]
theorem sigma_finsupp_equiv_dfinsupp_symm_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [has_zero N] (f : Π₀ (i : ι), η i →₀ N) (s : Σ (i : ι), η i) :
= (f s.fst) s.snd
@[simp]
theorem sigma_finsupp_equiv_dfinsupp_support {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [has_zero N] (f : (Σ (i : ι), η i) →₀ N) :
@[simp]
theorem sigma_finsupp_equiv_dfinsupp_single {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [has_zero N] (a : Σ (i : ι), η i) (n : N) :
@[simp]
theorem sigma_finsupp_equiv_dfinsupp_add {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} (f g : (Σ (i : ι), η i) →₀ N) :
noncomputable def sigma_finsupp_add_equiv_dfinsupp {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5}  :
((Σ (i : ι), η i) →₀ N) ≃+ Π₀ (i : ι), η i →₀ N

finsupp.split is an additive equivalence between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

Equations
@[simp]
theorem sigma_finsupp_add_equiv_dfinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} (ᾰ : (Σ (i : ι), η i) →₀ N) :
@[simp]
theorem sigma_finsupp_add_equiv_dfinsupp_symm_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} (ᾰ : Π₀ (i : ι), η i →₀ N) :
@[simp]
theorem sigma_finsupp_equiv_dfinsupp_smul {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} {R : Type u_2} [monoid R] [add_monoid N] [ N] (r : R) (f : (Σ (i : ι), η i) →₀ N) :
@[simp]
theorem sigma_finsupp_lequiv_dfinsupp_apply {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [semiring R] [ N] (ᾰ : (Σ (i : ι), η i) →₀ N) :
@[simp]
theorem sigma_finsupp_lequiv_dfinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [semiring R] [ N] (ᾰ : Π₀ (i : ι), η i →₀ N) :
noncomputable def sigma_finsupp_lequiv_dfinsupp {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [semiring R] [ N] :
((Σ (i : ι), η i) →₀ N) ≃ₗ[R] Π₀ (i : ι), η i →₀ N

finsupp.split is a linear equivalence between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

Equations