# Documentation

Mathlib.Data.Finsupp.ToDFinsupp

# 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.toDFinsupp : (ι →₀ M) → (Π₀ i : ι, M)
• DFinsupp.toFinsupp : (Π₀ i : ι, M) → (ι →₀ M)
• Bundled equiv versions of the above:
• finsuppEquivDFinsupp : (ι →₀ M) ≃ (Π₀ i : ι, M)
• finsuppAddEquivDFinsupp : (ι →₀ M) ≃+ (Π₀ i : ι, M)
• finsuppLequivDFinsupp R : (ι →₀ M) ≃ₗ[R] (Π₀ i : ι, M)
• stronger versions of Finsupp.split:
• sigmaFinsuppEquivDFinsupp : ((Σ i, η i) →₀ N) ≃ (Π₀ i, (η i →₀ N))
• sigmaFinsuppAddEquivDFinsupp : ((Σ i, η i) →₀ N) ≃+ (Π₀ i, (η i →₀ N))
• sigmaFinsuppLequivDFinsupp : ((Σ i, η i) →₀ N) ≃ₗ[R] (Π₀ i, (η i →₀ N))

## Theorems #

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

• Finsupp.toDFinsupp_coe
• Finsupp.toDFinsupp_support
• DFinsupp.toFinsupp_coe
• DFinsupp.toFinsupp_support

and therefore map Finsupp.single to DFinsupp.single and vice versa:

• Finsupp.toDFinsupp_single
• DFinsupp.toFinsupp_single

as well as preserving arithmetic operations.

For the bundled equivalences, we provide lemmas that they reduce to Finsupp.toDFinsupp:

• 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.toFinsupp and finsuppEquivDFinsupp computably by adding [DecidableEq ι] 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.toDFinsupp {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι →₀ M) :
Π₀ (x : ι), M

Interpret a Finsupp as a homogenous DFinsupp.

Instances For
@[simp]
theorem Finsupp.toDFinsupp_coe {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι →₀ M) :
↑() = f
@[simp]
theorem Finsupp.toDFinsupp_single {ι : Type u_1} {M : Type u_3} [] [Zero M] (i : ι) (m : M) :
(Finsupp.toDFinsupp fun₀ | i => m) =
@[simp]
theorem toDFinsupp_support {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] (f : ι →₀ M) :
= f.support
def DFinsupp.toFinsupp {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), 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.toFinsupp f : ι →₀ M) instead of f.toFinsupp, as for some unknown reason using dot notation or omitting the type ascription prevents the type being resolved correctly.

Instances For
@[simp]
theorem DFinsupp.toFinsupp_coe {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :
↑() = f
@[simp]
theorem DFinsupp.toFinsupp_support {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :
().support =
@[simp]
theorem DFinsupp.toFinsupp_single {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] (i : ι) (m : M) :
= fun₀ | i => m
@[simp]
theorem Finsupp.toDFinsupp_toFinsupp {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] (f : ι →₀ M) :
@[simp]
theorem DFinsupp.toFinsupp_toDFinsupp {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :

### Lemmas about arithmetic operations #

@[simp]
theorem Finsupp.toDFinsupp_zero {ι : Type u_1} {M : Type u_3} [Zero M] :
@[simp]
theorem Finsupp.toDFinsupp_add {ι : Type u_1} {M : Type u_3} [] (f : ι →₀ M) (g : ι →₀ M) :
@[simp]
theorem Finsupp.toDFinsupp_neg {ι : Type u_1} {M : Type u_3} [] (f : ι →₀ M) :
@[simp]
theorem Finsupp.toDFinsupp_sub {ι : Type u_1} {M : Type u_3} [] (f : ι →₀ M) (g : ι →₀ M) :
@[simp]
theorem Finsupp.toDFinsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] (r : R) (f : ι →₀ M) :
@[simp]
theorem DFinsupp.toFinsupp_zero {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] :
@[simp]
theorem DFinsupp.toFinsupp_add {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) (g : Π₀ (x : ι), M) :
@[simp]
theorem DFinsupp.toFinsupp_neg {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :
@[simp]
theorem DFinsupp.toFinsupp_sub {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) (g : Π₀ (x : ι), M) :
@[simp]
theorem DFinsupp.toFinsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [] [(m : M) → Decidable (m 0)] (r : R) (f : Π₀ (x : ι), M) :

### Bundled Equivs #

@[simp]
theorem finsuppEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] :
finsuppEquivDFinsupp = Finsupp.toDFinsupp
@[simp]
theorem finsuppEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] :
finsuppEquivDFinsupp.symm = DFinsupp.toFinsupp
def finsuppEquivDFinsupp {ι : Type u_1} {M : Type u_3} [] [Zero M] [(m : M) → Decidable (m 0)] :
(ι →₀ M) Π₀ (x : ι), M

Finsupp.toDFinsupp and DFinsupp.toFinsupp together form an equiv.

Instances For
@[simp]
theorem finsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
@[simp]
theorem finsuppAddEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
def finsuppAddEquivDFinsupp {ι : Type u_1} {M : Type u_3} [] [] [(m : M) → Decidable (m 0)] :
(ι →₀ M) ≃+ Π₀ (x : ι), M

The additive version of finsupp.toFinsupp. Note that this is noncomputable because Finsupp.add is noncomputable.

Instances For
def finsuppLequivDFinsupp {ι : Type u_1} (R : Type u_2) {M : Type u_3} [] [] [] [(m : M) → Decidable (m 0)] [Module R M] :
(ι →₀ M) ≃ₗ[R] Π₀ (x : ι), M

The additive version of Finsupp.toFinsupp. Note that this is noncomputable because Finsupp.add is noncomputable.

Instances For
@[simp]
theorem finsuppLequivDFinsupp_apply_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [] [] [] [(m : M) → Decidable (m 0)] [Module R M] :
= Finsupp.toDFinsupp
@[simp]
theorem finsuppLequivDFinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [] [] [] [(m : M) → Decidable (m 0)] [Module R M] :
= DFinsupp.toFinsupp

### Stronger versions of Finsupp.split#

def sigmaFinsuppEquivDFinsupp {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [Zero N] :
((i : ι) × η i →₀ N) Π₀ (i : ι), η i →₀ N

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

Instances For
@[simp]
theorem sigmaFinsuppEquivDFinsupp_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [Zero N] (f : (i : ι) × η i →₀ N) :
↑(sigmaFinsuppEquivDFinsupp f) =
@[simp]
theorem sigmaFinsuppEquivDFinsupp_symm_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [Zero N] (f : Π₀ (i : ι), η i →₀ N) (s : (i : ι) × η i) :
↑(sigmaFinsuppEquivDFinsupp.symm f) s = ↑(f s.fst) s.snd
@[simp]
theorem sigmaFinsuppEquivDFinsupp_support {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [] [Zero N] [(i : ι) → (x : η i →₀ N) → Decidable (x 0)] (f : (i : ι) × η i →₀ N) :
DFinsupp.support (sigmaFinsuppEquivDFinsupp f) =
@[simp]
theorem sigmaFinsuppEquivDFinsupp_single {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [] [Zero N] (a : (i : ι) × η i) (n : N) :
(sigmaFinsuppEquivDFinsupp fun₀ | a => n) = DFinsupp.single a.fst fun₀ | a.snd => n
@[simp]
theorem sigmaFinsuppEquivDFinsupp_add {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [] (f : (i : ι) × η i →₀ N) (g : (i : ι) × η i →₀ N) :
sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g
@[simp]
theorem sigmaFinsuppAddEquivDFinsupp_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [] (a : (i : ι) × η i →₀ N) :
@[simp]
theorem sigmaFinsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [] (a : Π₀ (i : ι), η i →₀ N) :
def sigmaFinsuppAddEquivDFinsupp {ι : 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).

Instances For
@[simp]
theorem sigmaFinsuppEquivDFinsupp_smul {ι : Type u_1} {η : ιType u_4} {N : Type u_5} {R : Type u_6} [] [] [] (r : R) (f : (i : ι) × η i →₀ N) :
sigmaFinsuppEquivDFinsupp (r f) = SMul.smul r (sigmaFinsuppEquivDFinsupp f)
@[simp]
theorem sigmaFinsuppLequivDFinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {η : ιType u_4} {N : Type u_5} [] [] [Module R N] (a : Π₀ (i : ι), η i →₀ N) :
= sigmaFinsuppEquivDFinsupp.symm a
@[simp]
theorem sigmaFinsuppLequivDFinsupp_apply {ι : Type u_1} (R : Type u_2) {η : ιType u_4} {N : Type u_5} [] [] [Module R N] (a : (i : ι) × η i →₀ N) :
= sigmaFinsuppEquivDFinsupp a
def sigmaFinsuppLequivDFinsupp {ι : Type u_1} (R : Type u_2) {η : ιType u_4} {N : Type u_5} [] [] [Module R N] :
((i : ι) × η i →₀ N) ≃ₗ[R] Π₀ (i : ι), η i →₀ N

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

Instances For