# `DFinsupp` on `Sigma` types #

## Main definitions #

- `DFinsupp.sigmaCurry`: turn a `DFinsupp` indexed by a `Sigma` type into a `DFinsupp` with two parameters.
- `DFinsupp.sigmaUncurry`: turn a `DFinsupp` with two parameters into a `DFinsupp` indexed by a `Sigma` type. Inverse of `DFinsupp.sigmaCurry`.
- `DFinsupp.sigmaCurryEquiv`: `DFinsupp.sigmaCurry` and `DFinsupp.sigmaUncurry` bundled into a bijection.

source
def DFinsupp.sigmaCurry {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :
Π₀ (i : ι) (j : α i), δ i j

The natural map between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`.

Equations

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

Instances For

source
@[simp]
theorem DFinsupp.sigmaCurry_apply {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) (i : ι) (j : α i) :
(f.sigmaCurry i) j = f ⟨i, j⟩
source
@[simp]
theorem DFinsupp.sigmaCurry_zero {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] :
sigmaCurry 0 = 0
source
@[simp]
theorem DFinsupp.sigmaCurry_add {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → AddZeroClass (δ i j)] (f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :
(f + g).sigmaCurry = f.sigmaCurry + g.sigmaCurry
source
@[simp]
theorem DFinsupp.sigmaCurry_smul {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [Monoid γ] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :
(r • f).sigmaCurry = r • f.sigmaCurry
source
@[simp]
theorem DFinsupp.sigmaCurry_single {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Zero (δ i j)] (ij : (i : ι) × α i) (x : δ ij.fst ij.snd) :
(single ij x).sigmaCurry = single ij.fst (single ij.snd x)
source
def DFinsupp.sigmaUncurry {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι] (f : Π₀ (i : ι) (j : α i), δ i j) :
Π₀ (i : (x : ι) × α x), δ i.fst i.snd

The natural map between `Π₀ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of `curry`.

Equations

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

Instances For

source
@[simp]
theorem DFinsupp.sigmaUncurry_apply {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : ι) (j : α i), δ i j) (i : ι) (j : α i) :
f.sigmaUncurry ⟨i, j⟩ = (f i) j
source
@[simp]
theorem DFinsupp.sigmaUncurry_zero {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] :
sigmaUncurry 0 = 0
source
@[simp]
theorem DFinsupp.sigmaUncurry_add {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → AddZeroClass (δ i j)] (f g : Π₀ (i : ι) (j : α i), δ i j) :
(f + g).sigmaUncurry = f.sigmaUncurry + g.sigmaUncurry
source
@[simp]
theorem DFinsupp.sigmaUncurry_smul {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [Monoid γ] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : ι) (j : α i), δ i j) :
(r • f).sigmaUncurry = r • f.sigmaUncurry
source
@[simp]
theorem DFinsupp.sigmaUncurry_single {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] (i : ι) (j : α i) (x : δ i j) :
(single i (single j x)).sigmaUncurry = single ⟨i, j⟩ x
source
def DFinsupp.sigmaCurryEquiv {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι] :
(Π₀ (i : (x : ι) × α x), δ i.fst i.snd) ≃ Π₀ (i : ι) (j : α i), δ i j

The natural bijection between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`.

This is the dfinsupp version of `Equiv.piCurry`.

Equations

- DFinsupp.sigmaCurryEquiv = { toFun := DFinsupp.sigmaCurry, invFun := DFinsupp.sigmaUncurry, left_inv := ⋯, right_inv := ⋯ }

Instances For