Mathlib.LinearAlgebra.Multilinear.Curry

LinearMap.uncurryLeft definition

(f : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂) : MultilinearMap R M M₂

Full source

/-- Given a linear map `f` from `M 0` to multilinear maps on `n` variables,
construct the corresponding multilinear map on `n+1` variables obtained by concatenating
the variables, given by `m ↦ f (m 0) (tail m)` -/
def LinearMap.uncurryLeft (f : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂) :
    MultilinearMap R M M₂ :=
  MultilinearMap.mk' (fun m ↦ f (m 0) (tail m))
    (fun m i x y ↦ by
      by_cases h : i = 0
      · subst i
        simp only [update_self, map_add, tail_update_zero, MultilinearMap.add_apply]
      · simp_rw [update_of_ne (Ne.symm h)]
        revert x y
        rw [← succ_pred i h]
        intro x y
        rw [tail_update_succ, MultilinearMap.map_update_add, tail_update_succ, tail_update_succ])
    (fun m i c x ↦ by
      by_cases h : i = 0
      · subst i
        simp only [update_self, map_smul, tail_update_zero, MultilinearMap.smul_apply]
      · simp_rw [update_of_ne (Ne.symm h)]
        revert x
        rw [← succ_pred i h]
        intro x
        rw [tail_update_succ, tail_update_succ, MultilinearMap.map_update_smul])

Uncurrying a linear map into a multilinear map

Informal description

Given a linear map $ f $ from $ M(0) $ to the space of multilinear maps on $ n $ variables (indexed by $ \text{Fin} \, n $), the function constructs a multilinear map on $ n+1 $ variables (indexed by $ \text{Fin} \, (n+1) $) by evaluating $ f $ at the first variable $ m(0) $ and applying the resulting multilinear map to the tail of $ m $, i.e., $ m \mapsto f (m(0)) (\text{tail} \, m) $.

LinearMap.uncurryLeft_apply theorem

 (f : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂) (m : ∀ i, M i) : f.uncurryLeft m = f (m 0) (tail m)

Full source

@[simp]
theorem LinearMap.uncurryLeft_apply (f : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂)
    (m : ∀ i, M i) : f.uncurryLeft m = f (m 0) (tail m) :=
  rfl

Evaluation Formula for Uncurried Left Multilinear Map

Informal description

Let $R$ be a semiring, $M : \text{Fin}(n+1) \to \text{Type}$ be a family of $R$-modules, and $M₂$ be an $R$-module. Given a linear map $f : M(0) \to \text{MultilinearMap}_R (M \circ \text{Fin.succ}) M₂$ and a tuple $m \in \prod_{i \in \text{Fin}(n+1)} M(i)$, the uncurried multilinear map satisfies \[ \text{uncurryLeft}(f)(m) = f(m(0))(\text{tail}(m)), \] where $\text{tail}(m)$ is the tuple obtained by removing the first element of $m$.

MultilinearMap.curryLeft definition

(f : MultilinearMap R M M₂) : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂

Full source

/-- Given a multilinear map `f` in `n+1` variables, split the first variable to obtain
a linear map into multilinear maps in `n` variables, given by `x ↦ (m ↦ f (cons x m))`. -/
def MultilinearMap.curryLeft (f : MultilinearMap R M M₂) :
    M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂ where
  toFun x := MultilinearMap.mk' (fun m => f (cons x m))
  map_add' x y := by
    ext m
    exact cons_add f m x y
  map_smul' c x := by
    ext m
    exact cons_smul f m c x

Left currying of a multilinear map

Informal description

Given a multilinear map $ f $ in $ n+1 $ variables (indexed by $\text{Fin} (n+1)$), the function $\text{curryLeft}$ constructs a linear map from $ M(0) $ to the space of multilinear maps in the remaining $ n $ variables (indexed by $\text{Fin} n$). Specifically, for any $ x \in M(0) $, the resulting multilinear map is given by $ m \mapsto f(\text{cons}\, x\, m) $, where $\text{cons}$ prepends $ x $ to the tuple $ m $.

MultilinearMap.curryLeft_apply theorem

(f : MultilinearMap R M M₂) (x : M 0) (m : ∀ i : Fin n, M i.succ) : f.curryLeft x m = f (cons x m)

Full source

@[simp]
theorem MultilinearMap.curryLeft_apply (f : MultilinearMap R M M₂) (x : M 0)
    (m : ∀ i : Fin n, M i.succ) : f.curryLeft x m = f (cons x m) :=
  rfl

Evaluation of Left-Curried Multilinear Map: $(f.\text{curryLeft}\, x)\, m = f(\text{cons}\, x\, m)$

Informal description

Let $R$ be a semiring, $M : \text{Fin}(n+1) \to \text{Type}$ be a family of $R$-modules, and $M₂$ be an $R$-module. Given a multilinear map $f : \text{MultilinearMap}\, R\, M\, M₂$ in $n+1$ variables, an element $x \in M(0)$, and a tuple $m \in \prod_{i \in \text{Fin} n} M(i.\text{succ})$, the left-curried map $f.\text{curryLeft}$ satisfies $(f.\text{curryLeft}\, x)\, m = f(\text{cons}\, x\, m)$, where $\text{cons}$ prepends $x$ to the tuple $m$.

LinearMap.curry_uncurryLeft theorem

(f : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂) : f.uncurryLeft.curryLeft = f

Full source

@[simp]
theorem LinearMap.curry_uncurryLeft (f : M 0 →ₗ[R] MultilinearMap R (fun i :
    Fin n => M i.succ) M₂) : f.uncurryLeft.curryLeft = f := by
  ext m x
  simp only [tail_cons, LinearMap.uncurryLeft_apply, MultilinearMap.curryLeft_apply]
  rw [cons_zero]

Left Currying and Uncurrying of Linear Maps into Multilinear Maps are Inverse Operations

Informal description

For any linear map $f$ from $M(0)$ to the space of multilinear maps on $n$ variables (indexed by $\text{Fin}\, n$), the left currying of the uncurried version of $f$ equals $f$ itself. That is, $(f.\text{uncurryLeft}).\text{curryLeft} = f$.

MultilinearMap.uncurry_curryLeft theorem

(f : MultilinearMap R M M₂) : f.curryLeft.uncurryLeft = f

Full source

@[simp]
theorem MultilinearMap.uncurry_curryLeft (f : MultilinearMap R M M₂) :
    f.curryLeft.uncurryLeft = f := by
  ext m
  simp

Left Uncurrying Recovers Original Multilinear Map

Informal description

For any multilinear map $f$ in $n+1$ variables (indexed by $\text{Fin}(n+1)$), the operation of left-currying followed by left-uncurrying recovers the original map. That is, $(f.\text{curryLeft}).\text{uncurryLeft} = f$.

multilinearCurryLeftEquiv definition

: MultilinearMap R M M₂ ≃ₗ[R] (M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂)

Full source

/-- The space of multilinear maps on `Π (i : Fin (n+1)), M i` is canonically isomorphic to
the space of linear maps from `M 0` to the space of multilinear maps on
`Π (i : Fin n), M i.succ`, by separating the first variable. We register this isomorphism as a
linear isomorphism in `multilinearCurryLeftEquiv R M M₂`.

The direct and inverse maps are given by `f.curryLeft` and `f.uncurryLeft`. Use these
unless you need the full framework of linear equivs. -/
def multilinearCurryLeftEquiv :
    MultilinearMapMultilinearMap R M M₂ ≃ₗ[R] (M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂) where
  toFun := MultilinearMap.curryLeft
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun := LinearMap.uncurryLeft
  left_inv := MultilinearMap.uncurry_curryLeft
  right_inv := LinearMap.curry_uncurryLeft

Canonical linear equivalence between multilinear maps and linear maps into multilinear maps via left currying

Informal description

The space of multilinear maps on $\prod_{i \in \text{Fin}(n+1)} M_i$ is canonically isomorphic to the space of linear maps from $M_0$ to the space of multilinear maps on $\prod_{i \in \text{Fin}(n)} M_{i+1}$. This isomorphism is given by the linear equivalence $\text{multilinearCurryLeftEquiv}$, where: - The forward map $\text{toFun}$ is the left currying operation $\text{curryLeft}$, which transforms a multilinear map $f$ in $n+1$ variables into a linear map from $M_0$ to multilinear maps in the remaining $n$ variables. - The inverse map $\text{invFun}$ is the left uncurrying operation $\text{uncurryLeft}$, which reconstructs the original multilinear map from its curried form. The isomorphism preserves addition and scalar multiplication, and satisfies $\text{uncurryLeft} \circ \text{curryLeft} = \text{id}$ and $\text{curryLeft} \circ \text{uncurryLeft} = \text{id}$.

MultilinearMap.uncurryRight definition

(f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) : MultilinearMap R M M₂

Full source

/-- Given a multilinear map `f` in `n` variables to the space of linear maps from `M (last n)` to
`M₂`, construct the corresponding multilinear map on `n+1` variables obtained by concatenating
the variables, given by `m ↦ f (init m) (m (last n))` -/
def MultilinearMap.uncurryRight
    (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) :
    MultilinearMap R M M₂ :=
  MultilinearMap.mk' (fun m ↦ f (init m) (m (last n)))
    (fun m i x y ↦ by
      by_cases h : i.val < n
      · have : lastlast n ≠ i := Ne.symm (ne_of_lt h)
        simp_rw [update_of_ne this]
        revert x y
        rw [(castSucc_castLT i h).symm]
        intro x y
        rw [init_update_castSucc, MultilinearMap.map_update_add, init_update_castSucc,
          init_update_castSucc, LinearMap.add_apply]
      · revert x y
        rw [eq_last_of_not_lt h]
        intro x y
        simp_rw [init_update_last, update_self, LinearMap.map_add])
    (fun m i c x ↦ by
      by_cases h : i.val < n
      · have : lastlast n ≠ i := Ne.symm (ne_of_lt h)
        simp_rw [update_of_ne this]
        revert x
        rw [(castSucc_castLT i h).symm]
        intro x
        rw [init_update_castSucc, init_update_castSucc, MultilinearMap.map_update_smul,
          LinearMap.smul_apply]
      · revert x
        rw [eq_last_of_not_lt h]
        intro x
        simp_rw [update_self, init_update_last, map_smul])

Uncurrying of a multilinear map with linear map values

Informal description

Given a multilinear map $f$ in $n$ variables (indexed by $\text{Fin}\, n$) taking values in the space of linear maps from $M (\text{last}\, n)$ to $M₂$, the operation $\text{uncurryRight}$ constructs the corresponding multilinear map in $n+1$ variables (indexed by $\text{Fin}\, (n+1)$) defined by $m \mapsto f (\text{init}\, m) (m (\text{last}\, n))$, where $\text{init}\, m$ is the initial segment of $m$ (the first $n$ components) and $m (\text{last}\, n)$ is the last component.

MultilinearMap.uncurryRight_apply theorem

 (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) (m : ∀ i, M i) :
  f.uncurryRight m = f (init m) (m (last n))

Full source

@[simp]
theorem MultilinearMap.uncurryRight_apply
    (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂))
    (m : ∀ i, M i) : f.uncurryRight m = f (init m) (m (last n)) :=
  rfl

Evaluation of Uncurried Right Multilinear Map: $(\text{uncurryRight}\,f)(m) = f(m_0, \dots, m_{n-1})(m_n)$

Informal description

Let $R$ be a semiring, $M$ a family of $R$-modules indexed by $\text{Fin}(n+1)$, and $M₂$ an $R$-module. Given a multilinear map $f$ in $n$ variables (indexed by $\text{Fin}(n)$) taking values in the space of linear maps from $M(\text{last}\,n)$ to $M₂$, the uncurried map $\text{uncurryRight}\,f$ evaluated at a tuple $m = (m_0, \dots, m_n)$ satisfies \[ (\text{uncurryRight}\,f)(m) = f(m_0, \dots, m_{n-1})(m_n). \]

MultilinearMap.curryRight definition

(f : MultilinearMap R M M₂) : MultilinearMap R (fun i : Fin n => M (Fin.castSucc i)) (M (last n) →ₗ[R] M₂)

Full source

/-- Given a multilinear map `f` in `n+1` variables, split the last variable to obtain
a multilinear map in `n` variables taking values in linear maps from `M (last n)` to `M₂`, given by
`m ↦ (x ↦ f (snoc m x))`. -/
def MultilinearMap.curryRight (f : MultilinearMap R M M₂) :
    MultilinearMap R (fun i : Fin n => M (Fin.castSucc i)) (M (last n) →ₗ[R] M₂) :=
  MultilinearMap.mk' (fun m ↦
    { toFun := fun x => f (snoc m x)
      map_add' := fun x y => by simp_rw [f.snoc_add]
      map_smul' := fun c x => by simp only [f.snoc_smul, RingHom.id_apply] })

Right currying of a multilinear map

Informal description

Given a multilinear map $ f $ in $ n+1 $ variables (indexed by $ \text{Fin } (n+1) $), the operation `curryRight` transforms $ f $ into a multilinear map in $ n $ variables (indexed by $ \text{Fin } n $) taking values in linear maps from $ M (\text{last } n) $ to $ M₂ $. Specifically, for any tuple $ m $ of $ n $ elements (where each $ m_i $ has type $ M (\text{castSucc } i) $), the resulting linear map is given by $ x \mapsto f (\text{snoc } m \ x) $, where $ \text{snoc } m \ x $ appends $ x $ to the tuple $ m $.

MultilinearMap.curryRight_apply theorem

(f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M (castSucc i)) (x : M (last n)) : f.curryRight m x = f (snoc m x)

Full source

@[simp]
theorem MultilinearMap.curryRight_apply (f : MultilinearMap R M M₂)
    (m : ∀ i : Fin n, M (castSucc i)) (x : M (last n)) : f.curryRight m x = f (snoc m x) :=
  rfl

Evaluation of Right-Curried Multilinear Map: $(f.\text{curryRight})(m)(x) = f(\text{snoc } m \ x)$

Informal description

Let $R$ be a semiring, $M : \text{Fin} (n+1) \to \text{Type}$ be a family of $R$-modules, and $M₂$ be an $R$-module. Given a multilinear map $f : \text{MultilinearMap}_R M M₂$ and a tuple $m = (m_i)_{i \in \text{Fin} n}$ where each $m_i \in M (\text{castSucc } i)$, then for any $x \in M (\text{last } n)$, the right-curried version of $f$ satisfies $(f.\text{curryRight})(m)(x) = f(\text{snoc } m \ x)$, where $\text{snoc } m \ x$ is the tuple obtained by appending $x$ to $m$.

MultilinearMap.curry_uncurryRight theorem

(f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) : f.uncurryRight.curryRight = f

Full source

@[simp]
theorem MultilinearMap.curry_uncurryRight
    (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) :
    f.uncurryRight.curryRight = f := by
  ext m x
  simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]
  rw [init_snoc]

Recovery of Original Map via Uncurrying and Right-Currying

Informal description

Let $R$ be a semiring, $M$ a family of $R$-modules indexed by $\text{Fin}\, (n+1)$, and $M₂$ an $R$-module. For any multilinear map $f$ in $n$ variables (indexed by $\text{Fin}\, n$) taking values in the space of linear maps from $M (\text{last}\, n)$ to $M₂$, the composition of uncurrying followed by right-currying recovers the original map, i.e., $(f.\text{uncurryRight}).\text{curryRight} = f$.

MultilinearMap.uncurry_curryRight theorem

(f : MultilinearMap R M M₂) : f.curryRight.uncurryRight = f

Full source

@[simp]
theorem MultilinearMap.uncurry_curryRight (f : MultilinearMap R M M₂) :
    f.curryRight.uncurryRight = f := by
  ext m
  simp

Recovery of Original Multilinear Map via Right-Curry and Uncurry: $\text{uncurryRight} \circ \text{curryRight} = \text{id}$

Informal description

For any multilinear map $f$ in $n+1$ variables (indexed by $\text{Fin}\, (n+1)$), the operation of right-currying followed by uncurrying recovers the original map. That is, $\text{uncurryRight}(\text{curryRight}(f)) = f$.

multilinearCurryRightEquiv definition

: MultilinearMap R M M₂ ≃ₗ[R] MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)

Full source

/-- The space of multilinear maps on `Π (i : Fin (n+1)), M i` is canonically isomorphic to
the space of linear maps from the space of multilinear maps on `Π (i : Fin n), M (castSucc i)` to
the space of linear maps on `M (last n)`, by separating the last variable. We register this
isomorphism as a linear isomorphism in `multilinearCurryRightEquiv R M M₂`.

The direct and inverse maps are given by `f.curryRight` and `f.uncurryRight`. Use these
unless you need the full framework of linear equivs. -/
def multilinearCurryRightEquiv :
    MultilinearMapMultilinearMap R M M₂ ≃ₗ[R]
      MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂) where
  toFun := MultilinearMap.curryRight
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun := MultilinearMap.uncurryRight
  left_inv := MultilinearMap.uncurry_curryRight
  right_inv := MultilinearMap.curry_uncurryRight

Linear equivalence between multilinear maps and their right-curried versions

Informal description

The space of multilinear maps on $\prod_{i \in \text{Fin}(n+1)} M_i$ is canonically isomorphic to the space of multilinear maps on $\prod_{i \in \text{Fin}(n)} M_{\text{castSucc}(i)}$ taking values in linear maps from $M_{\text{last}(n)}$ to $M_2$. This isomorphism is given by the linear equivalence $\text{multilinearCurryRightEquiv}_R M M_2$, where: - The forward map is $\text{curryRight}$, which transforms a multilinear map $f$ in $n+1$ variables into a multilinear map in $n$ variables with values in linear maps. - The inverse map is $\text{uncurryRight}$, which reconstructs the original multilinear map from its curried version.

MultilinearMap.currySum definition

 (f : MultilinearMap R N M₂) : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)

Full source

/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map
on `(fun _ : ι ⊕ ι' => M')` induces a multilinear map on
`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))`. -/
def currySum (f : MultilinearMap R N M₂) :
    MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂) where
  toFun u :=
    { toFun v := f (Sum.rec u v)
      map_update_add' := by letI := Classical.decEq ι; aesop
      map_update_smul' := by letI := Classical.decEq ι; aesop }
  map_update_add' u i x y :=
    ext fun _ ↦ by letI := Classical.decEq ι'; simp
  map_update_smul' u i c x :=
    ext fun _ ↦ by letI := Classical.decEq ι'; simp

Currying of a multilinear map over a sum of index types

Informal description

Given a family of modules $N : (\iota \oplus \iota') \to \text{Type}^*$ and a multilinear map $f$ on $(fun \_ : \iota \oplus \iota' \Rightarrow M')$, the function $\text{currySum}\, f$ is a multilinear map on $(fun (i : \iota) \mapsto N (\text{inl}\, i))$ taking values in the space of multilinear maps on $(fun (i : \iota') \mapsto N (\text{inr}\, i))$. More precisely, for any $u : \prod_{i \in \iota} N (\text{inl}\, i)$ and $v : \prod_{i \in \iota'} N (\text{inr}\, i)$, the evaluation $\text{currySum}\, f\, u\, v$ is equal to $f (\text{Sum.rec}\, u\, v)$, where $\text{Sum.rec}$ combines $u$ and $v$ into a function on $\iota \oplus \iota'$.

MultilinearMap.currySum_apply theorem

 (f : MultilinearMap R N M₂) (u : (i : ι) → N (Sum.inl i)) (v : (i : ι') → N (Sum.inr i)) :
  currySum f u v = f (Sum.rec u v)

Full source

@[simp low]
theorem currySum_apply (f : MultilinearMap R N M₂)
    (u : (i : ι) → N (Sum.inl i)) (v : (i : ι') → N (Sum.inr i)) :
    currySum f u v = f (Sum.rec u v) := rfl

Evaluation of Curried Multilinear Map over Sum of Indices

Informal description

Let $R$ be a semiring, $\iota$ and $\iota'$ be index types, $N : \iota \oplus \iota' \to \text{Type}^*$ be a family of $R$-modules, and $M₂$ be an $R$-module. For any multilinear map $f : \text{MultilinearMap}\, R\, N\, M₂$, vectors $u : \prod_{i \in \iota} N (\text{inl}\, i)$, and $v : \prod_{i \in \iota'} N (\text{inr}\, i)$, the evaluation of the curried map satisfies \[ \text{currySum}\, f\, u\, v = f (\text{Sum.rec}\, u\, v). \]

MultilinearMap.currySum_apply' theorem

 {N : Type*} [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun _ : ι ⊕ ι' ↦ N) M₂) (u : ι → N) (v : ι' → N) :
  currySum f u v = f (Sum.elim u v)

Full source

@[simp]
theorem currySum_apply' {N : Type*} [AddCommMonoid N] [Module R N]
    (f : MultilinearMap R (fun _ : ι ⊕ ι' ↦ N) M₂)
    (u : ι → N) (v : ι' → N) :
    currySum f u v = f (Sum.elim u v) := rfl

Evaluation of Curried Multilinear Map over Sum of Indices (Homogeneous Case)

Informal description

Let $R$ be a semiring, $\iota$ and $\iota'$ be index types, and $N$ be an $R$-module. Given a multilinear map $f$ from $\prod_{i \in \iota \oplus \iota'} N$ to $M₂$, and vectors $u \in \prod_{i \in \iota} N$ and $v \in \prod_{i \in \iota'} N$, the evaluation of the curried map satisfies \[ \text{currySum}\, f\, u\, v = f (\text{Sum.elim}\, u\, v), \] where $\text{Sum.elim}\, u\, v$ combines $u$ and $v$ into a function on $\iota \oplus \iota'$.

MultilinearMap.currySum_add theorem

(f₁ f₂ : MultilinearMap R N M₂) : currySum (f₁ + f₂) = currySum f₁ + currySum f₂

Full source

@[simp]
lemma currySum_add (f₁ f₂ : MultilinearMap R N M₂):
    currySum (f₁ + f₂) = currySum f₁ + currySum f₂ := rfl

Additivity of Currying for Multilinear Maps

Informal description

For any two multilinear maps $f_1$ and $f_2$ from $\prod_{i \in \iota \oplus \iota'} N(i)$ to $M_2$, the curried sum of their sum equals the sum of their curried sums. That is, \[ \text{currySum}(f_1 + f_2) = \text{currySum}(f_1) + \text{currySum}(f_2). \]

MultilinearMap.currySum_smul theorem

(r : R) (f : MultilinearMap R N M₂) : currySum (r • f) = r • currySum f

Full source

@[simp]
lemma currySum_smul (r : R) (f : MultilinearMap R N M₂):
    currySum (r • f) = r • currySum f := rfl

Scalar Multiplication Commutes with Currying of Multilinear Maps

Informal description

For any scalar $r$ in the semiring $R$ and any multilinear map $f$ from $\prod_{i \in \iota \oplus \iota'} N(i)$ to $M₂$, the curried version of the scalar multiple $r \cdot f$ is equal to the scalar multiple $r$ applied to the curried version of $f$. That is, $\text{currySum}\, (r \cdot f) = r \cdot \text{currySum}\, f$.

MultilinearMap.uncurrySum definition

 (g : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) : MultilinearMap R N M₂

Full source

/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map on
`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))` induces a multilinear map
on `(fun _ : ι ⊕ ι' => M')` induces. -/
def uncurrySum
    (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
    MultilinearMap R N M₂  where
  toFun u := g (fun i ↦ u (.inl i)) (fun i' ↦ u (.inr i'))
  map_update_add' := by
    letI := Classical.decEq ι
    letI := Classical.decEq ι'
    rintro _ _ (_ | _) _ _ <;> simp
  map_update_smul' := by
    letI := Classical.decEq ι
    letI := Classical.decEq ι'
    rintro _ _ (_ | _) _ _ <;> simp

Uncurrying of a multilinear map over a sum of indices

Informal description

Given a family of modules $ N : (\iota \oplus \iota') \to \text{Type}^* $, the operation `uncurrySum` transforms a multilinear map $ g $ on $ \prod_{i \in \iota} N(\text{inl } i) $ taking values in the space of multilinear maps on $ \prod_{i' \in \iota'} N(\text{inr } i') $ into a multilinear map on $ \prod_{i \in \iota \oplus \iota'} N(i) $. Specifically, for any $ u \in \prod_{i \in \iota \oplus \iota'} N(i) $, the uncurried map is defined by $ g(\lambda i. u(\text{inl } i))(\lambda i'. u(\text{inr } i')) $.

MultilinearMap.uncurrySum_apply theorem

 (g : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) (u) :
  g.uncurrySum u = g (fun i ↦ u (.inl i)) (fun i' ↦ u (.inr i'))

Full source

@[simp]
theorem uncurrySum_apply
    (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) (u) :
    g.uncurrySum u =
      g (fun i ↦ u (.inl i)) (fun i' ↦ u (.inr i')) := rfl

Evaluation of Uncurried Multilinear Map over Sum of Indices

Informal description

Let $N : \iota \oplus \iota' \to \text{Type}^*$ be a family of modules over a semiring $R$, and let $g$ be a multilinear map from $\prod_{i \in \iota} N(\text{inl } i)$ to the space of multilinear maps from $\prod_{i' \in \iota'} N(\text{inr } i')$ to $M₂$. For any $u \in \prod_{i \in \iota \oplus \iota'} N(i)$, the uncurried map $g.\text{uncurrySum}$ satisfies \[ g.\text{uncurrySum}(u) = g(\lambda i. u(\text{inl } i))(\lambda i'. u(\text{inr } i')). \]

MultilinearMap.uncurrySum_add theorem

 (g₁ g₂ : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
  uncurrySum (g₁ + g₂) = uncurrySum g₁ + uncurrySum g₂

Full source

@[simp]
lemma uncurrySum_add
    (g₁ g₂ : MultilinearMap R (fun i : ι ↦ N (.inl i))
      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
    uncurrySum (g₁ + g₂) = uncurrySum g₁ + uncurrySum g₂ :=
  rfl

Additivity of Uncurrying for Multilinear Maps over Sum of Indices

Informal description

Let $R$ be a semiring, $\iota$ and $\iota'$ be types, $N : \iota \oplus \iota' \to \text{Type}^*$ be a family of $R$-modules, and $M₂$ be an $R$-module. For any two multilinear maps $g₁, g₂ : \text{MultilinearMap}\, R\, (λi. N(\text{inl}\, i))\, (\text{MultilinearMap}\, R\, (λi. N(\text{inr}\, i))\, M₂)$, the uncurried sum of their sum equals the sum of their uncurried sums, i.e., \[ \text{uncurrySum}(g₁ + g₂) = \text{uncurrySum}(g₁) + \text{uncurrySum}(g₂). \]

MultilinearMap.uncurrySum_smul theorem

 (r : R) (g : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
  uncurrySum (r • g) = r • uncurrySum g

Full source

lemma uncurrySum_smul
    (r : R) (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
    uncurrySum (r • g) = r • uncurrySum g :=
  rfl

Scalar Multiplication Commutes with Uncurrying of Multilinear Maps

Informal description

Let $R$ be a semiring, $\iota$ and $\iota'$ be types, and $N : \iota \oplus \iota' \to \text{Type}^*$ be a family of $R$-modules. For any scalar $r \in R$ and any multilinear map $g$ from $\prod_{i \in \iota} N(\text{inl } i)$ to the space of multilinear maps from $\prod_{i' \in \iota'} N(\text{inr } i')$ to an $R$-module $M₂$, the uncurried version of the scalar multiple $r \cdot g$ is equal to the scalar multiple $r$ applied to the uncurried version of $g$. That is, $\text{uncurrySum}(r \cdot g) = r \cdot \text{uncurrySum}(g)$.

MultilinearMap.uncurrySum_currySum theorem

(f : MultilinearMap R N M₂) : uncurrySum (currySum f) = f

Full source

@[simp]
lemma uncurrySum_currySum (f : MultilinearMap R N M₂) :
    uncurrySum (currySum f) = f := by
  ext
  simp only [uncurrySum_apply, currySum_apply]
  congr
  ext (_ | _) <;> simp

Uncurrying of Curried Multilinear Map is Identity

Informal description

For any multilinear map $f$ from $\prod_{i \in \iota \oplus \iota'} N(i)$ to $M₂$, the uncurrying of the currying of $f$ equals $f$ itself. That is, $\text{uncurrySum}(\text{currySum}\, f) = f$.

MultilinearMap.currySum_uncurrySum theorem

 (g : MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
  currySum (uncurrySum g) = g

Full source

@[simp]
lemma currySum_uncurrySum
    (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
  currySum (uncurrySum g) = g :=
    rfl

Currying-Uncurrying Invariance for Multilinear Maps over Sum of Indices

Informal description

Let $R$ be a semiring, $\iota$ and $\iota'$ be index types, and $N : \iota \oplus \iota' \to \text{Type}^*$ be a family of $R$-modules. For any multilinear map $g$ from $\prod_{i \in \iota} N(\text{inl } i)$ to the space of multilinear maps from $\prod_{i' \in \iota'} N(\text{inr } i')$ to $M₂$, the composition of uncurrying followed by currying $g$ returns $g$ itself, i.e., $\text{currySum} (\text{uncurrySum } g) = g$.

MultilinearMap.currySumEquiv definition

 : MultilinearMap R N M₂ ≃ₗ[R] MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)

Full source

/-- Multilinear maps on `N : (ι ⊕ ι') → Type*` identify to multilinear maps
from `(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))`. -/
@[simps]
def currySumEquiv : MultilinearMapMultilinearMap R N M₂ ≃ₗ[R]
    MultilinearMap R (fun i : ι ↦ N (.inl i))
      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂) where
  toFun := currySum
  invFun := uncurrySum
  left_inv _ := by simp
  right_inv _ := rfl
  map_add' := by aesop
  map_smul' := by aesop

Linear Equivalence for Currying Multilinear Maps over a Sum of Indices

Informal description

The linear equivalence `MultilinearMap.currySumEquiv` establishes a bijection between the space of multilinear maps on $N : (\iota \oplus \iota') \to \text{Type}^*$ and the space of multilinear maps on $\prod_{i \in \iota} N(\text{inl } i)$ taking values in the space of multilinear maps on $\prod_{i' \in \iota'} N(\text{inr } i')$. Specifically, the forward direction (`toFun`) is given by `currySum`, which transforms a multilinear map $f$ on $\prod_{i \in \iota \oplus \iota'} N(i)$ into a multilinear map on $\prod_{i \in \iota} N(\text{inl } i)$ whose values are multilinear maps on $\prod_{i' \in \iota'} N(\text{inr } i')$. The inverse direction (`invFun`) is given by `uncurrySum`, which reconstructs the original multilinear map from its curried form. This equivalence preserves addition and scalar multiplication, making it a linear isomorphism.

MultilinearMap.coe_currySumEquiv theorem

: ⇑(currySumEquiv (R := R) (N := N) (M₂ := M₂)) = currySum

Full source

@[simp]
theorem coe_currySumEquiv : ⇑(currySumEquiv (R := R) (N := N) (M₂ := M₂)) = currySum :=
  rfl

Forward map of currying linear equivalence is `currySum`

Informal description

The forward map of the linear equivalence `currySumEquiv` between the space of multilinear maps on $N : (\iota \oplus \iota') \to \text{Type}^*$ and the space of multilinear maps on $\prod_{i \in \iota} N(\text{inl } i)$ taking values in the space of multilinear maps on $\prod_{i' \in \iota'} N(\text{inr } i')$ is equal to the currying operation `currySum`.

MultilinearMap.coe_currySumEquiv_symm theorem

: ⇑(currySumEquiv (R := R) (N := N) (M₂ := M₂)).symm = uncurrySum

Full source

@[simp]
theorem coe_currySumEquiv_symm : ⇑(currySumEquiv (R := R) (N := N) (M₂ := M₂)).symm = uncurrySum :=
  rfl

Inverse of Currying Equivalence for Multilinear Maps is Uncurrying

Informal description

The inverse of the linear equivalence `currySumEquiv` is given by the uncurrying operation `uncurrySum`. That is, for any family of modules $N : (\iota \oplus \iota') \to \text{Type}^*$ and module $M₂$, the inverse map of `currySumEquiv` is the function that takes a multilinear map on $\prod_{i \in \iota} N(\text{inl } i)$ with values in the space of multilinear maps on $\prod_{i' \in \iota'} N(\text{inr } i')$ and returns the corresponding uncurried multilinear map on $\prod_{i \in \iota \oplus \iota'} N(i)$.

MultilinearMap.curryFinFinset definition

 {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l) :
  MultilinearMap R (fun _ : Fin n => M') M₂ ≃ₗ[R]
    MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂)

Full source

/-- If `s : Finset (Fin n)` is a finite set of cardinality `k` and its complement has cardinality
`l`, then the space of multilinear maps on `fun i : Fin n => M'` is isomorphic to the space of
multilinear maps on `fun i : Fin k => M'` taking values in the space of multilinear maps
on `fun i : Fin l => M'`. -/
def curryFinFinset {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l) :
    MultilinearMapMultilinearMap R (fun _ : Fin n => M') M₂ ≃ₗ[R]
      MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂) :=
  (domDomCongrLinearEquiv R R M' M₂ (finSumEquivOfFinset hk hl).symm).trans
    currySumEquiv

Linear equivalence for currying multilinear maps over a finite partition of indices

Informal description

Given a finite set $s \subseteq \text{Fin}(n)$ with cardinality $k$ and its complement $s^\complement$ with cardinality $l$, there is a linear equivalence between the space of multilinear maps on $\text{Fin}(n) \to M'$ and the space of multilinear maps on $\text{Fin}(k) \to M'$ taking values in multilinear maps on $\text{Fin}(l) \to M'$. Explicitly, the equivalence transforms a multilinear map $f$ on $n$ variables into a multilinear map on $k$ variables whose values are multilinear maps on $l$ variables, and vice versa. The bijection is constructed by reindexing via the order-preserving equivalence $\text{finSumEquivOfFinset}$ between $\text{Fin}(k) \oplus \text{Fin}(l)$ and $\text{Fin}(n)$.

MultilinearMap.curryFinFinset_apply theorem

 {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l) (f : MultilinearMap R (fun _ : Fin n => M') M₂)
  (mk : Fin k → M') (ml : Fin l → M') :
  curryFinFinset R M₂ M' hk hl f mk ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)

Full source

@[simp]
theorem curryFinFinset_apply {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin n => M') M₂) (mk : Fin k → M') (ml : Fin l → M') :
    curryFinFinset R M₂ M' hk hl f mk ml =
      f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i) :=
  rfl

Evaluation of Curried Multilinear Map via Index Partition

Informal description

Let $R$ be a semiring, $M'$ and $M₂$ be $R$-modules, and $n,k,l$ be natural numbers. Given a finite subset $s \subseteq \text{Fin}(n)$ with cardinality $k$ (witnessed by $hk$) and its complement $s^\complement$ with cardinality $l$ (witnessed by $hl$), for any multilinear map $f : (\text{Fin}(n) \to M') \to M₂$ and vectors $m_k : \text{Fin}(k) \to M'$, $m_l : \text{Fin}(l) \to M'$, we have: $$\text{curryFinFinset}_{R,M₂,M'}(hk,hl,f)(m_k,m_l) = f\left(\lambda i.\ \text{Sum.elim}\ m_k\ m_l\ ((\text{finSumEquivOfFinset}\ hk\ hl)^{-1}(i))\right)$$ Here, $\text{finSumEquivOfFinset}\ hk\ hl$ is the order-preserving bijection between $\text{Fin}(k) \oplus \text{Fin}(l)$ and $\text{Fin}(n)$, and $\text{Sum.elim}$ combines the two functions $m_k$ and $m_l$ into a function on the disjoint union.

MultilinearMap.curryFinFinset_symm_apply theorem

 {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
  (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂)) (m : Fin n → M') :
  (curryFinFinset R M₂ M' hk hl).symm f m =
    f (fun i => m <| finSumEquivOfFinset hk hl (Sum.inl i)) fun i => m <| finSumEquivOfFinset hk hl (Sum.inr i)

Full source

@[simp]
theorem curryFinFinset_symm_apply {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k)
    (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂))
    (m : Fin n → M') :
    (curryFinFinset R M₂ M' hk hl).symm f m =
      f (fun i => m <| finSumEquivOfFinset hk hl (Sum.inl i)) fun i =>
        m <| finSumEquivOfFinset hk hl (Sum.inr i) :=
  rfl

Inverse of Multilinear Currying Equivalence Applied to a Function

Informal description

Let $k, l, n$ be natural numbers, and let $s$ be a finite subset of $\text{Fin}(n)$ with cardinality $k$ and complement $s^\complement$ of cardinality $l$. Given a multilinear map $f$ from $\text{Fin}(k) \to M'$ to multilinear maps from $\text{Fin}(l) \to M'$ to $M₂$, and a function $m : \text{Fin}(n) \to M'$, the inverse of the currying equivalence $\text{curryFinFinset}$ evaluated at $f$ and $m$ is equal to $f$ applied to the restriction of $m$ to the left component (via $\text{finSumEquivOfFinset}$) and the restriction of $m$ to the right component (via $\text{finSumEquivOfFinset}$). More precisely, we have: $$(\text{curryFinFinset}\, R\, M₂\, M'\, hk\, hl)^{-1}(f)(m) = f(\lambda i.\, m(\text{finSumEquivOfFinset}\, hk\, hl\, (\text{Sum.inl}\, i))) (\lambda i.\, m(\text{finSumEquivOfFinset}\, hk\, hl\, (\text{Sum.inr}\, i)))$$

MultilinearMap.curryFinFinset_symm_apply_piecewise_const theorem

 {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
  (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂)) (x y : M') :
  (curryFinFinset R M₂ M' hk hl).symm f (s.piecewise (fun _ => x) fun _ => y) = f (fun _ => x) fun _ => y

Full source

theorem curryFinFinset_symm_apply_piecewise_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k)
    (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂))
    (x y : M') :
    (curryFinFinset R M₂ M' hk hl).symm f (s.piecewise (fun _ => x) fun _ => y) =
      f (fun _ => x) fun _ => y := by
  rw [curryFinFinset_symm_apply]; congr
  · ext
    rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]
    apply Finset.orderEmbOfFin_mem
  · ext
    rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_not_mem]
    exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

Evaluation of Uncurried Multilinear Map at Piecewise Constant Function

Informal description

Let $k, l, n$ be natural numbers and $s \subseteq \mathrm{Fin}(n)$ a finite subset with cardinality $k$ and complement of cardinality $l$. For any multilinear map $f$ from $\mathrm{Fin}(k) \to M'$ to the space of multilinear maps from $\mathrm{Fin}(l) \to M'$ to $M₂$, and for any elements $x, y \in M'$, the uncurried version of $f$ evaluated at the piecewise constant function that equals $x$ on $s$ and $y$ on its complement equals $f$ evaluated at the constant function $\lambda \_, x$ in the first argument and $\lambda \_, y$ in the second argument. In symbols: $$(\text{curryFinFinset}\, R\, M₂\, M'\, hk\, hl)^{-1}(f)(s.\text{piecewise}\, (\lambda \_, x)\, (\lambda \_, y)) = f\, (\lambda \_, x)\, (\lambda \_, y)$$

MultilinearMap.curryFinFinset_symm_apply_const theorem

 {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l)
  (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂)) (x : M') :
  ((curryFinFinset R M₂ M' hk hl).symm f fun _ => x) = f (fun _ => x) fun _ => x

Full source

@[simp]
theorem curryFinFinset_symm_apply_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k)
    (hl : #sᶜ = l)
    (f : MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂))
    (x : M') : ((curryFinFinset R M₂ M' hk hl).symm f fun _ => x) = f (fun _ => x) fun _ => x :=
  rfl

Evaluation of Uncurried Multilinear Map at Constant Function

Informal description

Let $k, l, n$ be natural numbers and $s \subseteq \mathrm{Fin}(n)$ a finite subset with cardinality $k$ and complement of cardinality $l$. For any multilinear map $f$ from $\mathrm{Fin}(k) \to M'$ to the space of multilinear maps from $\mathrm{Fin}(l) \to M'$ to $M₂$, and for any constant $x \in M'$, the uncurried version of $f$ evaluated at the constant function $\lambda \_, x$ equals $f$ evaluated at the constant functions $\lambda \_, x$ in both arguments.

MultilinearMap.curryFinFinset_apply_const theorem

 {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ = l) (f : MultilinearMap R (fun _ : Fin n => M') M₂)
  (x y : M') : (curryFinFinset R M₂ M' hk hl f (fun _ => x) fun _ => y) = f (s.piecewise (fun _ => x) fun _ => y)

Full source

theorem curryFinFinset_apply_const {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k)
    (hl : #sᶜ = l) (f : MultilinearMap R (fun _ : Fin n => M') M₂) (x y : M') :
    (curryFinFinset R M₂ M' hk hl f (fun _ => x) fun _ => y) =
      f (s.piecewise (fun _ => x) fun _ => y) := by
  rw [← curryFinFinset_symm_apply_piecewise_const hk hl, LinearEquiv.symm_apply_apply]

Evaluation of Curried Multilinear Map at Constant Functions

Informal description

Let $k, l, n$ be natural numbers and $s \subseteq \mathrm{Fin}(n)$ a finite subset with cardinality $k$ and complement of cardinality $l$. For any multilinear map $f$ from $\mathrm{Fin}(n) \to M'$ to $M₂$, and for any elements $x, y \in M'$, the curried version of $f$ evaluated at the constant functions $\lambda \_, x$ and $\lambda \_, y$ equals $f$ evaluated at the piecewise constant function that equals $x$ on $s$ and $y$ on its complement. In symbols: $$\text{curryFinFinset}\, R\, M₂\, M'\, hk\, hl\, f\, (\lambda \_, x)\, (\lambda \_, y) = f\, (s.\text{piecewise}\, (\lambda \_, x)\, (\lambda \_, y))$$