Mathlib.Data.DFinsupp.Sigma

DFinsupp.sigmaCurry definition

[∀ i j, Zero (δ i j)] (f : Π₀ (i : Σ _, _), δ i.1 i.2) : Π₀ (i) (j), δ i j

Full source

/-- The natural map between `Π₀ (i : Σ i, α i), δ i.1 i.2` and `Π₀ i (j : α i), δ i j`. -/
def sigmaCurry [∀ i j, Zero (δ i j)] (f : Π₀ (i : Σ _, _), δ i.1 i.2) :
    Π₀ (i) (j), δ i j where
  toFun := fun i ↦
  { toFun := fun j ↦ f ⟨i, j⟩,
    support' := f.support'.map (fun ⟨m, hm⟩ ↦
      ⟨m.filterMap (fun ⟨i', j'⟩ ↦ if h : i' = i then some <| h.rec j' else none),
        fun j ↦ (hm ⟨i, j⟩).imp_left (fun h ↦ (m.mem_filterMap _).mpr ⟨⟨i, j⟩, h, dif_pos rfl⟩)⟩) }
  support' := f.support'.map (fun ⟨m, hm⟩ ↦
    ⟨m.map Sigma.fst, fun i ↦ Decidable.or_iff_not_imp_left.mpr (fun h ↦ DFinsupp.ext
      (fun j ↦ (hm ⟨i, j⟩).resolve_left (fun H ↦ (Multiset.mem_map.not.mp h) ⟨⟨i, j⟩, H, rfl⟩)))⟩)

Currying of dependent functions with finite support

Informal description

Given a family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has a zero element, the function `DFinsupp.sigmaCurry` transforms a dependent function $f$ with finite support indexed by pairs $(i,j) \in \Sigma i, \alpha i$ into a dependent function with two parameters $i$ and $j$, where $i$ ranges over some index type $\iota$ and $j$ ranges over $\alpha i$. The resulting function maps each pair $(i,j)$ to $f(i,j)$.

DFinsupp.sigmaCurry_apply theorem

[∀ i j, Zero (δ i j)] (f : Π₀ (i : Σ _, _), δ i.1 i.2) (i : ι) (j : α i) : sigmaCurry f i j = f ⟨i, j⟩

Full source

@[simp]
theorem sigmaCurry_apply [∀ i j, Zero (δ i j)] (f : Π₀ (i : Σ _, _), δ i.1 i.2) (i : ι) (j : α i) :
    sigmaCurry f i j = f ⟨i, j⟩ :=
  rfl

Evaluation of Curried Dependent Function with Finite Support

Informal description

For a family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has a zero element, and for any dependent function $f$ with finite support indexed by pairs $(i,j) \in \Sigma i, \alpha i$, the curried function `sigmaCurry f` satisfies $\text{sigmaCurry}\, f\, i\, j = f \langle i, j \rangle$ for all $i \in \iota$ and $j \in \alpha i$.

DFinsupp.sigmaCurry_zero theorem

[∀ i j, Zero (δ i j)] : sigmaCurry (0 : Π₀ (i : Σ _, _), δ i.1 i.2) = 0

Full source

@[simp]
theorem sigmaCurry_zero [∀ i j, Zero (δ i j)] :
    sigmaCurry (0 : Π₀ (i : Σ _, _), δ i.1 i.2) = 0 :=
  rfl

Currying Preserves the Zero Function

Informal description

For any family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has a zero element, the currying operation `sigmaCurry` maps the zero function (indexed by pairs $(i,j) \in \Sigma i, \alpha i$) to the zero function (with two parameters $i$ and $j$). That is, $\text{sigmaCurry}\, 0 = 0$.

DFinsupp.sigmaCurry_add theorem

 [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i : Σ _, _), δ i.1 i.2) :
  #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
      we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
  sigmaCurry (f + g) = (sigmaCurry f + sigmaCurry g : Π₀ (i) (j), δ i j)

Full source

@[simp]
theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i : Σ _, _), δ i.1 i.2) :
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
    we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
    sigmaCurry (f + g) = (sigmaCurry f + sigmaCurry g : Π₀ (i) (j), δ i j) := by
  ext (i j)
  rfl

Additivity of Currying for Dependent Functions with Finite Support

Informal description

For any family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has an additive zero class structure, and for any two dependent functions $f, g$ with finite support indexed by pairs $(i,j) \in \Sigma i, \alpha i$, the currying operation preserves addition. That is, \[ \text{sigmaCurry}(f + g) = \text{sigmaCurry}(f) + \text{sigmaCurry}(g). \]

DFinsupp.sigmaCurry_smul theorem

 [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i : Σ _, _), δ i.1 i.2) :
  #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
      we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
  sigmaCurry (r • f) = (r • sigmaCurry f : Π₀ (i) (j), δ i j)

Full source

@[simp]
theorem sigmaCurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)]
    (r : γ) (f : Π₀ (i : Σ _, _), δ i.1 i.2) :
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
    we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
    sigmaCurry (r • f) = (r • sigmaCurry f : Π₀ (i) (j), δ i j) := by
  ext (i j)
  rfl

Currying Commutes with Scalar Multiplication in Dependent Functions with Finite Support

Informal description

Let $\gamma$ be a monoid and let $(\delta_{i,j})_{i,j}$ be a family of additive monoids equipped with a distributive scalar multiplication action by $\gamma$. For any scalar $r \in \gamma$ and any dependent function $f$ with finite support indexed by pairs $(i,j) \in \Sigma i, \alpha i$, the currying operation commutes with scalar multiplication, i.e., $\text{sigmaCurry}(r \cdot f) = r \cdot \text{sigmaCurry}(f)$.

DFinsupp.sigmaCurry_single theorem

 [∀ i, DecidableEq (α i)] [∀ i j, Zero (δ i j)] (ij : Σ i, α i) (x : δ ij.1 ij.2) :
  sigmaCurry (single ij x) = single ij.1 (single ij.2 x : Π₀ j, δ ij.1 j)

Full source

@[simp]
theorem sigmaCurry_single [∀ i, DecidableEq (α i)] [∀ i j, Zero (δ i j)]
    (ij : Σ i, α i) (x : δ ij.1 ij.2) :
    sigmaCurry (single ij x) = single ij.1 (single ij.2 x : Π₀ j, δ ij.1 j) := by
  obtain ⟨i, j⟩ := ij
  ext i' j'
  dsimp only
  rw [sigmaCurry_apply]
  obtain rfl | hi := eq_or_ne i i'
  · rw [single_eq_same]
    obtain rfl | hj := eq_or_ne j j'
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne, single_eq_of_ne hj]
      simpa using hj
  · rw [single_eq_of_ne, single_eq_of_ne hi, zero_apply]
    simp [hi]

Currying of Single-Element Dependent Function: $\text{sigmaCurry}(\text{single}_{(i,j)}(x)) = \text{single}_i(\text{single}_j(x))$

Informal description

For any family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has a zero element, and for any pair of indices $(i,j) \in \Sigma i, \alpha i$ and element $x \in \delta_{i,j}$, the curried version of the single-element dependent function $\text{single}_{(i,j)}(x)$ equals the dependent function that maps $i$ to $\text{single}_j(x)$ (which is itself a dependent function mapping $j$ to $x$ and all other indices to zero). More precisely: \[ \text{sigmaCurry}\, (\text{single}_{(i,j)}(x)) = \text{single}_i(\text{single}_j(x)) \] where $\text{single}_j(x) \in \Pi₀ j, \delta_{i,j}$ is the dependent Kronecker delta function that maps $j$ to $x$ and all other $j'$ to zero.

DFinsupp.sigmaUncurry definition

[∀ i j, Zero (δ i j)] [DecidableEq ι] (f : Π₀ (i) (j), δ i j) : Π₀ i : Σ _, _, δ i.1 i.2

Full source

/-- The natural map between `Π₀ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
`curry`. -/
def sigmaUncurry [∀ i j, Zero (δ i j)] [DecidableEq ι] (f : Π₀ (i) (j), δ i j) :
    Π₀ i : Σ_, _, δ i.1 i.2 where
  toFun i := f i.1 i.2
  support' :=
    f.support'.bind fun s =>
      (Trunc.finChoice (fun i : ↥s.val.toFinset => (f i).support')).map fun fs =>
        ⟨s.val.toFinset.attach.val.bind fun i => (fs i).val.map (Sigma.mk i.val), by
          rintro ⟨i, a⟩
          cases s.prop i with
          | inl hi =>
            cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
            | inl ha =>
              left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach
            | inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]
          | inr hi => right; simp [toFun_eq_coe f ▸ hi]⟩

Uncurrying of dependent functions with finite support

Informal description

Given a dependent function with finite support `f : Π₀ (i) (j), δ i j` (where each `δ i j` has a zero element), the function `sigmaUncurry` transforms it into a dependent function with finite support indexed by the sigma type `Σ i, α i`, where the value at `⟨i, j⟩` is given by `f i j`. This operation is the inverse of `sigmaCurry`.

DFinsupp.sigmaUncurry_apply theorem

[∀ i j, Zero (δ i j)] (f : Π₀ (i) (j), δ i j) (i : ι) (j : α i) : sigmaUncurry f ⟨i, j⟩ = f i j

Full source

@[simp]
theorem sigmaUncurry_apply [∀ i j, Zero (δ i j)]
    (f : Π₀ (i) (j), δ i j) (i : ι) (j : α i) :
    sigmaUncurry f ⟨i, j⟩ = f i j :=
  rfl

Evaluation of Uncurried Dependent Function with Finite Support

Informal description

For any dependent function with finite support $f \in \Pi_0 (i) (j), \delta i j$ (where each $\delta i j$ has a zero element), and for any indices $i \in \iota$ and $j \in \alpha i$, the uncurried function $\mathrm{sigmaUncurry}\, f$ evaluated at the pair $\langle i, j \rangle$ equals $f i j$.

DFinsupp.sigmaUncurry_zero theorem

[∀ i j, Zero (δ i j)] : sigmaUncurry (0 : Π₀ (i) (j), δ i j) = 0

Full source

@[simp]
theorem sigmaUncurry_zero [∀ i j, Zero (δ i j)] :
    sigmaUncurry (0 : Π₀ (i) (j), δ i j) = 0 :=
  rfl

Uncurrying Preserves Zero in Dependent Functions with Finite Support

Informal description

For any family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has a zero element, the uncurrying operation applied to the zero dependent function with finite support yields the zero function, i.e., $\text{sigmaUncurry}(0) = 0$.

DFinsupp.sigmaUncurry_add theorem

[∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i) (j), δ i j) : sigmaUncurry (f + g) = sigmaUncurry f + sigmaUncurry g

Full source

@[simp]
theorem sigmaUncurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i) (j), δ i j) :
    sigmaUncurry (f + g) = sigmaUncurry f + sigmaUncurry g :=
  DFunLike.coe_injective rfl

Additivity of Uncurrying for Dependent Functions with Finite Support

Informal description

For any family of types $(\delta_{i,j})_{i \in \iota, j \in \alpha_i}$ where each $\delta_{i,j}$ has an additive zero class structure, and for any two dependent functions with finite support $f, g \in \Pi₀ (i) (j), \delta_{i,j}$, the uncurrying operation preserves addition, i.e., \[ \mathrm{sigmaUncurry}(f + g) = \mathrm{sigmaUncurry}(f) + \mathrm{sigmaUncurry}(g). \]

DFinsupp.sigmaUncurry_smul theorem

 [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ (i) (j), δ i j) :
  sigmaUncurry (r • f) = r • sigmaUncurry f

Full source

@[simp]
theorem sigmaUncurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)]
    [∀ i j, DistribMulAction γ (δ i j)]
    (r : γ) (f : Π₀ (i) (j), δ i j) : sigmaUncurry (r • f) = r • sigmaUncurry f :=
  DFunLike.coe_injective rfl

Scalar Multiplication Commutes with Uncurrying in Dependent Functions with Finite Support

Informal description

Let $\gamma$ be a monoid, and let $(\delta_{i,j})_{i,j}$ be a family of add monoids equipped with a distributive multiplicative action of $\gamma$. For any scalar $r \in \gamma$ and any dependent function with finite support $f \in \Pi₀ (i) (j), \delta_{i,j}$, the uncurrying operation commutes with scalar multiplication, i.e., \[ \text{sigmaUncurry}(r \cdot f) = r \cdot \text{sigmaUncurry}(f). \]

DFinsupp.sigmaUncurry_single theorem

 [∀ i j, Zero (δ i j)] [∀ i, DecidableEq (α i)] (i) (j : α i) (x : δ i j) :
  sigmaUncurry (single i (single j x : Π₀ j : α i, δ i j)) = single ⟨i, j⟩ (by exact x)

Full source

@[simp]
theorem sigmaUncurry_single [∀ i j, Zero (δ i j)] [∀ i, DecidableEq (α i)]
    (i) (j : α i) (x : δ i j) :
    sigmaUncurry (single i (single j x : Π₀ j : α i, δ i j)) = single ⟨i, j⟩ (by exact x) := by
  ext ⟨i', j'⟩
  dsimp only
  rw [sigmaUncurry_apply]
  obtain rfl | hi := eq_or_ne i i'
  · rw [single_eq_same]
    obtain rfl | hj := eq_or_ne j j'
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne hj, single_eq_of_ne]
      simpa using hj
  · rw [single_eq_of_ne hi, single_eq_of_ne, zero_apply]
    simp [hi]

Uncurrying of Dependent Kronecker Delta Functions: $\mathrm{sigmaUncurry}\, (\mathrm{single}_i (\mathrm{single}_j x)) = \mathrm{single}_{\langle i, j \rangle} x$

Informal description

For any family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has a zero element, and for any indices $i \in \iota$, $j \in \alpha i$, and element $x \in \delta_{i,j}$, the uncurried version of the dependent Kronecker delta function $\mathrm{single}_i(\mathrm{single}_j(x))$ is equal to the dependent Kronecker delta function $\mathrm{single}_{\langle i,j \rangle}(x)$. In other words, the following equality holds: \[ \mathrm{sigmaUncurry}\, \big(\mathrm{single}_i (\mathrm{single}_j x)\big) = \mathrm{single}_{\langle i, j \rangle} x. \]

DFinsupp.sigmaCurryEquiv definition

[∀ i j, Zero (δ i j)] [DecidableEq ι] : (Π₀ i : Σ _, _, δ i.1 i.2) ≃ Π₀ (i) (j), δ i j

Full source

/-- 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`. -/
def sigmaCurryEquiv [∀ i j, Zero (δ i j)] [DecidableEq ι] :
    (Π₀ i : Σ_, _, δ i.1 i.2) ≃ Π₀ (i) (j), δ i j where
  toFun := sigmaCurry
  invFun := sigmaUncurry
  left_inv f := by
    ext ⟨i, j⟩
    rw [sigmaUncurry_apply, sigmaCurry_apply]
  right_inv f := by
    ext i j
    rw [sigmaCurry_apply, sigmaUncurry_apply]

Bijection between sigma-indexed and curried dependent functions with finite support

Informal description

Given a family of types $(\delta_{i,j})_{i,j}$ where each $\delta_{i,j}$ has a zero element, and an index type $\iota$ with decidable equality, there is a natural bijection between the type of dependent functions with finite support indexed by pairs $(i,j) \in \Sigma i, \alpha i$ and the type of dependent functions with two parameters $i \in \iota$ and $j \in \alpha i$. The bijection is given by: - The forward map `sigmaCurry` transforms a function $f$ indexed by $\Sigma i, \alpha i$ into a function that takes two arguments $i$ and $j$ and returns $f(i,j)$. - The inverse map `sigmaUncurry` transforms a two-argument function $g$ into a function indexed by $\Sigma i, \alpha i$ that maps $\langle i, j \rangle$ to $g(i,j)$.

Main definitions