Documentation

Mathlib.Data.DFinsupp.Sigma

DFinsupp on Sigma types #

Main definitions #

def DFinsupp.sigmaCurry {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType 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 : ι) → α iType 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 : ι) → α iType v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] :
@[simp]
theorem DFinsupp.sigmaCurry_add {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [DecidableEq ι] [(i : ι) → (j : α i) → AddZeroClass (δ i j)] (f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :
@[simp]
theorem DFinsupp.sigmaCurry_smul {ι : Type u} {γ : Type w} {α : ιType u_2} {δ : (i : ι) → α iType v} [DecidableEq ι] [Monoid γ] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) :
@[simp]
theorem DFinsupp.sigmaCurry_single {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Zero (δ i j)] (ij : (i : ι) × α i) (x : δ ij.fst ij.snd) :
def DFinsupp.sigmaUncurry {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType 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 : ι) → α iType 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 : ι) → α iType v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] :
@[simp]
theorem DFinsupp.sigmaUncurry_add {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [DecidableEq ι] [(i : ι) → (j : α i) → AddZeroClass (δ i j)] (f g : Π₀ (i : ι) (j : α i), δ i j) :
@[simp]
theorem DFinsupp.sigmaUncurry_smul {ι : Type u} {γ : Type w} {α : ιType u_2} {δ : (i : ι) → α iType v} [DecidableEq ι] [Monoid γ] [(i : ι) → (j : α i) → AddMonoid (δ i j)] [(i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : ι) (j : α i), δ i j) :
@[simp]
theorem DFinsupp.sigmaUncurry_single {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType v} [DecidableEq ι] [(i : ι) → (j : α i) → Zero (δ i j)] [(i : ι) → DecidableEq (α i)] (i : ι) (j : α i) (x : δ i j) :
def DFinsupp.sigmaCurryEquiv {ι : Type u} {α : ιType u_2} {δ : (i : ι) → α iType 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