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 #

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
@[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} [add_zero_class M] (f g : ι →₀ M) :
@[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) :
@[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) :
@[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 ι] [add_zero_class M] [Π (m : M), decidable (m 0)] (f g : Π₀ (i : ι), M) :
@[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) :
@[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) :

Bundled equivs #

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