mathlib3 documentation

data.finsupp.to_dfinsupp

Conversion between `finsupp` and homogenous `dfinsupp` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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

as well as preserving arithmetic operations.

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

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

f.to_dfinsupp = {to_fun := ⇑f, support' := trunc.mk ⟨f.support.val, _⟩}

@[simp]

theorem finsupp.to_dfinsupp_coe {ι : Type u_1} {M : Type u_3} [has_zero M] (f : ι →₀ M) :

⇑(f.to_dfinsupp) = ⇑f

@[simp]

theorem finsupp.to_dfinsupp_single {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] (i : ι) (m : M) :

(finsupp.single i m).to_dfinsupp = dfinsupp.single i 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) :

f.to_dfinsupp.support = f.support

def dfinsupp.to_finsupp {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m ≠ 0)] (f : Π₀ (i : ι), 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

f.to_finsupp = {support := f.support, to_fun := ⇑f, mem_support_to_fun := _}

@[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) :

⇑(f.to_finsupp) = ⇑f

@[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) :

f.to_finsupp.support = f.support

@[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) :

(dfinsupp.single i m).to_finsupp = finsupp.single i 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) :

f.to_dfinsupp.to_finsupp = f

@[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) :

f.to_finsupp.to_dfinsupp = f

Lemmas about arithmetic operations #

@[simp]

theorem finsupp.to_dfinsupp_zero {ι : Type u_1} {M : Type u_3} [has_zero M] :

0.to_dfinsupp = 0

@[simp]

theorem finsupp.to_dfinsupp_add {ι : Type u_1} {M : Type u_3} [add_zero_class M] (f g : ι →₀ M) :

(f + g).to_dfinsupp = f.to_dfinsupp + g.to_dfinsupp

@[simp]

theorem finsupp.to_dfinsupp_neg {ι : Type u_1} {M : Type u_3} [add_group M] (f : ι →₀ M) :

(-f).to_dfinsupp = -f.to_dfinsupp

@[simp]

theorem finsupp.to_dfinsupp_sub {ι : Type u_1} {M : Type u_3} [add_group M] (f g : ι →₀ M) :

(f - g).to_dfinsupp = f.to_dfinsupp - 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] [distrib_mul_action R M] (r : R) (f : ι →₀ M) :

(r • f).to_dfinsupp = r • f.to_dfinsupp

@[simp]

theorem dfinsupp.to_finsupp_zero {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m ≠ 0)] :

0.to_finsupp = 0

@[simp]

theorem dfinsupp.to_finsupp_add {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_zero_class M] [Π (m : M), decidable (m ≠ 0)] (f g : Π₀ (i : ι), M) :

(f + g).to_finsupp = f.to_finsupp + 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) :

(-f).to_finsupp = -f.to_finsupp

@[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 = f.to_finsupp - 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] [distrib_mul_action R M] [Π (m : M), decidable (m ≠ 0)] (r : R) (f : Π₀ (i : ι), M) :

(r • f).to_finsupp = r • f.to_finsupp

Bundled `equiv`s #

@[simp]

theorem finsupp_equiv_dfinsupp_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m ≠ 0)] :

⇑finsupp_equiv_dfinsupp = finsupp.to_dfinsupp

@[simp]

theorem finsupp_equiv_dfinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [has_zero M] [Π (m : M), decidable (m ≠ 0)] :

⇑(finsupp_equiv_dfinsupp.symm) = dfinsupp.to_finsupp

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

finsupp_equiv_dfinsupp = {to_fun := finsupp.to_dfinsupp _inst_2, inv_fun := dfinsupp.to_finsupp (λ (m : M), _inst_3 m), left_inv := _, right_inv := _}

def finsupp_add_equiv_dfinsupp {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_zero_class M] [Π (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

finsupp_add_equiv_dfinsupp = {to_fun := finsupp.to_dfinsupp (add_zero_class.to_has_zero M), inv_fun := dfinsupp.to_finsupp (λ (m : M), _inst_3 m), left_inv := _, right_inv := _, map_add' := _}

@[simp]

theorem finsupp_add_equiv_dfinsupp_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_zero_class M] [Π (m : M), decidable (m ≠ 0)] :

⇑finsupp_add_equiv_dfinsupp = finsupp.to_dfinsupp

@[simp]

theorem finsupp_add_equiv_dfinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_zero_class M] [Π (m : M), decidable (m ≠ 0)] :

⇑(finsupp_add_equiv_dfinsupp.symm) = dfinsupp.to_finsupp

def finsupp_lequiv_dfinsupp {ι : Type u_1} (R : Type u_2) {M : Type u_3} [decidable_eq ι] [semiring R] [add_comm_monoid M] [Π (m : M), decidable (m ≠ 0)] [module R M] :

(ι →₀ M) ≃ₗ[R] Π₀ (i : ι), M

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

Equations

finsupp_lequiv_dfinsupp R = {to_fun := finsupp.to_dfinsupp (add_zero_class.to_has_zero M), map_add' := _, map_smul' := _, inv_fun := dfinsupp.to_finsupp (λ (m : M), _inst_4 m), left_inv := _, right_inv := _}

@[simp]

theorem finsupp_lequiv_dfinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [decidable_eq ι] [semiring R] [add_comm_monoid M] [Π (m : M), decidable (m ≠ 0)] [module R M] :

⇑((finsupp_lequiv_dfinsupp R).symm) = dfinsupp.to_finsupp

@[simp]

theorem finsupp_lequiv_dfinsupp_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [decidable_eq ι] [semiring R] [add_comm_monoid M] [Π (m : M), decidable (m ≠ 0)] [module R M] :

⇑(finsupp_lequiv_dfinsupp R) = finsupp.to_dfinsupp

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

sigma_finsupp_equiv_dfinsupp = {to_fun := λ (f : (Σ (i : ι), η i) →₀ N), {to_fun := f.split, support' := trunc.mk ⟨f.split_support.val, _⟩}, inv_fun := λ (f : Π₀ (i : ι), η i →₀ N), finsupp.on_finset (f.support.sigma (λ (j : ι), (⇑f j).support)) (λ (ji : Σ (i : ι), η i), ⇑(⇑f ji.fst) ji.snd) _, left_inv := _, right_inv := _}

@[simp]

theorem sigma_finsupp_equiv_dfinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [has_zero N] (f : (Σ (i : ι), η i) →₀ N) :

⇑(⇑sigma_finsupp_equiv_dfinsupp f) = f.split

@[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) :

⇑(⇑(sigma_finsupp_equiv_dfinsupp.symm) f) s = ⇑(⇑f s.fst) s.snd

@[simp]

theorem sigma_finsupp_equiv_dfinsupp_support {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [decidable_eq ι] [has_zero N] [Π (i : ι) (x : η i →₀ N), decidable (x ≠ 0)] (f : (Σ (i : ι), η i) →₀ N) :

(⇑sigma_finsupp_equiv_dfinsupp f).support = f.split_support

@[simp]

theorem sigma_finsupp_equiv_dfinsupp_single {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [decidable_eq ι] [has_zero N] (a : Σ (i : ι), η i) (n : N) :

⇑sigma_finsupp_equiv_dfinsupp (finsupp.single a n) = dfinsupp.single a.fst (finsupp.single a.snd n)

@[simp]

theorem sigma_finsupp_equiv_dfinsupp_add {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [add_zero_class N] (f g : (Σ (i : ι), η i) →₀ N) :

⇑sigma_finsupp_equiv_dfinsupp (f + g) = ⇑sigma_finsupp_equiv_dfinsupp f + ⇑sigma_finsupp_equiv_dfinsupp g

noncomputable def sigma_finsupp_add_equiv_dfinsupp {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [add_zero_class N] :

((Σ (i : ι), η i) →₀ N) ≃+ Π₀ (i : ι), η i →₀ N

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

Equations

sigma_finsupp_add_equiv_dfinsupp = {to_fun := ⇑sigma_finsupp_equiv_dfinsupp, inv_fun := ⇑(sigma_finsupp_equiv_dfinsupp.symm), left_inv := _, right_inv := _, map_add' := _}

@[simp]

theorem sigma_finsupp_add_equiv_dfinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [add_zero_class N] (ᾰ : (Σ (i : ι), η i) →₀ N) :

⇑sigma_finsupp_add_equiv_dfinsupp ᾰ = ⇑sigma_finsupp_equiv_dfinsupp ᾰ

@[simp]

theorem sigma_finsupp_add_equiv_dfinsupp_symm_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [add_zero_class N] (ᾰ : Π₀ (i : ι), η i →₀ N) :

⇑(sigma_finsupp_add_equiv_dfinsupp.symm) ᾰ = ⇑(sigma_finsupp_equiv_dfinsupp.symm) ᾰ

@[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] [distrib_mul_action R N] (r : R) (f : (Σ (i : ι), η i) →₀ N) :

⇑sigma_finsupp_equiv_dfinsupp (r • f) = r • ⇑sigma_finsupp_equiv_dfinsupp f

@[simp]

theorem sigma_finsupp_lequiv_dfinsupp_apply {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [semiring R] [add_comm_monoid N] [module R N] (ᾰ : (Σ (i : ι), η i) →₀ N) :

⇑(sigma_finsupp_lequiv_dfinsupp R) ᾰ = sigma_finsupp_add_equiv_dfinsupp.to_fun ᾰ

@[simp]

theorem sigma_finsupp_lequiv_dfinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [semiring R] [add_comm_monoid N] [module R N] (ᾰ : Π₀ (i : ι), η i →₀ N) :

⇑((sigma_finsupp_lequiv_dfinsupp R).symm) ᾰ = sigma_finsupp_add_equiv_dfinsupp.inv_fun ᾰ

noncomputable def sigma_finsupp_lequiv_dfinsupp {ι : Type u_1} (R : Type u_2) {η : ι → Type u_4} {N : Type u_5} [semiring R] [add_comm_monoid 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

sigma_finsupp_lequiv_dfinsupp R = {to_fun := sigma_finsupp_add_equiv_dfinsupp.to_fun, map_add' := _, map_smul' := _, inv_fun := sigma_finsupp_add_equiv_dfinsupp.inv_fun, left_inv := _, right_inv := _}