AlternatingMap.compLinearMap_injective
theorem AlternatingMap.compLinearMap_injective :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
[inst_6 : Module R M₂] (f : M₂ →ₗ[R] M), Function.Surjective ⇑f → Function.Injective fun g => g.compLinearMap f
The theorem `AlternatingMap.compLinearMap_injective` states that, given any semiring `R`, additively commutative monoids `M` and `N` that form modules over `R`, an index type `ι`, an additional additively commutative monoid `M₂` that forms a module over `R`, and a surjective linear map `f` from `M₂` to `M`, the composition of this map `f` with any other map `g` is an injective operation. In other words, if we have two maps producing the same result when composed with `f`, then these two maps are actually the same. This is a statement about the preservation of uniqueness in the context of linear maps and their compositions.
More concisely: Given a surjective linear map `f` from one additively commutative `R`-module `M₂` to another `R`-module `M`, if for all `x` in `M₂`, `f(g(x)) = f(h(x))` implies `g(x) = h(x)`, then `g = h`.
|
AlternatingMap.coeFn_smul
theorem AlternatingMap.coeFn_smul :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} [inst_5 : Monoid S]
[inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass R S N] (c : S) (f : M [⋀^ι]→ₗ[R] N), ⇑(c • f) = c • ⇑f
The theorem `AlternatingMap.coeFn_smul` states that for any semiring `R`, any type `M` with an additive commutative monoid structure and a module structure over `R`, any type `N` with an additive commutative monoid structure, a module structure over `R`, and a distributive multiplication action by a monoid `S`, and for any types `ι` and `S`, the result of applying a scalar multiplication by a scalar `c` from `S` to an alternating multilinear map `f` from `M` to `N` over `R` (denoted `c • f`) is the same as the result of applying `f` first and then multiplying the result by `c` (denoted `c • ⇑f`). This is, in essence, a statement about the compatibility of scalar multiplication with the action of an alternating multilinear map.
More concisely: For any semirings R, types M with additive commutative monoid and R-module structures, and N with additive commutative monoid, R-module, and distributive S-module structures, and for any alternating multilinear map f from M to N over R, the scalar multiplication of f by a scalar c from S is equivalent to applying c to each input and then applying f.
|
AlternatingMap.coe_injective
theorem AlternatingMap.coe_injective :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7}, Function.Injective DFunLike.coe
The theorem `AlternatingMap.coe_injective` states that for any semiring `R`, any type `M` with the structure of an `R`-module and an additive commutative monoid, any type `N` also with the structure of an `R`-module and an additive commutative monoid, and any type `ι`, the coercion from `DFunLike` to a function is injective. In other words, if two `DFunLike` objects have the same function when coerced, then they were originally the same `DFunLike` object.
More concisely: For any semirings R, types M and N with R-module and additive commutative monoid structures, and type ι, the coercion from DFunLike (R-module M x additive commutative monoid) to (M ⟹ N) is injective.
|
AlternatingMap.map_vecCons_add
theorem AlternatingMap.map_vecCons_add :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M),
f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)
This theorem, named `AlternatingMap.map_vecCons_add`, asserts that for any semiring `R`, any additively commutative monoid `M` that is also a module over `R`, and any other additively commutative monoid `N` that is also a module over `R`, if we have a multilinear map `f` from the multivector space of `M` of dimension `n+1` to `N`, a function `m` from `Fin n` to `M`, and two elements `x` and `y` of `M`, then applying `f` to the vector obtained by prepending `x + y` to `m` is the same as the sum of applying `f` to the vector obtained by prepending `x` to `m` and applying `f` to the vector obtained by prepending `y` to `m`.
In other words, for an alternating multilinear map, adding two inputs and then applying the map is the same as applying the map to each input separately and then adding the results.
More concisely: For any semiring `R`, additively commutative monoids `M` and `N` that are `R`-modules, multilinear map `f` from the multivector space of `M` of dimension `n+1` to `N`, function `m` from `Fin n` to `M`, and elements `x, y` of `M`, we have `f(x :: m ++ [x + y]) = f(x :: m) + f(y :: m)`.
|
AlternatingMap.map_linearDependent
theorem AlternatingMap.map_linearDependent :
∀ {ι : Type u_7} {K : Type u_12} [inst : Ring K] {M : Type u_13} [inst_1 : AddCommGroup M] [inst_2 : Module K M]
{N : Type u_14} [inst_3 : AddCommGroup N] [inst_4 : Module K N] [inst_5 : NoZeroSMulDivisors K N]
(f : M [⋀^ι]→ₗ[K] N) (v : ι → M), ¬LinearIndependent K v → f v = 0
This theorem states that for any type `ι`, ring `K`, types `M` and `N` with addition commutative groups structures and `K` module structures, if there is an alternating map `f` from `M` tensor power `ι` to `N`, and a family of vectors `v` of type `ι` to `M` that is not linearly independent over `K` (i.e., the vectors are linearly dependent), then the result of applying the map `f` to the vectors `v` is the zero element in `N`. Here, `NoZeroSMulDivisors K N` asserts that the scalar multiplication in the `K`-module `N` does not have zero divisors.
More concisely: If `f` is an alternating map from the tensor power of a type `ι` over a commutative ring `K` with no zero divisors, and `v` is a linearly dependent family of vectors in a `K`-module `M` with commutative addition, then `f v_1 ⊗ ... ⊗ v_n = 0` in `N`.
|
AlternatingMap.compLinearMap_id
theorem AlternatingMap.compLinearMap_id :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N),
f.compLinearMap LinearMap.id = f
The theorem `AlternatingMap.compLinearMap_id` states that for any semiring `R`, any `R`-module `M` and `N`, and any index set `ι`, for any alternating linear map `f` from the tensor power of `M` over `ι` to `N`, composing `f` with the identity linear map on `M` does not change `f`. In simpler terms, this theorem says that applying the identity transformation to the input of an alternating map doesn't change the map itself.
More concisely: For any semiring R, R-modules M and N, and index set ι, the composition of an alternating linear map f from the tensor power of M over ι to N with the identity linear map on M is equal to f itself.
|
AlternatingMap.map_zero
theorem AlternatingMap.map_zero :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) [inst_5 : Nonempty ι],
f 0 = 0
This theorem, `AlternatingMap.map_zero`, states that for any semiring `R`, an additively commutative monoid `M` that is also an `R`-module, an additively commutative monoid `N` that is also an `R`-module, and any type `ι`, given a linear map `f` from the `ι`-fold wedge product of `M` to `N` (which is an alternating multilinear map), if `ι` is nonempty, then the application of `f` to the zero element of the `ι`-fold wedge product of `M` is the zero element of `N`. In other words, applying an alternating multilinear map to zero yields zero.
More concisely: For any semiring `R`, additively commutative `R`-modules `M` and `N`, and an alternating multilinear map `f` from the `ι`-fold wedge product of `M` to `N`, if `ι` is nonempty, then `f(∧⁰ x:\_ | i:ι) 0 = 0`, where `∧⁰` denotes the `ι`-fold wedge product.
|
Basis.ext_alternating
theorem Basis.ext_alternating :
∀ {ι : Type u_7} {ι₁ : Type u_10} [inst : Finite ι] {R' : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13}
[inst : CommSemiring R'] [inst_1 : AddCommMonoid N₁] [inst_2 : AddCommMonoid N₂] [inst_3 : Module R' N₁]
[inst_4 : Module R' N₂] {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁),
(∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) → f = g
This theorem states that given two types `ι` and `ι₁`, and given `ι` is a finite type, alongside types `R'`, `N₁`, and `N₂`, with `R'` being a commutative semiring, and `N₁` and `N₂` being additive commutative monoids and also modules over `R'`, for any two linear maps `f` and `g` from the exterior product of `ι` with `N₁` to `N₂`, and a basis `e` of `N₁` over `R'` indexed by `ι₁`, if for any function `v` from `ι` to `ι₁` where `v` is injective, both `f` and `g` applied on the transformed basis vectors by `v` yield the same results, then `f` and `g` must be identical maps. This theorem addresses the equality of two alternating maps in the context of algebraic topology and linear algebra, particularly in relation with exterior algebra and basis transformation.
More concisely: Given a finite type `ι`, commutative semiring `R'`, additive commutative monoids and `R'`-modules `N₁` and `N₂`, and linear maps `f` and `g` from the exterior product of `ι` with `N₁` to `N₂`, if for any injective function `v` from `ι` to `ι₁`, `f(eₗₙ ⊤ i) = g(eₗₙ ⊤ (v i))` for all basis vectors `eₗₙ` indexed by `ι₁`, then `f = g`.
|
AlternatingMap.map_vecCons_smul
theorem AlternatingMap.map_vecCons_smul :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R)
(x : M), f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)
This theorem, `AlternatingMap.map_vecCons_smul`, states that for any semiring `R`, for any type `M` which is an additive commutative monoid and a module over `R`, and for any type `N` also an additive commutative monoid and a module over `R`, for any natural number `n`, and for any linear map `f` from the n-th exterior power of `M` to `N`, any function `m` from `Fin n` to `M`, any scalar `c` in `R`, and any vector `x` in `M`, the result of applying `f` to the vector obtained by prepending `c` scaled `x` to `m` is equal to `c` scaled by the result of applying `f` to the vector obtained by prepending `x` to `m`. In simpler terms, it's saying that scaling a vector and then applying a linear map is the same as applying the linear map and then scaling the result.
More concisely: For any semiring `R`, additive commutative monoids and `R`-modules `M` and `N`, natural number `n`, linear map `f` from the exterior power of `M` to `N`, function `m` from `Fin n` to `M`, scalar `c` in `R`, and vector `x` in `M`, we have `f (c % (vector.cons x m)) = c % (f (vector.cons x m))`.
|
AlternatingMap.coe_alternatization
theorem AlternatingMap.coe_alternatization :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
[inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
(a : M [⋀^ι]→ₗ[R] N'), MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a
This theorem states that if we alternatize an already alternating multilinear map, the result is scaled by the factorial of the number of inputs. More specifically, for any semiring `R`, additive commutative monoid `M`, `R`-module structure on `M`, additive commutative group `N'`, `R`-module structure on `N'`, and decidable equality and finite type of `ι`, if we have a multilinear map `a` from `M` to `N'` indexed by `ι`, then the alternatization of `a` equals the factorial of the cardinality (number of elements) of `ι` times `a`. In essence, alternatizing an alternating multilinear map only introduces a scaling factor equal to the factorial of the number of inputs.
More concisely: For any multilinear map `a` from a finite additive commutative monoid `M` to an `R`-module `N'`, where `R` is a semiring, the alternatization of `a` is equal to the factorial of the number of inputs times `a`.
|
AlternatingMap.compLinearMap_assoc
theorem AlternatingMap.compLinearMap_assoc :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
[inst_6 : Module R M₂] {M₃ : Type u_11} [inst_7 : AddCommMonoid M₃] [inst_8 : Module R M₃] (f : M [⋀^ι]→ₗ[R] N)
(g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂), (f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂)
The theorem `AlternatingMap.compLinearMap_assoc` states that for a given semiring `R`, modules `M`, `M₂`, `M₃`, and `N`, an alternating map `f` from `M` to `N`, and linear maps `g₁` from `M₂` to `M` and `g₂` from `M₃` to `M₂`, composing `f` with `g₁` and then with `g₂` is the same as composing `f` with the composition of `g₁` and `g₂`. This is an associative property that holds for the composition of linear maps in an alternating map context.
More concisely: For an alternating map `f` and linear maps `g₁` and `g₂`, `(f ∘ g₁) ∘ g₂ = f ∘ (g₁ ∘ g₂)` holds in a semiring `R` with modules `M`, `M₂`, `M₃`, and `N`.
|
AlternatingMap.curryLeft_same
theorem AlternatingMap.curryLeft_same :
∀ {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M'']
[inst_2 : AddCommMonoid N''] [inst_3 : Module R' M''] [inst_4 : Module R' N''] {n : ℕ}
(f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N'') (m : M''), (f.curryLeft m).curryLeft m = 0
This theorem, "AlternatingMap.curryLeft_same", states that for any commutative semiring `R'`, additively commutative monoids `M''` and `N''`, modules `M''` and `N''` over `R'`, natural number `n` and linear map `f` from `M''` tensor product to `N''`, and any element `m` of `M''`, applying the curryLeft operation twice on the same element `m` yields the zero map. The curryLeft operation here refers to a transformation that changes the input of a function from a tuple to a single argument.
More concisely: For any commutative semiring R, additively commutative monoids M and N, modules M and N over R, natural number n, and linear map f : M ⊗ N → N, the curried application of f to an element m in M, applied twice, equals the zero map. In Lean notation: ∀ (R : Type u), (comm_semiring R), (M : Type u), (N : Type u), ([M : add_monoid M] : Type u), ([N : add_monoid N] : Type u)), ([M : add_module M R] : Type u), ([N : add_module N R] : Type u)), (n : ℕ), (f : M ⊗ N → N), (m : M), (curried_f : M → N) (hM : add_map curried_f M N), (curried_f '' m) '' m = 0.
|
AlternatingMap.map_eq_zero_of_eq'
theorem AlternatingMap.map_eq_zero_of_eq' :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (self : M [⋀^ι]→ₗ[R] N) (v : ι → M) (i j : ι),
v i = v j → i ≠ j → self.toFun v = 0
This theorem states that for any semiring `R`, any modules `M` and `N` over `R`, and any function `v` from some index type `ι` into `M`, if there exist two distinct indices `i` and `j` such that `v(i)` equals `v(j)`, then applying an alternating map `f` (represented by `self.toFun`) to `v` yields zero. In other words, an alternating map applied to a function with at least two equal but differently indexed values always results in zero.
More concisely: For any semiring `R`, modules `M` and `N` over `R`, and function `v` from an index type `ι` into `M` having distinct indices `i` and `j` such that `v(i) = v(j)`, the alternating map `f` applied to `v` results in zero.
|
AlternatingMap.map_perm
theorem AlternatingMap.map_perm :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
[inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [inst_5 : DecidableEq ι]
[inst_6 : Fintype ι] (v : ι → M) (σ : Equiv.Perm ι), g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v
The theorem `AlternatingMap.map_perm` states that for any semiring `R`, and for any modules `M` and `N'` over `R`, and any type `ι` with decidable equality and that is finite, given an alternating multilinear map `g : M [⋀^ι]→ₗ[R] N'`, a function `v : ι → M`, and a permutation `σ : Equiv.Perm ι`, the result of applying `g` to the composition of `v` and `σ` equals to the signature of `σ` times the result of applying `g` to `v`. In other words, permuting the arguments of an alternating multilinear map and scaling by the signature of the permutation does not change the result of the map.
More concisely: For any semiring `R`, finite type `ι` with decidable equality, modules `M` and `N'` over `R`, and alternating multilinear map `g : M [⋀^ι] →ₗ[R] N'`, the application of `g` to the composition of a function `v : ι → M` and a permutation `σ : Equiv.Perm ι` equals the signature of `σ` times the application of `g` to `v`.
|
AlternatingMap.compLinearEquiv_eq_zero_iff
theorem AlternatingMap.compLinearEquiv_eq_zero_iff :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
[inst_6 : Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M), f.compLinearMap ↑g = 0 ↔ f = 0
This theorem states that for a given semiring `R`, a module `M` over `R`, a module `N` over `R`, a module `M₂` over `R`, an alternating map `f` from the tensor product of `M` with itself (iterated over the index set `ι`) to `N`, and a linear equivalence `g` from `M₂` to `M`, the composition of the alternating map `f` with the linear map corresponding to `g` is the zero map if and only if `f` is the zero map. This theorem is significant in the theory of linear algebra, particularly in relation to alternating maps and tensor products.
More concisely: For any semiring R, modules M, N, and M₂ over R, an alternating map f from M∫ι to N, and a linear equivalence g from M₂ to M, if and only if f is the zero map, then the composition of f with the linear map induced by g is the zero map.
|
AlternatingMap.domDomCongr_eq_iff
theorem AlternatingMap.domDomCongr_eq_iff :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι')
(f g : M [⋀^ι]→ₗ[R] N), AlternatingMap.domDomCongr σ f = AlternatingMap.domDomCongr σ g ↔ f = g
This theorem states that for any semiring `R`, additive commutative monoids `M` and `N` which are also `R`-modules, and types `ι` and `ι'`, where `σ` is a type equivalence between `ι` and `ι'`, and `f` and `g` are linear maps from `M` to `N` with the alternating property over index type `ι`, the result of applying the `domDomCongr` (domain-domain congruence) operation to `f` and `g` with `σ` are equal if and only if `f` and `g` are equal. In other words, `domDomCongr` operation preserves the equality of linear maps with the alternating property.
More concisely: For any semiring `R`, additive commutative `R`-modules `M` and `N`, type equivalences `σ : ι ≈ ι'`, and linear maps `f, g : M → N` with the alternating property over index type `ι`, `domDomCongr f σ = domDomCongr g σ` if and only if `f = g`.
|
AlternatingMap.ext
theorem AlternatingMap.ext :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {f f' : M [⋀^ι]→ₗ[R] N},
(∀ (x : ι → M), f x = f' x) → f = f'
This theorem, named `AlternatingMap.ext`, asserts that for any semiring `R`, additive commutative monoid `M`, and module `M` over `R`, and any other additive commutative monoid `N` and module `N` over `R`, along with a type `ι` and two linear maps `f` and `f'` from the tensor power of `M` indexed by `ι` to `N`, if `f` and `f'` are equal for all mappings from `ι` to `M`, then `f` and `f'` are indeed the same linear map. This is a form of extensionality for alternating maps in the setting of module theory.
More concisely: If two linear maps between tensor powers of modules over a semiring, indexed by the same type, have the same value for all mappings from the type to the base modules, then they are equal.
|
AlternatingMap.map_eq_zero_of_eq
theorem AlternatingMap.map_eq_zero_of_eq :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) {i j : ι},
v i = v j → i ≠ j → f v = 0
This theorem states that for any semiring `R`, if `M` and `N` are both modules over `R`, and `f` is an alternating map from `M` to `N`, then if there exist indices `i` and `j` such that `i` is not equal to `j` and the `i`th and `j`th elements of a function `v` from `ι` to `M` are equal, then applying `f` to `v` yields zero. In other words, an alternating map applied to a function where at least two values are equal (and the indices of these values are not the same) gives zero.
More concisely: For any semiring `R`, if `f` is an alternating map from a module `M` over `R` to another module `N` over `R`, then applying `f` to any function `v` from an indexed set to `M` with distinct indices `i` and `j` such that `v i = v j`, yields zero.
|
LinearMap.compMultilinearMap_alternatization
theorem LinearMap.compMultilinearMap_alternatization :
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
[inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} {N'₂ : Type u_10} [inst_5 : AddCommGroup N'₂]
[inst_6 : Module R N'₂] [inst_7 : DecidableEq ι] [inst_8 : Fintype ι] (g : N' →ₗ[R] N'₂)
(f : MultilinearMap R (fun x => M) N'),
MultilinearMap.alternatization (g.compMultilinearMap f) =
g.compAlternatingMap (MultilinearMap.alternatization f)
The theorem `LinearMap.compMultilinearMap_alternatization` states that for any semiring `R`, any additively commutative monoid `M` that is also a module over `R`, any additively commutative group `N'` that is also a module over `R`, any type `ι` with decidable equality and which is finite, any linear map `g` from `N'` to another additively commutative group `N'₂` that is also a module over `R`, and any multilinear map `f` from `ι`-indexed tuples of `M` to `N'`, the result of taking the alternatization of the composition of `g` and `f` (in that order) is the same as the result of first taking the alternatization of `f` and then composing `g`. Here, alternatization refers to a process that makes a multilinear map into an alternating multilinear map (which is antisymmetric).
More concisely: For any semiring R, additively commutative monoid M over R, additively commutative group N' and N'_2, finite type ι with decidable equality, linear map g from N' to N'_2 over R, and multilinear map f from ι-indexed tuples of M to N', the alternation of g ∘ f equals the alternation of f ∘ g.
|