mathlib documentation

linear_algebra.alternating

Alternating Maps #

We construct the bundled function alternating_map, which extends multilinear_map with all the arguments of the same type.

Main definitions #

Implementation notes #

alternating_map is defined in terms of map_eq_zero_of_eq, as this is easier to work with than using map_swap as a definition, and does not require has_neg N.

alternating_maps are provided with a coercion to multilinear_map, along with a set of norm_cast lemmas that act on the algebraic structure:

def alternating_map.to_multilinear_map {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (self : alternating_map R M N ι) :
multilinear_map R (λ (i : ι), M) N

The multilinear map associated to an alternating map

structure alternating_map (R : Type u_1) [semiring R] (M : Type u_2) [add_comm_monoid M] [module R M] (N : Type u_3) [add_comm_monoid N] [module R N] (ι : Type u_6) [decidable_eq ι] :
Type (max u_2 u_3 u_6)

An alternating map is a multilinear map that vanishes when two of its arguments are equal.

Basic coercion simp lemmas, largely copied from ring_hom and multilinear_map

@[instance]
def alternating_map.has_coe_to_fun {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
Equations
@[simp]
theorem alternating_map.to_fun_eq_coe {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) :
@[simp]
theorem alternating_map.coe_mk {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : (ι → M) → N) (h₁ : ∀ (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), f (function.update m i (x + y)) = f (function.update m i x) + f (function.update m i y)) (h₂ : ∀ (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), f (function.update m i (c x)) = c f (function.update m i x)) (h₃ : ∀ (v : ι → M) (i j : ι), v i = v ji jf v = 0) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, map_eq_zero_of_eq' := h₃} = f
theorem alternating_map.congr_fun {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {f g : alternating_map R M N ι} (h : f = g) (x : ι → M) :
f x = g x
theorem alternating_map.congr_arg {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) {x y : ι → M} (h : x = y) :
f x = f y
theorem alternating_map.coe_inj {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] ⦃f g : alternating_map R M N ι⦄ (h : f = g) :
f = g
@[ext]
theorem alternating_map.ext {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {f f' : alternating_map R M N ι} (H : ∀ (x : Π (i : ι), (λ (i : ι), M) i), f x = f' x) :
f = f'
theorem alternating_map.ext_iff {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {f g : alternating_map R M N ι} :
f = g ∀ (x : Π (i : ι), (λ (i : ι), M) i), f x = g x
@[instance]
def alternating_map.multilinear_map.has_coe {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
has_coe (alternating_map R M N ι) (multilinear_map R (λ (i : ι), M) N)
Equations
@[simp]
theorem alternating_map.coe_multilinear_map {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) :
theorem alternating_map.coe_multilinear_map_injective {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
@[simp]
theorem alternating_map.to_multilinear_map_eq_coe {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) :
@[simp]
theorem alternating_map.coe_multilinear_map_mk {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : (ι → M) → N) (h₁ : ∀ (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), f (function.update m i (x + y)) = f (function.update m i x) + f (function.update m i y)) (h₂ : ∀ (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), f (function.update m i (c x)) = c f (function.update m i x)) (h₃ : ∀ (v : ι → M) (i j : ι), v i = v ji jf v = 0) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, map_eq_zero_of_eq' := h₃} = {to_fun := f, map_add' := h₁, map_smul' := h₂}

Simp-normal forms of the structure fields #

These are expressed in terms of ⇑f instead of f.to_fun.

@[simp]
theorem alternating_map.map_add {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (v : ι → M) (i : ι) (x y : M) :
f (function.update v i (x + y)) = f (function.update v i x) + f (function.update v i y)
@[simp]
theorem alternating_map.map_sub {R : Type u_1} [semiring R] {M' : Type u_4} [add_comm_group M'] [module R M'] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g' : alternating_map R M' N' ι) (v' : ι → M') (i : ι) (x y : M') :
g' (function.update v' i (x - y)) = g' (function.update v' i x) - g' (function.update v' i y)
@[simp]
theorem alternating_map.map_neg {R : Type u_1} [semiring R] {M' : Type u_4} [add_comm_group M'] [module R M'] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g' : alternating_map R M' N' ι) (v' : ι → M') (i : ι) (x : M') :
g' (function.update v' i (-x)) = -g' (function.update v' i x)
@[simp]
theorem alternating_map.map_smul {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (v : ι → M) (i : ι) (r : R) (x : M) :
f (function.update v i (r x)) = r f (function.update v i x)
@[simp]
theorem alternating_map.map_eq_zero_of_eq {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (v : ι → M) {i j : ι} (h : v i = v j) (hij : i j) :
f v = 0
theorem alternating_map.map_coord_zero {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) {m : ι → M} (i : ι) (h : m i = 0) :
f m = 0
@[simp]
theorem alternating_map.map_update_zero {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (m : ι → M) (i : ι) :
f (function.update m i 0) = 0
@[simp]
theorem alternating_map.map_zero {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) [nonempty ι] :
f 0 = 0

Algebraic structure inherited from multilinear_map #

alternating_map carries the same add_comm_monoid, add_comm_group, and module structure as multilinear_map

@[instance]
def alternating_map.has_add {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
Equations
@[simp]
theorem alternating_map.add_apply {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f f' : alternating_map R M N ι) (v : ι → M) :
(f + f') v = f v + f' v
theorem alternating_map.coe_add {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f f' : alternating_map R M N ι) :
(f + f') = f + f'
@[instance]
def alternating_map.has_zero {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
Equations
@[simp]
theorem alternating_map.zero_apply {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (v : ι → M) :
0 v = 0
theorem alternating_map.coe_zero {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
0 = 0
@[instance]
def alternating_map.inhabited {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
Equations
@[instance]
def alternating_map.add_comm_monoid {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] :
Equations
@[instance]
def alternating_map.has_neg {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] :
Equations
@[simp]
theorem alternating_map.neg_apply {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g : alternating_map R M N' ι) (m : ι → M) :
(-g) m = -g m
theorem alternating_map.coe_neg {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g : alternating_map R M N' ι) :
@[instance]
def alternating_map.has_sub {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] :
Equations
@[simp]
theorem alternating_map.sub_apply {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g g₂ : alternating_map R M N' ι) (m : ι → M) :
(g - g₂) m = g m - g₂ m
theorem alternating_map.coe_sub {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g g₂ : alternating_map R M N' ι) :
(g - g₂) = g - g₂
@[instance]
def alternating_map.add_comm_group {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] :
Equations
@[instance]
def alternating_map.has_scalar {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {S : Type u_7} [monoid S] [distrib_mul_action S N] [smul_comm_class R S N] :
Equations
@[simp]
theorem alternating_map.smul_apply {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) {S : Type u_7} [monoid S] [distrib_mul_action S N] [smul_comm_class R S N] (c : S) (m : ι → M) :
(c f) m = c f m
theorem alternating_map.coe_smul {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) {S : Type u_7} [monoid S] [distrib_mul_action S N] [smul_comm_class R S N] (c : S) :
(c f) = c f
@[instance]
def alternating_map.distrib_mul_action {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {S : Type u_7} [monoid S] [distrib_mul_action S N] [smul_comm_class R S N] :
Equations
@[instance]
def alternating_map.module {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {S : Type u_7} [semiring S] [module S N] [smul_comm_class R S N] :
module S (alternating_map R M N ι)

The space of multilinear maps over an algebra over R is a module over R, for the pointwise addition and scalar multiplication.

Equations

Composition with linear maps #

def linear_map.comp_alternating_map {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] (g : N →ₗ[R] N₂) :
alternating_map R M N ι →+ alternating_map R M N₂ ι

Composing a alternating map with a linear map gives again a alternating map.

Equations
@[simp]
theorem linear_map.coe_comp_alternating_map {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] (g : N →ₗ[R] N₂) (f : alternating_map R M N ι) :
theorem linear_map.comp_alternating_map_apply {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] (g : N →ₗ[R] N₂) (f : alternating_map R M N ι) (m : ι → M) :

Other lemmas from multilinear_map #

theorem alternating_map.map_update_sum {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) {α : Type u_4} (t : finset α) (i : ι) (g : α → M) (m : ι → M) :
f (function.update m i (∑ (a : α) in t, g a)) = ∑ (a : α) in t, f (function.update m i (g a))

Theorems specific to alternating maps #

Various properties of reordered and repeated inputs which follow from alternating_map.map_eq_zero_of_eq.

theorem alternating_map.map_update_self {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (v : ι → M) {i j : ι} (hij : i j) :
f (function.update v i (v j)) = 0
theorem alternating_map.map_update_update {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (v : ι → M) {i j : ι} (hij : i j) (m : M) :
theorem alternating_map.map_swap_add {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (v : ι → M) {i j : ι} (hij : i j) :
f (v (equiv.swap i j)) + f v = 0
theorem alternating_map.map_add_swap {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N : Type u_3} [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) (v : ι → M) {i j : ι} (hij : i j) :
f v + f (v (equiv.swap i j)) = 0
theorem alternating_map.map_swap {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g : alternating_map R M N' ι) (v : ι → M) {i j : ι} (hij : i j) :
g (v (equiv.swap i j)) = -g v
theorem alternating_map.map_perm {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g : alternating_map R M N' ι) [fintype ι] (v : ι → M) (σ : equiv.perm ι) :
theorem alternating_map.map_congr_perm {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g : alternating_map R M N' ι) (v : ι → M) [fintype ι] (σ : equiv.perm ι) :
theorem alternating_map.coe_dom_dom_congr {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] (g : alternating_map R M N' ι) [fintype ι] (σ : equiv.perm ι) :
theorem alternating_map.map_linear_dependent {ι : Type u_6} [decidable_eq ι] {K : Type u_1} [ring K] {M : Type u_2} [add_comm_group M] [module K M] {N : Type u_3} [add_comm_group N] [module K N] [no_zero_smul_divisors K N] (f : alternating_map K M N ι) (v : ι → M) (h : ¬linear_independent K v) :
f v = 0

If the arguments are linearly dependent then the result is 0.

def multilinear_map.alternatization {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] [fintype ι] :
multilinear_map R (λ (i : ι), M) N' →+ alternating_map R M N' ι

Produce an alternating_map out of a multilinear_map, by summing over all argument permutations.

Equations
theorem multilinear_map.alternatization_def {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] [fintype ι] (m : multilinear_map R (λ (i : ι), M) N') :
theorem multilinear_map.alternatization_coe {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] [fintype ι] (m : multilinear_map R (λ (i : ι), M) N') :
theorem multilinear_map.alternatization_apply {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] [fintype ι] (m : multilinear_map R (λ (i : ι), M) N') (v : ι → M) :
theorem alternating_map.coe_alternatization {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] [fintype ι] (a : alternating_map R M N' ι) :

Alternatizing a multilinear map that is already alternating results in a scale factor of n!, where n is the number of inputs.

theorem linear_map.comp_multilinear_map_alternatization {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {N' : Type u_5} [add_comm_group N'] [module R N'] {ι : Type u_6} [decidable_eq ι] {N'₂ : Type u_7} [add_comm_group N'₂] [module R N'₂] [fintype ι] (g : N' →ₗ[R] N'₂) (f : multilinear_map R (λ (_x : ι), M) N') :

Composition with a linear map before and after alternatization are equivalent.

def equiv.perm.mod_sum_congr (α : Type u_1) (β : Type u_2) :
Type (max u_1 u_2)

Elements which are considered equivalent if they differ only by swaps within α or β

theorem equiv.perm.mod_sum_congr.swap_smul_involutive {α : Type u_1} {β : Type u_2} [decidable_eq β)] (i j : α β) :
def alternating_map.dom_coprod.summand {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) (σ : equiv.perm.mod_sum_congr ιa ιb) :
multilinear_map R' (λ (_x : ιa ιb), Mᵢ) (N₁ N₂)

summand used in alternating_map.dom_coprod

Equations
theorem alternating_map.dom_coprod.summand_mk' {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) (σ : equiv.perm (ιa ιb)) :
theorem alternating_map.dom_coprod.summand_add_swap_smul_eq_zero {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) (σ : equiv.perm.mod_sum_congr ιa ιb) {v : ιa ιb → Mᵢ} {i j : ιa ιb} (hv : v i = v j) (hij : i j) :

Swapping elements in σ with equal values in v results in an addition that cancels

theorem alternating_map.dom_coprod.summand_eq_zero_of_smul_invariant {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) (σ : equiv.perm.mod_sum_congr ιa ιb) {v : ιa ιb → Mᵢ} {i j : ιa ιb} (hv : v i = v j) (hij : i j) :

Swapping elements in σ with equal values in v result in zero if the swap has no effect on the quotient.

def alternating_map.dom_coprod {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) :
alternating_map R' Mᵢ (N₁ N₂) (ιa ιb)

Like multilinear_map.dom_coprod, but ensures the result is also alternating.

Note that this is usually defined (for instance, as used in Proposition 22.24 in [GQ11]) over integer indices ιa = fin n and ιb = fin m, as $$ (f \wedge g)(u_1, \ldots, u_{m+n}) = \sum_{\operatorname{shuffle}(m, n)} \operatorname{sign}(\sigma) f(u_{\sigma(1)}, \ldots, u_{\sigma(m)}) g(u_{\sigma(m+1)}, \ldots, u_{\sigma(m+n)}), $$ where $\operatorname{shuffle}(m, n)$ consists of all permutations of $[1, m+n]$ such that $\sigma(1) < \cdots < \sigma(m)$ and $\sigma(m+1) < \cdots < \sigma(m+n)$.

Here, we generalize this by replacing:

  • the product in the sum with a tensor product
  • the filtering of $[1, m+n]$ to shuffles with an isomorphic quotient
  • the additions in the subscripts of $\sigma$ with an index of type sum

The specialized version can be obtained by combining this definition with fin_sum_fin_equiv and algebra.lmul'.

Equations
@[simp]
theorem alternating_map.dom_coprod_apply {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) (v : Π (i : ιa ιb), (λ (i : ιa ιb), Mᵢ) i) :
theorem alternating_map.dom_coprod_coe {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) :
def alternating_map.dom_coprod' {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] :
alternating_map R' Mᵢ N₁ ιa alternating_map R' Mᵢ N₂ ιb →ₗ[R'] alternating_map R' Mᵢ (N₁ N₂) (ιa ιb)

A more bundled version of alternating_map.dom_coprod that maps ((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.

Equations
@[simp]
theorem alternating_map.dom_coprod'_apply {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) :
theorem multilinear_map.dom_coprod_alternization_coe {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : multilinear_map R' (λ (_x : ιa), Mᵢ) N₁) (b : multilinear_map R' (λ (_x : ιb), Mᵢ) N₂) :

A helper lemma for multilinear_map.dom_coprod_alternization.

theorem multilinear_map.dom_coprod_alternization {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : multilinear_map R' (λ (_x : ιa), Mᵢ) N₁) (b : multilinear_map R' (λ (_x : ιb), Mᵢ) N₂) :

Computing the multilinear_map.alternatization of the multilinear_map.dom_coprod is the same as computing the alternating_map.dom_coprod of the multilinear_map.alternatizations.

theorem multilinear_map.dom_coprod_alternization_eq {ιa : Type u_7} {ιb : Type u_8} [decidable_eq ιa] [decidable_eq ιb] [fintype ιa] [fintype ιb] {R' : Type u_9} {Mᵢ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] (a : alternating_map R' Mᵢ N₁ ιa) (b : alternating_map R' Mᵢ N₂ ιb) :

Taking the multilinear_map.alternatization of the multilinear_map.dom_coprod of two alternating_maps gives a scaled version of the alternating_map.coprod of those maps.