MultilinearMap.comp_linearEquiv_eq_zero_iff
theorem MultilinearMap.comp_linearEquiv_eq_zero_iff :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] {M₁' : ι → Type u_1} [inst_5 : (i : ι) → AddCommMonoid (M₁' i)]
[inst_6 : (i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i ≃ₗ[R] M₁' i),
(g.compLinearMap fun i => ↑(f i)) = 0 ↔ g = 0
This theorem states that for any semiring `R`, index type `ι`, type families `M₁` and `M₁'` (indexed by `ι`), and type `M₂`, each having appropriate algebraic structures, given a multilinear map `g` from `M₁'` to `M₂` and a family of linear equivalences `f` from `M₁` to `M₁'` (one for each index), composing the multilinear map `g` with each linear equivalence in `f` (i.e., applying `g.compLinearMap fun i => ↑(f i)`) gives the zero map if and only if `g` itself is the zero map. In mathematical terms, if `g` composed with `f` is zero, then `g` must be zero, and vice versa.
More concisely: For any semiring `R`, if for all indices `ι`, the multilinear map `g : M₁' ➝ M₂` and the family of linear equivalences `f : M₁ ≃ M₁'` satisfy `g.compLinearMap i = 0` for all `i`, then `g = 0`, and conversely.
|
MultilinearMap.map_piecewise_add
theorem MultilinearMap.map_piecewise_add :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m m' : (i : ι) → M₁ i)
(t : Finset ι), f (t.piecewise (m + m') m') = t.powerset.sum fun s => f (s.piecewise m m')
This theorem states that for a multilinear map `f` and two vectors `m` and `m'`, if you add `m` to `m'` but only at coordinates specified by a finset `t`, then the result of applying `f` to this new vector is equal to the sum of applying `f` to the piecewise addition of `m` and `m'` over all subsets of `t`. This result is expressed as `f (Finset.piecewise t (m + m') m') = Finset.sum (Finset.powerset t) fun s => f (Finset.piecewise s m m')`. This theorem is primarily used as an auxiliary statement for proving another result where `t` is the universal set, although it might be useful in its own right given that it does not require the index set `ι` to be finite.
More concisely: For a multilinear map `f`, the application of `f` to the piecewise sum of two vectors with respect to a finite set `t` is equal to the sum of the applications of `f` to the piecewise sums of the vectors over all subsets of `t`.
|
MultilinearMap.map_sum_finset
theorem MultilinearMap.map_sum_finset :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ι → Type u_1} (g : (i : ι) → α i → M₁ i)
(A : (i : ι) → Finset (α i)) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι],
(f fun i => (A i).sum fun j => g i j) = (Fintype.piFinset A).sum fun r => f fun i => g i (r i)
The theorem `MultilinearMap.map_sum_finset` states that for a multilinear map `f`, the application of `f` on a tuple, where each entry of the tuple is the sum of a set of elements from a corresponding finite set `A`, is equal to the sum of `f` applied on each possible tuple that can be formed by picking one element from each of these finite sets. Here, the function `g` is used to map elements from the finite sets to the domain of `f`. The sum over a finite set `A` is denoted by `Σ_{j ∈ A} g j`. The tuple is represented by a function `r` such that `r i` is an element of `A i` for each `i`. The sum over all possible tuples is represented by `Σ_{r} f r` where `r` ranges over all functions that pick one element from each finite set `A i`. This theorem is a consequence of the multilinearity of `f`, which allows us to expand `f` successively with respect to each coordinate.
More concisely: For a multilinear map `f` and finite sets `A_i` with elements mapped to `f`'s domain via functions `g_i`, the application of `f` to the sum of elements from each `A_i` is equal to the sum of applications of `f` to tuples, where each entry is an element from a corresponding `A_i` chosen via functions `g_i`.
|
MultilinearMap.map_zero
theorem MultilinearMap.map_zero :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : Nonempty ι], f 0 = 0
The theorem `MultilinearMap.map_zero` states that for any semiring `R`, any types `ι`, `M₁`, and `M₂`, where `M₁` is indexed by `ι`, along with the appropriate algebraic structures (`AddCommMonoid` and `Module`), if we have a multilinear map `f` from `M₁` to `M₂` and `ι` is not empty, then `f` applied to the zero element of `M₁` produces the zero element in `M₂`. In other words, a multilinear map sends the zero vector to the zero vector.
More concisely: For any semiring `R`, any type `ι` with non-empty indexed type `M₁`, and any multilinear map `f` from `M₁` to `M₂`, we have `f (0) = 0`, where `0` denotes the additive identity in `M₁` and `M₂`, respectively.
|
MultilinearMap.cons_smul
theorem MultilinearMap.cons_smul :
∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
[inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
(m : (i : Fin n) → M i.succ) (c : R) (x : M 0), f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
This theorem, "MultilinearMap.cons_smul", states that for any semiring `R`, natural number `n`, types `M` indexed by `Fin (n+1)` and `M₂`, where `M i` and `M₂` are modules over `R` and the elements of `M` are additive commutative monoids, if we have a multilinear map `f` from `M` to `M₂`, a function `m` mapping elements of `Fin n` to `M (Fin.succ i)`, a scalar `c` from `R`, and an element `x` of `M 0`, then the multilinear map `f` exhibits multiplicativity along the first variable when constructed with `Fin.cons`. Specifically, applying `f` to the tuple obtained by scaling `x` by `c` and then constructing a `Fin.cons` tuple with `m` equals the result of scaling by `c` the output of `f` applied to the `Fin.cons` tuple of `x` and `m`.
More concisely: For any semiring `R`, natural number `n`, additive commutative `R`-modules `M` indexed by `Fin (n+1)` and `M₂`, and multilinear map `f` from `M` to `M₂`, if `x` is an element of `M 0`, `c` is a scalar from `R`, and `m` is a function mapping elements of `Fin n` to `M (Fin.succ i)`, then `f (c * x, Fin.cons ⟨i, m i⟩) = c * f (x, Fin.cons ⟨i, m⟩)`.
|
MultilinearMap.map_add_univ
theorem MultilinearMap.map_add_univ :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
(m m' : (i : ι) → M₁ i), f (m + m') = Finset.univ.sum fun s => f (s.piecewise m m')
This theorem establishes the additivity of a multilinear map along all coordinates at the same time. Given any semiring `R`, a type `ι`, a type family `M₁` indexed by `ι`, and a type `M₂`, along with their appropriate algebraic structures (additive commutative monoids for `M₁ i` and `M₂`, and `R`-module structures for `M₁ i` and `M₂`). The theorem states that for any multilinear map `f` from `M₁` to `M₂`, any two functions `m` and `m'` from `ι` to `M₁ i`, and given that equality for `ι` is decidable and `ι` is finite, the value of `f` at the pointwise sum of `m` and `m'` is equal to the sum (over all finite subsets `s` of `ι`) of `f` evaluated at `s.piecewise m m'`. Here, `s.piecewise m m'` means the function that equals `m` at coordinates in `s` and equals `m'` at the coordinates not in `s`.
More concisely: Given a semiring `R`, a finite index set `ι`, a type family `M₁(i)` over `ι` with additive commutative monoid structures, a type `M₂` with `R`-module structures, and a multilinear map `f : ∏ i, M₁ i → M₂`, the map `f` is additive along all coordinates, i.e., for any functions `m, m' : ι → M₁` and given decidable equality on `ι`, `f (∑ i in ι, m i) = ∑ i in fin ι, f (s.piecewise m m')`, where `s.piecewise m m'` is the function equal to `m` on `s` and `m'` elsewhere.
|
MultilinearMap.map_sum_finset_aux
theorem MultilinearMap.map_sum_finset_aux :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ι → Type u_1} (g : (i : ι) → α i → M₁ i)
(A : (i : ι) → Finset (α i)) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] {n : ℕ},
(Finset.univ.sum fun i => (A i).card) = n →
(f fun i => (A i).sum fun j => g i j) = (Fintype.piFinset A).sum fun r => f fun i => g i (r i)
This theorem, named `MultilinearMap.map_sum_finset_aux`, states that for a given multilinear map `f` over a semiring `R`, with domains `M₁ i` and codomain `M₂`, and a family of functions `g : (i : ι) → α i → M₁ i` defined on finsets `A i`, the image of the sum of images of `g` over each finset under `f` is equal to the sum of the image of `g i (r i)` under `f`, where `r` ranges over all functions such that `r i` belongs to the finset `A i` for each `i`.
This is the auxiliary statement for an inductive proof, the main theorem being `map_sum_finset`. This is essentially an application of the multilinearity property, which involves successive expansions with respect to each coordinate. The condition `(Finset.univ.sum fun i => (A i).card) = n` ensures that the total number of elements in all the finsets is `n`.
In simpler terms, this theorem shows a way to distribute a multilinear operation over a sum in the context of finsets.
More concisely: Given a multilinear map `f` over a semiring `R`, and functions `g : ι → M₁ → M₂` defined on finsets `A i`, if the total number of elements in all `A i` is `n`, then `f (∑ i, ∑ x in A i, g i x) = ∑ i, g i r i` for some functions `r : ι → A i`.
|
MultilinearMap.map_smul'
theorem MultilinearMap.map_smul' :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (self : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι)
(c : R) (x : M₁ i), self.toFun (Function.update m i (c • x)) = c • self.toFun (Function.update m i x)
This theorem asserts that a multilinear map, when applied to a function whose value at a particular point `i` has been scaled by a scalar `c`, is equivalent to the scalar `c` times the value of the multilinear map applied to the original function. In other words, if `self` is a multilinear map, `m` is a function from index set `ι` to respective modules `M₁ i`, `i` is an index, `c` is a scalar, and `x` is a value in the module `M₁ i`, then scaling the value of function `m` at index `i` by `c` and then applying the multilinear map `self`, is the same as first applying the multilinear map `self` to the function `m` where the value at index `i` is replaced by `x`, and then scaling the result by `c`. This statement holds for all semirings `R`, and for all additively commutative monoids `M₁ i` and `M₂` which are modules over the semiring `R`. Here, `M₁` is a family of modules indexed by `ι`. The proof of this theorem is not shown here.
More concisely: For any multilinear map `self` over a semiring `R`, and functions `m: ι → M₁ i` and `n: ι → M₂` from index sets `ι` to modules `M₁ i` and `M₂` over `R`, respectively, if `c` is a scalar in `R` and `x ∈ M₁ i`, then `self (λ i, if i = i then c * m i else m i) = c * (self m)`.
|
MultilinearMap.domDomCongr_eq_iff
theorem MultilinearMap.domDomCongr_eq_iff :
∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
[inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2}
(σ : ι₁ ≃ ι₂) (f g : MultilinearMap R (fun x => M₂) M₃),
MultilinearMap.domDomCongr σ f = MultilinearMap.domDomCongr σ g ↔ f = g
This theorem, `MultilinearMap.domDomCongr_eq_iff`, states that for any semiring `R`, additive commutative monoids `M₂` and `M₃`, modules `M₂` and `M₃` over `R`, types `ι₁` and `ι₂`, bijection `σ` between `ι₁` and `ι₂`, and multilinear maps `f` and `g` from `ι₁` to the module `M₃`, the result of applying the congruence operation `domDomCongr` with the bijection `σ` to `f` and `g` are equal if and only if `f` and `g` are themselves equal. In other words, the `domDomCongr` operation preserves the equality of multilinear maps.
More concisely: For any semiring `R`, additive commutative monoids `M₂` and `M₃`, modules `M₂` and `M₃` over `R`, types `ι₁` and `ι₂`, bijection `σ` between `ι₁` and `ι₂`, and multilinear maps `f` and `g` from `ι₁` to `M₃`, `domDomCongr σ f = domDomCongr σ g` if and only if `f = g`.
|
MultilinearMap.map_nonempty
theorem MultilinearMap.map_nonempty :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Ring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] [inst_5 : Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : (i : ι) → Submodule R (M₁ i)),
(↑(f.map p)).Nonempty
This theorem states that for any ring `R`, any type `ι`, any family of types `M₁` indexed by `ι`, any type `M₂`, given the conditions that `M₁ i` and `M₂` are additive commutative monoids and `R`-modules for every `i` in `ι`, and `ι` is nonempty, then for any multilinear map `f` from `M₁` to `M₂` and any family of `R`-submodules `p` of `M₁ i` for each `i` in `ι`, the image of `f` mapped over `p` is always nonempty. This lemma is often needed to apply the `SubMulAction.zero_mem` lemma.
More concisely: For any ring `R`, any nonempty index type `ι`, any family of additive commutative monoids and `R`-modules `M₁ i` indexed by `ι`, any additive commutative monoid and `R`-module `M₂`, and any multilinear map `f` from `M₁` to `M₂`, the image of `f` over any family of `R`-submodules `p` of `M₁ i` is nonempty.
|
MultilinearMap.map_smul
theorem MultilinearMap.map_smul :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R)
(x : M₁ i), f (Function.update m i (c • x)) = c • f (Function.update m i x)
This theorem, `MultilinearMap.map_smul`, states that for any semiring `R`, an index type `ι`, and types `M₁` and `M₂` indexed by `ι` such that `M₁` and `M₂` are modules over `R`, a multilinear map `f` from `M₁` to `M₂`, a function `m` from `ι` to `M₁`, an index `i` in `ι`, and a scalar `c` in `R`, and a value `x` in `M₁ i`, if we update the value of `m` at `i` with `c` times `x`, and then apply the multilinear map `f`, we get the same result as if we first update the value of `m` at `i` with `x`, apply `f`, and then multiply by `c`. In mathematical terms, this theorem says that multilinear maps respect scalar multiplication, that is, $f(c \cdot x) = c \cdot f(x)$ for all scalars $c$ and all vectors $x$.
More concisely: For any semiring `R`, multilinear maps `f` from `M₁` to `M₂` over `R`, functions `m` from `ι` to `M₁`, scalars `c` in `R`, and values `x` in `M₁ i`, we have `f (c * x) = c * f x`.
|
MultilinearMap.ext
theorem MultilinearMap.ext :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] {f f' : MultilinearMap R M₁ M₂}, (∀ (x : (i : ι) → M₁ i), f x = f' x) → f = f'
This theorem, `MultilinearMap.ext`, states that for any semiring `R`, an index type `ι`, function types `M₁ : ι → Type v₁` and `M₂ : Type v₂`, where each `M₁ i` and `M₂` are an additive commutative monoid and `R`-module, if we have two multilinear maps `f` and `f'` from `M₁` to `M₂`, then `f` and `f'` are equal if and only if they map every `x` in the domain (which is a function from `ι` to `M₁`) to the same value. In other words, two multilinear maps are equal if they agree on all inputs.
More concisely: Two multilinear maps from a semiring-valued function type to an additive commutative monoid and R-module are equal if and only if they map every input function to the same output.
|
MultilinearMap.map_smul_univ
theorem MultilinearMap.map_smul_univ :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : Fintype ι] (c : ι → R) (m : (i : ι) → M₁ i),
(f fun i => c i • m i) = (Finset.univ.prod fun i => c i) • f m
This theorem states that for a multilinear map `f`, the application of `f` to each element `i` in a finite set, where each element is multiplied by a scalar `c i`, is equal to the product of those scalars times the application of `f` to the set. More formally, if `f` is a multilinear map from a space `M₁` to a space `M₂` over a commutative semiring `R`, and if `c` is a function that assigns a scalar from `R` to each index `i` in a finite set `ι`, and `m` is a function that assigns a vector from `M₁` to each index `i` in `ι`, then `f (fun i => c i • m i)` equals `(∏ i, c i) • f m`, where the product is taken over all indices in `ι`. This encapsulates the idea of the distributivity property in the context of multilinear mappings.
More concisely: For a multilinear map `f` over a commutative semiring `R`, and a finite function `c` mapping indices to scalars in `R`, and a function `m` mapping indices to vectors in the domain of `f`, the product of `c` applied to the indices and `f` applied to the function `x => c x • m x` equals `f` applied to the function `x => c x • m x`.
|
MultilinearMap.map_coord_zero
theorem MultilinearMap.map_coord_zero :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {m : (i : ι) → M₁ i} (i : ι), m i = 0 → f m = 0
This theorem states that for any given semiring `R`, type `ι`, and types `M₁` and `M₂` indexed by `ι`, if we have an additive commutative monoid for each `M₁ i` and `M₂`, and if each `M₁ i` and `M₂` are also `R`-modules. Then for any multilinear map `f` from `M₁` to `M₂`, if the `i-th` element of a collection `m` (indexed by `ι`) equals zero, then the multilinear map `f` applied to `m` will yield zero.
More concisely: If `R` is a semiring, `ι` is a type, and `M₁ i` and `M₂` are additive commutative monoids and `R`-modules indexed by `ι`, then for any multilinear map `f` from `M₁` to `M₂`, if all `i-th` elements of `m` in `M₁` are zero, then `f` applied to `m` is zero.
|
MultilinearMap.map_piecewise_sub_map_piecewise
theorem MultilinearMap.map_piecewise_sub_map_piecewise :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : LinearOrder ι] (a b v : (i : ι) → M₁ i)
(s : Finset ι),
f (s.piecewise a v) - f (s.piecewise b v) =
s.sum fun i => 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
This theorem calculates the differences between the values of a multilinear map at two different arguments that deviate on a finite set `s` of `ι`. It requires a linear order on `ι` to articulate the result. In concrete terms, for given semiring `R`, index type `ι`, types `M₁` and `M₂` defined for each `ι`, and a multilinear map `f : MultilinearMap R M₁ M₂`, the difference between `f` evaluated at `s.piecewise a v` and `s.piecewise b v` equals the sum over the finite set `s` of `f` evaluated at a function, which for each `j` gives `a j` if `j` is in `s` and less than `i`, `a j - b j` if `j` is in `s` and equals `i`, `b j` if `j` is in `s` but not less than or equals to `i`, and `v j` otherwise.
More concisely: For a multilinear map `f : MultilinearMap R M₁ M₂` over a semiring `R`, index type `ι`, and given `s : Finset ι`, the difference between `f (s.piecewise a) (v)` and `f (s.piecewise b) (v)` is equal to the sum over `s` of `f (λ (i : ι), if h : i ∈ s then if h.property i < i then a i - b i else a i - b i + b i else v i) (v)`, where `h.property` is the order relation on `ι`.
|
MultilinearMap.compLinearMap_injective
theorem MultilinearMap.compLinearMap_injective :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] {M₁' : ι → Type u_1} [inst_5 : (i : ι) → AddCommMonoid (M₁' i)]
[inst_6 : (i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i),
(∀ (i : ι), Function.Surjective ⇑(f i)) → Function.Injective fun g => g.compLinearMap f
The theorem `MultilinearMap.compLinearMap_injective` states that for any semiring `R`, any type `ι`, families of types `M₁` and `M₁'` indexed by `ι`, and a type `M₂`, given that each `M₁` and `M₁'` are additively commutative monoids and modules over `R`, and a family of surjective linear maps `f` from each `M₁` to each corresponding `M₁'`, then the function that takes a multilinear map and composes it with each of the linear maps `f` is an injective function. In simpler terms, if we compose a multilinear map with a family of surjective linear maps, we always get a unique result for each unique multilinear map.
More concisely: Given a semiring `R`, families of additively commutative monoid and `R`-module types `M₁`, `M₁'`, and a type `M₂`, if each `M₁` and `M₁'` are indexed by the same type `ι` and each `M₁` has a family of surjective `R`-linear maps to the corresponding `M₁'`, then the function that composes a multilinear map with each of these linear maps is injective.
|
MultilinearMap.map_sum
theorem MultilinearMap.map_sum :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ι → Type u_1} (g : (i : ι) → α i → M₁ i)
[inst_5 : DecidableEq ι] [inst_6 : Fintype ι] [inst_7 : (i : ι) → Fintype (α i)],
(f fun i => Finset.univ.sum fun j => g i j) = Finset.univ.sum fun r => f fun i => g i (r i)
The theorem `MultilinearMap.map_sum` states that for any semiring `R`, types `ι`, `M₁`, `M₂` along with their additional structures, a multilinear map `f` from `M₁` to `M₂`, and a function `g`, the evaluation of `f` on a sum where each term is the sum of `g i j` over all `j` in the universal finite set `Finset.univ`, is equal to the sum over all functions `r` of `f` evaluated at `g i (r i)`. This is a result of the multilinearity of `f`, where multilinearity allows for the expansion of `f` with respect to each coordinate. Note that `DecidableEq ι` and `Fintype ι` state that equality is decidable for each `ι` and there is a finite number of `ι`, respectively. Finally, `Fintype (α i)` indicates that for each `ι`, the corresponding `α i` is finite.
More concisely: For any semiring `R`, types `ι`, `M₁`, `M₂`, multilinear map `f` from `M₁` to `M₂`, and function `g` such that `DecidableEq ι`, `Fintype ι`, and `Fintype (α i)` hold, the evaluation of `f` on the sum of `g i j` over all `j` in `Finset.univ` is equal to the sum over all functions `r` of `f` evaluated at `g i r`.
|
MultilinearMap.zero_compLinearMap
theorem MultilinearMap.zero_compLinearMap :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] {M₁' : ι → Type u_1} [inst_5 : (i : ι) → AddCommMonoid (M₁' i)]
[inst_6 : (i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i), MultilinearMap.compLinearMap 0 f = 0
This theorem in Lean 4 is stating that if you have a multi-index `ι` and for each index `i` in `ι` you have a linear map `f` from a module `M₁ i` to a module `M₁' i` over a semiring `R`, then composing the zero multilinear map with `f` in each argument gives you the zero multilinear map. A multilinear map here is a map that takes several vector arguments and is linear in each of them. This theorem hence essentially emphasizes that zero, when composed with any function, remains zero.
More concisely: If `f` is a multilinear map from a module `M₁ i` to `M₁' i` over a semiring `R` for each index `i` in a multi-index `ι`, then the multilinear map formed by composing the zero multilinear map with `f` in each argument is the zero multilinear map.
|
LinearMap.compMultilinearMap_codRestrict
theorem LinearMap.compMultilinearMap_codRestrict :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
[inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃)
(f : MultilinearMap R M₁ M₂) (p : Submodule R M₃) (h : ∀ (c : M₂), g c ∈ p),
(LinearMap.codRestrict p g h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p ⋯
This theorem, `LinearMap.compMultilinearMap_codRestrict`, states that for any semiring `R`, any type `ι`, and any types `M₁`, `M₂`, and `M₃` that form modules over `R` (with `M₁` being a multilinear map indexed by `ι`), if we have a linear map `g` from `M₂` to `M₃`, a multilinear map `f` from `M₁` to `M₂`, a submodule `p` of `M₃`, and if the image of every element of `M₂` under `g` lies in `p`, then composing first `f` with `g` and then restricting to `p` is the same as first restricting `g` to `p` and then composing with `f`. This establishes an equivalence between two operations: the composition of a multilinear map and a restricted linear map, and the restriction of a composed multilinear map.
More concisely: For any semiring `R`, any type `ι`, and multilinear maps `f: M₁ →ₗ[R] M₂` and `g: M₂ →ₗ[R] M₃`, submodule `p ⊆ M₃`, and given that `g(M₂) ⊆ p`, the restriction of `(g ∘ f)` to `p` equals the restriction of `g` to `p` composed with `f`.
|
MultilinearMap.map_add
theorem MultilinearMap.map_add :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι)
(x y : M₁ i), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
This theorem, `MultilinearMap.map_add`, states that for any semiring `R`, types `ι`, `M₁` indexed by `ι`, and `M₂`, given instances of `AddCommMonoid` for `M₁ i` and `M₂`, and `Module R` for `M₁ i` and `M₂`, a multilinear map `f` from `M₁` to `M₂`, a decidable equality on ι, and a function `m` from `ι` to `M₁ i`, for any `ι` value and two elements of `M₁ i`, the result of updating the function `m` at `i` with the sum of these two elements and applying the multilinear map `f` on it, is equal to the sum of the results of separately updating the function `m` at `i` with each of these two elements and applying `f`. In mathematical terms, `f(m(i ↦ x + y)) = f(m(i ↦ x)) + f(m(i ↦ y))` for a multilinear map `f` and elements `x`, `y` of a module over a semiring.
More concisely: For any semiring `R`, types `ι`, `M₁` indexed by `ι`, and `M₂`, given instances of `AddCommMonoid` for `M₁ i` and `M₂`, and a multilinear map `f` from `M₁` to `M₂`, the operation of updating `m : ι → M₁ i` at `i` with the sum of two elements `x` and `y` in `M₁ i`, and applying `f`, equals the sum of the results of updating `m` at `i` with each of `x` and `y` separately and applying `f`. In symbols, `f(m.update i (x + y)) = f(m.update i x) + f(m.update i y)`.
|
MultilinearMap.map_add'
theorem MultilinearMap.map_add' :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (self : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι)
(x y : M₁ i),
self.toFun (Function.update m i (x + y)) =
self.toFun (Function.update m i x) + self.toFun (Function.update m i y)
The theorem `MultilinearMap.map_add'` states that for any semiring `R`, any type `ι`, types `M₁` and `M₂` where `M₁` is a type-dependent type indexed by `ι`, such that each `M₁ i` is a commutative additive monoid and a module over `R`, and `M₂` is also a commutative additive monoid and a module over `R`, for any multilinear map from `M₁` to `M₂`, and for any choice of elements in `M₁` indexed by `ι` (denoted as `m`), for any index `i` in `ι`, and for any two elements `x` and `y` in `M₁ i`, the value of the multilinear map at the point where `i`-th coordinate of `m` is updated to `x + y` is equal to the sum of the values of the multilinear map at the points where `i`-th coordinate of `m` is updated to `x` and `y`, respectively. This essentially states that a multilinear map is additive in every argument.
More concisely: For any commutative additive `R`-module-valued multilinear map, the value at the sum of inputs is equal to the sum of values at each input.
|
MultilinearMap.map_add_sub_map_add_sub_linearDeriv
theorem MultilinearMap.map_add_sub_map_add_sub_linearDeriv :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
(x h h' : (i : ι) → M₁ i),
f (x + h) - f (x + h') - (f.linearDeriv x) (h - h') =
(Finset.filter (fun x => 2 ≤ x.card) Finset.univ.powerset).sum fun s =>
f (s.piecewise h x) - f (s.piecewise h' x)
This theorem describes the change in the value of a multilinear map when evaluated at two points "near" a given point `x`, in terms of the derivative of the map at `x` and other higher order terms. Given a semiring `R`, a set `ι`, types `M₁` indexed by `ι` and another type `M₂`, along with their additive group and `R`-module structures, the theorem states that for any multilinear map `f` from `M₁` to `M₂`, and any three points `x`, `h`, `h'` in `M₁`, the difference in the values of the multilinear map at `x + h` and `x + h'`, minus the derivative of `f` at `x` evaluated at `h - h'`, equals to the sum over all subsets `s` of the universal finite set with size at least 2, of the differences in the values of `f` at `s.piecewise h x` and `s.piecewise h' x`. Here, `s.piecewise h x` gives the element `h` for indices in `s` and `x` for indices not in `s`.
More concisely: For any multilinear map $f$ from a semiring $R$-module $M\_1$ to another $R$-module $M\_2$, and any three points $x, h, h'\in M\_1$, the difference between $f(x+h)$ and $f(x+h')$ is equal to the derivative of $f$ at $x$ evaluated at $h-h'$ plus the sum of differences in values of $f$ at subset-wise combinations of $h$ and $x$, and $h'$ and $x$, for all subsets $s$ of the universal finite set with size at least 2.
|
MultilinearMap.cons_add
theorem MultilinearMap.cons_add :
∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
[inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
(m : (i : Fin n) → M i.succ) (x y : M 0), f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
The theorem `MultilinearMap.cons_add` enunciates the property of additivity of a multilinear map along its first variable in the specific scenario where the domain is indexed by `Fin (n+1)`, and the elements are constructed using the function `cons`. More concretely, given a Semiring `R`, a natural number `n`, types `M` indexed by `Fin (Nat.succ n)`, and `M₂`, assuming that the types `M i` and `M₂` are modules over `R` and have an additive commutative monoid structure, if `f` is a multilinear map from `M` to `M₂`, `m` is a map from `Fin n` to `M (Fin.succ i)`, and `x` and `y` are elements of `M 0`, then applying `f` to the `cons` of `x + y` and `m` is equivalent to the sum of applying `f` to the `cons` of `x` and `m` and applying `f` to the `cons` of `y` and `m`.
More concisely: Given a multilinear map `f` from a finite indexed module `M` to another additive module `M₂`, and `x`, `y` in `M₀`, and a map `m` from `Fin n` to `M (Fin.succ i)`, the application of `f` to `cons (x + y) m` equals the sum of the applications of `f` to `cons x m` and `cons y m`.
|
MultilinearMap.snoc_smul
theorem MultilinearMap.snoc_smul :
∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
[inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
(m : (i : Fin n) → M i.castSucc) (c : R) (x : M (Fin.last n)), f (Fin.snoc m (c • x)) = c • f (Fin.snoc m x)
This theorem states that for a specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where an element of the function type `∀ (i : Fin (n+1)), M i` can be built using `cons`, the multiplicativity of a multilinear map along the first variable can be directly expressed. More precisely, for all elements of a Semiring `R`, for any natural number `n`, for all types `M` that map `Fin n.succ` to another type, for another type `M₂`, given the Additive Commutative Monoid structure on `M i` and `M₂`, and the Module structure over `R` on `M i` and `M₂`, for a multilinear map `f` from `M` to `M₂`, for a function `m` from `Fin n` to `M i.castSucc`, for a scalar `c` in `R`, and for an element `x` of `M (Fin.last n)`, the value of the multilinear map `f` at the `n+1`-tuple obtained by appending the scaled vector `c • x` to `m` (using the function `Fin.snoc`) is the same as the scaled vector `c •` the value of the multilinear map `f` at the `n+1`-tuple obtained by appending `x` to `m`.
More concisely: For a multilinear map from a type `M` indexed by `Fin (n+1)` with Additive Commutative Monoid and Module structures over a semiring `R`, the value of applying the map to a scaled vector `c • x` appended to a function `m` is equal to the scaled vector `c •` the value of the map applied to `x` appended to `m`.
|
MultilinearMap.compLinearMap_id
theorem MultilinearMap.compLinearMap_id :
∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
{M₁' : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (M₁' i)] [inst_4 : (i : ι) → Module R (M₁' i)]
(g : MultilinearMap R M₁' M₂), (g.compLinearMap fun x => LinearMap.id) = g
The theorem `MultilinearMap.compLinearMap_id` states that for any multilinear map `g`, when composed with the identity linear map in each of its arguments, it remains unchanged. This theorem holds for any semiring `R`, any indexing type `ι`, and any type `M₂` that is a module over `R`. The fact that `g` remains unchanged when composed with the identity linear map is a property that holds for multilinear maps, similar to how the identity function behaves with respect to function composition in general.
More concisely: For any multilinear map `g` and indexing type `ι`, `M₂` being a module over a semiring `R`, `g` commutes with the identity linear maps in each argument, i.e., `g ∘ idₙ = g` for all `n ∈ ι`.
|
MultilinearMap.snoc_add
theorem MultilinearMap.snoc_add :
∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
[inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
(m : (i : Fin n) → M i.castSucc) (x y : M (Fin.last n)),
f (Fin.snoc m (x + y)) = f (Fin.snoc m x) + f (Fin.snoc m y)
This theorem, `MultilinearMap.snoc_add`, states that for any semiring `R`, natural number `n`, a function `M` from `Fin n.succ` to some type, and another type `M₂`, given that for every `i` in `Fin n.succ`, `M i` is an additive commutative monoid and is a module over `R`, and `M₂` is also a module over `R`, for any multilinear map `f` from `M` to `M₂`, and any function `m` from `Fin n` to `M i.castSucc`, and any two elements `x` and `y` of type `M (Fin.last n)`, the map `f` applied to the `snoc` of `m` and the sum of `x` and `y` is equal to the sum of `f` applied to the `snoc` of `m` and `x` and `f` applied to the `snoc` of `m` and `y`. In simpler terms, this theorem expresses the property of additivity of a multilinear map along the last coordinate when the map's domain is a space indexed by `Fin (n+1)`.
More concisely: Given a semiring `R`, a multilinear map `f` from a product of an `(n+1)`-element additive commutative monoid `M` over `R` to a module `M₂` over `R`, and functions `m : Fin n -> M`, `x, y : M (Fin.last n)`, the equation `f (snoc (m) (x + y)) = f (snoc (m) x) + f (snoc (m) y)` holds.
|
LinearMap.subtype_compMultilinearMap_codRestrict
theorem LinearMap.subtype_compMultilinearMap_codRestrict :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p),
p.subtype.compMultilinearMap (f.codRestrict p h) = f
This theorem, `LinearMap.subtype_compMultilinearMap_codRestrict`, states that for any semiring `R`, index type `ι`, types `M₁` indexed by `ι`, type `M₂`, a multilinear map `f` from `M₁` to `M₂`, submodule `p` of `M₂`, and a proof `h` that for all `v` of type `M₁`, `f v` belongs to `p`, the composition of the subtype of `p` and the codomain restriction of `f` to `p` (with proof `h`) is equal to `f`. In other words, restricting the codomain of `f` to the submodule `p` and then composing with the inclusion map (subtype) gives back `f` itself.
More concisely: For any semiring `R`, index type `ι`, types `M₁` and `M₂`, a multilinear map `f` from `M₁` to `M₂`, submodule `p` of `M₂`, and proof `h` that `f(v) ∈ p` for all `v` in `M₁`, the subtype inclusion of `p` and the codomain restriction of `f` to `p` (with proof `h`) equal `f`.
|
MultilinearMap.map_piecewise_smul
theorem MultilinearMap.map_piecewise_smul :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (c : ι → R) (m : (i : ι) → M₁ i)
(s : Finset ι), f (s.piecewise (fun i => c i • m i) m) = (s.prod fun i => c i) • f m
This theorem states that for a given multilinear map `f`, if we multiply the coordinates in a finset `s` by `c i` and apply `f` to the result, it is equivalent to multiplying the result of applying `f` to the original coordinates by the product of `c i` over all `i` in `s`. In more mathematical terms, `f((c i) * m i) = (∏ i in s, c i) * f(m)` for all `i` in `s`, where `m` is a function mapping from the index set `ι` to the modules `M₁ i`, `s` is a subset of `ι`, and `c` is a function mapping from `ι` to the ring `R`. This result does not require the index set `ι` to be finite.
More concisely: For a multilinear map `f` and functions `c: ι -> R` and `m: ι -> M₁ i`, the equation `f(∑ i in s, c i * mi) = ∏ i in s, c i * f(mi)` holds for any subset `s` of the index set `ι`.
|
MultilinearMap.coe_injective
theorem MultilinearMap.coe_injective :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂], Function.Injective DFunLike.coe
This theorem, `MultilinearMap.coe_injective`, states that for any semiring `R`, any type `ι`, any type function `M₁ : ι → Type v₁`, any type `M₂ : Type v₂`, and given that `M₁ i` and `M₂` are additive commutative monoids and modules over `R` for all `i : ι`, the coercion function `DFunLike.coe` is injective. In other words, if `DFunLike.coe` applied to two objects results in two identical functions, then those two original objects were identical themselves. This is a property of function-like objects, saying that no two different function-like objects can result in the same function when coerced.
More concisely: For any semiring `R`, given type functions `M₁ : ι → Type v₁` and `M₂ : Type v₂`, if `M₁ i` and `M₂` are additive commutative monoids and modules over `R` for all `i : ι`, then the coercion function `DFunLike.coe` from `M₁ i` to `M₂` is injective.
|
MultilinearMap.compLinearMap_assoc
theorem MultilinearMap.compLinearMap_assoc :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] {M₁' : ι → Type u_1} [inst_5 : (i : ι) → AddCommMonoid (M₁' i)]
[inst_6 : (i : ι) → Module R (M₁' i)] {M₁'' : ι → Type u_2} [inst_7 : (i : ι) → AddCommMonoid (M₁'' i)]
[inst_8 : (i : ι) → Module R (M₁'' i)] (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
The theorem `MultilinearMap.compLinearMap_assoc` states that for any semiring `R`, index type `ι`, types `M₁`, `M₁'`, `M₁''` based on `ι`, and a type `M₂`, given certain conditions such as each `M₁`, `M₁'`, and `M₁''` being an R-module and `M₂` being an additive commutative monoid, then for a multilinear map `g` from `M₁''` to `M₂`, and two sets of linear maps `f₁` and `f₂` from `M₁'` to `M₁''` and `M₁` to `M₁'` respectively, composing `g` with `f₁` and then with `f₂` is the same as composing `g` with the composition of `f₁` and `f₂`. This is a statement about the associative property of function composition in the context of multilinear and linear maps.
More concisely: For any semiring R, index type ι, and multilinear map g from an R-module M₁'' to an additive commutative monoid M₂, the composition g ∘ (f₁ ∘ f₂) equals the composition (g ∘ f₁) ∘ f₂, where f₁ is a linear map from M₁ to M₁' and f₂ is a linear map from M₁' to M₁''.
|
MultilinearMap.map_sub
theorem MultilinearMap.map_sub :
∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
[inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι)
(x y : M₁ i), f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
This theorem asserts that for any semiring `R`, any type `ι`, any `ι`-indexed family of types `M₁`, and any type `M₂`, given the addition commutative group structures on each `M₁ i` and `M₂`, and the module structures over `R` on each `M₁ i` and `M₂`, for any multilinear map `f : MultilinearMap R M₁ M₂`, any `ι`-indexed family of elements `m : (i : ι) → M₁ i`, any index `i : ι`, and any two elements `x, y : M₁ i`, if we replace the `i`-th component of `m` by `x - y`, the result of applying `f` to this new family is equal to the difference of the result of applying `f` to the family obtained by replacing the `i`-th component of `m` by `x`, and the result of applying `f` to the family obtained by replacing the `i`-th component of `m` by `y`. In mathematical terms, this theorem states the linearity of the multilinear map `f` with respect to subtraction in each component of the domain.
More concisely: For any semiring `R`, multilinear map `f : MultilinearMap R (ι → M₁) M₂`, `ι`-indexed family `m : (i : ι) → M₁ i`, and `ι`-indexed family of elements `(x\_i : M₁ i)`, if `M₁ i` is an additive group for all `i : ι`, and `M₂` is an `R`-module, then `f (m.map (λ i, x\_i - x\_i.get i)) = f (m.map (λ i, x\_i)) - f (m.map (λ i, x\_i.get i))`.
|