Mathlib.LinearAlgebra.Multilinear.Basic

MultilinearMap structure

 (R : Type uR) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [Semiring R] [∀ i, AddCommMonoid (M₁ i)]
  [AddCommMonoid M₂] [∀ i, Module R (M₁ i)] [Module R M₂]

Full source

/-- Multilinear maps over the ring `R`, from `∀ i, M₁ i` to `M₂` where `M₁ i` and `M₂` are modules
over `R`. -/
structure MultilinearMap (R : Type uR) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [Semiring R]
  [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M₂] [∀ i, Module R (M₁ i)] [Module R M₂] where
  /-- The underlying multivariate function of a multilinear map. -/
  toFun : (∀ i, M₁ i) → M₂
  /-- A multilinear map is additive in every argument. -/
  map_update_add' :
    ∀ [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i),
      toFun (update m i (x + y)) = toFun (update m i x) + toFun (update m i y)
  /-- A multilinear map is compatible with scalar multiplication in every argument. -/
  map_update_smul' :
    ∀ [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i),
      toFun (update m i (c • x)) = c • toFun (update m i x)

Multilinear Map

Informal description

The structure `MultilinearMap R M₁ M₂` represents the space of multilinear maps from the product space `∀ (i : ι), M₁ i` to `M₂`, where each `M₁ i` and `M₂` are modules over a semiring `R`. A map is multilinear if it is linear in each coordinate when all other coordinates are fixed.

MultilinearMap.instFunLikeForall instance

: FunLike (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂

Full source

instance : FunLike (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂ where
  coe f := f.toFun
  coe_injective' f g h := by cases f; cases g; cases h; rfl

Function-Like Structure on Multilinear Maps

Informal description

The space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ from $\prod_{i \in \iota} M₁_i$ to $M₂$ has a function-like structure, where each multilinear map can be treated as a function from $\prod_{i \in \iota} M₁_i$ to $M₂$.

MultilinearMap.toFun_eq_coe theorem

: f.toFun = ⇑f

Full source

@[simp]
theorem toFun_eq_coe : f.toFun = ⇑f :=
  rfl

Equality of Underlying Function and Coercion for Multilinear Maps

Informal description

For any multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function.

MultilinearMap.coe_mk theorem

(f : (∀ i, M₁ i) → M₂) (h₁ h₂) : ⇑(⟨f, h₁, h₂⟩ : MultilinearMap R M₁ M₂) = f

Full source

@[simp]
theorem coe_mk (f : (∀ i, M₁ i) → M₂) (h₁ h₂) : ⇑(⟨f, h₁, h₂⟩ : MultilinearMap R M₁ M₂) = f :=
  rfl

Coercion of Constructed Multilinear Map Equals Original Function

Informal description

For any function $ f : \prod_{i \in \iota} M₁_i \to M₂ $ that is multilinear (i.e., linear in each coordinate when the others are fixed), the coercion of the multilinear map constructed from $ f $ (with proofs $ h₁ $ and $ h₂ $ of its linearity properties) is equal to $ f $ itself. In other words, the underlying function of the constructed multilinear map coincides with $ f $.

MultilinearMap.congr_fun theorem

{f g : MultilinearMap R M₁ M₂} (h : f = g) (x : ∀ i, M₁ i) : f x = g x

Full source

theorem congr_fun {f g : MultilinearMap R M₁ M₂} (h : f = g) (x : ∀ i, M₁ i) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of Multilinear Maps: $f = g \implies f(x) = g(x)$ for all $x$

Informal description

For any two multilinear maps $f$ and $g$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, if $f = g$, then for all $x \in \prod_{i \in \iota} M₁_i$, we have $f(x) = g(x)$.

MultilinearMap.congr_arg theorem

(f : MultilinearMap R M₁ M₂) {x y : ∀ i, M₁ i} (h : x = y) : f x = f y

Full source

nonrec theorem congr_arg (f : MultilinearMap R M₁ M₂) {x y : ∀ i, M₁ i} (h : x = y) : f x = f y :=
  DFunLike.congr_arg f h

Multilinear Map Argument Congruence: $x = y \implies f(x) = f(y)$

Informal description

For any multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$ and any vectors $x, y \in \prod_{i \in \iota} M₁_i$, if $x = y$, then $f(x) = f(y)$.

MultilinearMap.coe_injective theorem

: Injective ((↑) : MultilinearMap R M₁ M₂ → (∀ i, M₁ i) → M₂)

Full source

theorem coe_injective : Injective ((↑) : MultilinearMap R M₁ M₂ → (∀ i, M₁ i) → M₂) :=
  DFunLike.coe_injective

Injectivity of the Multilinear Map Embedding

Informal description

The canonical embedding from the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ to the space of functions $(\forall i, M₁ i) \to M₂$ is injective. That is, if two multilinear maps $f$ and $g$ satisfy $f(x) = g(x)$ for all $x \in \prod_{i \in \iota} M₁_i$, then $f = g$.

MultilinearMap.coe_inj theorem

{f g : MultilinearMap R M₁ M₂} : (f : (∀ i, M₁ i) → M₂) = g ↔ f = g

Full source

@[norm_cast]
theorem coe_inj {f g : MultilinearMap R M₁ M₂} : (f : (∀ i, M₁ i) → M₂) = g ↔ f = g :=
  DFunLike.coe_fn_eq

Equality of Multilinear Maps via Underlying Functions

Informal description

For any two multilinear maps $f$ and $g$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, the equality of their underlying functions $(f : \prod_{i} M₁_i \to M₂) = g$ holds if and only if $f = g$ as multilinear maps.

MultilinearMap.ext theorem

{f f' : MultilinearMap R M₁ M₂} (H : ∀ x, f x = f' x) : f = f'

Full source

@[ext]
theorem ext {f f' : MultilinearMap R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=
  DFunLike.ext _ _ H

Extensionality of Multilinear Maps

Informal description

For any two multilinear maps $f, f' \colon \prod_{i \in \iota} M₁_i \to M₂$, if $f(x) = f'(x)$ for all $x \in \prod_{i \in \iota} M₁_i$, then $f = f'$.

MultilinearMap.mk_coe theorem

(f : MultilinearMap R M₁ M₂) (h₁ h₂) : (⟨f, h₁, h₂⟩ : MultilinearMap R M₁ M₂) = f

Full source

@[simp]
theorem mk_coe (f : MultilinearMap R M₁ M₂) (h₁ h₂) :
    (⟨f, h₁, h₂⟩ : MultilinearMap R M₁ M₂) = f := rfl

Constructor Equality for Multilinear Maps

Informal description

For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ and any proofs $h₁$, $h₂$ of its linearity properties, the constructed multilinear map $\langle f, h₁, h₂ \rangle$ is equal to $f$ itself.

MultilinearMap.map_update_add theorem

 [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) : f (update m i (x + y)) = f (update m i x) + f (update m i y)

Full source

@[simp]
protected theorem map_update_add [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) :
    f (update m i (x + y)) = f (update m i x) + f (update m i y) :=
  f.map_update_add' m i x y

Additivity of Multilinear Maps in Each Coordinate

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁_i$ and $M₂$ be $R$-modules for each $i \in \iota$. For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, vector $m \in \prod_{i \in \iota} M₁_i$, index $i \in \iota$, and elements $x, y \in M₁_i$, we have: \[ f(m[i \mapsto x + y]) = f(m[i \mapsto x]) + f(m[i \mapsto y]) \] where $m[i \mapsto v]$ denotes the vector obtained by updating the $i$-th coordinate of $m$ to $v$.

MultilinearMap.map_update_smul theorem

[DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) : f (update m i (c • x)) = c • f (update m i x)

Full source

/-- Earlier, this name was used by what is now called `MultilinearMap.map_update_smul_left`. -/
@[simp]
protected theorem map_update_smul [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) :
    f (update m i (c • x)) = c • f (update m i x) :=
  f.map_update_smul' m i c x

Multilinearity condition: scaling in one coordinate

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁ : \iota \to \text{Type}$, $M₂$ be $R$-modules. For any multilinear map $f : \text{MultilinearMap}\, R\, M₁\, M₂$, vector $m \in \prod_{i \in \iota} M₁ i$, index $i \in \iota$, scalar $c \in R$, and vector $x \in M₁ i$, we have: \[ f(m[i \mapsto c \cdot x]) = c \cdot f(m[i \mapsto x]) \] where $m[i \mapsto y]$ denotes the vector equal to $m$ except at index $i$ where it takes value $y$.

MultilinearMap.map_coord_zero theorem

{m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0

Full source

theorem map_coord_zero {m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0 := by
  classical
    have : (0 : R) • (0 : M₁ i) = 0 := by simp
    rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]

Vanishing of Multilinear Maps at Zero Coordinates

Informal description

Let $R$ be a semiring, $\iota$ a type, and $M₁ : \iota \to \text{Type}$, $M₂$ be $R$-modules. For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ and vector $m \in \prod_{i \in \iota} M₁_i$, if there exists an index $i \in \iota$ such that $m_i = 0$, then $f(m) = 0$.

MultilinearMap.map_update_zero theorem

[DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : f (update m i 0) = 0

Full source

@[simp]
theorem map_update_zero [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : f (update m i 0) = 0 :=
  f.map_coord_zero i (update_self i 0 m)

Vanishing of Multilinear Maps under Zero Update

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁ : \iota \to \text{Type}$, $M₂$ be $R$-modules. For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ and vector $m \in \prod_{i \in \iota} M₁_i$, updating $m$ at any index $i \in \iota$ to zero yields $f(m[i \mapsto 0]) = 0$.

MultilinearMap.map_zero theorem

[Nonempty ι] : f 0 = 0

Full source

@[simp]
theorem map_zero [Nonempty ι] : f 0 = 0 := by
  obtain ⟨i, _⟩ : ∃ i : ι, i ∈ Set.univ := Set.exists_mem_of_nonempty ι
  exact map_coord_zero f i rfl

Multilinear Maps Vanish at Zero Vector

Informal description

For any nonempty type $\iota$ and any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, the evaluation of $f$ at the zero vector is zero, i.e., $f(0) = 0$.

MultilinearMap.instAdd instance

: Add (MultilinearMap R M₁ M₂)

Full source

instance : Add (MultilinearMap R M₁ M₂) :=
  ⟨fun f f' =>
    ⟨fun x => f x + f' x, fun m i x y => by simp [add_left_comm, add_assoc], fun m i c x => by
      simp [smul_add]⟩⟩

Addition of Multilinear Maps

Informal description

The space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ has an additive structure, where the sum of two multilinear maps $f$ and $f'$ is defined pointwise by $(f + f')(m) = f(m) + f'(m)$ for all $m \in \prod_{i \in \iota} M₁_i$.

MultilinearMap.add_apply theorem

(m : ∀ i, M₁ i) : (f + f') m = f m + f' m

Full source

@[simp]
theorem add_apply (m : ∀ i, M₁ i) : (f + f') m = f m + f' m :=
  rfl

Pointwise Addition of Multilinear Maps

Informal description

For any multilinear maps $f$ and $f'$ in $\text{MultilinearMap}\, R\, M₁\, M₂$ and any vector $m \in \prod_{i \in \iota} M₁_i$, the evaluation of the sum $f + f'$ at $m$ equals the sum of the evaluations of $f$ and $f'$ at $m$, i.e., $(f + f')(m) = f(m) + f'(m)$.

MultilinearMap.instZero instance

: Zero (MultilinearMap R M₁ M₂)

Full source

instance : Zero (MultilinearMap R M₁ M₂) :=
  ⟨⟨fun _ => 0, fun _ _ _ _ => by simp, fun _ _ c _ => by simp⟩⟩

Zero Multilinear Map

Informal description

For any semiring $R$, type $\iota$, family of $R$-modules $M₁ : \iota \to \text{Type}$, and $R$-module $M₂$, the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ has a zero element. This zero multilinear map sends every input $(m_i)_{i \in \iota}$ to the zero element of $M₂$.

MultilinearMap.instInhabited instance

: Inhabited (MultilinearMap R M₁ M₂)

Full source

instance : Inhabited (MultilinearMap R M₁ M₂) :=
  ⟨0⟩

Inhabited Space of Multilinear Maps

Informal description

For any semiring $R$, type $\iota$, family of $R$-modules $M₁ : \iota \to \text{Type}$, and $R$-module $M₂$, the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ is inhabited. In particular, the zero multilinear map serves as a canonical inhabitant.

MultilinearMap.zero_apply theorem

(m : ∀ i, M₁ i) : (0 : MultilinearMap R M₁ M₂) m = 0

Full source

@[simp]
theorem zero_apply (m : ∀ i, M₁ i) : (0 : MultilinearMap R M₁ M₂) m = 0 :=
  rfl

Zero Multilinear Map Evaluates to Zero

Informal description

For any family of modules $(M_i)_{i \in \iota}$ over a semiring $R$ and any module $M₂$ over $R$, the zero multilinear map $0 \in \text{MultilinearMap}\, R\, M\, M₂$ satisfies $0(m) = 0$ for all $m \in \prod_{i \in \iota} M_i$.

MultilinearMap.instSMul instance

: SMul S (MultilinearMap R M₁ M₂)

Full source

instance : SMul S (MultilinearMap R M₁ M₂) :=
  ⟨fun c f =>
    ⟨fun m => c • f m, fun m i x y => by simp [smul_add], fun l i x d => by
      simp [← smul_comm x c (_ : M₂)]⟩⟩

Scalar Multiplication on Multilinear Maps

Informal description

For a semiring $R$, an arbitrary type $\iota$, a family of $R$-modules $M₁ : \iota \to \text{Type}$, and an $R$-module $M₂$, the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ has a scalar multiplication structure induced by any scalar multiplication on $M₂$. That is, for any scalar $c$ in a suitable scalar ring $S$ and any multilinear map $f$, the map $c \cdot f$ defined by $(c \cdot f)(m) = c \cdot f(m)$ is also multilinear.

MultilinearMap.smul_apply theorem

(f : MultilinearMap R M₁ M₂) (c : S) (m : ∀ i, M₁ i) : (c • f) m = c • f m

Full source

@[simp]
theorem smul_apply (f : MultilinearMap R M₁ M₂) (c : S) (m : ∀ i, M₁ i) : (c • f) m = c • f m :=
  rfl

Scalar Multiplication Evaluation for Multilinear Maps: $(c \cdot f)(m) = c \cdot f(m)$

Informal description

Let $R$ be a semiring, $\iota$ an arbitrary type, $M₁ : \iota \to \text{Type}$ a family of $R$-modules, and $M₂$ an $R$-module. For any multilinear map $f \in \text{MultilinearMap}\, R\, M₁\, M₂$, scalar $c \in S$, and vector $m \in \prod_{i \in \iota} M₁_i$, the evaluation of the scalar multiple $c \cdot f$ at $m$ equals $c$ multiplied by the evaluation of $f$ at $m$, i.e., $(c \cdot f)(m) = c \cdot f(m)$.

MultilinearMap.coe_smul theorem

(c : S) (f : MultilinearMap R M₁ M₂) : ⇑(c • f) = c • (⇑f)

Full source

theorem coe_smul (c : S) (f : MultilinearMap R M₁ M₂) : ⇑(c • f) = c • (⇑ f) := rfl

Scalar Multiplication Commutes with Function Application for Multilinear Maps: $(c \cdot f)(m) = c \cdot f(m)$

Informal description

For any scalar $c$ in $S$ and any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, the underlying function of the scalar multiple $c \cdot f$ is equal to the scalar multiple of the underlying function of $f$, i.e., $(c \cdot f)(m) = c \cdot f(m)$ for all $m \in \prod_{i \in \iota} M₁_i$.

MultilinearMap.addCommMonoid instance

: AddCommMonoid (MultilinearMap R M₁ M₂)

Full source

instance addCommMonoid : AddCommMonoid (MultilinearMap R M₁ M₂) :=
  coe_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl

Additive Commutative Monoid Structure on Multilinear Maps

Informal description

The space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ forms an additive commutative monoid under pointwise addition. That is, for any semiring $R$, type $\iota$, family of $R$-modules $M₁ : \iota \to \text{Type}$, and $R$-module $M₂$, the set of multilinear maps from $\prod_{i \in \iota} M₁_i$ to $M₂$ is equipped with a commutative addition operation and a zero element, satisfying the usual monoid axioms.

MultilinearMap.coeAddMonoidHom definition

: MultilinearMap R M₁ M₂ →+ (((i : ι) → M₁ i) → M₂)

Full source

/-- Coercion of a multilinear map to a function as an additive monoid homomorphism. -/
@[simps] def coeAddMonoidHom : MultilinearMapMultilinearMap R M₁ M₂ →+ (((i : ι) → M₁ i) → M₂) where
  toFun := DFunLike.coe; map_zero' := rfl; map_add' _ _ := rfl

Coercion of multilinear maps to functions as an additive monoid homomorphism

Informal description

The additive monoid homomorphism that coerces a multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ to its underlying function. This homomorphism preserves the zero map and pointwise addition of multilinear maps.

MultilinearMap.coe_sum theorem

{α : Type*} (f : α → MultilinearMap R M₁ M₂) (s : Finset α) : ⇑(∑ a ∈ s, f a) = ∑ a ∈ s, ⇑(f a)

Full source

@[simp]
theorem coe_sum {α : Type*} (f : α → MultilinearMap R M₁ M₂) (s : Finset α) :
    ⇑(∑ a ∈ s, f a) = ∑ a ∈ s, ⇑(f a) :=
  map_sum coeAddMonoidHom f s

Sum of Multilinear Maps Equals Sum of Their Underlying Functions

Informal description

For any family of multilinear maps $f \colon \alpha \to \text{MultilinearMap}\, R\, M₁\, M₂$ and any finite set $s \subset \alpha$, the underlying function of the sum $\sum_{a \in s} f_a$ is equal to the sum of the underlying functions $\sum_{a \in s} f_a$. In other words, the function obtained by summing multilinear maps over a finite set $s$ is equal to the sum of the corresponding functions evaluated pointwise.

MultilinearMap.sum_apply theorem

 {α : Type*} (f : α → MultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) {s : Finset α} : (∑ a ∈ s, f a) m = ∑ a ∈ s, f a m

Full source

theorem sum_apply {α : Type*} (f : α → MultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) {s : Finset α} :
    (∑ a ∈ s, f a) m = ∑ a ∈ s, f a m := by simp

Evaluation of Sum of Multilinear Maps Equals Sum of Evaluations

Informal description

For any family of multilinear maps $f \colon \alpha \to \text{MultilinearMap}\, R\, M₁\, M₂$, any element $m \in \prod_{i \in \iota} M₁_i$, and any finite subset $s \subset \alpha$, the evaluation of the sum of multilinear maps at $m$ equals the sum of the evaluations of each multilinear map at $m$, i.e., \[ \left(\sum_{a \in s} f_a\right)(m) = \sum_{a \in s} f_a(m). \]

MultilinearMap.toLinearMap definition

[DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : M₁ i →ₗ[R] M₂

Full source

/-- If `f` is a multilinear map, then `f.toLinearMap m i` is the linear map obtained by fixing all
coordinates but `i` equal to those of `m`, and varying the `i`-th coordinate. -/
@[simps]
def toLinearMap [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) : M₁ i →ₗ[R] M₂ where
  toFun x := f (update m i x)
  map_add' x y := by simp
  map_smul' c x := by simp

Linearization of a multilinear map at a fixed point

Informal description

Given a multilinear map $ f $ from $ \prod_{i \in \iota} M₁_i $ to $ M₂ $ and a fixed element $ m \in \prod_{i \in \iota} M₁_i $, the function $ f.toLinearMap \, m \, i $ is the linear map obtained by fixing all coordinates except the $ i $-th coordinate to be those of $ m $, and varying the $ i $-th coordinate. Formally, for any $ x \in M₁_i $, we have $ f.toLinearMap \, m \, i \, x = f (m[j \mapsto x \text{ if } j = i \text{ else } m_j]) $.

MultilinearMap.prod definition

(f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₃) : MultilinearMap R M₁ (M₂ × M₃)

Full source

/-- The cartesian product of two multilinear maps, as a multilinear map. -/
@[simps]
def prod (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₃) :
    MultilinearMap R M₁ (M₂ × M₃) where
  toFun m := (f m, g m)
  map_update_add' m i x y := by simp
  map_update_smul' m i c x := by simp

Cartesian product of multilinear maps

Informal description

Given two multilinear maps $ f : \prod_{i \in \iota} M₁_i \to M₂ $ and $ g : \prod_{i \in \iota} M₁_i \to M₃ $ over a semiring $ R $, the cartesian product $ f \times g $ is the multilinear map from $ \prod_{i \in \iota} M₁_i $ to $ M₂ \times M₃ $ defined by $ (f \times g)(m) = (f(m), g(m)) $ for all $ m \in \prod_{i \in \iota} M₁_i $. This map is multilinear because $ f $ and $ g $ are multilinear in each coordinate.

MultilinearMap.pi definition

 {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, Module R (M' i)]
  (f : ∀ i, MultilinearMap R M₁ (M' i)) : MultilinearMap R M₁ (∀ i, M' i)

Full source

/-- Combine a family of multilinear maps with the same domain and codomains `M' i` into a
multilinear map taking values in the space of functions `∀ i, M' i`. -/
@[simps]
def pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i, Module R (M' i)]
    (f : ∀ i, MultilinearMap R M₁ (M' i)) : MultilinearMap R M₁ (∀ i, M' i) where
  toFun m i := f i m
  map_update_add' _ _ _ _ := funext fun j => (f j).map_update_add _ _ _ _
  map_update_smul' _ _ _ _ := funext fun j => (f j).map_update_smul _ _ _ _

Combination of multilinear maps into a product map

Informal description

Given a family of multilinear maps $ f_i : \prod_{j \in \iota} M₁_j \to M'_i $ indexed by $ i \in \iota' $, where each $ M'_i $ is an $ R $-module, the function `MultilinearMap.pi` combines them into a single multilinear map $ f : \prod_{j \in \iota} M₁_j \to \prod_{i \in \iota'} M'_i $ defined by $ f(m)(i) = f_i(m) $ for all $ i \in \iota' $. This map is multilinear because each $ f_i $ is multilinear in its arguments.

MultilinearMap.ofSubsingleton definition

[Subsingleton ι] (i : ι) : (M₂ →ₗ[R] M₃) ≃ MultilinearMap R (fun _ : ι ↦ M₂) M₃

Full source

/-- Equivalence between linear maps `M₂ →ₗ[R] M₃` and one-multilinear maps. -/
@[simps]
def ofSubsingleton [Subsingleton ι] (i : ι) :
    (M₂ →ₗ[R] M₃) ≃ MultilinearMap R (fun _ : ι ↦ M₂) M₃ where
  toFun f :=
    { toFun := fun x ↦ f (x i)
      map_update_add' := by intros; simp [update_eq_const_of_subsingleton]
      map_update_smul' := by intros; simp [update_eq_const_of_subsingleton] }
  invFun f :=
    { toFun := fun x ↦ f fun _ ↦ x
      map_add' := fun x y ↦ by
        simpa [update_eq_const_of_subsingleton] using f.map_update_add 0 i x y
      map_smul' := fun c x ↦ by
        simpa [update_eq_const_of_subsingleton] using f.map_update_smul 0 i c x }
  left_inv _ := rfl
  right_inv f := by ext x; refine congr_arg f ?_; exact (eq_const_of_subsingleton _ _).symm

Equivalence between linear maps and multilinear maps on subsingleton index types

Informal description

Given a type $\iota$ with at most one element (i.e., a subsingleton) and a fixed index $i \in \iota$, there is a natural equivalence between linear maps $M_2 \to_{R} M_3$ and multilinear maps $\prod_{i \in \iota} M_2 \to M_3$. Specifically: - The forward direction takes a linear map $f : M_2 \to_{R} M_3$ and constructs a multilinear map that evaluates $f$ at the $i$-th coordinate of its input. - The backward direction takes a multilinear map $f : \prod_{i \in \iota} M_2 \to M_3$ and constructs a linear map by applying $f$ to a constant family where every coordinate equals the input. This equivalence holds because, when $\iota$ is a subsingleton, a multilinear map depends only on the value at the single (or nonexistent) coordinate, reducing to the linear case.

MultilinearMap.constOfIsEmpty definition

[IsEmpty ι] (m : M₂) : MultilinearMap R M₁ M₂

Full source

/-- The constant map is multilinear when `ι` is empty. -/
@[simps -fullyApplied]
def constOfIsEmpty [IsEmpty ι] (m : M₂) : MultilinearMap R M₁ M₂ where
  toFun := Function.const _ m
  map_update_add' _ := isEmptyElim
  map_update_smul' _ := isEmptyElim

Constant multilinear map for empty index type

Informal description

Given a semiring $R$, a family of $R$-modules $(M₁_i)_{i \in \iota}$, and an $R$-module $M₂$, when the index type $\iota$ is empty, the constant function that maps every element of the product space $\prod_{i \in \iota} M₁_i$ to a fixed element $m \in M₂$ is a multilinear map. This is because there are no coordinates to vary, making the linearity conditions vacuously true.

MultilinearMap.restr definition

 {k n : ℕ} (f : MultilinearMap R (fun _ : Fin n => M') M₂) (s : Finset (Fin n)) (hk : #s = k) (z : M') :
  MultilinearMap R (fun _ : Fin k => M') M₂

Full source

/-- Given a multilinear map `f` on `n` variables (parameterized by `Fin n`) and a subset `s` of `k`
of these variables, one gets a new multilinear map on `Fin k` by varying these variables, and fixing
the other ones equal to a given value `z`. It is denoted by `f.restr s hk z`, where `hk` is a
proof that the cardinality of `s` is `k`. The implicit identification between `Fin k` and `s` that
we use is the canonical (increasing) bijection. -/
def restr {k n : ℕ} (f : MultilinearMap R (fun _ : Fin n => M') M₂) (s : Finset (Fin n))
    (hk : #s = k) (z : M') : MultilinearMap R (fun _ : Fin k => M') M₂ where
  toFun v := f fun j => if h : j ∈ s then v ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z
  /- Porting note: The proofs of the following two lemmas used to only use `erw` followed by `simp`,
  but it seems `erw` no longer unfolds or unifies well enough to work without more help. -/
  map_update_add' v i x y := by
    erw [dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv,
      dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv,
      dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv]
    simp
  map_update_smul' v i c x := by
    erw [dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv,
      dite_comp_equiv_update (s.orderIsoOfFin hk).toEquiv]
    simp

Restriction of a multilinear map to a subset of variables

Informal description

Given a multilinear map $ f $ on $ n $ variables (indexed by $ \text{Fin}\, n $) with values in $ M₂ $, a subset $ s $ of $ \text{Fin}\, n $ with cardinality $ k $, and a fixed value $ z \in M' $, the restriction $ f.restr\, s\, hk\, z $ is a multilinear map on $ k $ variables (indexed by $ \text{Fin}\, k $) obtained by varying the variables in $ s $ and fixing the others to $ z $. Here, $ hk $ is a proof that the cardinality of $ s $ is $ k $, and the variables in $ s $ are identified with $ \text{Fin}\, k $ via the canonical increasing bijection. Explicitly, for $ v \in \prod_{i \in \text{Fin}\, k} M' $, the map evaluates as: \[ f.restr\, s\, hk\, z\, v = f \left( \lambda j \in \text{Fin}\, n, \begin{cases} v((s.orderIsoOfFin\, hk)^{-1} \langle j, h \rangle) & \text{if } j \in s, \\ z & \text{otherwise.} \end{cases} \right) \]

MultilinearMap.cons_add theorem

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

Full source

/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `cons`, one can express directly the additivity of a
multilinear map along the first variable. -/
theorem cons_add (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (x y : M 0) :
    f (cons (x + y) m) = f (cons x m) + f (cons y m) := by
  simp_rw [← update_cons_zero x m (x + y), f.map_update_add, update_cons_zero]

Additivity of Multilinear Maps in the First Coordinate via $\text{cons}$

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 \colon \prod_{i \in \text{Fin} (n+1)} M_i \to M₂$, any tuple $m \in \prod_{i \in \text{Fin} n} M_{i.\text{succ}}$, and any elements $x, y \in M_0$, we have: \[ f(\text{cons}(x + y, m)) = f(\text{cons}(x, m)) + f(\text{cons}(y, m)), \] where $\text{cons}(x, m)$ denotes the tuple obtained by prepending $x$ to $m$ in the first coordinate.

MultilinearMap.cons_smul theorem

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

Full source

/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `cons`, one can express directly the multiplicativity
of a multilinear map along the first variable. -/
theorem cons_smul (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (c : R) (x : M 0) :
    f (cons (c • x) m) = c • f (cons x m) := by
  simp_rw [← update_cons_zero x m (c • x), f.map_update_smul, update_cons_zero]

Multilinearity of prepended tuple under scalar multiplication: $f(\text{cons}(c x, m)) = c f(\text{cons}(x, m))$

Informal description

Let $R$ be a semiring, $M : \text{Fin} (n+1) \to \text{Type}$ a family of $R$-modules, and $M₂$ an $R$-module. For any multilinear map $f : \text{MultilinearMap}\, R\, M\, M₂$, tuple $m \in \prod_{i \in \text{Fin} n} M (i.\text{succ})$, scalar $c \in R$, and vector $x \in M 0$, we have: \[ f(\text{cons}(c \cdot x, m)) = c \cdot f(\text{cons}(x, m)) \] where $\text{cons}(x, m)$ denotes the tuple in $\prod_{i \in \text{Fin} (n+1)} M i$ obtained by prepending $x$ to $m$.

MultilinearMap.snoc_add theorem

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

Full source

/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `snoc`, one can express directly the additivity of a
multilinear map along the first variable. -/
theorem snoc_add (f : MultilinearMap R M M₂)
    (m : ∀ i : Fin n, M (castSucc i)) (x y : M (last n)) :
    f (snoc m (x + y)) = f (snoc m x) + f (snoc m y) := by
  simp_rw [← update_snoc_last x m (x + y), f.map_update_add, update_snoc_last]

Additivity of Multilinear Maps in the Last Coordinate via `snoc`

Informal description

Let $R$ be a semiring, $n$ a natural number, and $M$ a family of $R$-modules indexed by $\text{Fin } (n+1)$. For any multilinear map $f \colon \prod_{i \in \text{Fin } (n+1)} M_i \to M_2$, any tuple $m \in \prod_{i \in \text{Fin } n} M_{i.\text{castSucc}}$, and any elements $x, y \in M_{\text{last } n}$, we have: \[ f(\text{snoc}(m, x + y)) = f(\text{snoc}(m, x)) + f(\text{snoc}(m, y)), \] where $\text{snoc}(m, z)$ denotes the tuple obtained by appending $z$ to $m$ at the last position.

MultilinearMap.snoc_smul theorem

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

Full source

/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `cons`, one can express directly the multiplicativity
of a multilinear map along the first variable. -/
theorem snoc_smul (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M (castSucc i)) (c : R)
    (x : M (last n)) : f (snoc m (c • x)) = c • f (snoc m x) := by
  simp_rw [← update_snoc_last x m (c • x), f.map_update_smul, update_snoc_last]

Multilinearity of snoc: $f(\text{snoc}(m, c \cdot x)) = c \cdot f(\text{snoc}(m, x))$

Informal description

Let $R$ be a semiring, $M$ a family of $R$-modules indexed by $\text{Fin}(n+1)$, and $M₂$ another $R$-module. For any multilinear map $f : \text{MultilinearMap}\, R\, M\, M₂$, tuple $m \in \prod_{i=0}^{n-1} M_i$, scalar $c \in R$, and vector $x \in M_n$, we have: \[ f(\text{snoc}(m, c \cdot x)) = c \cdot f(\text{snoc}(m, x)) \] where $\text{snoc}(m, y)$ denotes the tuple obtained by appending $y$ to $m$.

MultilinearMap.compLinearMap definition

(g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i →ₗ[R] M₁' i) : MultilinearMap R M₁ M₂

Full source

/-- If `g` is a multilinear map and `f` is a collection of linear maps,
then `g (f₁ m₁, ..., fₙ mₙ)` is again a multilinear map, that we call
`g.compLinearMap f`. -/
def compLinearMap (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i →ₗ[R] M₁' i) :
    MultilinearMap R M₁ M₂ where
  toFun m := g fun i => f i (m i)
  map_update_add' m i x y := by
    have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
      Function.apply_update (fun k => f k) _ _ _ _
    simp [this]
  map_update_smul' m i c x := by
    have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
      Function.apply_update (fun k => f k) _ _ _ _
    simp [this]

Composition of a multilinear map with linear maps

Informal description

Given a multilinear map $ g $ from $ \prod_{i \in \iota} M'_i $ to $ M_2 $ and a collection of linear maps $ f_i : M_i \to M'_i $ for each $ i \in \iota $, the composition $ g \circ (f_1, \dots, f_n) $ is a multilinear map from $ \prod_{i \in \iota} M_i $ to $ M_2 $. This composition is denoted by $ g \circ \text{LinearMap} \, f $ and is defined by applying each linear map $ f_i $ to the corresponding coordinate of the input before applying $ g $.

MultilinearMap.compLinearMap_apply theorem

 (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i →ₗ[R] M₁' i) (m : ∀ i, M₁ i) : g.compLinearMap f m = g fun i => f i (m i)

Full source

@[simp]
theorem compLinearMap_apply (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i →ₗ[R] M₁' i)
    (m : ∀ i, M₁ i) : g.compLinearMap f m = g fun i => f i (m i) :=
  rfl

Evaluation of Composition of Multilinear Map with Linear Maps

Informal description

Let $R$ be a semiring, $\iota$ be a type, and for each $i \in \iota$, let $M_i$, $M'_i$, and $M_2$ be $R$-modules. Given a multilinear map $g : \prod_{i \in \iota} M'_i \to M_2$ and a family of linear maps $f_i : M_i \to M'_i$ for each $i \in \iota$, the evaluation of the composition $g \circ (f_i)_{i \in \iota}$ at a point $(m_i)_{i \in \iota} \in \prod_{i \in \iota} M_i$ is equal to $g$ evaluated at $(f_i(m_i))_{i \in \iota}$. In other words, $$(g \circ (f_i)_{i \in \iota})((m_i)_{i \in \iota}) = g((f_i(m_i))_{i \in \iota}).$$

MultilinearMap.compLinearMap_assoc theorem

 (g : MultilinearMap R M₁'' M₂) (f₁ : ∀ i, M₁' i →ₗ[R] M₁'' i) (f₂ : ∀ i, M₁ i →ₗ[R] M₁' i) :
  (g.compLinearMap f₁).compLinearMap f₂ = g.compLinearMap fun i => f₁ i ∘ₗ f₂ i

Full source

/-- Composing a multilinear map twice with a linear map in each argument is
the same as composing with their composition. -/
theorem compLinearMap_assoc (g : MultilinearMap R M₁'' M₂) (f₁ : ∀ i, M₁' i →ₗ[R] M₁'' i)
    (f₂ : ∀ i, M₁ i →ₗ[R] M₁' i) :
    (g.compLinearMap f₁).compLinearMap f₂ = g.compLinearMap fun i => f₁ i ∘ₗ f₂ i :=
  rfl

Associativity of Composition for Multilinear Maps with Linear Maps

Informal description

Let $R$ be a semiring, $\iota$ be a type, and for each $i \in \iota$, let $M_i$, $M'_i$, and $M''_i$ be $R$-modules. Given a multilinear map $g : \prod_{i \in \iota} M''_i \to M_2$, linear maps $f_1^i : M'_i \to M''_i$ for each $i \in \iota$, and linear maps $f_2^i : M_i \to M'_i$ for each $i \in \iota$, the following equality holds: \[ (g \circ f_1) \circ f_2 = g \circ (f_1 \circ f_2), \] where $\circ$ denotes the composition of multilinear maps with linear maps in each coordinate.

MultilinearMap.zero_compLinearMap theorem

(f : ∀ i, M₁ i →ₗ[R] M₁' i) : (0 : MultilinearMap R M₁' M₂).compLinearMap f = 0

Full source

/-- Composing the zero multilinear map with a linear map in each argument. -/
@[simp]
theorem zero_compLinearMap (f : ∀ i, M₁ i →ₗ[R] M₁' i) :
    (0 : MultilinearMap R M₁' M₂).compLinearMap f = 0 :=
  ext fun _ => rfl

Composition of Zero Multilinear Map with Linear Maps Yields Zero Map

Informal description

For any collection of linear maps $ f_i \colon M_i \to M'_i $ indexed by $ i \in \iota $, the composition of the zero multilinear map $ 0 \colon \prod_{i \in \iota} M'_i \to M_2 $ with the linear maps $ f_i $ is equal to the zero multilinear map $ 0 \colon \prod_{i \in \iota} M_i \to M_2 $. That is, $ 0 \circ (f_1, \dots, f_n) = 0 $.

MultilinearMap.compLinearMap_id theorem

(g : MultilinearMap R M₁' M₂) : (g.compLinearMap fun _ => LinearMap.id) = g

Full source

/-- Composing a multilinear map with the identity linear map in each argument. -/
@[simp]
theorem compLinearMap_id (g : MultilinearMap R M₁' M₂) :
    (g.compLinearMap fun _ => LinearMap.id) = g :=
  ext fun _ => rfl

Identity Composition of Multilinear Maps: $g \circ \text{id} = g$

Informal description

Given a multilinear map $g \colon \prod_{i \in \iota} M'_i \to M_2$, the composition of $g$ with the identity linear map in each coordinate is equal to $g$ itself. That is, $g \circ (\lambda i, \text{id}_{M'_i}) = g$.

MultilinearMap.compLinearMap_injective theorem

 (f : ∀ i, M₁ i →ₗ[R] M₁' i) (hf : ∀ i, Surjective (f i)) :
  Injective fun g : MultilinearMap R M₁' M₂ => g.compLinearMap f

Full source

/-- Composing with a family of surjective linear maps is injective. -/
theorem compLinearMap_injective (f : ∀ i, M₁ i →ₗ[R] M₁' i) (hf : ∀ i, Surjective (f i)) :
    Injective fun g : MultilinearMap R M₁' M₂ => g.compLinearMap f := fun g₁ g₂ h =>
  ext fun x => by
    simpa [fun i => surjInv_eq (hf i)]
      using MultilinearMap.ext_iff.mp h fun i => surjInv (hf i) (x i)

Injectivity of Multilinear Map Composition with Surjective Linear Maps

Informal description

Let $R$ be a semiring, $\iota$ an arbitrary type, and for each $i \in \iota$, let $M_i$ and $M'_i$ be $R$-modules. Given a family of surjective linear maps $f_i \colon M_i \to M'_i$ for each $i \in \iota$, the composition map \[ g \mapsto g \circ (f_1, \dots, f_n) \] from the space of multilinear maps $\text{MultilinearMap}_R(M'_1, \dots, M'_n, M_2)$ to $\text{MultilinearMap}_R(M_1, \dots, M_n, M_2)$ is injective. In other words, if two multilinear maps $g_1$ and $g_2$ satisfy $g_1 \circ (f_1, \dots, f_n) = g_2 \circ (f_1, \dots, f_n)$, then $g_1 = g_2$.

MultilinearMap.compLinearMap_inj theorem

 (f : ∀ i, M₁ i →ₗ[R] M₁' i) (hf : ∀ i, Surjective (f i)) (g₁ g₂ : MultilinearMap R M₁' M₂) :
  g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂

Full source

theorem compLinearMap_inj (f : ∀ i, M₁ i →ₗ[R] M₁' i) (hf : ∀ i, Surjective (f i))
    (g₁ g₂ : MultilinearMap R M₁' M₂) : g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂ :=
  (compLinearMap_injective _ hf).eq_iff

Injectivity of Multilinear Map Composition with Surjective Linear Maps

Informal description

Let $R$ be a semiring, $\iota$ an arbitrary type, and for each $i \in \iota$, let $M_i$ and $M'_i$ be $R$-modules. Given a family of surjective linear maps $f_i \colon M_i \to M'_i$ for each $i \in \iota$, and two multilinear maps $g_1, g_2 \colon \prod_{i \in \iota} M'_i \to M_2$, we have that $g_1 \circ (f_1, \dots, f_n) = g_2 \circ (f_1, \dots, f_n)$ if and only if $g_1 = g_2$.

MultilinearMap.comp_linearEquiv_eq_zero_iff theorem

 (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i ≃ₗ[R] M₁' i) :
  (g.compLinearMap fun i => (f i : M₁ i →ₗ[R] M₁' i)) = 0 ↔ g = 0

Full source

/-- Composing a multilinear map with a linear equiv on each argument gives the zero map
if and only if the multilinear map is the zero map. -/
@[simp]
theorem comp_linearEquiv_eq_zero_iff (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i ≃ₗ[R] M₁' i) :
    (g.compLinearMap fun i => (f i : M₁ i →ₗ[R] M₁' i)) = 0 ↔ g = 0 := by
  set f' := fun i => (f i : M₁ i →ₗ[R] M₁' i)
  rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]

Composition with Linear Equivalences Yields Zero Map if and Only if Original Map is Zero

Informal description

Let $R$ be a semiring, $\iota$ an arbitrary type, and for each $i \in \iota$, let $M_i$ and $M'_i$ be $R$-modules. Given a multilinear map $g \colon \prod_{i \in \iota} M'_i \to M_2$ and a family of linear equivalences $f_i \colon M_i \simeq M'_i$ for each $i \in \iota$, the composition $g \circ (f_1, \dots, f_n)$ is the zero map if and only if $g$ is the zero map.

MultilinearMap.map_piecewise_add theorem

 [DecidableEq ι] (m m' : ∀ i, M₁ i) (t : Finset ι) :
  f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')

Full source

/-- If one adds to a vector `m'` another vector `m`, but only for coordinates in a finset `t`, then
the image under a multilinear map `f` is the sum of `f (s.piecewise m m')` along all subsets `s` of
`t`. This is mainly an auxiliary statement to prove the result when `t = univ`, given in
`map_add_univ`, although it can be useful in its own right as it does not require the index set `ι`
to be finite. -/
theorem map_piecewise_add [DecidableEq ι] (m m' : ∀ i, M₁ i) (t : Finset ι) :
    f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m') := by
  revert m'
  refine Finset.induction_on t (by simp) ?_
  intro i t hit Hrec m'
  have A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i) :=
    t.piecewise_insert _ _ _
  have B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [hit]
    · simp [h]
  let m'' := update m' i (m i)
  have C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m'' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [m'', hit]
    · by_cases h' : j ∈ t <;> simp [m'', h, hit, h']
  rw [A, f.map_update_add, B, C, Finset.sum_powerset_insert hit, Hrec, Hrec, add_comm (_ : M₂)]
  congr 1
  refine Finset.sum_congr rfl fun s hs => ?_
  have : (insert i s).piecewise m m' = s.piecewise m m'' := by
    ext j
    by_cases h : j = i
    · rw [h]
      simp [m'', Finset.not_mem_of_mem_powerset_of_not_mem hs hit]
    · by_cases h' : j ∈ s <;> simp [m'', h, h']
  rw [this]

Multilinear Summation over Piecewise Additions on Finite Subsets

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, vectors $m, m' \in \prod_{i \in \iota} M₁_i$, and a finite subset $t \subseteq \iota$, we have: \[ f\big(t.\text{piecewise}(m + m', m')\big) = \sum_{s \in \mathcal{P}(t)} f\big(s.\text{piecewise}(m, m')\big) \] where: - $t.\text{piecewise}(m + m', m')$ denotes the vector equal to $m + m'$ on $t$ and $m'$ elsewhere - $s.\text{piecewise}(m, m')$ denotes the vector equal to $m$ on $s$ and $m'$ elsewhere - $\mathcal{P}(t)$ is the powerset of $t$

MultilinearMap.map_add_univ theorem

[DecidableEq ι] [Fintype ι] (m m' : ∀ i, M₁ i) : f (m + m') = ∑ s : Finset ι, f (s.piecewise m m')

Full source

/-- Additivity of a multilinear map along all coordinates at the same time,
writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`. -/
theorem map_add_univ [DecidableEq ι] [Fintype ι] (m m' : ∀ i, M₁ i) :
    f (m + m') = ∑ s : Finset ι, f (s.piecewise m m') := by
  simpa using f.map_piecewise_add m m' Finset.univ

Multilinear Additivity over All Coordinates: $f(m + m') = \sum_{s \subseteq \iota} f(s.\text{piecewise}(m, m'))$

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$ and vectors $m, m' \in \prod_{i \in \iota} M₁ i$, we have: \[ f(m + m') = \sum_{s \subseteq \iota} f(s.\text{piecewise}(m, m')) \] where $s.\text{piecewise}(m, m')$ denotes the vector equal to $m$ on $s$ and $m'$ on its complement.

MultilinearMap.map_sum_finset_aux theorem

 [DecidableEq ι] [Fintype ι] {n : ℕ} (h : (∑ i, #(A i)) = n) :
  (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)

Full source

/-- If `f` is multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate. Here, we give an auxiliary statement tailored for an inductive proof. Use instead
`map_sum_finset`. -/
theorem map_sum_finset_aux [DecidableEq ι] [Fintype ι] {n : ℕ} (h : (∑ i, #(A i)) = n) :
    (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i) := by
  letI := fun i => Classical.decEq (α i)
  induction n using Nat.strong_induction_on generalizing A with | h n IH =>
  -- If one of the sets is empty, then all the sums are zero
  by_cases Ai_empty : ∃ i, A i = ∅
  · obtain ⟨i, hi⟩ : ∃ i, ∑ j ∈ A i, g i j = 0 := Ai_empty.imp fun i hi ↦ by simp [hi]
    have hpi : piFinset A = ∅ := by simpa
    rw [f.map_coord_zero i hi, hpi, Finset.sum_empty]
  push_neg at Ai_empty
  -- Otherwise, if all sets are at most singletons, then they are exactly singletons and the result
  -- is again straightforward
  by_cases Ai_singleton : ∀ i, #(A i) ≤ 1
  · have Ai_card : ∀ i, #(A i) = 1 := by
      intro i
      have pos : #(A i)#(A i) ≠ 0 := by simp [Finset.card_eq_zero, Ai_empty i]
      have : #(A i) ≤ 1 := Ai_singleton i
      exact le_antisymm this (Nat.succ_le_of_lt (_root_.pos_iff_ne_zero.mpr pos))
    have :
      ∀ r : ∀ i, α i, r ∈ piFinset A → (f fun i => g i (r i)) = f fun i => ∑ j ∈ A i, g i j := by
      intro r hr
      congr with i
      have : ∀ j ∈ A i, g i j = g i (r i) := by
        intro j hj
        congr
        apply Finset.card_le_one_iff.1 (Ai_singleton i) hj
        exact mem_piFinset.mp hr i
      simp only [Finset.sum_congr rfl this, Finset.mem_univ, Finset.sum_const, Ai_card i, one_nsmul]
    simp only [Finset.sum_congr rfl this, Ai_card, card_piFinset, prod_const_one, one_nsmul,
      Finset.sum_const]
  -- Remains the interesting case where one of the `A i`, say `A i₀`, has cardinality at least 2.
  -- We will split into two parts `B i₀` and `C i₀` of smaller cardinality, let `B i = C i = A i`
  -- for `i ≠ i₀`, apply the inductive assumption to `B` and `C`, and add up the corresponding
  -- parts to get the sum for `A`.
  push_neg at Ai_singleton
  obtain ⟨i₀, hi₀⟩ : ∃ i, 1 < #(A i) := Ai_singleton
  obtain ⟨j₁, j₂, _, hj₂, _⟩ : ∃ j₁ j₂, j₁ ∈ A i₀ ∧ j₂ ∈ A i₀ ∧ j₁ ≠ j₂ :=
    Finset.one_lt_card_iff.1 hi₀
  let B := Function.update A i₀ (A i₀ \ {j₂})
  let C := Function.update A i₀ {j₂}
  have B_subset_A : ∀ i, B i ⊆ A i := by
    intro i
    by_cases hi : i = i₀
    · rw [hi]
      simp only [B, sdiff_subset, update_self]
    · simp only [B, hi, update_of_ne, Ne, not_false_iff, Finset.Subset.refl]
  have C_subset_A : ∀ i, C i ⊆ A i := by
    intro i
    by_cases hi : i = i₀
    · rw [hi]
      simp only [C, hj₂, Finset.singleton_subset_iff, update_self]
    · simp only [C, hi, update_of_ne, Ne, not_false_iff, Finset.Subset.refl]
  -- split the sum at `i₀` as the sum over `B i₀` plus the sum over `C i₀`, to use additivity.
  have A_eq_BC :
    (fun i => ∑ j ∈ A i, g i j) =
      Function.update (fun i => ∑ j ∈ A i, g i j) i₀
        ((∑ j ∈ B i₀, g i₀ j) + ∑ j ∈ C i₀, g i₀ j) := by
    ext i
    by_cases hi : i = i₀
    · rw [hi, update_self]
      have : A i₀ = B i₀ ∪ C i₀ := by
        simp only [B, C, Function.update_self, Finset.sdiff_union_self_eq_union]
        symm
        simp only [hj₂, Finset.singleton_subset_iff, Finset.union_eq_left]
      rw [this]
      refine Finset.sum_union <| Finset.disjoint_right.2 fun j hj => ?_
      have : j = j₂ := by
        simpa [C] using hj
      rw [this]
      simp only [B, mem_sdiff, eq_self_iff_true, not_true, not_false_iff, Finset.mem_singleton,
        update_self, and_false]
    · simp [hi]
  have Beq :
    Function.update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i =>
      ∑ j ∈ B i, g i j := by
    ext i
    by_cases hi : i = i₀
    · rw [hi]
      simp only [update_self]
    · simp only [B, hi, update_of_ne, Ne, not_false_iff]
  have Ceq :
    Function.update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i =>
      ∑ j ∈ C i, g i j := by
    ext i
    by_cases hi : i = i₀
    · rw [hi]
      simp only [update_self]
    · simp only [C, hi, update_of_ne, Ne, not_false_iff]
  -- Express the inductive assumption for `B`
  have Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i) := by
    have : ∑ i, #(B i) < ∑ i, #(A i) := by
      refine sum_lt_sum (fun i _ => card_le_card (B_subset_A i)) ⟨i₀, mem_univ _, ?_⟩
      have : {j₂}{j₂} ⊆ A i₀ := by simp [hj₂]
      simp only [B, Finset.card_sdiff this, Function.update_self, Finset.card_singleton]
      exact Nat.pred_lt (ne_of_gt (lt_trans Nat.zero_lt_one hi₀))
    rw [h] at this
    exact IH _ this B rfl
  -- Express the inductive assumption for `C`
  have Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i) := by
    have : (∑ i, #(C i)) < ∑ i, #(A i) :=
      Finset.sum_lt_sum (fun i _ => Finset.card_le_card (C_subset_A i))
        ⟨i₀, Finset.mem_univ _, by simp [C, hi₀]⟩
    rw [h] at this
    exact IH _ this C rfl
  have D : Disjoint (piFinset B) (piFinset C) :=
    haveI : Disjoint (B i₀) (C i₀) := by simp [B, C]
    piFinset_disjoint_of_disjoint B C this
  have pi_BC : piFinset A = piFinsetpiFinset B ∪ piFinset C := by
    apply Finset.Subset.antisymm
    · intro r hr
      by_cases hri₀ : r i₀ = j₂
      · apply Finset.mem_union_right
        refine mem_piFinset.2 fun i => ?_
        by_cases hi : i = i₀
        · have : r i₀ ∈ C i₀ := by simp [C, hri₀]
          rwa [hi]
        · simp [C, hi, mem_piFinset.1 hr i]
      · apply Finset.mem_union_left
        refine mem_piFinset.2 fun i => ?_
        by_cases hi : i = i₀
        · have : r i₀ ∈ B i₀ := by simp [B, hri₀, mem_piFinset.1 hr i₀]
          rwa [hi]
        · simp [B, hi, mem_piFinset.1 hr i]
    · exact
        Finset.union_subset (piFinset_subset _ _ fun i => B_subset_A i)
          (piFinset_subset _ _ fun i => C_subset_A i)
  rw [A_eq_BC]
  simp only [MultilinearMap.map_update_add, Beq, Ceq, Brec, Crec, pi_BC]
  rw [← Finset.sum_union D]

Multilinearity of Sums over Finite Sets: $f(\sum_{j \in A_i} g_i(j)) = \sum_{r \in \prod_i A_i} f(g_i(r(i)))$

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Let $f \colon \prod_{i \in \iota} M₁_i \to M₂$ be a multilinear map. For each $i \in \iota$, let $A_i$ be a finite set and $g_i \colon A_i \to M₁_i$ be a function. Suppose the total cardinality $\sum_{i \in \iota} |A_i|$ equals $n \in \mathbb{N}$. Then, \[ f\left(\lambda i, \sum_{j \in A_i} g_i(j)\right) = \sum_{r \in \prod_{i \in \iota} A_i} f\left(\lambda i, g_i(r(i))\right) \] where $\prod_{i \in \iota} A_i$ denotes the product set of the $A_i$'s.

MultilinearMap.map_sum_finset theorem

[DecidableEq ι] [Fintype ι] : (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)

Full source

/-- If `f` is multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate. -/
theorem map_sum_finset [DecidableEq ι] [Fintype ι] :
    (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i) :=
  f.map_sum_finset_aux _ _ rfl

Multilinearity of Finite Sums: $f(\sum_{j \in A_i} g_i(j)) = \sum_{r \in \prod_i A_i} f(g_i(r(i)))$

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, finite sets $A_i$ for each $i \in \iota$, and functions $g_i \colon A_i \to M₁_i$, we have: \[ f\left(\lambda i, \sum_{j \in A_i} g_i(j)\right) = \sum_{r \in \prod_{i \in \iota} A_i} f\left(\lambda i, g_i(r(i))\right), \] where $\prod_{i \in \iota} A_i$ denotes the product set of the $A_i$'s.

MultilinearMap.map_sum theorem

 [DecidableEq ι] [Fintype ι] [∀ i, Fintype (α i)] : (f fun i => ∑ j, g i j) = ∑ r : ∀ i, α i, f fun i => g i (r i)

Full source

/-- If `f` is multilinear, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from
multilinearity by expanding successively with respect to each coordinate. -/
theorem map_sum [DecidableEq ι] [Fintype ι] [∀ i, Fintype (α i)] :
    (f fun i => ∑ j, g i j) = ∑ r : ∀ i, α i, f fun i => g i (r i) :=
  f.map_sum_finset g fun _ => Finset.univ

Multilinear Expansion of Sums over Finite Types: $f(\sum_j g_i(j)) = \sum_r f(g_i(r(i)))$

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ and for each $i \in \iota$, a finite type $\alpha_i$ and a function $g_i \colon \alpha_i \to M₁_i$, we have: \[ f\left(\lambda i, \sum_{j \in \alpha_i} g_i(j)\right) = \sum_{r \in \prod_{i \in \iota} \alpha_i} f\left(\lambda i, g_i(r(i))\right), \] where the sum on the right is taken over all functions $r \colon \iota \to \bigcup_{i \in \iota} \alpha_i$ such that $r(i) \in \alpha_i$ for each $i \in \iota$.

MultilinearMap.map_update_sum theorem

 {α : Type*} [DecidableEq ι] (t : Finset α) (i : ι) (g : α → M₁ i) (m : ∀ i, M₁ i) :
  f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a))

Full source

theorem map_update_sum {α : Type*} [DecidableEq ι] (t : Finset α) (i : ι) (g : α → M₁ i)
    (m : ∀ i, M₁ i) : f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a)) := by
  classical
    induction t using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, ih]

Linearity of Multilinear Maps under Finite Sum Updates in a Single Coordinate

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁_i$ and $M₂$ be $R$-modules for each $i \in \iota$. For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, finite set $t$ of type $\alpha$, index $i \in \iota$, function $g \colon \alpha \to M₁_i$, and vector $m \in \prod_{i \in \iota} M₁_i$, we have: \[ f\left(m[i \mapsto \sum_{a \in t} g(a)]\right) = \sum_{a \in t} f\left(m[i \mapsto g(a)]\right) \] where $m[i \mapsto v]$ denotes the vector obtained by updating the $i$-th coordinate of $m$ to $v$.

MultilinearMap.codRestrict definition

(f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ v, f v ∈ p) : MultilinearMap R M₁ p

Full source

/-- Restrict the codomain of a multilinear map to a submodule.

This is the multilinear version of `LinearMap.codRestrict`. -/
@[simps]
def codRestrict (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ v, f v ∈ p) :
    MultilinearMap R M₁ p where
  toFun v := ⟨f v, h v⟩
  map_update_add' _ _ _ _ := Subtype.ext <| MultilinearMap.map_update_add _ _ _ _ _
  map_update_smul' _ _ _ _ := Subtype.ext <| MultilinearMap.map_update_smul _ _ _ _ _

Codomain restriction of a multilinear map to a submodule

Informal description

Given a multilinear map $ f $ from $ \prod_{i \in \iota} M₁_i $ to $ M₂ $ and a submodule $ p $ of $ M₂ $ such that $ f(v) \in p $ for all $ v \in \prod_{i \in \iota} M₁_i $, the function `codRestrict` restricts the codomain of $ f $ to $ p $. Specifically, it constructs a new multilinear map from $ \prod_{i \in \iota} M₁_i $ to $ p $ by mapping each $ v $ to $ \langle f(v), h(v) \rangle $, where $ h(v) $ is the proof that $ f(v) \in p $.

MultilinearMap.restrictScalars definition

(f : MultilinearMap A M₁ M₂) : MultilinearMap R M₁ M₂

Full source

/-- Reinterpret an `A`-multilinear map as an `R`-multilinear map, if `A` is an algebra over `R`
and their actions on all involved modules agree with the action of `R` on `A`. -/
def restrictScalars (f : MultilinearMap A M₁ M₂) : MultilinearMap R M₁ M₂ where
  toFun := f
  map_update_add' := f.map_update_add
  map_update_smul' m i := (f.toLinearMap m i).map_smul_of_tower

Restriction of scalars for multilinear maps

Informal description

Given a semiring $A$ that is an algebra over another semiring $R$, and modules $M₁_i$ and $M₂$ over $A$ (which are also modules over $R$ via the algebra structure), any $A$-multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ can be reinterpreted as an $R$-multilinear map. This reinterpretation preserves the multilinear structure, meaning the map remains linear in each coordinate when the others are fixed.

MultilinearMap.coe_restrictScalars theorem

(f : MultilinearMap A M₁ M₂) : ⇑(f.restrictScalars R) = f

Full source

@[simp]
theorem coe_restrictScalars (f : MultilinearMap A M₁ M₂) : ⇑(f.restrictScalars R) = f :=
  rfl

Underlying Function Equality for Scalar-Restricted Multilinear Maps

Informal description

For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ over a semiring $A$ that is an algebra over $R$, the underlying function of the scalar-restricted map $f.\text{restrictScalars}\, R$ is equal to $f$ itself.

MultilinearMap.domDomCongr definition

 (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) : MultilinearMap R (fun _ : ι₂ => M₂) M₃

Full source

/-- Transfer the arguments to a map along an equivalence between argument indices.

The naming is derived from `Finsupp.domCongr`, noting that here the permutation applies to the
domain of the domain. -/
@[simps apply]
def domDomCongr (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
    MultilinearMap R (fun _ : ι₂ => M₂) M₃ where
  toFun v := m fun i => v (σ i)
  map_update_add' v i a b := by
    letI := σ.injective.decidableEq
    simp_rw [Function.update_apply_equiv_apply v]
    rw [m.map_update_add]
  map_update_smul' v i a b := by
    letI := σ.injective.decidableEq
    simp_rw [Function.update_apply_equiv_apply v]
    rw [m.map_update_smul]

Multilinear map reindexing via equivalence

Informal description

Given an equivalence (bijection) $\sigma : \iota_1 \simeq \iota_2$ between index types and a multilinear map $m$ from $\prod_{i \in \iota_1} M_2$ to $M_3$, the function constructs a new multilinear map from $\prod_{i \in \iota_2} M_2$ to $M_3$ by reindexing the input via $\sigma$. Specifically, for any vector $v \in \prod_{i \in \iota_2} M_2$, the new map evaluates to $m(\lambda i, v(\sigma i))$. This operation preserves multilinearity, meaning the resulting map is linear in each coordinate when the others are fixed.

MultilinearMap.domDomCongr_trans theorem

 (σ₁ : ι₁ ≃ ι₂) (σ₂ : ι₂ ≃ ι₃) (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
  m.domDomCongr (σ₁.trans σ₂) = (m.domDomCongr σ₁).domDomCongr σ₂

Full source

theorem domDomCongr_trans (σ₁ : ι₁ ≃ ι₂) (σ₂ : ι₂ ≃ ι₃)
    (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
    m.domDomCongr (σ₁.trans σ₂) = (m.domDomCongr σ₁).domDomCongr σ₂ :=
  rfl

Composition Property of Multilinear Map Reindexing

Informal description

Let $\sigma_1 : \iota_1 \simeq \iota_2$ and $\sigma_2 : \iota_2 \simeq \iota_3$ be equivalences between index types, and let $m$ be a multilinear map from $\prod_{i \in \iota_1} M_2$ to $M_3$. Then the reindexing of $m$ via the composition $\sigma_1 \circ \sigma_2$ is equal to the reindexing of $m$ via $\sigma_1$ followed by reindexing via $\sigma_2$. In other words, we have: \[ m.\text{domDomCongr}(\sigma_1 \circ \sigma_2) = (m.\text{domDomCongr} \sigma_1).\text{domDomCongr} \sigma_2 \]

MultilinearMap.domDomCongr_mul theorem

 (σ₁ : Equiv.Perm ι₁) (σ₂ : Equiv.Perm ι₁) (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
  m.domDomCongr (σ₂ * σ₁) = (m.domDomCongr σ₁).domDomCongr σ₂

Full source

theorem domDomCongr_mul (σ₁ : Equiv.Perm ι₁) (σ₂ : Equiv.Perm ι₁)
    (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
    m.domDomCongr (σ₂ * σ₁) = (m.domDomCongr σ₁).domDomCongr σ₂ :=
  rfl

Composition of Permutations and Multilinear Map Reindexing

Informal description

Let $M_2$ and $M_3$ be modules over a semiring $R$, and let $\sigma_1, \sigma_2$ be permutations of an index set $\iota_1$. For any multilinear map $m$ from $\prod_{i \in \iota_1} M_2$ to $M_3$, the reindexing of $m$ by the composition $\sigma_2 \circ \sigma_1$ is equal to first reindexing $m$ by $\sigma_1$ and then reindexing the result by $\sigma_2$. In other words, the following equality holds: $$ m \circ (\sigma_2 \circ \sigma_1) = (m \circ \sigma_1) \circ \sigma_2. $$

MultilinearMap.domDomCongrEquiv definition

 (σ : ι₁ ≃ ι₂) : MultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃+ MultilinearMap R (fun _ : ι₂ => M₂) M₃

Full source

/-- `MultilinearMap.domDomCongr` as an equivalence.

This is declared separately because it does not work with dot notation. -/
@[simps apply symm_apply]
def domDomCongrEquiv (σ : ι₁ ≃ ι₂) :
    MultilinearMapMultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃+ MultilinearMap R (fun _ : ι₂ => M₂) M₃ where
  toFun := domDomCongr σ
  invFun := domDomCongr σ.symm
  left_inv m := by
    ext
    simp [domDomCongr]
  right_inv m := by
    ext
    simp [domDomCongr]
  map_add' a b := by
    ext
    simp [domDomCongr]

Additive equivalence of multilinear maps via index reindexing

Informal description

Given an equivalence (bijection) $\sigma : \iota_1 \simeq \iota_2$ between index types, the function constructs an additive equivalence between the space of multilinear maps from $\prod_{i \in \iota_1} M_2$ to $M_3$ and the space of multilinear maps from $\prod_{i \in \iota_2} M_2$ to $M_3$. The forward direction reindexes the input via $\sigma$, while the inverse direction reindexes via $\sigma^{-1}$. This equivalence preserves addition of multilinear maps.

MultilinearMap.domDomCongr_eq_iff theorem

 (σ : ι₁ ≃ ι₂) (f g : MultilinearMap R (fun _ : ι₁ => M₂) M₃) : f.domDomCongr σ = g.domDomCongr σ ↔ f = g

Full source

/-- The results of applying `domDomCongr` to two maps are equal if
and only if those maps are. -/
@[simp]
theorem domDomCongr_eq_iff (σ : ι₁ ≃ ι₂) (f g : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
    f.domDomCongr σ = g.domDomCongr σ ↔ f = g :=
  (domDomCongrEquiv σ : _ ≃+ MultilinearMap R (fun _ => M₂) M₃).apply_eq_iff_eq

Equality of Reindexed Multilinear Maps via Equivalence

Informal description

Let $R$ be a semiring, $\iota_1$ and $\iota_2$ be types, $M_2$ be an $R$-module, and $M_3$ be an $R$-module. Given an equivalence $\sigma : \iota_1 \simeq \iota_2$ and two multilinear maps $f, g : \text{MultilinearMap}_R (\lambda \_, M_2) M_3$, the reindexed maps $f \circ \sigma$ and $g \circ \sigma$ are equal if and only if $f = g$.

MultilinearMap.domDomRestrict_aux theorem

 {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*} [DecidableEq { a // P a }]
  (x : (i : { a // P a }) → M₁ i) (z : (i : { a // ¬P a }) → M₁ i) (i : { a : ι // P a }) (c : M₁ i) :
  (fun j ↦ if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c

Full source

lemma domDomRestrict_aux {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*}
    [DecidableEq {a // P a}]
    (x : (i : {a // P a}) → M₁ i) (z : (i : {a // ¬ P a}) → M₁ i) (i : {a : ι // P a})
    (c : M₁ i) : (fun j ↦ if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c := by
  ext j
  by_cases h : j = i
  · rw [h, Function.update_self]
    simp only [i.2, update_self, dite_true]
  · rw [Function.update_of_ne h]
    by_cases h' : P j
    · simp only [h', ne_eq, Subtype.mk.injEq, dite_true]
      have h'' : ¬ ⟨j, h'⟩ = i :=
        fun he => by apply_fun (fun x => x.1) at he; exact h he
      rw [Function.update_of_ne h'']
    · simp only [h', ne_eq, Subtype.mk.injEq, dite_false]

Equality of Updated Piecewise Functions for Multilinear Map Domain Restriction

Informal description

Let $\iota$ be a type with decidable equality, $P : \iota \to \text{Prop}$ a decidable predicate, and $M_1 : \iota \to \text{Type*}$ a family of types. For any $x : \prod_{i \in \{a // P a\}} M_1 i$, $z : \prod_{i \in \{a // \neg P a\}} M_1 i$, $i \in \{a // P a\}$, and $c \in M_1 i$, the following equality holds: \[ \left(\lambda j, \text{if } h : P j \text{ then } \text{update } x \, i \, c \, \langle j, h \rangle \text{ else } z \, \langle j, h \rangle\right) = \text{update } (\lambda j, \text{if } h : P j \text{ then } x \, \langle j, h \rangle \text{ else } z \, \langle j, h \rangle) \, i \, c \]

MultilinearMap.domDomRestrict_aux_right theorem

 {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*} [DecidableEq { a // ¬P a }]
  (x : (i : { a // P a }) → M₁ i) (z : (i : { a // ¬P a }) → M₁ i) (i : { a : ι // ¬P a }) (c : M₁ i) :
  (fun j ↦ if h : P j then x ⟨j, h⟩ else Function.update z i c ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c

Full source

lemma domDomRestrict_aux_right {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*}
    [DecidableEq {a // ¬ P a}]
    (x : (i : {a // P a}) → M₁ i) (z : (i : {a // ¬ P a}) → M₁ i) (i : {a : ι // ¬ P a})
    (c : M₁ i) : (fun j ↦ if h : P j then x ⟨j, h⟩ else Function.update z i c ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c := by
  simpa only [dite_not] using domDomRestrict_aux _ z (fun j ↦ x ⟨j.1, not_not.mp j.2⟩) i c

Equality of Updated Piecewise Functions for Multilinear Map Domain Restriction (Right Case)

Informal description

Let $\iota$ be a type with decidable equality, $P : \iota \to \text{Prop}$ a decidable predicate, and $M_1 : \iota \to \text{Type*}$ a family of types. For any $x : \prod_{i \in \{a // P a\}} M_1 i$, $z : \prod_{i \in \{a // \neg P a\}} M_1 i$, $i \in \{a // \neg P a\}$, and $c \in M_1 i$, the following equality holds: \[ \left(\lambda j, \text{if } h : P j \text{ then } x \langle j, h \rangle \text{ else } \text{update } z \, i \, c \, \langle j, h \rangle\right) = \text{update } (\lambda j, \text{if } h : P j \text{ then } x \langle j, h \rangle \text{ else } z \langle j, h \rangle) \, i \, c \]

MultilinearMap.domDomRestrict definition

 (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P] (z : (i : { a : ι // ¬P a }) → M₁ i) :
  MultilinearMap R (fun (i : { a : ι // P a }) => M₁ i) M₂

Full source

/-- Given a multilinear map `f` on `(i : ι) → M i`, a (decidable) predicate `P` on `ι` and
an element `z` of `(i : {a // ¬ P a}) → M₁ i`, construct a multilinear map on
`(i : {a // P a}) → M₁ i)` whose value at `x` is `f` evaluated at the vector with `i`th coordinate
`x i` if `P i` and `z i` otherwise.

The naming is similar to `MultilinearMap.domDomCongr`: here we are applying the restriction to the
domain of the domain.

For a linear map version, see `MultilinearMap.domDomRestrictₗ`.
-/
def domDomRestrict (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P]
    (z : (i : {a : ι // ¬ P a}) → M₁ i) :
    MultilinearMap R (fun (i : {a : ι // P a}) => M₁ i) M₂ where
  toFun x := f (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩)
  map_update_add' x i a b := by
    classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_add]
  map_update_smul' z i c a := by
    classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_smul]

Restriction of a multilinear map to a subdomain defined by a predicate

Informal description

Given a multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, a decidable predicate $P$ on $\iota$, and a fixed element $z$ of $\prod_{i \in \{a \mid \neg P a\}} M₁_i$, the function `MultilinearMap.domDomRestrict` constructs a multilinear map from $\prod_{i \in \{a \mid P a\}} M₁_i$ to $M₂$. This new map evaluates at $x$ by extending $x$ with $z$ on the coordinates where $P$ does not hold and then applying $f$ to the resulting vector.

MultilinearMap.domDomRestrict_apply theorem

 (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P] (x : (i : { a // P a }) → M₁ i)
  (z : (i : { a // ¬P a }) → M₁ i) : f.domDomRestrict P z x = f (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩)

Full source

@[simp]
lemma domDomRestrict_apply (f : MultilinearMap R M₁ M₂) (P : ι → Prop)
    [DecidablePred P] (x : (i : {a // P a}) → M₁ i) (z : (i : {a // ¬ P a}) → M₁ i) :
    f.domDomRestrict P z x = f (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) := rfl

Evaluation of Restricted Multilinear Map via Piecewise Extension

Informal description

Let $R$ be a semiring, $\iota$ a type, and $M₁ : \iota \to \text{Type}$ and $M₂$ be $R$-modules. Given a multilinear map $f : \text{MultilinearMap}\, R\, M₁\, M₂$, a decidable predicate $P : \iota \to \text{Prop}$, and a fixed element $z \in \prod_{i \in \{a \mid \neg P a\}} M₁ i$, the restricted multilinear map $f.\text{domDomRestrict}\, P\, z$ evaluated at $x \in \prod_{i \in \{a \mid P a\}} M₁ i$ satisfies: \[ f.\text{domDomRestrict}\, P\, z\, x = f \left(\lambda j, \begin{cases} x \langle j, h \rangle & \text{if } h : P j \\ z \langle j, h \rangle & \text{otherwise} \end{cases} \right) \] where $\langle j, h \rangle$ denotes the subtype element.

MultilinearMap.linearDeriv definition

 [DecidableEq ι] [Fintype ι] (f : MultilinearMap R M₁ M₂) (x : (i : ι) → M₁ i) : ((i : ι) → M₁ i) →ₗ[R] M₂

Full source

/-- The "derivative" of a multilinear map, as a linear map from `(i : ι) → M₁ i` to `M₂`.
For continuous multilinear maps, this will indeed be the derivative. -/
def linearDeriv [DecidableEq ι] [Fintype ι] (f : MultilinearMap R M₁ M₂)
    (x : (i : ι) → M₁ i) : ((i : ι) → M₁ i) →ₗ[R] M₂ :=
  ∑ i : ι, (f.toLinearMap x i).comp (LinearMap.proj i)

Linear derivative of a multilinear map

Informal description

Given a multilinear map $ f $ from $ \prod_{i \in \iota} M₁_i $ to $ M₂ $ (where $ \iota $ is a finite type with decidable equality) and a fixed element $ x \in \prod_{i \in \iota} M₁_i $, the linear derivative $ \text{linearDeriv} $ of $ f $ at $ x $ is the linear map from $ \prod_{i \in \iota} M₁_i $ to $ M₂ $ defined by: \[ \text{linearDeriv}_f(x)(y) = \sum_{i \in \iota} f(x_1, \dots, x_{i-1}, y_i, x_{i+1}, \dots, x_n) \] where $ y \in \prod_{i \in \iota} M₁_i $.

MultilinearMap.linearDeriv_apply theorem

 [DecidableEq ι] [Fintype ι] (f : MultilinearMap R M₁ M₂) (x y : (i : ι) → M₁ i) :
  f.linearDeriv x y = ∑ i, f (update x i (y i))

Full source

@[simp]
lemma linearDeriv_apply [DecidableEq ι] [Fintype ι] (f : MultilinearMap R M₁ M₂)
    (x y : (i : ι) → M₁ i) :
    f.linearDeriv x y = ∑ i, f (update x i (y i)) := by
  unfold linearDeriv
  simp only [LinearMap.coeFn_sum, LinearMap.coe_comp, LinearMap.coe_proj, Finset.sum_apply,
    Function.comp_apply, Function.eval, toLinearMap_apply]

Sum Formula for the Linear Derivative of a Multilinear Map

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and $M₁ : \iota \to \text{Type}$ and $M₂$ be $R$-modules. For any multilinear map $f : \text{MultilinearMap}\, R\, M₁\, M₂$ and vectors $x, y \in \prod_{i \in \iota} M₁_i$, the linear derivative of $f$ at $x$ applied to $y$ satisfies: \[ f.\text{linearDeriv}(x)(y) = \sum_{i \in \iota} f(x_1, \dots, x_{i-1}, y_i, x_{i+1}, \dots, x_n) \] where $x_j$ denotes the $j$-th component of $x$ and similarly for $y_j$.

LinearMap.compMultilinearMap definition

(g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) : MultilinearMap R M₁ M₃

Full source

/-- Composing a multilinear map with a linear map gives again a multilinear map. -/
def compMultilinearMap (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) : MultilinearMap R M₁ M₃ where
  toFun := g ∘ f
  map_update_add' m i x y := by simp
  map_update_smul' m i c x := by simp

Composition of a linear map with a multilinear map

Informal description

Given a linear map $ g : M₂ \to M₃ $ and a multilinear map $ f : \prod_{i \in \iota} M₁_i \to M₂ $, the composition $ g \circ f $ is a multilinear map from $ \prod_{i \in \iota} M₁_i $ to $ M₃ $. This composition preserves the multilinearity of $ f $, meaning it remains linear in each coordinate when all other coordinates are fixed.

LinearMap.coe_compMultilinearMap theorem

(g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) : ⇑(g.compMultilinearMap f) = g ∘ f

Full source

@[simp]
theorem coe_compMultilinearMap (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
    ⇑(g.compMultilinearMap f) = g ∘ f :=
  rfl

Composition of Linear and Multilinear Maps Preserves Underlying Function

Informal description

Let $R$ be a semiring, $\iota$ be a type, and for each $i \in \iota$, let $M₁_i$ and $M₂, M₃$ be $R$-modules. Given a linear map $g : M₂ \to M₃$ and a multilinear map $f : \prod_{i \in \iota} M₁_i \to M₂$, the underlying function of the composition $g \circ f$ is equal to the pointwise composition of $g$ with $f$.

LinearMap.compMultilinearMap_apply theorem

(g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) : g.compMultilinearMap f m = g (f m)

Full source

@[simp]
theorem compMultilinearMap_apply (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) :
    g.compMultilinearMap f m = g (f m) :=
  rfl

Evaluation of Linear-Multilinear Map Composition: $(g \circ f)(m) = g(f(m))$

Informal description

Let $R$ be a semiring, $\iota$ be an index type, and $M₁ : \iota \to \text{Type}$ and $M₂, M₃$ be modules over $R$. Given a linear map $g : M₂ \to M₃$ and a multilinear map $f : \prod_{i \in \iota} M₁_i \to M₂$, the composition $g \circ f$ evaluated at a point $m \in \prod_{i \in \iota} M₁_i$ equals $g$ applied to $f(m)$, i.e., $$(g \circ f)(m) = g(f(m)).$$

LinearMap.compMultilinearMap_zero theorem

(g : M₂ →ₗ[R] M₃) : g.compMultilinearMap (0 : MultilinearMap R M₁ M₂) = 0

Full source

@[simp]
theorem compMultilinearMap_zero (g : M₂ →ₗ[R] M₃) :
    g.compMultilinearMap (0 : MultilinearMap R M₁ M₂) = 0 :=
  MultilinearMap.ext fun _ => map_zero g

Composition with Zero Multilinear Map Yields Zero

Informal description

For any linear map $g \colon M_2 \to M_3$ over a semiring $R$, the composition of $g$ with the zero multilinear map in $\text{MultilinearMap}\, R\, M_1\, M_2$ equals the zero multilinear map in $\text{MultilinearMap}\, R\, M_1\, M_3$. That is, $g \circ 0 = 0$.

LinearMap.zero_compMultilinearMap theorem

(f : MultilinearMap R M₁ M₂) : (0 : M₂ →ₗ[R] M₃).compMultilinearMap f = 0

Full source

@[simp]
theorem zero_compMultilinearMap (f : MultilinearMap R M₁ M₂) :
    (0 : M₂ →ₗ[R] M₃).compMultilinearMap f = 0 := rfl

Composition of Zero Linear Map with Any Multilinear Map Yields Zero Map

Informal description

For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$ over a semiring $R$, the composition of the zero linear map $0 \colon M₂ \to M₃$ with $f$ is the zero multilinear map, i.e., $0 \circ f = 0$.

LinearMap.compMultilinearMap_add theorem

 (g : M₂ →ₗ[R] M₃) (f₁ f₂ : MultilinearMap R M₁ M₂) :
  g.compMultilinearMap (f₁ + f₂) = g.compMultilinearMap f₁ + g.compMultilinearMap f₂

Full source

@[simp]
theorem compMultilinearMap_add (g : M₂ →ₗ[R] M₃) (f₁ f₂ : MultilinearMap R M₁ M₂) :
    g.compMultilinearMap (f₁ + f₂) = g.compMultilinearMap f₁ + g.compMultilinearMap f₂ :=
  MultilinearMap.ext fun _ => map_add g _ _

Additivity of Linear Map Composition with Multilinear Maps

Informal description

Let $R$ be a semiring, $\iota$ be a type, and $M₁ : \iota \to \text{Type}$ and $M₂, M₃$ be $R$-modules. For any linear map $g : M₂ \to M₃$ and any two multilinear maps $f₁, f₂ : \text{MultilinearMap}_R M₁ M₂$, the composition of $g$ with the sum of $f₁$ and $f₂$ equals the sum of the compositions of $g$ with $f₁$ and $g$ with $f₂$. That is, $$ g \circ (f₁ + f₂) = (g \circ f₁) + (g \circ f₂). $$

LinearMap.add_compMultilinearMap theorem

 (g₁ g₂ : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
  (g₁ + g₂).compMultilinearMap f = g₁.compMultilinearMap f + g₂.compMultilinearMap f

Full source

@[simp]
theorem add_compMultilinearMap (g₁ g₂ : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
    (g₁ + g₂).compMultilinearMap f = g₁.compMultilinearMap f + g₂.compMultilinearMap f := rfl

Additivity of Linear Map Composition with Multilinear Maps

Informal description

Let $R$ be a semiring, $\iota$ be a type, and $M₁ : \iota \to \text{Type}$ and $M₂, M₃$ be $R$-modules. For any two linear maps $g₁, g₂ : M₂ \to M₃$ and any multilinear map $f : \prod_{i \in \iota} M₁_i \to M₂$, the composition of the sum $g₁ + g₂$ with $f$ is equal to the sum of the compositions $g₁ \circ f$ and $g₂ \circ f$. That is, $$(g₁ + g₂) \circ f = g₁ \circ f + g₂ \circ f.$$

LinearMap.compMultilinearMap_smul theorem

 [DistribSMul S M₂] [DistribSMul S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃] [CompatibleSMul M₂ M₃ S R]
  (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) : g.compMultilinearMap (s • f) = s • g.compMultilinearMap f

Full source

@[simp]
theorem compMultilinearMap_smul [DistribSMul S M₂] [DistribSMul S M₃]
    [SMulCommClass R S M₂] [SMulCommClass R S M₃] [CompatibleSMul M₂ M₃ S R]
    (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
    g.compMultilinearMap (s • f) = s • g.compMultilinearMap f :=
  MultilinearMap.ext fun _ => g.map_smul_of_tower _ _

Compatibility of Linear Composition with Scalar Multiplication for Multilinear Maps

Informal description

Let $R$ be a semiring, $S$ a scalar type, and $M₂$, $M₃$ be $R$-modules with compatible scalar multiplication by $S$. For any linear map $g \colon M₂ \to M₃$ and any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, the composition of $g$ with the scalar multiple $s \cdot f$ equals the scalar multiple $s \cdot (g \circ f)$. That is, \[ g \circ (s \cdot f) = s \cdot (g \circ f). \]

LinearMap.smul_compMultilinearMap theorem

 [Monoid S] [DistribMulAction S M₃] [SMulCommClass R S M₃] (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
  (s • g).compMultilinearMap f = s • g.compMultilinearMap f

Full source

@[simp]
theorem smul_compMultilinearMap [Monoid S] [DistribMulAction S M₃] [SMulCommClass R S M₃]
    (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
    (s • g).compMultilinearMap f = s • g.compMultilinearMap f := rfl

Scalar Multiplication Commutes with Linear-Multilinear Composition

Informal description

Let $S$ be a monoid acting distributively on an $R$-module $M₃$, with the action commuting with the $R$-module structure. For any linear map $g : M₂ \to M₃$, scalar $s \in S$, and multilinear map $f : \prod_{i \in \iota} M₁_i \to M₂$, we have: $$(s \cdot g) \circ f = s \cdot (g \circ f)$$ where $\circ$ denotes composition of multilinear maps and $\cdot$ denotes the scalar action.

LinearMap.subtype_compMultilinearMap_codRestrict theorem

(f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h) : p.subtype.compMultilinearMap (f.codRestrict p h) = f

Full source

/-- The multilinear version of `LinearMap.subtype_comp_codRestrict` -/
@[simp]
theorem subtype_compMultilinearMap_codRestrict (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂)
    (h) : p.subtype.compMultilinearMap (f.codRestrict p h) = f :=
  rfl

Submodule Inclusion Composed with Codomain-Restricted Multilinear Map Equals Original Map

Informal description

Let $R$ be a semiring, $\iota$ a type, and $M_1 : \iota \to \text{Type}$, $M_2$ be $R$-modules. Given a multilinear map $f : \text{MultilinearMap}\, R\, M_1\, M_2$, a submodule $p$ of $M_2$, and a proof $h$ that $f(v) \in p$ for all $v \in \prod_{i \in \iota} M_1(i)$, then the composition of the submodule inclusion $\text{subtype} : p \hookrightarrow M_2$ with the codomain-restricted map $f.\text{codRestrict}\, p\, h$ equals the original multilinear map $f$.

LinearMap.compMultilinearMap_codRestrict theorem

 (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (p : Submodule R M₃) (h) :
  (g.codRestrict p h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p fun v => h (f v)

Full source

/-- The multilinear version of `LinearMap.comp_codRestrict` -/
@[simp]
theorem compMultilinearMap_codRestrict (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂)
    (p : Submodule R M₃) (h) :
    (g.codRestrict p h).compMultilinearMap f =
      (g.compMultilinearMap f).codRestrict p fun v => h (f v) :=
  rfl

Compatibility of Linear Map Composition and Codomain Restriction for Multilinear Maps

Informal description

Let $R$ be a semiring, $\iota$ be a type, and $M₁ : \iota \to \text{Type}$ and $M₂, M₃$ be modules over $R$. Given a linear map $g : M₂ \to M₃$, a multilinear map $f : \prod_{i \in \iota} M₁ i \to M₂$, and a submodule $p$ of $M₃$ such that $g(f(v)) \in p$ for all $v \in \prod_{i \in \iota} M₁ i$, the following equality holds: \[ (g \text{ restricted to } p).compMultilinearMap\, f = (g.compMultilinearMap\, f) \text{ restricted to } p. \] Here, the restriction of $g$ to $p$ is the linear map obtained by composing $g$ with the inclusion of $p$ into $M₃$, and the right-hand side is the codomain restriction of the composition of $g$ with $f$ to the submodule $p$.

LinearMap.compMultilinearMap_domDomCongr theorem

 (σ : ι₁ ≃ ι₂) (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R (fun _ : ι₁ => M') M₂) :
  (g.compMultilinearMap f).domDomCongr σ = g.compMultilinearMap (f.domDomCongr σ)

Full source

@[simp]
theorem compMultilinearMap_domDomCongr (σ : ι₁ ≃ ι₂) (g : M₂ →ₗ[R] M₃)
    (f : MultilinearMap R (fun _ : ι₁ => M') M₂) :
    (g.compMultilinearMap f).domDomCongr σ = g.compMultilinearMap (f.domDomCongr σ) := by
  ext
  simp [MultilinearMap.domDomCongr]

Compatibility of Linear Map Composition with Multilinear Map Reindexing

Informal description

Let $\sigma : \iota_1 \simeq \iota_2$ be an equivalence between index types, $g : M_2 \to M_3$ a linear map, and $f : \prod_{i \in \iota_1} M' \to M_2$ a multilinear map. Then the composition of $g$ with the reindexed multilinear map $f$ via $\sigma$ is equal to the reindexing via $\sigma$ of the composition of $g$ with $f$. That is, $$(g \circ f) \circ \sigma = g \circ (f \circ \sigma).$$

MultilinearMap.instDistribMulActionOfSMulCommClass instance

 [Monoid S] [DistribMulAction S M₂] [Module R M₂] [SMulCommClass R S M₂] : DistribMulAction S (MultilinearMap R M₁ M₂)

Full source

instance [Monoid S] [DistribMulAction S M₂] [Module R M₂] [SMulCommClass R S M₂] :
    DistribMulAction S (MultilinearMap R M₁ M₂) :=
  coe_injective.distribMulAction coeAddMonoidHom fun _ _ ↦ rfl

Distributive Multiplicative Action on Multilinear Maps with Commuting Scalars

Informal description

For any monoid $S$ acting distributively on an $R$-module $M₂$ with commuting scalar actions of $R$ and $S$, the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ inherits a distributive multiplicative action from $S$. This means that for any scalar $s \in S$ and multilinear maps $f, g$, we have $s \cdot (f + g) = s \cdot f + s \cdot g$ and $(s_1 \cdot s_2) \cdot f = s_1 \cdot (s_2 \cdot f)$.

MultilinearMap.instModule instance

: Module S (MultilinearMap R M₁ M₂)

Full source

/-- The space of multilinear maps over an algebra over `R` is a module over `R`, for the pointwise
addition and scalar multiplication. -/
instance : Module S (MultilinearMap R M₁ M₂) :=
  coe_injective.module _ coeAddMonoidHom fun _ _ ↦ rfl

Module Structure on Multilinear Maps

Informal description

The space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ forms a module over $S$ under pointwise scalar multiplication. That is, for any semiring $R$, type $\iota$, family of $R$-modules $M₁ : \iota \to \text{Type}$, and $R$-module $M₂$, the set of multilinear maps from $\prod_{i \in \iota} M₁_i$ to $M₂$ is equipped with a scalar multiplication operation by elements of $S$ and an addition operation, satisfying the usual module axioms.

MultilinearMap.instNoZeroSMulDivisors instance

[NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (MultilinearMap R M₁ M₂)

Full source

instance [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (MultilinearMap R M₁ M₂) :=
  coe_injective.noZeroSMulDivisors _ rfl coe_smul

No Zero Scalar Divisors in Multilinear Maps

Informal description

For any semiring $R$, type $\iota$, family of $R$-modules $M₁ : \iota \to \text{Type}$, and $R$-module $M₂$ with no zero scalar divisors with respect to a scalar ring $S$, the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ also has no zero scalar divisors with respect to $S$. This means that for any scalar $c \in S$ and any multilinear map $f$, if $c \cdot f = 0$, then either $c = 0$ or $f = 0$.

LinearMap.compMultilinearMapₗ definition

 [Semiring S] [Module S M₂] [Module S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃]
  [LinearMap.CompatibleSMul M₂ M₃ S R] (g : M₂ →ₗ[R] M₃) : MultilinearMap R M₁ M₂ →ₗ[S] MultilinearMap R M₁ M₃

Full source

/-- `LinearMap.compMultilinearMap` as an `S`-linear map. -/
@[simps]
def _root_.LinearMap.compMultilinearMapₗ [Semiring S] [Module S M₂] [Module S M₃]
    [SMulCommClass R S M₂] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₂ M₃ S R]
    (g : M₂ →ₗ[R] M₃) :
    MultilinearMapMultilinearMap R M₁ M₂ →ₗ[S] MultilinearMap R M₁ M₃ where
  toFun := g.compMultilinearMap
  map_add' := g.compMultilinearMap_add
  map_smul' := g.compMultilinearMap_smul

$S$-linear composition of a linear map with multilinear maps

Informal description

Given a semiring $R$, a type $\iota$, a family of $R$-modules $M₁ : \iota \to \text{Type}$, and $R$-modules $M₂$ and $M₃$, and a semiring $S$ such that $M₂$ and $M₃$ are also $S$-modules with compatible scalar actions, the function that composes a linear map $g : M₂ \to M₃$ with a multilinear map $f : \prod_{i \in \iota} M₁_i \to M₂$ is itself an $S$-linear map from the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ to $\text{MultilinearMap}\, R\, M₁\, M₃$. More precisely, for any linear map $g : M₂ \to M₃$, the map $f \mapsto g \circ f$ is $S$-linear, meaning it preserves addition and scalar multiplication: - $(g \circ (f₁ + f₂)) = (g \circ f₁) + (g \circ f₂)$ for any multilinear maps $f₁, f₂$, - $(g \circ (c \cdot f)) = c \cdot (g \circ f)$ for any scalar $c \in S$ and multilinear map $f$.

MultilinearMap.ofSubsingletonₗ definition

[Subsingleton ι] (i : ι) : (M₂ →ₗ[R] M₃) ≃ₗ[S] MultilinearMap R (fun _ : ι ↦ M₂) M₃

Full source

/-- Linear equivalence between linear maps `M₂ →ₗ[R] M₃`
and one-multilinear maps `MultilinearMap R (fun _ : ι ↦ M₂) M₃`. -/
@[simps +simpRhs]
def ofSubsingletonₗ [Subsingleton ι] (i : ι) :
    (M₂ →ₗ[R] M₃) ≃ₗ[S] MultilinearMap R (fun _ : ι ↦ M₂) M₃ :=
  { ofSubsingleton R M₂ M₃ i with
    map_add' := fun _ _ ↦ rfl
    map_smul' := fun _ _ ↦ rfl }

Linear equivalence between linear maps and multilinear maps on subsingleton index types

Informal description

Given a type $\iota$ with at most one element (i.e., a subsingleton) and a fixed index $i \in \iota$, there is a natural linear equivalence between linear maps $M_2 \to_{R} M_3$ and multilinear maps $\prod_{i \in \iota} M_2 \to M_3$. Specifically: - The forward direction takes a linear map $f : M_2 \to_{R} M_3$ and constructs a multilinear map that evaluates $f$ at the $i$-th coordinate of its input. - The backward direction takes a multilinear map $f : \prod_{i \in \iota} M_2 \to M_3$ and constructs a linear map by applying $f$ to a constant family where every coordinate equals the input. This equivalence holds because, when $\iota$ is a subsingleton, a multilinear map depends only on the value at the single (or nonexistent) coordinate, reducing to the linear case. The equivalence is linear with respect to the scalar ring $S$.

MultilinearMap.domDomCongrLinearEquiv' definition

 {ι' : Type*} (σ : ι ≃ ι') : MultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R (fun i => M₁ (σ.symm i)) M₂

Full source

/-- The dependent version of `MultilinearMap.domDomCongrLinearEquiv`. -/
@[simps apply symm_apply]
def domDomCongrLinearEquiv' {ι' : Type*} (σ : ι ≃ ι') :
    MultilinearMapMultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R (fun i => M₁ (σ.symm i)) M₂ where
  toFun f :=
    { toFun := f ∘ (σ.piCongrLeft' M₁).symm
      map_update_add' := fun m i => by
        letI := σ.decidableEq
        rw [← σ.apply_symm_apply i]
        intro x y
        simp only [comp_apply, piCongrLeft'_symm_update, f.map_update_add]
      map_update_smul' := fun m i c => by
        letI := σ.decidableEq
        rw [← σ.apply_symm_apply i]
        intro x
        simp only [Function.comp, piCongrLeft'_symm_update, f.map_update_smul] }
  invFun f :=
    { toFun := f ∘ σ.piCongrLeft' M₁
      map_update_add' := fun m i => by
        letI := σ.symm.decidableEq
        rw [← σ.symm_apply_apply i]
        intro x y
        simp only [comp_apply, piCongrLeft'_update, f.map_update_add]
      map_update_smul' := fun m i c => by
        letI := σ.symm.decidableEq
        rw [← σ.symm_apply_apply i]
        intro x
        simp only [Function.comp, piCongrLeft'_update, f.map_update_smul] }
  map_add' f₁ f₂ := by
    ext
    simp only [Function.comp, coe_mk, add_apply]
  map_smul' c f := by
    ext
    simp only [Function.comp, coe_mk, smul_apply, RingHom.id_apply]
  left_inv f := by
    ext
    simp only [coe_mk, comp_apply, Equiv.symm_apply_apply]
  right_inv f := by
    ext
    simp only [coe_mk, comp_apply, Equiv.apply_symm_apply]

Linear equivalence of multilinear maps under reindexing

Informal description

Given an equivalence $\sigma : \iota \simeq \iota'$ between index types, the linear equivalence `MultilinearMap.domDomCongrLinearEquiv'` constructs an isomorphism between the spaces of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ and $\text{MultilinearMap}\, R\, (M₁ \circ \sigma^{-1})\, M₂$. Specifically: - The forward map sends a multilinear map $f$ to the composition $f \circ (\sigma.\text{piCongrLeft'}\, M₁)^{-1}$, which reindexes the input via $\sigma^{-1}$ before applying $f$. - The inverse map sends a multilinear map $g$ to the composition $g \circ \sigma.\text{piCongrLeft'}\, M₁$, which reindexes the input via $\sigma$ before applying $g$. This equivalence preserves the multilinear structure and is linear in the coefficients.

MultilinearMap.constLinearEquivOfIsEmpty definition

[IsEmpty ι] : M₂ ≃ₗ[S] MultilinearMap R M₁ M₂

Full source

/-- The space of constant maps is equivalent to the space of maps that are multilinear with respect
to an empty family. -/
@[simps]
def constLinearEquivOfIsEmpty [IsEmpty ι] : M₂ ≃ₗ[S] MultilinearMap R M₁ M₂ where
  toFun := MultilinearMap.constOfIsEmpty R _
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun f := f 0
  left_inv _ := rfl
  right_inv f := ext fun _ => MultilinearMap.congr_arg f <| Subsingleton.elim _ _

Linear equivalence between a module and multilinear maps over an empty index type

Informal description

When the index type $\iota$ is empty, there is a linear equivalence between the module $M₂$ and the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$. Specifically: - The forward map sends any element $m \in M₂$ to the constant multilinear map that always returns $m$. - The inverse map evaluates a multilinear map at the zero tuple (which is the only input when $\iota$ is empty). - This equivalence preserves addition and scalar multiplication.

MultilinearMap.domDomCongrLinearEquiv definition

 {ι₁ ι₂} (σ : ι₁ ≃ ι₂) : MultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃ₗ[S] MultilinearMap R (fun _ : ι₂ => M₂) M₃

Full source

/-- `MultilinearMap.domDomCongr` as a `LinearEquiv`. -/
@[simps apply symm_apply]
def domDomCongrLinearEquiv {ι₁ ι₂} (σ : ι₁ ≃ ι₂) :
    MultilinearMapMultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃ₗ[S] MultilinearMap R (fun _ : ι₂ => M₂) M₃ :=
  { (domDomCongrEquiv σ :
      MultilinearMapMultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃+ MultilinearMap R (fun _ : ι₂ => M₂) M₃) with
    map_smul' := fun c f => by
      ext
      simp [MultilinearMap.domDomCongr] }

Linear equivalence of multilinear maps via index bijection

Informal description

Given a semiring $R$, a commutative semiring $S$, modules $M₂$ and $M₃$ over $R$, and a bijection $\sigma : \iota₁ \simeq \iota₂$ between index types, there is a linear equivalence between the space of multilinear maps from $\prod_{i \in \iota₁} M₂$ to $M₃$ and the space of multilinear maps from $\prod_{i \in \iota₂} M₂$ to $M₃$. This equivalence reindexes the input via $\sigma$ and preserves both the additive structure and scalar multiplication by elements of $S$.

MultilinearMap.domDomRestrictₗ definition

 (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P] :
  MultilinearMap R (fun (i : { a : ι // ¬P a }) => M₁ i) (MultilinearMap R (fun (i : { a : ι // P a }) => M₁ i) M₂)

Full source

/-- Given a predicate `P`, one may associate to a multilinear map `f` a multilinear map
from the elements satisfying `P` to the multilinear maps on elements not satisfying `P`.
In other words, splitting the variables into two subsets one gets a multilinear map into
multilinear maps.
This is a linear map version of the function `MultilinearMap.domDomRestrict`. -/
def domDomRestrictₗ (f : MultilinearMap R M₁ M₂) (P : ι → Prop) [DecidablePred P] :
    MultilinearMap R (fun (i : {a : ι // ¬ P a}) => M₁ i)
      (MultilinearMap R (fun (i : {a : ι // P a}) => M₁ i) M₂) where
  toFun := fun z ↦ domDomRestrict f P z
  map_update_add' := by
    intro h m i x y
    classical
    ext v
    simp [domDomRestrict_aux_right]
  map_update_smul' := by
    intro h m i c x
    classical
    ext v
    simp [domDomRestrict_aux_right]

Linearized restriction of a multilinear map to a subdomain defined by a predicate

Informal description

Given a multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, a decidable predicate $P$ on $\iota$, the function `MultilinearMap.domDomRestrictₗ` constructs a multilinear map from $\prod_{i \in \{a \mid \neg P a\}} M₁_i$ to the space of multilinear maps from $\prod_{i \in \{a \mid P a\}} M₁_i$ to $M₂$. For any fixed element $z$ in $\prod_{i \in \{a \mid \neg P a\}} M₁_i$, the resulting multilinear map evaluates at $x$ by extending $x$ with $z$ on the coordinates where $P$ does not hold and then applying $f$ to the resulting vector.

MultilinearMap.iteratedFDeriv_aux theorem

 {ι} {M₁ : ι → Type*} {α : Type*} [DecidableEq α] (s : Set ι) [DecidableEq { x // x ∈ s }] (e : α ≃ s)
  (m : α → ((i : ι) → M₁ i)) (a : α) (z : (i : ι) → M₁ i) :
  (fun i ↦ update m a z (e.symm i) i) = (fun i ↦ update (fun j ↦ m (e.symm j) j) (e a) (z (e a)) i)

Full source

lemma iteratedFDeriv_aux {ι} {M₁ : ι → Type*} {α : Type*} [DecidableEq α]
    (s : Set ι) [DecidableEq { x // x ∈ s }] (e : α ≃ s)
    (m : α → ((i : ι) → M₁ i)) (a : α) (z : (i : ι) → M₁ i) :
    (fun i ↦ update m a z (e.symm i) i) =
      (fun i ↦ update (fun j ↦ m (e.symm j) j) (e a) (z (e a)) i) := by
  ext i
  rcases eq_or_ne a (e.symm i) with rfl | hne
  · rw [Equiv.apply_symm_apply e i, update_self, update_self]
  · rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]

Equality of Iterated Function Updates via Bijection

Informal description

Let $\iota$ be a type, $M₁ : \iota \to \text{Type*}$ a family of types, and $\alpha$ a type with decidable equality. Given a subset $s \subseteq \iota$ with decidable equality on its elements, and a bijection $e : \alpha \simeq s$, for any family of functions $m : \alpha \to (\prod_{i \in \iota} M₁ i)$, any index $a \in \alpha$, and any function $z : \prod_{i \in \iota} M₁ i$, the following equality holds: \[ \big(\lambda i \mapsto \text{update } m \, a \, z \, (e^{-1}(i)) \, i\big) = \big(\lambda i \mapsto \text{update } (\lambda j \mapsto m (e^{-1}(j)) \, j) \, (e(a)) \, (z (e(a))) \, i\big). \] Here, $\text{update } f \, a' \, v$ denotes the function that is equal to $f$ everywhere except at $a'$, where it takes the value $v$.

MultilinearMap.iteratedFDerivComponent definition

 {α : Type*} (f : MultilinearMap R M₁ M₂) {s : Set ι} (e : α ≃ s) [DecidablePred (· ∈ s)] :
  MultilinearMap R (fun (i : { a : ι // a ∉ s }) ↦ M₁ i) (MultilinearMap R (fun (_ : α) ↦ (∀ i, M₁ i)) M₂)

Full source

/-- One of the components of the iterated derivative of a multilinear map. Given a bijection `e`
between a type `α` (typically `Fin k`) and a subset `s` of `ι`, this component is a multilinear map
of `k` vectors `v₁, ..., vₖ`, mapping them to `f (x₁, (v_{e.symm 2})₂, x₃, ...)`, where at
indices `i` in `s` one uses the `i`-th coordinate of the vector `v_{e.symm i}` and otherwise one
uses the `i`-th coordinate of a reference vector `x`.
This is multilinear in the components of `x` outside of `s`, and in the `v_j`. -/
noncomputable def iteratedFDerivComponent {α : Type*}
    (f : MultilinearMap R M₁ M₂) {s : Set ι} (e : α ≃ s) [DecidablePred (· ∈ s)] :
    MultilinearMap R (fun (i : {a : ι // a ∉ s}) ↦ M₁ i)
      (MultilinearMap R (fun (_ : α) ↦ (∀ i, M₁ i)) M₂) where
  toFun := fun z ↦
    { toFun := fun v ↦ domDomRestrictₗ f (fun i ↦ i ∈ s) z (fun i ↦ v (e.symm i) i)
      map_update_add' := by classical simp [iteratedFDeriv_aux]
      map_update_smul' := by classical simp [iteratedFDeriv_aux] }
  map_update_add' := by intros; ext; simp
  map_update_smul' := by intros; ext; simp

Component of Iterated Derivative of a Multilinear Map via Bijection

Informal description

Given a multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, a subset $s \subseteq \iota$, and a bijection $e$ between a type $\alpha$ and $s$, the function `MultilinearMap.iteratedFDerivComponent` constructs a multilinear map from $\prod_{i \in \iota \setminus s} M₁_i$ to the space of multilinear maps from $\prod_{i \in \alpha} (\prod_{j \in \iota} M₁_j)$ to $M₂$. For any fixed element $z$ in $\prod_{i \in \iota \setminus s} M₁_i$, the resulting multilinear map evaluates at $v$ by extending $v$ with $z$ on the coordinates outside $s$ and then applying $f$ to the resulting vector, where the coordinates in $s$ are determined via the bijection $e$.

MultilinearMap.iteratedFDeriv definition

 [Fintype ι] (f : MultilinearMap R M₁ M₂) (k : ℕ) (x : (i : ι) → M₁ i) :
  MultilinearMap R (fun (_ : Fin k) ↦ (∀ i, M₁ i)) M₂

Full source

/-- The `k`-th iterated derivative of a multilinear map `f` at the point `x`. It is a multilinear
map of `k` vectors `v₁, ..., vₖ` (with the same type as `x`), mapping them
to `∑ f (x₁, (v_{i₁})₂, x₃, ...)`, where at each index `j` one uses either `xⱼ` or one
of the `(vᵢ)ⱼ`, and each `vᵢ` has to be used exactly once.
The sum is parameterized by the embeddings of `Fin k` in the index type `ι` (or, equivalently,
by the subsets `s` of `ι` of cardinality `k` and then the bijections between `Fin k` and `s`).

For the continuous version, see `ContinuousMultilinearMap.iteratedFDeriv`. -/
protected noncomputable def iteratedFDeriv [Fintype ι]
    (f : MultilinearMap R M₁ M₂) (k : ℕ) (x : (i : ι) → M₁ i) :
    MultilinearMap R (fun (_ : Fin k) ↦ (∀ i, M₁ i)) M₂ :=
  ∑ e : Fin k ↪ ι, iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)

Iterated derivative of a multilinear map

Informal description

Given a multilinear map $ f $ from $ \prod_{i \in \iota} M₁_i $ to $ M₂ $, a natural number $ k $, and a point $ x \in \prod_{i \in \iota} M₁_i $, the $ k $-th iterated derivative of $ f $ at $ x $ is a multilinear map from $ (\prod_{i \in \iota} M₁_i)^k $ to $ M₂ $. It is defined as the sum over all embeddings $ e $ of $ \text{Fin}(k) $ into $ \iota $, where each term is the evaluation of $ f $ at $ x $ modified by replacing the coordinates in the range of $ e $ with the corresponding input vectors.

MultilinearMap.compLinearMapₗ definition

(f : Π (i : ι), M₁ i →ₗ[R] M₁' i) : (MultilinearMap R M₁' M₂) →ₗ[R] MultilinearMap R M₁ M₂

Full source

/-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap`
sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g`. -/
@[simps] def compLinearMapₗ (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) :
    (MultilinearMap R M₁' M₂) →ₗ[R] MultilinearMap R M₁ M₂ where
  toFun := fun g ↦ g.compLinearMap f
  map_add' := fun _ _ ↦ rfl
  map_smul' := fun _ _ ↦ rfl

Linear construction of multilinear map composition with linear maps

Informal description

Given a family of linear maps $ f_i : M_i \to M'_i $ for each $ i \in \iota $, the construction $ \text{compLinearMap}_\text{ₗ} $ sends a multilinear map $ g : \prod_{i \in \iota} M'_i \to M_2 $ to the multilinear map $ g \circ (f_1, \dots, f_n) : \prod_{i \in \iota} M_i \to M_2 $. This construction is linear in $ g $.

MultilinearMap.compLinearMapMultilinear definition

 :
  @MultilinearMap R ι (fun i ↦ M₁ i →ₗ[R] M₁' i) ((MultilinearMap R M₁' M₂) →ₗ[R] MultilinearMap R M₁ M₂) _ _ _
    (fun _ ↦ LinearMap.module) _

Full source

/-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap`
sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g` and multilinear in
`f₁, ..., fₙ`. -/
@[simps] def compLinearMapMultilinear :
  @MultilinearMap R ι (fun i ↦ M₁ i →ₗ[R] M₁' i)
    ((MultilinearMap R M₁' M₂) →ₗ[R] MultilinearMap R M₁ M₂) _ _ _
      (fun _ ↦ LinearMap.module) _ where
  toFun := MultilinearMap.compLinearMapₗ
  map_update_add' := by
    intro _ f i f₁ f₂
    ext g x
    change (g fun j ↦ update f i (f₁ + f₂) j <| x j) =
        (g fun j ↦ update f i f₁ j <|x j) + g fun j ↦ update f i f₂ j (x j)
    let c : Π (i : ι), (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
    convert g.map_update_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i)) with j j j
    · exact Function.apply_update c f i (f₁ + f₂) j
    · exact Function.apply_update c f i f₁ j
    · exact Function.apply_update c f i f₂ j
  map_update_smul' := by
    intro _ f i a f₀
    ext g x
    change (g fun j ↦ update f i (a • f₀) j <| x j) = a • g fun j ↦ update f i f₀ j (x j)
    let c : Π (i : ι), (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
    convert g.map_update_smul (fun j ↦ f j (x j)) i a (f₀ (x i)) with j j j
    · exact Function.apply_update c f i (a • f₀) j
    · exact Function.apply_update c f i f₀ j

Multilinear construction of composition with linear maps

Informal description

Given a family of $R$-modules $\{M_i\}_{i \in \iota}$ and $\{M'_i\}_{i \in \iota}$, the construction $\text{compLinearMapMultilinear}$ is a multilinear map that takes a family of linear maps $\{f_i : M_i \to M'_i\}_{i \in \iota}$ and produces a linear map from $\text{MultilinearMap}\, R\, M'\, M_2$ to $\text{MultilinearMap}\, R\, M\, M_2$. Specifically, it sends a multilinear map $g : \prod_{i \in \iota} M'_i \to M_2$ to the composition $g \circ (f_1, \dots, f_n) : \prod_{i \in \iota} M_i \to M_2$. This construction is multilinear in the family $\{f_i\}$.

MultilinearMap.piLinearMap definition

 : MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂)

Full source

/--
Let `M₁ᵢ` and `M₁ᵢ'` be two families of `R`-modules and `M₂` an `R`-module.
Let us denote `Π i, M₁ᵢ` and `Π i, M₁ᵢ'` by `M` and `M'` respectively.
If `g` is a multilinear map `M' → M₂`, then `g` can be reinterpreted as a multilinear
map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` via `(fᵢ) ↦ v ↦ g(fᵢ vᵢ)`.
-/
@[simps!] def piLinearMap :
    MultilinearMapMultilinearMap R M₁' M₂ →ₗ[R]
    MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) where
  toFun g := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear
  map_add' := by simp
  map_smul' := by simp

Linear map from multilinear maps to multilinear maps of linear maps

Informal description

Given two families of $R$-modules $\{M_i\}_{i \in \iota}$ and $\{M'_i\}_{i \in \iota}$, and an $R$-module $M_2$, the construction $\text{piLinearMap}$ is a linear map that takes a multilinear map $g : \prod_{i \in \iota} M'_i \to M_2$ and produces a multilinear map from $\prod_{i \in \iota} (M_i \to M'_i)$ to $\text{MultilinearMap}\, R\, M_1\, M_2$. Specifically, it sends $g$ to the map $(f_i)_{i \in \iota} \mapsto (v \mapsto g(f_i(v_i))_{i \in \iota})$, which is multilinear in the family $\{f_i\}$.

MultilinearMap.map_piecewise_smul theorem

 [DecidableEq ι] (c : ι → R) (m : ∀ i, M₁ i) (s : Finset ι) :
  f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m

Full source

/-- If one multiplies by `c i` the coordinates in a finset `s`, then the image under a multilinear
map is multiplied by `∏ i ∈ s, c i`. This is mainly an auxiliary statement to prove the result when
`s = univ`, given in `map_smul_univ`, although it can be useful in its own right as it does not
require the index set `ι` to be finite. -/
theorem map_piecewise_smul [DecidableEq ι] (c : ι → R) (m : ∀ i, M₁ i) (s : Finset ι) :
    f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m := by
  refine s.induction_on (by simp) ?_
  intro j s j_not_mem_s Hrec
  have A :
    Function.update (s.piecewise (fun i => c i • m i) m) j (m j) =
      s.piecewise (fun i => c i • m i) m := by
    ext i
    by_cases h : i = j
    · rw [h]
      simp [j_not_mem_s]
    · simp [h]
  rw [s.piecewise_insert, f.map_update_smul, A, Hrec]
  simp [j_not_mem_s, mul_smul]

Multilinear map evaluation on piecewise scaled vectors equals product of scalars times evaluation

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁ : \iota \to \text{Type}$, $M₂$ be $R$-modules. For any multilinear map $f : \text{MultilinearMap}\, R\, M₁\, M₂$, vector $m \in \prod_{i \in \iota} M₁ i$, finite subset $s \subseteq \iota$, and scalar function $c : \iota \to R$, we have: \[ f\left(s.\text{piecewise}\, (\lambda i, c i \cdot m i)\, m\right) = \left(\prod_{i \in s} c i\right) \cdot f m \] where $s.\text{piecewise}\, g\, h$ denotes the function equal to $g$ on $s$ and $h$ outside $s$.

MultilinearMap.map_smul_univ theorem

[Fintype ι] (c : ι → R) (m : ∀ i, M₁ i) : (f fun i => c i • m i) = (∏ i, c i) • f m

Full source

/-- Multiplicativity of a multilinear map along all coordinates at the same time,
writing `f (fun i => c i • m i)` as `(∏ i, c i) • f m`. -/
theorem map_smul_univ [Fintype ι] (c : ι → R) (m : ∀ i, M₁ i) :
    (f fun i => c i • m i) = (∏ i, c i) • f m := by
  classical simpa using map_piecewise_smul f c m Finset.univ

Multilinear map evaluation on scaled vectors equals product of scalars times evaluation

Informal description

Let $R$ be a semiring, $\iota$ a finite type, and $M₁ : \iota \to \text{Type}$, $M₂$ be $R$-modules. For any multilinear map $f : \text{MultilinearMap}\, R\, M₁\, M₂$, vector $m \in \prod_{i \in \iota} M₁ i$, and scalar function $c : \iota \to R$, we have: \[ f(\lambda i, c i \cdot m i) = \left(\prod_{i \in \iota} c i\right) \cdot f m. \]

MultilinearMap.map_update_smul_left theorem

 [DecidableEq ι] [Fintype ι] (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) :
  f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)

Full source

@[simp]
theorem map_update_smul_left [DecidableEq ι] [Fintype ι]
    (m : ∀ i, M₁ i) (i : ι) (c : R) (x : M₁ i) :
    f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x) := by
  have :
    f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
      (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x) :=
    map_piecewise_smul f _ _ _
  simpa [← Function.update_smul c m] using this

Multilinear map evaluation on scaled update: $f(\text{update}\, (c \cdot m)\, i\, x) = c^{|\iota| - 1} \cdot f(\text{update}\, m\, i\, x)$

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and $M₁ : \iota \to \text{Type}$, $M₂$ be $R$-modules. For any multilinear map $f : \text{MultilinearMap}\, R\, M₁\, M₂$, vector $m \in \prod_{i \in \iota} M₁ i$, index $i \in \iota$, scalar $c \in R$, and element $x \in M₁ i$, we have: \[ f\left(\text{update}\, (c \cdot m)\, i\, x\right) = c^{|\iota| - 1} \cdot f\left(\text{update}\, m\, i\, x\right), \] where $|\iota|$ denotes the cardinality of $\iota$ and $\text{update}\, f\, i\, x$ denotes the function equal to $f$ everywhere except at $i$, where it takes the value $x$.

MultilinearMap.mkPiAlgebra definition

: MultilinearMap R (fun _ : ι => A) A

Full source

/-- Given an `R`-algebra `A`, `mkPiAlgebra` is the multilinear map on `A^ι` associating
to `m` the product of all the `m i`.

See also `MultilinearMap.mkPiAlgebraFin` for a version that works with a non-commutative
algebra `A` but requires `ι = Fin n`. -/
protected def mkPiAlgebra : MultilinearMap R (fun _ : ι => A) A where
  toFun m := ∏ i, m i
  map_update_add' m i x y := by simp [Finset.prod_update_of_mem, add_mul]
  map_update_smul' m i c x := by simp [Finset.prod_update_of_mem]

Multilinear product map on a commutative algebra

Informal description

Given a commutative $R$-algebra $A$ and a finite type $\iota$, the multilinear map $\text{mkPiAlgebra}$ on $A^\iota$ associates to each tuple $m = (m_i)_{i \in \iota}$ the product $\prod_{i \in \iota} m_i$.

MultilinearMap.mkPiAlgebra_apply theorem

(m : ι → A) : MultilinearMap.mkPiAlgebra R ι A m = ∏ i, m i

Full source

@[simp]
theorem mkPiAlgebra_apply (m : ι → A) : MultilinearMap.mkPiAlgebra R ι A m = ∏ i, m i :=
  rfl

Evaluation of Multilinear Product Map: $\text{mkPiAlgebra}(m) = \prod_{i} m_i$

Informal description

For any tuple $m = (m_i)_{i \in \iota}$ of elements in a commutative $R$-algebra $A$, the evaluation of the multilinear product map $\text{mkPiAlgebra}$ at $m$ is equal to the product $\prod_{i \in \iota} m_i$.

MultilinearMap.mkPiAlgebraFin definition

: MultilinearMap R (fun _ : Fin n => A) A

Full source

/-- Given an `R`-algebra `A`, `mkPiAlgebraFin` is the multilinear map on `A^n` associating
to `m` the product of all the `m i`.

See also `MultilinearMap.mkPiAlgebra` for a version that assumes `[CommSemiring A]` but works
for `A^ι` with any finite type `ι`. -/
protected def mkPiAlgebraFin : MultilinearMap R (fun _ : Fin n => A) A :=
  MultilinearMap.mk' (fun m ↦ (List.ofFn m).prod)
    (fun m i x y ↦ by
      have : (List.finRange n).idxOf i < n := by simp
      simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, add_mul, this,
        mul_add, add_mul])
    (fun m i c x ↦ by
      have : (List.finRange n).idxOf i < n := by simp
      simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set, this])

Multilinear product map on $A^n$

Informal description

Given a semiring $R$, an $R$-algebra $A$, and a natural number $n$, the multilinear map $\text{mkPiAlgebraFin}$ on $A^n$ associates to each tuple $m = (m_1, \dots, m_n) \in A^n$ the product $\prod_{i=1}^n m_i$.

MultilinearMap.mkPiAlgebraFin_apply theorem

(m : Fin n → A) : MultilinearMap.mkPiAlgebraFin R n A m = (List.ofFn m).prod

Full source

@[simp]
theorem mkPiAlgebraFin_apply (m : Fin n → A) :
    MultilinearMap.mkPiAlgebraFin R n A m = (List.ofFn m).prod :=
  rfl

Evaluation of Multilinear Product Map: $\text{mkPiAlgebraFin}(m) = \prod_{i=1}^n m_i$

Informal description

For any tuple $m = (m_1, \dots, m_n) \in A^n$ where $A$ is an $R$-algebra, the evaluation of the multilinear product map $\text{mkPiAlgebraFin}$ at $m$ equals the product of the elements in the list representation of $m$, i.e., $\text{mkPiAlgebraFin}(m) = \prod_{i=1}^n m_i$.

MultilinearMap.mkPiAlgebraFin_apply_const theorem

(a : A) : (MultilinearMap.mkPiAlgebraFin R n A fun _ => a) = a ^ n

Full source

theorem mkPiAlgebraFin_apply_const (a : A) :
    (MultilinearMap.mkPiAlgebraFin R n A fun _ => a) = a ^ n := by simp

Evaluation of Multilinear Product Map on Constant Tuple: $\text{mkPiAlgebraFin}\, (a, \dots, a) = a^n$

Informal description

For any element $a$ in an $R$-algebra $A$ and any natural number $n$, the evaluation of the multilinear product map $\text{mkPiAlgebraFin}$ at the constant tuple $(a, \dots, a) \in A^n$ is equal to $a^n$.

MultilinearMap.smulRight definition

(f : MultilinearMap R M₁ R) (z : M₂) : MultilinearMap R M₁ M₂

Full source

/-- Given an `R`-multilinear map `f` taking values in `R`, `f.smulRight z` is the map
sending `m` to `f m • z`. -/
def smulRight (f : MultilinearMap R M₁ R) (z : M₂) : MultilinearMap R M₁ M₂ :=
  (LinearMap.smulRight LinearMap.id z).compMultilinearMap f

Scalar multiplication of a multilinear map's output by a fixed element

Informal description

Given an $R$-multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $R$ and an element $z \in M₂$, the function `smulRight` constructs a new multilinear map from $\prod_{i \in \iota} M₁_i$ to $M₂$ that sends each input tuple $m$ to $f(m) \cdot z$.

MultilinearMap.smulRight_apply theorem

(f : MultilinearMap R M₁ R) (z : M₂) (m : ∀ i, M₁ i) : f.smulRight z m = f m • z

Full source

@[simp]
theorem smulRight_apply (f : MultilinearMap R M₁ R) (z : M₂) (m : ∀ i, M₁ i) :
    f.smulRight z m = f m • z :=
  rfl

Evaluation of Scalar-Right-Multiplied Multilinear Map: $(f.\text{smulRight}\, z)(m) = f(m) \cdot z$

Informal description

Let $R$ be a semiring, $\iota$ a type, and $M₁ : \iota \to \text{Type}$ and $M₂$ be $R$-modules. For any multilinear map $f : \text{MultilinearMap}\, R\, M₁\, R$, any element $z \in M₂$, and any tuple $m \in \prod_{i \in \iota} M₁_i$, the evaluation of the multilinear map $f.\text{smulRight}\, z$ at $m$ equals the scalar multiplication of $f(m)$ by $z$, i.e., $$(f.\text{smulRight}\, z)(m) = f(m) \cdot z.$$

MultilinearMap.mkPiRing definition

[Fintype ι] (z : M₂) : MultilinearMap R (fun _ : ι => R) M₂

Full source

/-- The canonical multilinear map on `R^ι` when `ι` is finite, associating to `m` the product of
all the `m i` (multiplied by a fixed reference element `z` in the target module). See also
`mkPiAlgebra` for a more general version. -/
protected def mkPiRing [Fintype ι] (z : M₂) : MultilinearMap R (fun _ : ι => R) M₂ :=
  (MultilinearMap.mkPiAlgebra R ι R).smulRight z

Multilinear product map on $R^\iota$ with scalar multiplication by a fixed element

Informal description

Given a finite type $\iota$, a semiring $R$, and an $R$-module $M₂$, the function $\text{mkPiRing}$ constructs a multilinear map from the product space $\prod_{i \in \iota} R$ to $M₂$. For a fixed element $z \in M₂$, this map sends a tuple $m = (m_i)_{i \in \iota}$ to the product $(\prod_{i \in \iota} m_i) \cdot z$.

MultilinearMap.mkPiRing_apply theorem

[Fintype ι] (z : M₂) (m : ι → R) : (MultilinearMap.mkPiRing R ι z : (ι → R) → M₂) m = (∏ i, m i) • z

Full source

@[simp]
theorem mkPiRing_apply [Fintype ι] (z : M₂) (m : ι → R) :
    (MultilinearMap.mkPiRing R ι z : (ι → R) → M₂) m = (∏ i, m i) • z :=
  rfl

Evaluation of Multilinear Product Map: $(\text{mkPiRing}\, z)(m) = (\prod_i m_i) \cdot z$

Informal description

Let $R$ be a semiring, $\iota$ a finite type, and $M₂$ an $R$-module. For any element $z \in M₂$ and any function $m : \iota \to R$, the evaluation of the multilinear map $\text{mkPiRing}\, R\, \iota\, z$ at $m$ is equal to the scalar multiplication of the product $\prod_{i \in \iota} m(i)$ by $z$, i.e., $$(\text{mkPiRing}\, R\, \iota\, z)(m) = \left(\prod_{i \in \iota} m(i)\right) \cdot z.$$

MultilinearMap.mkPiRing_apply_one_eq_self theorem

[Fintype ι] (f : MultilinearMap R (fun _ : ι => R) M₂) : MultilinearMap.mkPiRing R ι (f fun _ => 1) = f

Full source

theorem mkPiRing_apply_one_eq_self [Fintype ι] (f : MultilinearMap R (fun _ : ι => R) M₂) :
    MultilinearMap.mkPiRing R ι (f fun _ => 1) = f := by
  ext m
  have : m = fun i => m i • (1 : R) := by
    ext j
    simp
  conv_rhs => rw [this, f.map_smul_univ]
  rfl

Recovery of Multilinear Map via Evaluation at Unit Tuple: $\text{mkPiRing}\, (f(1,\ldots,1)) = f$

Informal description

Let $R$ be a semiring, $\iota$ a finite type, and $M₂$ an $R$-module. For any multilinear map $f \colon \prod_{i \in \iota} R \to M₂$, the multilinear product map $\text{mkPiRing}\, R\, \iota\, (f(\lambda i, 1))$ is equal to $f$ itself. In other words, constructing a multilinear map by scaling with $f$ evaluated at the constant tuple $(1)_{i \in \iota}$ recovers $f$.

MultilinearMap.mkPiRing_eq_iff theorem

[Fintype ι] {z₁ z₂ : M₂} : MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂

Full source

theorem mkPiRing_eq_iff [Fintype ι] {z₁ z₂ : M₂} :
    MultilinearMap.mkPiRingMultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂ := by
  simp_rw [MultilinearMap.ext_iff, mkPiRing_apply]
  constructor <;> intro h
  · simpa using h fun _ => 1
  · intro x
    simp [h]

Equality of Multilinear Product Maps via Scalar Elements

Informal description

Let $R$ be a semiring, $\iota$ a finite type, and $M₂$ an $R$-module. For any two elements $z₁, z₂ \in M₂$, the multilinear maps $\text{mkPiRing}\, R\, \iota\, z₁$ and $\text{mkPiRing}\, R\, \iota\, z₂$ are equal if and only if $z₁ = z₂$.

MultilinearMap.mkPiRing_zero theorem

[Fintype ι] : MultilinearMap.mkPiRing R ι (0 : M₂) = 0

Full source

theorem mkPiRing_zero [Fintype ι] : MultilinearMap.mkPiRing R ι (0 : M₂) = 0 := by
  ext; rw [mkPiRing_apply, smul_zero, MultilinearMap.zero_apply]

Zero Multilinear Product Map is Zero

Informal description

For a finite type $\iota$ and a semiring $R$, the multilinear product map $\text{mkPiRing}\, R\, \iota$ evaluated at the zero element $0 \in M₂$ is equal to the zero multilinear map, i.e., $$\text{mkPiRing}\, R\, \iota\, 0 = 0.$$

MultilinearMap.mkPiRing_eq_zero_iff theorem

[Fintype ι] (z : M₂) : MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Full source

theorem mkPiRing_eq_zero_iff [Fintype ι] (z : M₂) : MultilinearMap.mkPiRingMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0 := by
  rw [← mkPiRing_zero, mkPiRing_eq_iff]

Characterization of Zero Multilinear Product Map: $\text{mkPiRing}\, R\, \iota\, z = 0 \leftrightarrow z = 0$

Informal description

Let $R$ be a semiring, $\iota$ a finite type, and $M₂$ an $R$-module. For any element $z \in M₂$, the multilinear product map $\text{mkPiRing}\, R\, \iota\, z$ is equal to the zero multilinear map if and only if $z = 0$.

MultilinearMap.instNeg instance

: Neg (MultilinearMap R M₁ M₂)

Full source

instance : Neg (MultilinearMap R M₁ M₂) :=
  ⟨fun f => ⟨fun m => -f m, fun m i x y => by simp [add_comm], fun m i c x => by simp⟩⟩

Negation Operation on Multilinear Maps

Informal description

For any semiring $R$, type $\iota$, family of additive commutative monoids $(M₁_i)_{i \in \iota}$, and additive commutative monoid $M₂$ where each $M₁_i$ and $M₂$ are $R$-modules, the space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ has a negation operation. Given a multilinear map $f \in \text{MultilinearMap}\, R\, M₁\, M₂$, its negation $-f$ is defined pointwise by $(-f)(m) = -f(m)$ for all $m \in \prod_{i \in \iota} M₁_i$.

MultilinearMap.neg_apply theorem

(m : ∀ i, M₁ i) : (-f) m = -f m

Full source

@[simp]
theorem neg_apply (m : ∀ i, M₁ i) : (-f) m = -f m :=
  rfl

Pointwise Negation of Multilinear Maps: $(-f)(m) = -f(m)$

Informal description

For any multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$ and any element $m \in \prod_{i \in \iota} M₁_i$, the evaluation of the negated multilinear map $-f$ at $m$ equals the negation of the evaluation of $f$ at $m$, i.e., $(-f)(m) = -f(m)$.

MultilinearMap.instSub instance

: Sub (MultilinearMap R M₁ M₂)

Full source

instance : Sub (MultilinearMap R M₁ M₂) :=
  ⟨fun f g =>
    ⟨fun m => f m - g m, fun m i x y => by
      simp only [MultilinearMap.map_update_add, sub_eq_add_neg, neg_add]
      abel,
      fun m i c x => by simp only [MultilinearMap.map_update_smul, smul_sub]⟩⟩

Subtraction Operation on Multilinear Maps

Informal description

The space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ is equipped with a subtraction operation. Given two multilinear maps $f, g \in \text{MultilinearMap}\, R\, M₁\, M₂$, their difference $f - g$ is defined pointwise by $(f - g)(m) = f(m) - g(m)$ for all $m \in \prod_{i \in \iota} M₁_i$.

MultilinearMap.sub_apply theorem

(m : ∀ i, M₁ i) : (f - g) m = f m - g m

Full source

@[simp]
theorem sub_apply (m : ∀ i, M₁ i) : (f - g) m = f m - g m :=
  rfl

Pointwise Subtraction of Multilinear Maps: $(f - g)(m) = f(m) - g(m)$

Informal description

For any multilinear maps $f, g \colon \prod_{i \in \iota} M₁_i \to M₂$ and any vector $m \in \prod_{i \in \iota} M₁_i$, the evaluation of the difference $f - g$ at $m$ is equal to the difference of the evaluations, i.e., $(f - g)(m) = f(m) - g(m)$.

MultilinearMap.instAddCommGroup instance

: AddCommGroup (MultilinearMap R M₁ M₂)

Full source

instance : AddCommGroup (MultilinearMap R M₁ M₂) :=
  { MultilinearMap.addCommMonoid with
    neg_add_cancel := fun _ => MultilinearMap.ext fun _ => neg_add_cancel _
    sub_eq_add_neg := fun _ _ => MultilinearMap.ext fun _ => sub_eq_add_neg _ _
    zsmul := fun n f =>
      { toFun := fun m => n • f m
        map_update_add' := fun m i x y => by simp [smul_add]
        map_update_smul' := fun l i x d => by simp [← smul_comm x n (_ : M₂)] }
    zsmul_zero' := fun _ => MultilinearMap.ext fun _ => SubNegMonoid.zsmul_zero' _
    zsmul_succ' := fun _ _ => MultilinearMap.ext fun _ => SubNegMonoid.zsmul_succ' _ _
    zsmul_neg' := fun _ _ => MultilinearMap.ext fun _ => SubNegMonoid.zsmul_neg' _ _ }

Additive Commutative Group Structure on Multilinear Maps

Informal description

The space of multilinear maps $\text{MultilinearMap}\, R\, M₁\, M₂$ forms an additive commutative group under pointwise addition and negation. That is, for any semiring $R$, type $\iota$, family of $R$-modules $M₁ : \iota \to \text{Type}$, and $R$-module $M₂$, the set of multilinear maps from $\prod_{i \in \iota} M₁_i$ to $M₂$ is equipped with a commutative addition operation, a zero element, and a negation operation, satisfying the usual group axioms.

MultilinearMap.map_update_neg theorem

[DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x : M₁ i) : f (update m i (-x)) = -f (update m i x)

Full source

@[simp]
theorem map_update_neg [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x : M₁ i) :
    f (update m i (-x)) = -f (update m i x) :=
  eq_neg_of_add_eq_zero_left <| by
    rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]

Negation Property of Multilinear Maps: $f(m[i \mapsto -x]) = -f(m[i \mapsto x])$

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁_i$ and $M₂$ be $R$-modules for each $i \in \iota$. For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, vector $m \in \prod_{i \in \iota} M₁_i$, index $i \in \iota$, and element $x \in M₁_i$, we have: \[ f(m[i \mapsto -x]) = -f(m[i \mapsto x]) \] where $m[i \mapsto v]$ denotes the vector obtained by updating the $i$-th coordinate of $m$ to $v$.

MultilinearMap.map_update_sub theorem

 [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) : f (update m i (x - y)) = f (update m i x) - f (update m i y)

Full source

@[simp]
theorem map_update_sub [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) :
    f (update m i (x - y)) = f (update m i x) - f (update m i y) := by
  rw [sub_eq_add_neg, sub_eq_add_neg, MultilinearMap.map_update_add, map_update_neg]

Subtraction Property of Multilinear Maps: $f(m[i \mapsto x - y]) = f(m[i \mapsto x]) - f(m[i \mapsto y])$

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁_i$ and $M₂$ be $R$-modules for each $i \in \iota$. For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, vector $m \in \prod_{i \in \iota} M₁_i$, index $i \in \iota$, and elements $x, y \in M₁_i$, we have: \[ f(m[i \mapsto x - y]) = f(m[i \mapsto x]) - f(m[i \mapsto y]) \] where $m[i \mapsto v]$ denotes the vector obtained by updating the $i$-th coordinate of $m$ to $v$.

MultilinearMap.map_update theorem

[DecidableEq ι] (x : (i : ι) → M₁ i) (i : ι) (v : M₁ i) : f (update x i v) = f x - f (update x i (x i - v))

Full source

lemma map_update [DecidableEq ι] (x : (i : ι) → M₁ i) (i : ι) (v : M₁ i)  :
    f (update x i v) = f x - f (update x i (x i - v)) := by
  rw [map_update_sub, update_eq_self, sub_sub_cancel]

Update Formula for Multilinear Maps: $f(x[i \mapsto v]) = f(x) - f(x[i \mapsto x_i - v])$

Informal description

Let $R$ be a semiring, $\iota$ a type with decidable equality, and $M₁_i$ and $M₂$ be $R$-modules for each $i \in \iota$. For any multilinear map $f \colon \prod_{i \in \iota} M₁_i \to M₂$, vector $x \in \prod_{i \in \iota} M₁_i$, index $i \in \iota$, and element $v \in M₁_i$, we have: \[ f(x[i \mapsto v]) = f(x) - f(x[i \mapsto x_i - v]) \] where $x[i \mapsto w]$ denotes the vector obtained by updating the $i$-th coordinate of $x$ to $w$.

MultilinearMap.map_sub_map_piecewise theorem

 [LinearOrder ι] (a b : (i : ι) → M₁ i) (s : Finset ι) :
  f a - f (s.piecewise b a) = ∑ i ∈ s, f (fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j)

Full source

lemma map_sub_map_piecewise [LinearOrder ι] (a b : (i : ι) → M₁ i) (s : Finset ι) :
    f a - f (s.piecewise b a) =
    ∑ i ∈ s, f (fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j) := by
  refine s.induction_on_min ?_ fun k s hk ih ↦ ?_
  · rw [Finset.piecewise_empty, sum_empty, sub_self]
  rw [Finset.piecewise_insert, map_update, ← sub_add, ih,
      add_comm, sum_insert (lt_irrefl _ <| hk k ·)]
  simp_rw [s.mem_insert]
  congr 1
  · congr; ext i; split_ifs with h₁ h₂
    · rw [update_of_ne, Finset.piecewise_eq_of_not_mem]
      · exact fun h ↦ (hk i h).not_lt (h₁ <| .inr h)
      · exact fun h ↦ (h₁ <| .inl h).ne h
    · cases h₂
      rw [update_self, s.piecewise_eq_of_not_mem _ _ (lt_irrefl _ <| hk k ·)]
    · push_neg at h₁
      rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]
  · apply sum_congr rfl; intro i hi; congr; ext j; congr 1; apply propext
    simp_rw [imp_iff_not_or, not_or]; apply or_congr_left'
    intro h; rw [and_iff_right]; rintro rfl; exact h (hk i hi)

Difference of Multilinear Maps Evaluated at Piecewise Vectors

Informal description

Let $R$ be a semiring, $\iota$ a linearly ordered type, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, vectors $a, b \in \prod_{i \in \iota} M₁ i$, and a finite subset $s \subseteq \iota$, we have: \[ f(a) - f(s.\text{piecewise}(b, a)) = \sum_{i \in s} f \left( \lambda j, \begin{cases} a_j & \text{if } j \in s \to j < i, \\ a_j - b_j & \text{if } i = j, \\ b_j & \text{otherwise.} \end{cases} \right) \] where $s.\text{piecewise}(b, a)$ denotes the vector equal to $b$ on $s$ and $a$ on its complement.

MultilinearMap.map_piecewise_sub_map_piecewise theorem

 [LinearOrder ι] (a b v : (i : ι) → M₁ i) (s : Finset ι) :
  f (s.piecewise a v) - f (s.piecewise b v) =
    ∑ i ∈ s, f fun j ↦ if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j

Full source

/-- This calculates the differences between the values of a multilinear map at
two arguments that differ on a finset `s` of `ι`. It requires a
linear order on `ι` in order to express the result. -/
lemma map_piecewise_sub_map_piecewise [LinearOrder ι] (a b v : (i : ι) → M₁ i) (s : Finset ι) :
    f (s.piecewise a v) - f (s.piecewise b v) = ∑ i ∈ s, f
      fun j ↦ if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j := by
  rw [← s.piecewise_idem_right b a, map_sub_map_piecewise]
  refine Finset.sum_congr rfl fun i hi ↦ congr_arg f <| funext fun j ↦ ?_
  by_cases hjs : j ∈ s
  · rw [if_pos hjs]; by_cases hji : j < i
    · rw [if_pos fun _ ↦ hji, if_pos hji, s.piecewise_eq_of_mem _ _ hjs]
    rw [if_neg (Classical.not_imp.mpr ⟨hjs, hji⟩), if_neg hji]
    obtain rfl | hij := eq_or_ne i j
    · rw [if_pos rfl, if_pos rfl, s.piecewise_eq_of_mem _ _ hi]
    · rw [if_neg hij, if_neg hij.symm]
  · rw [if_neg hjs, if_pos fun h ↦ (hjs h).elim, s.piecewise_eq_of_not_mem _ _ hjs]

Difference of Multilinear Maps Evaluated at Piecewise Vectors with Common Complement

Informal description

Let $R$ be a semiring, $\iota$ a linearly ordered type, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$, vectors $a, b, v \in \prod_{i \in \iota} M₁ i$, and a finite subset $s \subseteq \iota$, we have: \[ f(s.\text{piecewise}(a, v)) - f(s.\text{piecewise}(b, v)) = \sum_{i \in s} f \left( \lambda j, \begin{cases} a_j & \text{if } j \in s \text{ and } j < i, \\ a_j - b_j & \text{if } j \in s \text{ and } j = i, \\ b_j & \text{if } j \in s \text{ and } j > i, \\ v_j & \text{if } j \notin s. \end{cases} \right) \] where $s.\text{piecewise}(a, v)$ denotes the vector equal to $a$ on $s$ and $v$ on its complement.

MultilinearMap.map_add_eq_map_add_linearDeriv_add theorem

 [DecidableEq ι] [Fintype ι] (x h : (i : ι) → M₁ i) :
  f (x + h) = f x + f.linearDeriv x h + ∑ s with 2 ≤ #s, f (s.piecewise h x)

Full source

lemma map_add_eq_map_add_linearDeriv_add [DecidableEq ι] [Fintype ι] (x h : (i : ι) → M₁ i) :
    f (x + h) = f x + f.linearDeriv x h + ∑ s with 2 ≤ #s, f (s.piecewise h x) := by
  rw [add_comm, map_add_univ, ← Finset.powerset_univ,
      ← sum_filter_add_sum_filter_not _ (2 ≤ #·)]
  simp_rw [not_le, Nat.lt_succ, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or,
    ← powersetCard_eq_filter, sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one),
    powersetCard_zero, powersetCard_one, sum_singleton, Finset.piecewise_empty, sum_map,
    Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply, add_comm]

Multilinear Taylor Expansion: $f(x + h) = f(x) + Df(x)(h) + \sum_{|s| \geq 2} f(s.\text{piecewise}(h, x))$

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$ and vectors $x, h \in \prod_{i \in \iota} M₁ i$, we have: \[ f(x + h) = f(x) + f.\text{linearDeriv}(x)(h) + \sum_{\substack{s \subseteq \iota \\ |s| \geq 2}} f(s.\text{piecewise}(h, x)) \] where $s.\text{piecewise}(h, x)$ denotes the vector equal to $h$ on $s$ and $x$ on its complement, and $f.\text{linearDeriv}(x)(h)$ is the linear derivative of $f$ at $x$ applied to $h$.

MultilinearMap.map_add_sub_map_add_sub_linearDeriv theorem

 [DecidableEq ι] [Fintype ι] (x h h' : (i : ι) → M₁ i) :
  f (x + h) - f (x + h') - f.linearDeriv x (h - h') = ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Full source

/-- This expresses the difference between the values of a multilinear map
at two points "close to `x`" in terms of the "derivative" of the multilinear map at `x`
and of "second-order" terms. -/
lemma map_add_sub_map_add_sub_linearDeriv [DecidableEq ι] [Fintype ι] (x h h' : (i : ι) → M₁ i) :
    f (x + h) - f (x + h') - f.linearDeriv x (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x)) := by
  simp_rw [map_add_eq_map_add_linearDeriv_add, add_assoc, add_sub_add_comm, sub_self, zero_add,
    ← LinearMap.map_sub, add_sub_cancel_left, sum_sub_distrib]

Difference of Multilinear Taylor Expansions: $f(x+h) - f(x+h') - Df(x)(h-h') = \sum_{|s|\geq 2} (f(s.piecewise(h,x)) - f(s.piecewise(h',x)))$

Informal description

Let $R$ be a semiring, $\iota$ a finite type with decidable equality, and for each $i \in \iota$, let $M₁_i$ and $M₂$ be $R$-modules. Given a multilinear map $f \colon \prod_{i \in \iota} M₁ i \to M₂$ and vectors $x, h, h' \in \prod_{i \in \iota} M₁ i$, we have: \[ f(x + h) - f(x + h') - Df(x)(h - h') = \sum_{\substack{s \subseteq \iota \\ |s| \geq 2}} \left(f(s.\text{piecewise}(h, x)) - f(s.\text{piecewise}(h', x))\right) \] where $Df(x)(h - h')$ is the linear derivative of $f$ at $x$ applied to $h - h'$, and $s.\text{piecewise}(h, x)$ denotes the vector equal to $h$ on $s$ and $x$ on its complement.

MultilinearMap.piRingEquiv definition

[Fintype ι] : M₂ ≃ₗ[R] MultilinearMap R (fun _ : ι => R) M₂

Full source

/-- When `ι` is finite, multilinear maps on `R^ι` with values in `M₂` are in bijection with `M₂`,
as such a multilinear map is completely determined by its value on the constant vector made of ones.
We register this bijection as a linear equivalence in `MultilinearMap.piRingEquiv`. -/
protected def piRingEquiv [Fintype ι] : M₂ ≃ₗ[R] MultilinearMap R (fun _ : ι => R) M₂ where
  toFun z := MultilinearMap.mkPiRing R ι z
  invFun f := f fun _ => 1
  map_add' z z' := by
    ext m
    simp [smul_add]
  map_smul' c z := by
    ext m
    simp [smul_smul, mul_comm]
  left_inv z := by simp
  right_inv f := f.mkPiRing_apply_one_eq_self

Linear equivalence between $M₂$ and multilinear maps on $R^\iota$

Informal description

When the index type $\iota$ is finite, there is a linear equivalence between the module $M₂$ and the space of multilinear maps from the product space $\prod_{i \in \iota} R$ to $M₂$. This equivalence is given by sending an element $z \in M₂$ to the multilinear map that takes a tuple $(m_i)_{i \in \iota}$ to $(\prod_{i \in \iota} m_i) \cdot z$, and its inverse sends a multilinear map $f$ to $f(1, \ldots, 1)$.

MultilinearMap.map definition

[Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : ∀ i, Submodule R (M₁ i)) : SubMulAction R M₂

Full source

/-- The pushforward of an indexed collection of submodule `p i ⊆ M₁ i` by `f : M₁ → M₂`.

Note that this is not a submodule - it is not closed under addition. -/
def map [Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : ∀ i, Submodule R (M₁ i)) :
    SubMulAction R M₂ where
  carrier := f '' { v | ∀ i, v i ∈ p i }
  smul_mem' := fun c _ ⟨x, hx, hf⟩ => by
    let ⟨i⟩ := ‹Nonempty ι›
    letI := Classical.decEq ι
    refine ⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩
    · rw [hij, update_self]
      exact (p i).smul_mem _ (hx i)
    · rw [update_of_ne hij]
      exact hx j
    · rw [f.map_update_smul, update_eq_self]

Image of submodules under a multilinear map

Informal description

Given a nonempty index type $\iota$, a multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, and a family of submodules $p_i \subseteq M₁_i$ for each $i \in \iota$, the `map` operation constructs the subset of $M₂$ consisting of all elements of the form $f(v)$ where $v$ is any vector satisfying $v_i \in p_i$ for all $i \in \iota$. This subset is closed under scalar multiplication by elements of $R$.

MultilinearMap.map_nonempty theorem

[Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : ∀ i, Submodule R (M₁ i)) : (map f p : Set M₂).Nonempty

Full source

/-- The map is always nonempty. This lemma is needed to apply `SubMulAction.zero_mem`. -/
theorem map_nonempty [Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : ∀ i, Submodule R (M₁ i)) :
    (map f p : Set M₂).Nonempty :=
  ⟨f 0, 0, fun i => (p i).zero_mem, rfl⟩

Nonemptiness of Multilinear Map Image on Submodules

Informal description

For a nonempty index type $\iota$, a multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, and a family of submodules $p_i \subseteq M₁_i$ for each $i \in \iota$, the image of the product of submodules under $f$ is nonempty. That is, the set $\{f(v) \mid v \in \prod_{i \in \iota} p_i\}$ is nonempty.

MultilinearMap.range definition

[Nonempty ι] (f : MultilinearMap R M₁ M₂) : SubMulAction R M₂

Full source

/-- The range of a multilinear map, closed under scalar multiplication. -/
def range [Nonempty ι] (f : MultilinearMap R M₁ M₂) : SubMulAction R M₂ :=
  f.map fun _ => ⊤

Range of a multilinear map

Informal description

Given a nonempty index type $\iota$ and a multilinear map $f$ from $\prod_{i \in \iota} M₁_i$ to $M₂$, the range of $f$ is the subset of $M₂$ consisting of all elements of the form $f(v)$ where $v$ ranges over all possible vectors in $\prod_{i \in \iota} M₁_i$. This subset is closed under scalar multiplication by elements of the semiring $R$.

Mathlib.LinearAlgebra.Multilinear.Basic

Main definitions

Implementation notes