# Conversion between `Finsupp` and homogeneous `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 #

source
def Finsupp.toDFinsupp {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι →₀ M) :
Π₀ (x : ι), M

Interpret a `Finsupp` as a homogeneous `DFinsupp`.

Equations

- f.toDFinsupp = { toFun := ⇑f, support' := Trunc.mk ⟨f.support.val, ⋯⟩ }

Instances For

source
@[simp]
theorem Finsupp.toDFinsupp_coe {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι →₀ M) :
⇑f.toDFinsupp = ⇑f
source
@[simp]
theorem Finsupp.toDFinsupp_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] (i : ι) (m : M) :
(single i m).toDFinsupp = DFinsupp.single i m
source
@[simp]
theorem toDFinsupp_support {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : ι →₀ M) :
f.toDFinsupp.support = f.support
source
def DFinsupp.toFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
ι →₀ M

Interpret a homogeneous `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.

Equations

- f.toFinsupp = { support := f.support, toFun := ⇑f, mem_support_toFun := ⋯ }

Instances For

source
@[simp]
theorem DFinsupp.toFinsupp_coe {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
⇑f.toFinsupp = ⇑f
source
@[simp]
theorem DFinsupp.toFinsupp_support {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
f.toFinsupp.support = f.support
source
@[simp]
theorem DFinsupp.toFinsupp_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (i : ι) (m : M) :
(single i m).toFinsupp = Finsupp.single i m
source
@[simp]
theorem Finsupp.toDFinsupp_toFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : ι →₀ M) :
f.toDFinsupp.toFinsupp = f
source
@[simp]
theorem DFinsupp.toFinsupp_toDFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
f.toFinsupp.toDFinsupp = f

### Lemmas about arithmetic operations #

source
@[simp]
theorem Finsupp.toDFinsupp_zero {ι : Type u_1} {M : Type u_3} [Zero M] :
toDFinsupp 0 = 0
source
@[simp]
theorem Finsupp.toDFinsupp_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f g : ι →₀ M) :
(f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp
source
@[simp]
theorem Finsupp.toDFinsupp_neg {ι : Type u_1} {M : Type u_3} [AddGroup M] (f : ι →₀ M) :
(-f).toDFinsupp = -f.toDFinsupp
source
@[simp]
theorem Finsupp.toDFinsupp_sub {ι : Type u_1} {M : Type u_3} [AddGroup M] (f g : ι →₀ M) :
(f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp
source
@[simp]
theorem Finsupp.toDFinsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid R] [AddMonoid M] [DistribMulAction R M] (r : R) (f : ι →₀ M) :
(r • f).toDFinsupp = r • f.toDFinsupp
source
@[simp]
theorem DFinsupp.toFinsupp_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] :
toFinsupp 0 = 0
source
@[simp]
theorem DFinsupp.toFinsupp_add {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] (f g : Π₀ (x : ι), M) :
(f + g).toFinsupp = f.toFinsupp + g.toFinsupp
source
@[simp]
theorem DFinsupp.toFinsupp_neg {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddGroup M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
(-f).toFinsupp = -f.toFinsupp
source
@[simp]
theorem DFinsupp.toFinsupp_sub {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddGroup M] [(m : M) → Decidable (m ≠ 0)] (f g : Π₀ (x : ι), M) :
(f - g).toFinsupp = f.toFinsupp - g.toFinsupp
source
@[simp]
theorem DFinsupp.toFinsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Monoid R] [AddMonoid M] [DistribMulAction R M] [(m : M) → Decidable (m ≠ 0)] (r : R) (f : Π₀ (x : ι), M) :
(r • f).toFinsupp = r • f.toFinsupp

### Bundled `Equiv`s #

source
def finsuppEquivDFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] :
(ι →₀ M) ≃ Π₀ (x : ι), M

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

Equations

- finsuppEquivDFinsupp = { toFun := Finsupp.toDFinsupp, invFun := DFinsupp.toFinsupp, left_inv := ⋯, right_inv := ⋯ }

Instances For

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

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

Equations

- finsuppAddEquivDFinsupp = { toFun := Finsupp.toDFinsupp, invFun := DFinsupp.toFinsupp, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem finsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] :
⇑finsuppAddEquivDFinsupp.symm = DFinsupp.toFinsupp
source
@[simp]
theorem finsuppAddEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] :
⇑finsuppAddEquivDFinsupp = Finsupp.toDFinsupp
source
def finsuppLequivDFinsupp {ι : Type u_1} (R : Type u_2) {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [(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.

Equations

- finsuppLequivDFinsupp R = { toFun := Finsupp.toDFinsupp, map_add' := ⋯, map_smul' := ⋯, invFun := DFinsupp.toFinsupp, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem finsuppLequivDFinsupp_apply_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [(m : M) → Decidable (m ≠ 0)] [Module R M] :
⇑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
source
@[simp]
theorem finsuppLequivDFinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [(m : M) → Decidable (m ≠ 0)] [Module R M] :
⇑(finsuppLequivDFinsupp R).symm = DFinsupp.toFinsupp

### Stronger versions of `Finsupp.split` #

source
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)`.

Equations

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

Instances For

source
@[simp]
theorem sigmaFinsuppEquivDFinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [Zero N] (f : (i : ι) × η i →₀ N) :
⇑(sigmaFinsuppEquivDFinsupp f) = f.split
source
@[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
source
@[simp]
theorem sigmaFinsuppEquivDFinsupp_support {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [DecidableEq ι] [Zero N] [(i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)] (f : (i : ι) × η i →₀ N) :
(sigmaFinsuppEquivDFinsupp f).support = f.splitSupport
source
@[simp]
theorem sigmaFinsuppEquivDFinsupp_single {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [DecidableEq ι] [Zero N] (a : (i : ι) × η i) (n : N) :
sigmaFinsuppEquivDFinsupp (Finsupp.single a n) = DFinsupp.single a.fst (Finsupp.single a.snd n)
source
@[simp]
theorem sigmaFinsuppEquivDFinsupp_add {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (f g : (i : ι) × η i →₀ N) :
sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g
source
def sigmaFinsuppAddEquivDFinsupp {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] :
((i : ι) × η i →₀ N) ≃+ Π₀ (i : ι), η i →₀ N

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

Equations

- sigmaFinsuppAddEquivDFinsupp = { toFun := ⇑sigmaFinsuppEquivDFinsupp, invFun := ⇑sigmaFinsuppEquivDFinsupp.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem sigmaFinsuppAddEquivDFinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (a : (i : ι) × η i →₀ N) :
sigmaFinsuppAddEquivDFinsupp a = sigmaFinsuppEquivDFinsupp a
source
@[simp]
theorem sigmaFinsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (a : Π₀ (i : ι), η i →₀ N) :
sigmaFinsuppAddEquivDFinsupp.symm a = sigmaFinsuppEquivDFinsupp.symm a
source
@[simp]
theorem sigmaFinsuppEquivDFinsupp_smul {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} {R : Type u_6} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R) (f : (i : ι) × η i →₀ N) :
sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f
source
def sigmaFinsuppLequivDFinsupp {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] :
((i : ι) × η i →₀ N) ≃ₗ[R] Π₀ (i : ι), η i →₀ N

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

Equations

- sigmaFinsuppLequivDFinsupp R = { toFun := sigmaFinsuppAddEquivDFinsupp.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := sigmaFinsuppAddEquivDFinsupp.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem sigmaFinsuppLequivDFinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] (a✝ : Π₀ (i : ι), η i →₀ N) :
(sigmaFinsuppLequivDFinsupp R).symm a✝ = sigmaFinsuppAddEquivDFinsupp.invFun a✝
source
@[simp]
theorem sigmaFinsuppLequivDFinsupp_apply {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] (a✝ : (i : ι) × η i →₀ N) :
(sigmaFinsuppLequivDFinsupp R) a✝ = sigmaFinsuppAddEquivDFinsupp.toFun a✝