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

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, ⋯⟩ }

@[simp]

theorem Finsupp.toDFinsupp_coe {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι →₀ M) : ⇑f.toDFinsupp = ⇑f

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

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

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 := ⋯ }

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

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

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

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

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

@[simp]

theorem Finsupp.toDFinsupp_zero {ι : Type u_1} {M : Type u_3} [Zero M] : toDFinsupp 0 = 0

@[simp]

theorem Finsupp.toDFinsupp_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f g : ι →₀ M) : (f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp

@[simp]

theorem Finsupp.toDFinsupp_neg {ι : Type u_1} {M : Type u_3} [AddGroup M] (f : ι →₀ M) : (-f).toDFinsupp = -f.toDFinsupp

@[simp]

theorem Finsupp.toDFinsupp_sub {ι : Type u_1} {M : Type u_3} [AddGroup M] (f g : ι →₀ M) : (f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp

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

@[simp]

theorem DFinsupp.toFinsupp_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] : toFinsupp 0 = 0

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

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

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

@[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 Equivs

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 := ⋯ }

@[simp]

theorem finsuppEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] : ⇑finsuppEquivDFinsupp.symm = DFinsupp.toFinsupp

@[simp]

theorem finsuppEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] : ⇑finsuppEquivDFinsupp = Finsupp.toDFinsupp

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' := ⋯ }

@[simp]

theorem finsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] : ⇑finsuppAddEquivDFinsupp.symm = DFinsupp.toFinsupp

@[simp]

theorem finsuppAddEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] : ⇑finsuppAddEquivDFinsupp = Finsupp.toDFinsupp

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 := ⋯ }

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

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

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.

@[simp]

theorem sigmaFinsuppEquivDFinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [Zero N] (f : (i : ι) × η i →₀ N) : ⇑(sigmaFinsuppEquivDFinsupp f) = f.split

@[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} [DecidableEq ι] [Zero N] [(i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)] (f : (i : ι) × η i →₀ N) : (sigmaFinsuppEquivDFinsupp f).support = f.splitSupport

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

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

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' := ⋯ }

@[simp]

theorem sigmaFinsuppAddEquivDFinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (a : (i : ι) × η i →₀ N) : sigmaFinsuppAddEquivDFinsupp a = sigmaFinsuppEquivDFinsupp a

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

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

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 := ⋯ }

@[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✝

@[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✝