Mathlib.Data.Finsupp.ToDFinsupp

Module docstring

{"# 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 ","### Lemmas about arithmetic operations ","### Bundled Equivs ","### Stronger versions of Finsupp.split "}

Finsupp.toDFinsupp definition

[Zero M] (f : ι →₀ M) : Π₀ _ : ι, M

Full source

/-- Interpret a `Finsupp` as a homogeneous `DFinsupp`. -/
def Finsupp.toDFinsupp [Zero M] (f : ι →₀ M) : Π₀ _ : ι, M where
  toFun := f
  support' :=
    Trunc.mk
      ⟨f.support.1, fun i => (Classical.em (f i = 0)).symm.imp_left Finsupp.mem_support_iff.mpr⟩

Conversion from `Finsupp` to `DFinsupp`

Informal description

The function converts a finitely supported function $f \colon \iota \to M$ (where $M$ has a zero element) into a dependent finitely supported function $\Pi₀ i \colon \iota, M$. The conversion preserves the function values and the support of $f$.

Finsupp.toDFinsupp_coe theorem

[Zero M] (f : ι →₀ M) : ⇑f.toDFinsupp = f

Full source

@[simp]
theorem Finsupp.toDFinsupp_coe [Zero M] (f : ι →₀ M) : ⇑f.toDFinsupp = f :=
  rfl

Function Preservation under `Finsupp` to `DFinsupp` Conversion

Informal description

For any finitely supported function $f \colon \iota \to M$ (where $M$ has a zero element), the underlying function of the converted dependent finitely supported function $f.\text{toDFinsupp}$ is equal to $f$ itself. In other words, the conversion preserves the function values pointwise.

Finsupp.toDFinsupp_single theorem

(i : ι) (m : M) : (Finsupp.single i m).toDFinsupp = DFinsupp.single i m

Full source

@[simp]
theorem Finsupp.toDFinsupp_single (i : ι) (m : M) :
    (Finsupp.single i m).toDFinsupp = DFinsupp.single i m := by
  ext
  simp [Finsupp.single_apply, DFinsupp.single_apply]

Preservation of Single-Element Construction under `Finsupp` to `DFinsupp` Conversion

Informal description

For any index $i \in \iota$ and element $m \in M$, the conversion of the finitely supported function `Finsupp.single i m` to a dependent finitely supported function yields `DFinsupp.single i m$. That is, the conversion preserves the single-element construction in both representations.

toDFinsupp_support theorem

(f : ι →₀ M) : f.toDFinsupp.support = f.support

Full source

@[simp]
theorem toDFinsupp_support (f : ι →₀ M) : f.toDFinsupp.support = f.support := by
  ext
  simp

Support Preservation under `Finsupp` to `DFinsupp` Conversion

Informal description

For any finitely supported function $f \colon \iota \to M$, the support of the converted dependent finitely supported function $f.\text{toDFinsupp}$ is equal to the support of $f$.

DFinsupp.toFinsupp definition

(f : Π₀ _ : ι, M) : ι →₀ M

Full source

/-- 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. -/
def DFinsupp.toFinsupp (f : Π₀ _ : ι, M) : ι →₀ M :=
  ⟨f.support, f, fun i => by simp only [DFinsupp.mem_support_iff]⟩

Conversion from dependent functions with finite support to finitely supported functions

Informal description

The function converts a homogeneous dependent function with finite support (of type `Π₀ i : ι, M`) to a finitely supported function (of type `ι →₀ M`). The resulting function has the same support and values as the original dependent function.

DFinsupp.toFinsupp_coe theorem

(f : Π₀ _ : ι, M) : ⇑f.toFinsupp = f

Full source

@[simp]
theorem DFinsupp.toFinsupp_coe (f : Π₀ _ : ι, M) : ⇑f.toFinsupp = f :=
  rfl

Coefficient Preservation in Conversion from DFinsupp to Finsupp

Informal description

For any dependent function with finite support $f : \Pi\_{i : \iota} M$, the underlying function of its conversion to a finitely supported function equals $f$ itself, i.e., $f.\text{toFinsupp} = f$.

DFinsupp.toFinsupp_support theorem

(f : Π₀ _ : ι, M) : f.toFinsupp.support = f.support

Full source

@[simp]
theorem DFinsupp.toFinsupp_support (f : Π₀ _ : ι, M) : f.toFinsupp.support = f.support := by
  ext
  simp

Support Preservation in Conversion from DFinsupp to Finsupp

Informal description

For any dependent function with finite support $f : \Pi\_{i \in \iota} M$, the support of the converted finitely supported function $f.\text{toFinsupp}$ is equal to the support of $f$.

DFinsupp.toFinsupp_single theorem

(i : ι) (m : M) : (DFinsupp.single i m : Π₀ _ : ι, M).toFinsupp = Finsupp.single i m

Full source

@[simp]
theorem DFinsupp.toFinsupp_single (i : ι) (m : M) :
    (DFinsupp.single i m : Π₀ _ : ι, M).toFinsupp = Finsupp.single i m := by
  ext
  simp [Finsupp.single_apply, DFinsupp.single_apply]

Conversion Preserves Single Element Construction: $\text{DFinsupp.single}\ i\ m \to \text{Finsupp.single}\ i\ m$

Informal description

For any index $i \in \iota$ and element $m \in M$, the conversion of the dependent function with finite support $\text{DFinsupp.single}\ i\ m$ to a finitely supported function equals the finitely supported function $\text{Finsupp.single}\ i\ m$.

Finsupp.toDFinsupp_toFinsupp theorem

(f : ι →₀ M) : f.toDFinsupp.toFinsupp = f

Full source

@[simp]
theorem Finsupp.toDFinsupp_toFinsupp (f : ι →₀ M) : f.toDFinsupp.toFinsupp = f :=
  DFunLike.coe_injective rfl

Round-trip Conversion Identity: $\text{Finsupp} \to \text{DFinsupp} \to \text{Finsupp}$

Informal description

For any finitely supported function $f \colon \iota \to M$, the composition of the conversion from `Finsupp` to `DFinsupp` followed by the conversion back to `Finsupp` yields the original function $f$. That is, $\text{toFinsupp}(\text{toDFinsupp}(f)) = f$.

DFinsupp.toFinsupp_toDFinsupp theorem

(f : Π₀ _ : ι, M) : f.toFinsupp.toDFinsupp = f

Full source

@[simp]
theorem DFinsupp.toFinsupp_toDFinsupp (f : Π₀ _ : ι, M) : f.toFinsupp.toDFinsupp = f :=
  DFunLike.coe_injective rfl

Round-trip Conversion Identity: $\text{DFinsupp} \to \text{Finsupp} \to \text{DFinsupp}$

Informal description

For any dependent function with finite support $f \colon \Pi₀ i \colon \iota, M$, the composition of the conversion from `DFinsupp` to `Finsupp` followed by the conversion back to `DFinsupp` yields the original function $f$. That is, $\text{toDFinsupp}(\text{toFinsupp}(f)) = f$.

Finsupp.toDFinsupp_zero theorem

[Zero M] : (0 : ι →₀ M).toDFinsupp = 0

Full source

@[simp]
theorem toDFinsupp_zero [Zero M] : (0 : ι →₀ M).toDFinsupp = 0 :=
  DFunLike.coe_injective rfl

Conversion of Zero Function from `Finsupp` to `DFinsupp` Preserves Zero

Informal description

For any type $M$ with a zero element, the conversion of the zero function in `Finsupp` (i.e., $0 \colon \iota \to M$) to `DFinsupp` yields the zero function in `DFinsupp`. That is, $\text{toDFinsupp}(0) = 0$.

Finsupp.toDFinsupp_add theorem

[AddZeroClass M] (f g : ι →₀ M) : (f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp

Full source

@[simp]
theorem toDFinsupp_add [AddZeroClass M] (f g : ι →₀ M) :
    (f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp :=
  DFunLike.coe_injective rfl

Additivity of `Finsupp.toDFinsupp`

Informal description

For any two finitely supported functions $f, g \colon \iota \to M$ (where $M$ has an addition operation with a zero element), the conversion to dependent finitely supported functions preserves addition, i.e., $(f + g).\text{toDFinsupp} = f.\text{toDFinsupp} + g.\text{toDFinsupp}$.

Finsupp.toDFinsupp_neg theorem

[AddGroup M] (f : ι →₀ M) : (-f).toDFinsupp = -f.toDFinsupp

Full source

@[simp]
theorem toDFinsupp_neg [AddGroup M] (f : ι →₀ M) : (-f).toDFinsupp = -f.toDFinsupp :=
  DFunLike.coe_injective rfl

Negation Preservation in `Finsupp.toDFinsupp` Conversion

Informal description

For any finitely supported function $f \colon \iota \to M$ where $M$ is an additive group, the conversion to a dependent finitely supported function preserves negation, i.e., $(-f).\text{toDFinsupp} = -f.\text{toDFinsupp}$.

Finsupp.toDFinsupp_sub theorem

[AddGroup M] (f g : ι →₀ M) : (f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp

Full source

@[simp]
theorem toDFinsupp_sub [AddGroup M] (f g : ι →₀ M) :
    (f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp :=
  DFunLike.coe_injective rfl

Subtraction Preservation in `Finsupp.toDFinsupp` Conversion

Informal description

For any finitely supported functions $f, g \colon \iota \to M$ where $M$ is an additive group, the conversion to dependent finitely supported functions preserves subtraction, i.e., $(f - g).\text{toDFinsupp} = f.\text{toDFinsupp} - g.\text{toDFinsupp}$.

Finsupp.toDFinsupp_smul theorem

[Monoid R] [AddMonoid M] [DistribMulAction R M] (r : R) (f : ι →₀ M) : (r • f).toDFinsupp = r • f.toDFinsupp

Full source

@[simp]
theorem toDFinsupp_smul [Monoid R] [AddMonoid M] [DistribMulAction R M] (r : R) (f : ι →₀ M) :
    (r • f).toDFinsupp = r • f.toDFinsupp :=
  DFunLike.coe_injective rfl

Scalar Multiplication Preservation in `Finsupp.toDFinsupp` Conversion

Informal description

Let $R$ be a monoid, $M$ an additive monoid, and suppose $R$ acts distributively on $M$. For any scalar $r \in R$ and any finitely supported function $f \colon \iota \to M$, the conversion of the scalar multiple $r \cdot f$ to a dependent finitely supported function equals the scalar multiple of the converted function, i.e., $(r \cdot f).\text{toDFinsupp} = r \cdot f.\text{toDFinsupp}$.

DFinsupp.toFinsupp_zero theorem

[Zero M] [∀ m : M, Decidable (m ≠ 0)] : toFinsupp 0 = (0 : ι →₀ M)

Full source

@[simp]
theorem toFinsupp_zero [Zero M] [∀ m : M, Decidable (m ≠ 0)] : toFinsupp 0 = (0 : ι →₀ M) :=
  DFunLike.coe_injective rfl

Zero Preservation in Conversion from DFinsupp to Finsupp

Informal description

For a type $M$ with a zero element and a decidable predicate for non-zero elements, the conversion of the zero dependent function with finite support (of type $\Pi₀ i : \iota, M$) to a finitely supported function (of type $\iota \to₀ M$) yields the zero function.

DFinsupp.toFinsupp_add theorem

 [AddZeroClass M] [∀ m : M, Decidable (m ≠ 0)] (f g : Π₀ _ : ι, M) :
  (toFinsupp (f + g) : ι →₀ M) = toFinsupp f + toFinsupp g

Full source

@[simp]
theorem toFinsupp_add [AddZeroClass M] [∀ m : M, Decidable (m ≠ 0)] (f g : Π₀ _ : ι, M) :
    (toFinsupp (f + g) : ι →₀ M) = toFinsupp f + toFinsupp g :=
  DFunLike.coe_injective <| DFinsupp.coe_add _ _

Additivity of Conversion from DFinsupp to Finsupp

Informal description

Let $M$ be an additive monoid with a decidable predicate for non-zero elements. For any two dependent functions with finite support $f, g : \Pi\_{i : \iota} M$, the conversion to finitely supported functions satisfies $\text{toFinsupp}(f + g) = \text{toFinsupp}(f) + \text{toFinsupp}(g)$.

DFinsupp.toFinsupp_neg theorem

[AddGroup M] [∀ m : M, Decidable (m ≠ 0)] (f : Π₀ _ : ι, M) : (toFinsupp (-f) : ι →₀ M) = -toFinsupp f

Full source

@[simp]
theorem toFinsupp_neg [AddGroup M] [∀ m : M, Decidable (m ≠ 0)] (f : Π₀ _ : ι, M) :
    (toFinsupp (-f) : ι →₀ M) = -toFinsupp f :=
  DFunLike.coe_injective <| DFinsupp.coe_neg _

Negation Preserved in Conversion from DFinsupp to Finsupp

Informal description

Let $M$ be an additive group with a decidable predicate for non-zero elements. For any dependent function with finite support $f : \Pi\_{i : \iota} M$, the conversion to a finitely supported function satisfies $\text{toFinsupp}(-f) = -\text{toFinsupp}(f)$.

DFinsupp.toFinsupp_sub theorem

 [AddGroup M] [∀ m : M, Decidable (m ≠ 0)] (f g : Π₀ _ : ι, M) :
  (toFinsupp (f - g) : ι →₀ M) = toFinsupp f - toFinsupp g

Full source

@[simp]
theorem toFinsupp_sub [AddGroup M] [∀ m : M, Decidable (m ≠ 0)] (f g : Π₀ _ : ι, M) :
    (toFinsupp (f - g) : ι →₀ M) = toFinsupp f - toFinsupp g :=
  DFunLike.coe_injective <| DFinsupp.coe_sub _ _

Subtraction Preserved in Conversion from DFinsupp to Finsupp

Informal description

Let $M$ be an additive group with a decidable predicate for non-zero elements. For any two dependent functions with finite support $f, g : \Pi\_{i : \iota} M$, the conversion to finitely supported functions satisfies $\text{toFinsupp}(f - g) = \text{toFinsupp}(f) - \text{toFinsupp}(g)$.

DFinsupp.toFinsupp_smul theorem

 [Monoid R] [AddMonoid M] [DistribMulAction R M] [∀ m : M, Decidable (m ≠ 0)] (r : R) (f : Π₀ _ : ι, M) :
  (toFinsupp (r • f) : ι →₀ M) = r • toFinsupp f

Full source

@[simp]
theorem toFinsupp_smul [Monoid R] [AddMonoid M] [DistribMulAction R M] [∀ m : M, Decidable (m ≠ 0)]
    (r : R) (f : Π₀ _ : ι, M) : (toFinsupp (r • f) : ι →₀ M) = r • toFinsupp f :=
  DFunLike.coe_injective <| DFinsupp.coe_smul _ _

Scalar Multiplication Preserved in Conversion from DFinsupp to Finsupp

Informal description

Let $R$ be a monoid acting distributively on an additive monoid $M$, with a decidable predicate for non-zero elements in $M$. For any scalar $r \in R$ and any dependent function with finite support $f : \Pi\_{i : \iota} M$, the conversion to a finitely supported function satisfies $\text{toFinsupp}(r \cdot f) = r \cdot \text{toFinsupp}(f)$.

finsuppEquivDFinsupp definition

[DecidableEq ι] [Zero M] [∀ m : M, Decidable (m ≠ 0)] : (ι →₀ M) ≃ Π₀ _ : ι, M

Full source

/-- `Finsupp.toDFinsupp` and `DFinsupp.toFinsupp` together form an equiv. -/
@[simps -fullyApplied]
def finsuppEquivDFinsupp [DecidableEq ι] [Zero M] [∀ m : M, Decidable (m ≠ 0)] :
    (ι →₀ M) ≃ Π₀ _ : ι, M where
  toFun := Finsupp.toDFinsupp
  invFun := DFinsupp.toFinsupp
  left_inv := Finsupp.toDFinsupp_toFinsupp
  right_inv := DFinsupp.toFinsupp_toDFinsupp

Equivalence between finitely supported functions and homogeneous dependent functions

Informal description

The equivalence `finsuppEquivDFinsupp` establishes a bijection between finitely supported functions `ι →₀ M` and homogeneous dependent functions with finite support `Π₀ i : ι, M`. The conversion preserves function values and supports, with: - The forward direction given by `Finsupp.toDFinsupp` - The backward direction given by `DFinsupp.toFinsupp` - The composition in either direction yields the original function (`toDFinsupp ∘ toFinsupp = id` and `toFinsupp ∘ toDFinsupp = id`) This holds when: - The index type `ι` has decidable equality - The codomain `M` has a zero element - There's a decidable predicate for non-zero elements in `M`

finsuppAddEquivDFinsupp definition

[DecidableEq ι] [AddZeroClass M] [∀ m : M, Decidable (m ≠ 0)] : (ι →₀ M) ≃+ Π₀ _ : ι, M

Full source

/-- The additive version of `finsupp.toFinsupp`. Note that this is `noncomputable` because
`Finsupp.add` is noncomputable. -/
@[simps -fullyApplied]
def finsuppAddEquivDFinsupp [DecidableEq ι] [AddZeroClass M] [∀ m : M, Decidable (m ≠ 0)] :
    (ι →₀ M) ≃+ Π₀ _ : ι, M :=
  { finsuppEquivDFinsupp with
    toFun := Finsupp.toDFinsupp
    invFun := DFinsupp.toFinsupp
    map_add' := Finsupp.toDFinsupp_add }

Additive equivalence between finitely supported functions and dependent functions

Informal description

The additive equivalence `finsuppAddEquivDFinsupp` establishes an isomorphism between the additive structures of finitely supported functions `ι →₀ M` and homogeneous dependent functions with finite support `Π₀ i : ι, M`. The conversion preserves function values, supports, and addition, with: - The forward direction given by `Finsupp.toDFinsupp` - The backward direction given by `DFinsupp.toFinsupp` - The composition in either direction yields the original function - The addition operation is preserved: `toDFinsupp(f + g) = toDFinsupp(f) + toDFinsupp(g)` This holds when: - The index type `ι` has decidable equality - The codomain `M` forms an additive monoid with zero - There's a decidable predicate for non-zero elements in `M`

finsuppLequivDFinsupp definition

 [DecidableEq ι] [Semiring R] [AddCommMonoid M] [∀ m : M, Decidable (m ≠ 0)] [Module R M] : (ι →₀ M) ≃ₗ[R] Π₀ _ : ι, M

Full source

/-- The additive version of `Finsupp.toFinsupp`. Note that this is `noncomputable` because
`Finsupp.add` is noncomputable. -/
def finsuppLequivDFinsupp [DecidableEq ι] [Semiring R] [AddCommMonoid M]
    [∀ m : M, Decidable (m ≠ 0)] [Module R M] : (ι →₀ M) ≃ₗ[R] Π₀ _ : ι, M :=
  { finsuppEquivDFinsupp with
    toFun := Finsupp.toDFinsupp
    invFun := DFinsupp.toFinsupp
    map_smul' := Finsupp.toDFinsupp_smul
    map_add' := Finsupp.toDFinsupp_add }

Linear equivalence between finitely supported functions and homogeneous dependent functions

Informal description

The linear equivalence `finsuppLequivDFinsupp` establishes a bijection between finitely supported functions `ι →₀ M` and homogeneous dependent functions with finite support `Π₀ i : ι, M`, which preserves addition and scalar multiplication. The conversion preserves function values and supports, with: - The forward direction given by `Finsupp.toDFinsupp` - The backward direction given by `DFinsupp.toFinsupp` - The composition in either direction yields the original function (`toDFinsupp ∘ toFinsupp = id` and `toFinsupp ∘ toDFinsupp = id`) This holds when: - The index type `ι` has decidable equality - The codomain `M` is an additive commutative monoid - There's a decidable predicate for non-zero elements in `M` - `M` is a module over a semiring `R`

finsuppLequivDFinsupp_apply_apply theorem

 [DecidableEq ι] [Semiring R] [AddCommMonoid M] [∀ m : M, Decidable (m ≠ 0)] [Module R M] :
  (↑(finsuppLequivDFinsupp (M := M) R) : (ι →₀ M) → _) = Finsupp.toDFinsupp

Full source

@[simp]
theorem finsuppLequivDFinsupp_apply_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]
    [∀ m : M, Decidable (m ≠ 0)] [Module R M] :
    (↑(finsuppLequivDFinsupp (M := M) R) : (ι →₀ M) → _) = Finsupp.toDFinsupp := rfl

Linear equivalence `finsuppLequivDFinsupp` coincides with `Finsupp.toDFinsupp`

Informal description

For a semiring $R$, an additive commutative monoid $M$ (with decidable equality for non-zero elements), and an index type $\iota$ with decidable equality, the linear equivalence `finsuppLequivDFinsupp` between finitely supported functions $\iota \to₀ M$ and homogeneous dependent functions $\Pi₀ i : \iota, M$ satisfies that its underlying function is equal to `Finsupp.toDFinsupp`. That is, the coercion of `finsuppLequivDFinsupp` to a function coincides with the conversion map from `Finsupp` to `DFinsupp`.

finsuppLequivDFinsupp_symm_apply theorem

 [DecidableEq ι] [Semiring R] [AddCommMonoid M] [∀ m : M, Decidable (m ≠ 0)] [Module R M] :
  ↑(LinearEquiv.symm (finsuppLequivDFinsupp (ι := ι) (M := M) R)) = DFinsupp.toFinsupp

Full source

@[simp]
theorem finsuppLequivDFinsupp_symm_apply [DecidableEq ι] [Semiring R] [AddCommMonoid M]
    [∀ m : M, Decidable (m ≠ 0)] [Module R M] :
    ↑(LinearEquiv.symm (finsuppLequivDFinsupp (ι := ι) (M := M) R)) = DFinsupp.toFinsupp :=
  rfl

Inverse of Linear Equivalence Between Finitely Supported and Dependent Functions is Conversion Function

Informal description

Let $ι$ be a type with decidable equality, $R$ a semiring, and $M$ an $R$-module that is also an additive commutative monoid with a decidable predicate for non-zero elements. Then the inverse of the linear equivalence `finsuppLequivDFinsupp` from finitely supported functions $ι →₀ M$ to homogeneous dependent functions with finite support $Π₀ i : ι, M$ is equal to the conversion function `DFinsupp.toFinsupp`. That is, for any $f ∈ Π₀ i : ι, M$, we have: \[ \text{finsuppLequivDFinsupp}^{-1}(f) = \text{DFinsupp.toFinsupp}(f). \]

sigmaFinsuppEquivDFinsupp definition

[Zero N] : ((Σ i, η i) →₀ N) ≃ Π₀ i, η i →₀ N

Full source

/-- `Finsupp.split` is an equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
def sigmaFinsuppEquivDFinsupp [Zero N] : ((Σ i, η i) →₀ N) ≃ Π₀ i, η i →₀ N where
  toFun f := ⟨split f, Trunc.mk ⟨(splitSupport f : Finset ι).val, fun i => by
          rw [← Finset.mem_def, mem_splitSupport_iff_nonzero]
          exact (em _).symm⟩⟩
  invFun f := by
    haveI := Classical.decEq ι
    haveI := fun i => Classical.decEq (η i →₀ N)
    refine
      onFinset (Finset.sigma f.support fun j => (f j).support) (fun ji => f ji.1 ji.2) fun g hg =>
        Finset.mem_sigma.mpr ⟨?_, mem_support_iff.mpr hg⟩
    simp only [Ne, DFinsupp.mem_support_toFun]
    intro h
    dsimp at hg
    rw [h] at hg
    simp only [coe_zero, Pi.zero_apply, not_true] at hg
  left_inv f := by ext; simp [split]
  right_inv f := by ext; simp [split]

Equivalence between finitely supported functions and dependent finitely supported functions

Informal description

The equivalence `sigmaFinsuppEquivDFinsupp` establishes a bijection between the type of finitely supported functions `(Σ i, η i) →₀ N` (functions from a dependent pair type to `N` with finite support) and the type of dependent finitely supported functions `Π₀ i, (η i →₀ N)` (where each component is itself a finitely supported function). This equivalence maps a function `f : (Σ i, η i) →₀ N` to its split form `Finsupp.split f`, which is a dependent function where each component `i` is the restriction of `f` to `η i`. The inverse operation reconstructs the original function from its split form by combining the components. The equivalence preserves the support structure, meaning that the support of the original function corresponds appropriately to the supports in the dependent version.

sigmaFinsuppEquivDFinsupp_apply theorem

[Zero N] (f : (Σ i, η i) →₀ N) : (sigmaFinsuppEquivDFinsupp f : ∀ i, η i →₀ N) = Finsupp.split f

Full source

@[simp]
theorem sigmaFinsuppEquivDFinsupp_apply [Zero N] (f : (Σ i, η i) →₀ N) :
    (sigmaFinsuppEquivDFinsupp f : ∀ i, η i →₀ N) = Finsupp.split f :=
  rfl

Equivalence Application Formula: $\text{sigmaFinsuppEquivDFinsupp}(f) = \text{Finsupp.split}(f)$

Informal description

For any finitely supported function $f : (\Sigma i, \eta i) \to N$ where $N$ has a zero element, the application of the equivalence $\text{sigmaFinsuppEquivDFinsupp}$ to $f$ yields a dependent finitely supported function that is equal to $\text{Finsupp.split}(f)$, i.e., \[ \text{sigmaFinsuppEquivDFinsupp}(f) = \text{Finsupp.split}(f). \]

sigmaFinsuppEquivDFinsupp_symm_apply theorem

 [Zero N] (f : Π₀ i, η i →₀ N) (s : Σ i, η i) : (sigmaFinsuppEquivDFinsupp.symm f : (Σ i, η i) →₀ N) s = f s.1 s.2

Full source

@[simp]
theorem sigmaFinsuppEquivDFinsupp_symm_apply [Zero N] (f : Π₀ i, η i →₀ N) (s : Σ i, η i) :
    (sigmaFinsuppEquivDFinsupp.symm f : (Σ i, η i) →₀ N) s = f s.1 s.2 :=
  rfl

Inverse Equivalence Formula: $\text{sigmaFinsuppEquivDFinsupp}^{-1}(f)(i,j) = f_i(j)$

Informal description

For any dependent finitely supported function $f : \Pi_{i} (\eta i \to N)$ where $N$ has a zero element, and for any element $s = (i, j) \in \Sigma i, \eta i$, the application of the inverse equivalence $\text{sigmaFinsuppEquivDFinsupp}^{-1}(f)$ to $s$ satisfies: \[ \text{sigmaFinsuppEquivDFinsupp}^{-1}(f)(s) = f_i(j), \] where $f_i$ is the $i$-th component of $f$ (a finitely supported function $\eta i \to N$).

sigmaFinsuppEquivDFinsupp_support theorem

 [DecidableEq ι] [Zero N] [∀ (i : ι) (x : η i →₀ N), Decidable (x ≠ 0)] (f : (Σ i, η i) →₀ N) :
  (sigmaFinsuppEquivDFinsupp f).support = Finsupp.splitSupport f

Full source

@[simp]
theorem sigmaFinsuppEquivDFinsupp_support [DecidableEq ι] [Zero N]
    [∀ (i : ι) (x : η i →₀ N), Decidable (x ≠ 0)] (f : (Σ i, η i) →₀ N) :
    (sigmaFinsuppEquivDFinsupp f).support = Finsupp.splitSupport f := by
  ext
  rw [DFinsupp.mem_support_toFun]
  exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm

Support Preservation under $\text{sigmaFinsuppEquivDFinsupp}$

Informal description

For a finitely supported function $f : (\Sigma i, \eta i) \to N$ where $N$ has a zero element, the support of the dependent finitely supported function obtained via the equivalence $\text{sigmaFinsuppEquivDFinsupp}(f)$ is equal to the split support of $f$, i.e., \[ \text{support}(\text{sigmaFinsuppEquivDFinsupp}(f)) = \text{splitSupport}(f). \]

sigmaFinsuppEquivDFinsupp_single theorem

 [DecidableEq ι] [Zero N] (a : Σ i, η i) (n : N) :
  sigmaFinsuppEquivDFinsupp (Finsupp.single a n) = @DFinsupp.single _ (fun i => η i →₀ N) _ _ a.1 (Finsupp.single a.2 n)

Full source

@[simp]
theorem sigmaFinsuppEquivDFinsupp_single [DecidableEq ι] [Zero N] (a : Σ i, η i) (n : N) :
    sigmaFinsuppEquivDFinsupp (Finsupp.single a n) =
      @DFinsupp.single _ (fun i => η i →₀ N) _ _ a.1 (Finsupp.single a.2 n) := by
  obtain ⟨i, a⟩ := a
  ext j b
  by_cases h : i = j
  · subst h
    classical simp [split_apply, Finsupp.single_apply]
  suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
  have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h]
  classical rw [Finsupp.single_apply, if_neg H]

Preservation of Single Function under $\text{sigmaFinsuppEquivDFinsupp}$

Informal description

For any element $a = (i, j)$ in the dependent pair type $\Sigma i, \eta i$ and any element $n$ in a type $N$ with a zero element, the equivalence `sigmaFinsuppEquivDFinsupp` maps the finitely supported single function `Finsupp.single a n` to the dependent finitely supported single function `DFinsupp.single i (Finsupp.single j n)`. In other words, the equivalence preserves the single function construction, mapping it from the non-dependent to the dependent setting.

sigmaFinsuppEquivDFinsupp_add theorem

 [AddZeroClass N] (f g : (Σ i, η i) →₀ N) :
  sigmaFinsuppEquivDFinsupp (f + g) = (sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g : Π₀ i : ι, η i →₀ N)

Full source

@[simp]
theorem sigmaFinsuppEquivDFinsupp_add [AddZeroClass N] (f g : (Σ i, η i) →₀ N) :
    sigmaFinsuppEquivDFinsupp (f + g) =
      (sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g : Π₀ i : ι, η i →₀ N) := by
  ext
  rfl

Preservation of Addition under $\text{sigmaFinsuppEquivDFinsupp}$

Informal description

For any two finitely supported functions $f, g : (\Sigma i, \eta i) \to N$ where $N$ is an additive zero class, the equivalence $\text{sigmaFinsuppEquivDFinsupp}$ preserves addition, i.e., \[ \text{sigmaFinsuppEquivDFinsupp}(f + g) = \text{sigmaFinsuppEquivDFinsupp}(f) + \text{sigmaFinsuppEquivDFinsupp}(g). \]

sigmaFinsuppAddEquivDFinsupp definition

[AddZeroClass N] : ((Σ i, η i) →₀ N) ≃+ Π₀ i, η i →₀ N

Full source

/-- `Finsupp.split` is an additive equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
@[simps]
def sigmaFinsuppAddEquivDFinsupp [AddZeroClass N] : ((Σ i, η i) →₀ N) ≃+ Π₀ i, η i →₀ N :=
  { sigmaFinsuppEquivDFinsupp with
    toFun := sigmaFinsuppEquivDFinsupp
    invFun := sigmaFinsuppEquivDFinsupp.symm
    map_add' := sigmaFinsuppEquivDFinsupp_add }

Additive equivalence between finitely supported functions and dependent finitely supported functions

Informal description

The additive equivalence `sigmaFinsuppAddEquivDFinsupp` establishes a bijection between the type of finitely supported functions `(Σ i, η i) →₀ N` (functions from a dependent pair type to `N` with finite support) and the type of dependent finitely supported functions `Π₀ i, (η i →₀ N)` (where each component is itself a finitely supported function), preserving the additive structure. This means that for any two finitely supported functions `f, g : (Σ i, η i) →₀ N`, the equivalence satisfies: \[ \text{sigmaFinsuppAddEquivDFinsupp}(f + g) = \text{sigmaFinsuppAddEquivDFinsupp}(f) + \text{sigmaFinsuppAddEquivDFinsupp}(g). \]

sigmaFinsuppEquivDFinsupp_smul theorem

 {R} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R) (f : (Σ i, η i) →₀ N) :
  sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f

Full source

@[simp]
theorem sigmaFinsuppEquivDFinsupp_smul {R} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R)
    (f : (Σ i, η i) →₀ N) :
    sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f := by
  ext
  rfl

Preservation of Scalar Multiplication under $\text{sigmaFinsuppEquivDFinsupp}$

Informal description

Let $R$ be a monoid, $N$ be an additive monoid equipped with a distributive multiplicative action of $R$, and $r \in R$. For any finitely supported function $f : (\Sigma i, \eta i) \to N$, the equivalence $\text{sigmaFinsuppEquivDFinsupp}$ preserves scalar multiplication, i.e., \[ \text{sigmaFinsuppEquivDFinsupp}(r \cdot f) = r \cdot \text{sigmaFinsuppEquivDFinsupp}(f). \]

sigmaFinsuppLequivDFinsupp definition

[AddCommMonoid N] [Module R N] : ((Σ i, η i) →₀ N) ≃ₗ[R] Π₀ i, η i →₀ N

Full source

/-- `Finsupp.split` is a linear equivalence between `(Σ i, η i) →₀ N` and `Π₀ i, (η i →₀ N)`. -/
@[simps]
def sigmaFinsuppLequivDFinsupp [AddCommMonoid N] [Module R N] :
    ((Σ i, η i) →₀ N) ≃ₗ[R] Π₀ i, η i →₀ N :=
  { sigmaFinsuppAddEquivDFinsupp with
    map_smul' := sigmaFinsuppEquivDFinsupp_smul }

Linear equivalence between finitely supported functions and dependent finitely supported functions

Informal description

The linear equivalence `sigmaFinsuppLequivDFinsupp` establishes a bijection between the type of finitely supported functions `(Σ i, η i) →₀ N` (functions from a dependent pair type to `N` with finite support) and the type of dependent finitely supported functions `Π₀ i, (η i →₀ N)` (where each component is itself a finitely supported function), preserving both the additive and linear structures. This means that for any scalar `r` in `R` and any finitely supported functions `f, g : (Σ i, η i) →₀ N`, the equivalence satisfies: \[ \text{sigmaFinsuppLequivDFinsupp}(f + g) = \text{sigmaFinsuppLequivDFinsupp}(f) + \text{sigmaFinsuppLequivDFinsupp}(g) \] and \[ \text{sigmaFinsuppLequivDFinsupp}(r \cdot f) = r \cdot \text{sigmaFinsuppLequivDFinsupp}(f). \]