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.

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.

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

@[simp]

theorem DFinsupp.sigmaCurry_zero {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] : DFinsupp.sigmaCurry 0 = 0

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

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

@[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) : (DFinsupp.single ij x).sigmaCurry = DFinsupp.single ij.fst (DFinsupp.single ij.snd x)

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.

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

@[simp]

theorem DFinsupp.sigmaUncurry_zero {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] : DFinsupp.sigmaUncurry 0 = 0

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

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

@[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) : (DFinsupp.single i (DFinsupp.single j x)).sigmaUncurry = DFinsupp.single ⟨i, j⟩ x

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