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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule R N] {ι : Type u_6} [decidable_eq ι] (s : 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] [semimodule R M] (N : Type u_3) [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule R N] {ι : Type u_6} [decidable_eq ι] (f : alternating_map R M N ι) :
@[simp]
theorem alternating_map.to_multilinear_map_eq_coe {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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'] [semimodule R M'] {N' : Type u_5} [add_comm_group N'] [semimodule 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'] [semimodule R M'] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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

Algebraic structure inherited from multilinear_map #

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

@[instance]
def alternating_map.has_add {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule R N'] {ι : Type u_6} [decidable_eq ι] (g g₂ : alternating_map R M N' ι) :
(g - g₂) = g - g₂
@[instance]
def alternating_map.has_scalar {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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.semimodule {R : Type u_1} [semiring R] {M : Type u_2} [add_comm_monoid M] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule R N] {ι : Type u_6} [decidable_eq ι] {S : Type u_7} [semiring S] [semimodule S N] [smul_comm_class R S 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule R N] {ι : Type u_6} [decidable_eq ι] {N₂ : Type u_7} [add_comm_monoid N₂] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule R N] {ι : Type u_6} [decidable_eq ι] {N₂ : Type u_7} [add_comm_monoid N₂] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule R N] {ι : Type u_6} [decidable_eq ι] {N₂ : Type u_7} [add_comm_monoid N₂] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N : Type u_3} [add_comm_monoid N] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule K M] {N : Type u_3} [add_comm_group N] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule 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] [semimodule R M] {N' : Type u_5} [add_comm_group N'] [semimodule R N'] {ι : Type u_6} [decidable_eq ι] {N'₂ : Type u_7} [add_comm_group N'₂] [semimodule 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.