AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero
theorem AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero :
∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
{N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
[inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
[inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
(σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb},
v i = v j →
i ≠ j →
(AlternatingMap.domCoprod.summand a b σ) v + (AlternatingMap.domCoprod.summand a b (Equiv.swap i j • σ)) v =
0
This theorem states that for any given types `{ιa : Type u_1}` and `{ιb : Type u_2}` equipped with finiteness (`[inst : Fintype ιa]` and `[inst_1 : Fintype ιb]`), a commutative semiring `{R' : Type u_3}`, and types `{Mᵢ : Type u_4}`, `{N₁ : Type u_5}`, `{N₂ : Type u_6}` that are modules over `R'` and have additional structures (`[inst_3 : AddCommGroup N₁]`, `[inst_4 : Module R' N₁]`, `[inst_5 : AddCommGroup N₂]`, `[inst_6 : Module R' N₂]`, `[inst_7 : AddCommMonoid Mᵢ]`, `[inst_8 : Module R' Mᵢ]`), along with decidable equality on `ιa` and `ιb` (`[inst_9 : DecidableEq ιa]`, `[inst_10 : DecidableEq ιb]`), given two linear maps `a : Mᵢ [⋀^ιa]→ₗ[R'] N₁` and `b : Mᵢ [⋀^ιb]→ₗ[R'] N₂`, a permutation `σ : Equiv.Perm.ModSumCongr ιa ιb`, and a function `v : ιa ⊕ ιb → Mᵢ`, if two elements `i, j : ιa ⊕ ιb` of the disjoint union of `ιa` and `ιb` satisfy `v i = v j` and `i ≠ j`, then the sum of the alternating map applied to `v` under `σ` and the same alternating map applied to `v` under a permutation that swaps `i` and `j` in `σ` equals zero. In summary, swapping elements with equal values in the function `v` results in the cancellation of the sum of the alternating maps.
More concisely: For commutative semirings R', modules N₁, N₂, and Mᵢ over R' with additional structures, and given decidable equality on types ιa and ιb and linear maps a and b, if permutation σ preserves the values of function v on disjoint union elements i and j with equal values and i ≠ j, then the alternating sum of a under σ and the alternating sum of a under the permutation swapping i and j equals zero.
|
MultilinearMap.domCoprod_alternization_eq
theorem MultilinearMap.domCoprod_alternization_eq :
∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
{N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
[inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
[inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂),
MultilinearMap.alternatization (a.domCoprod ↑b) =
((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b
This theorem states that for any types `ιa` and `ιb` (where both `ιa` and `ιb` are finite sets), for any commutative semiring `R'`, additive commutative groups `N₁` and `N₂`, and an `R'`-module `Mᵢ`, if we have decidable equality on `ιa` and `ιb`, and if we have two linear maps `a` and `b` from `Mᵢ` to `N₁` and `N₂` respectively (alternating over `ιa` and `ιb`), then the alternatization of the domain coproduct of `a` and `b` equals a scaled version (by the factorials of the cardinalities of `ιa` and `ιb`) of the domain coproduct of `a` and `b`.
The alternatization of a multilinear map is a process that symmetrizes the map with a specific scaling factor, while the domain coproduct of two maps is a new map that combines the actions of the original two maps. The theorem therefore relates these two operations of alternatization and domain coproduct in a specific way.
More concisely: Given finite sets `ιa` and `ιb`, commutative semiring `R'`, additive commutative groups `N₁` and `N₂`, an `R'`-module `Mᵢ`, decidable equality on `ιa` and `ιb`, and linear maps `a : Mᵢ → N₁` and `b : Mᵢ → N₂`, the alternatization of their domain coproduct equals the scaled version of the coproduct of `a` and `b` by the factorials of `ιa` and `ιb`'s cardinalities.
|
MultilinearMap.domCoprod_alternization_coe
theorem MultilinearMap.domCoprod_alternization_coe :
∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
{N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
[inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
[inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : MultilinearMap R' (fun x => Mᵢ) N₁)
(b : MultilinearMap R' (fun x => Mᵢ) N₂),
(MultilinearMap.alternatization a).domCoprod ↑(MultilinearMap.alternatization b) =
Finset.univ.sum fun σa =>
Finset.univ.sum fun σb =>
Equiv.Perm.sign σa •
Equiv.Perm.sign σb • (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b)
This theorem states that for all multilinear maps `a` and `b` from an arbitrary type `Mᵢ` to types `N₁` and `N₂` respectively, over a commutative semiring `R'`, the coproduct of their alternatizations is equal to the sum over all permutations `σa` and `σb` of types `ιa` and `ιb` (where `ιa` and `ιb` are types with decidable equality and finite number of elements), of the product of the signs of `σa` and `σb` and the coproduct of the domain congruences of `a` and `b` under `σa` and `σb` respectively. The sign of a permutation is `1` for even permutations and `-1` for odd permutations. The alternatization of a multilinear map is a multilinear map where the sum of all permutations of its inputs is taken. The domain congruence of a multilinear map under a permutation is the multilinear map obtained by permuting its inputs according to the permutation.
More concisely: For all multilinear maps `a:` Mᵢ -> N₁ and `b:` Mᵢ -> N₂ over a commutative semiring R', the coproduct of their alternatizations equals the sum over all permutations σ of types ιa and ιb with decidable equality and finite number of elements, of the signs of σ and the coproducts of `a` and `b` under σ.
|
AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant
theorem AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant :
∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
{N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
[inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
[inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
(σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb},
v i = v j → i ≠ j → Equiv.swap i j • σ = σ → (AlternatingMap.domCoprod.summand a b σ) v = 0
The theorem `AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant` states that for any types `ιa` and `ιb`, both of finite size, and for any types `R'` (a commutative semiring), `Mᵢ` (an additive commutative monoid with an `R'` module structure), `N₁` and `N₂` (both additive commutative groups with an `R'` module structure). Let `a` be a linear map from `Mᵢ` to `N₁` and `b` a linear map from `Mᵢ` to `N₂`. Let `σ` be an equivalence class of permutations that are identical up to swapping elements within `ιa` or `ιb`. Given any function `v` from the sum type `ιa ⊕ ιb` to `Mᵢ`, and any distinct `i` and `j` in `ιa ⊕ ιb` such that `v(i) = v(j)` and swapping `i` and `j` in `σ` does not affect `σ`, then the input `v` to the function `AlternatingMap.domCoprod.summand a b σ` will yield a zero output.
More concisely: For any commutative semiring R, finite types ιa and ιb, additive commutative monoid Mᵢ with R module structure, additive commutative groups N₁ and N₂ with R module structures, linear maps a from Mᵢ to N₁ and b from Mᵢ to N₂, equivalence class σ of permutations on ιa ⊕ ιb that only swap elements within each type, and any function v from ιa ⊕ ιb to Mᵢ with distinct i and j such that v(i) = v(j) and swapping i and j in σ does not affect it, the application of AlternatingMap.domCoprod.summand a b σ to v yields the zero output.
|
MultilinearMap.domCoprod_alternization
theorem MultilinearMap.domCoprod_alternization :
∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
{N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
[inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
[inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : MultilinearMap R' (fun x => Mᵢ) N₁)
(b : MultilinearMap R' (fun x => Mᵢ) N₂),
MultilinearMap.alternatization (a.domCoprod b) =
(MultilinearMap.alternatization a).domCoprod (MultilinearMap.alternatization b)
This theorem states that for all types `ιa`, `ιb`, `R'`, `Mᵢ`, `N₁`, and `N₂`, if `ιa` and `ιb` are finite types, `R'` is a commutative semiring, `N₁` and `N₂` are modules over `R'` and additive groups, `Mᵢ` is an additive monoid and a module over `R'`, and both `ιa` and `ιb` have decidable equality, then for any two multilinear maps `a` and `b` from `R'` to `Mᵢ` with codomains `N₁` and `N₂` respectively, the alternatization of the domain coproduct of `a` and `b` is equal to the domain coproduct of the alternatizations of `a` and `b`. In mathematical terms, this establishes a certain equality in the manipulation of multilinear maps, particularly when it comes to their alternatization and domain coproduct.
More concisely: For finite types `ιa` and `ιb`, commutative semiring `R'`, modules `N₁`, `N₂`, and additive monoid `Mᵢ` over `R'`, if `ιa` and `ιb` have decidable equality and `a` and `b` are multilinear maps from `R'` to `Mᵢ` with codomains `N₁` and `N₂` respectively, then the alternatization of the domain coproduct of `a` and `b` equals the domain coproduct of the alternatizations of `a` and `b`.
|