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

@[protected, 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 ι] :
has_coe_to_fun (alternating_map R M N ι) (λ (_x : alternating_map R M N ι), (ι → M) → N)
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_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, norm_cast]
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 ι} :
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 : ι → M), 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 : ι → M), f x = g x
@[protected, 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, norm_cast]
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
theorem alternating_map.map_eq_zero_of_not_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 ι] (f : alternating_map R M N ι) (v : ι → M) (hv : ¬function.injective v) :
f v = 0

Algebraic structure inherited from multilinear_map #

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

@[protected, 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
@[norm_cast]
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
theorem alternating_map.coe_fn_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 ι] {S : Type u_7} [monoid S] [distrib_mul_action S N] [smul_comm_class R S N] (c : S) (f : alternating_map R M N ι) :
(c f) = c f
@[protected, 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
@[norm_cast]
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'
@[protected, 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
@[norm_cast]
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
@[protected, 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
@[protected, 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
@[protected, 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
@[norm_cast]
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' ι) :
@[protected, 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
@[norm_cast]
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₂
@[protected, 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
  • alternating_map.add_comm_group = function.injective.add_comm_group coe_fn alternating_map.add_comm_group._proof_3 alternating_map.add_comm_group._proof_4 alternating_map.add_comm_group._proof_5 alternating_map.add_comm_group._proof_6 alternating_map.add_comm_group._proof_7 alternating_map.add_comm_group._proof_8 alternating_map.add_comm_group._proof_9
@[protected, 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
@[protected, 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
@[protected, instance]
def alternating_map.no_zero_smul_divisors {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] [no_zero_smul_divisors S N] :
@[simp]
theorem alternating_map.of_subsingleton_apply (R : Type u_1) [semiring R] (N : Type u_3) [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] [subsingleton ι] (i : ι) (f : Π (x : ι), (λ (i : ι), (λ (i : ι), N) i) x) :
def alternating_map.of_subsingleton (R : Type u_1) [semiring R] (N : Type u_3) [add_comm_monoid N] [module R N] {ι : Type u_6} [decidable_eq ι] [subsingleton ι] (i : ι) :

The evaluation map from ι → N to N at a given i is alternating when ι is subsingleton.

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 on the left gives again an 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) :
def alternating_map.comp_linear_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (f : alternating_map R M N ι) (g : M₂ →ₗ[R] M) :
alternating_map R M₂ N ι

Composing a alternating map with the same linear map on each argument gives again an alternating map.

Equations
theorem alternating_map.coe_comp_linear_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (f : alternating_map R M N ι) (g : M₂ →ₗ[R] M) :
@[simp]
theorem alternating_map.comp_linear_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (f : alternating_map R M N ι) (g : M₂ →ₗ[R] M) (v : ι → M₂) :
(f.comp_linear_map g) v = f (λ (i : ι), g (v i))
theorem alternating_map.comp_linear_map_assoc {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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_8} [add_comm_monoid M₃] [module R M₃] (f : alternating_map R M N ι) (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂) :

Composing an alternating map twice with the same linear map in each argument is the same as composing with their composition.

@[simp]
theorem alternating_map.zero_comp_linear_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (g : M₂ →ₗ[R] M) :
@[simp]
theorem alternating_map.add_comp_linear_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (f₁ f₂ : alternating_map R M N ι) (g : M₂ →ₗ[R] M) :
(f₁ + f₂).comp_linear_map g = f₁.comp_linear_map g + f₂.comp_linear_map g
@[simp]
theorem alternating_map.comp_linear_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] [nonempty ι] (f : alternating_map R M N ι) :
@[simp]
theorem alternating_map.comp_linear_map_id {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 ι) :

Composing an alternating map with the identity linear map in each argument.

theorem alternating_map.comp_linear_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (f : M₂ →ₗ[R] M) (hf : function.surjective f) :

Composing with a surjective linear map is injective.

theorem alternating_map.comp_linear_map_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (f : M₂ →ₗ[R] M) (hf : function.surjective f) (g₁ g₂ : alternating_map R M N ι) :
g₁.comp_linear_map f = g₂.comp_linear_map f g₁ = g₂
def alternating_map.dom_lcongr (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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (S : Type u_9) [semiring S] [module S N] [smul_comm_class R S N] (e : M ≃ₗ[R] M₂) :

Construct a linear equivalence between maps from a linear equivalence between domains.

Equations
@[simp]
theorem alternating_map.dom_lcongr_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (S : Type u_9) [semiring S] [module S N] [smul_comm_class R S N] (e : M ≃ₗ[R] M₂) (f : alternating_map R M N ι) :
@[simp]
theorem alternating_map.dom_lcongr_refl (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_9) [semiring S] [module S N] [smul_comm_class R S N] :
@[simp]
theorem alternating_map.dom_lcongr_symm (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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (S : Type u_9) [semiring S] [module S N] [smul_comm_class R S N] (e : M ≃ₗ[R] M₂) :
theorem alternating_map.dom_lcongr_trans (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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] {M₃ : Type u_8} [add_comm_monoid M₃] [module R M₃] (S : Type u_9) [semiring S] [module S N] [smul_comm_class R S N] (e : M ≃ₗ[R] M₂) (f : M₂ ≃ₗ[R] M₃) :
@[simp]
theorem alternating_map.comp_linear_equiv_eq_zero_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 ι] {M₂ : Type u_7} [add_comm_monoid M₂] [module R M₂] (f : alternating_map R M N ι) (g : M₂ ≃ₗ[R] M) :

Composing an alternating map with the same linear equiv on each argument gives the zero map if and only if the alternating map is the zero map.

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.

theorem basis.ext_alternating {ι : Type u_6} [decidable_eq ι] {ι₁ : Type u_7} [fintype ι] {R' : Type u_8} {N₁ : Type u_9} {N₂ : Type u_10} [comm_semiring R'] [add_comm_monoid N₁] [add_comm_monoid N₂] [module R' N₁] [module R' N₂] {f g : alternating_map R' N₁ N₂ ι} (e : basis ι₁ R' N₁) (h : ∀ (v : ι → ι₁), function.injective vf (λ (i : ι), e (v i)) = g (λ (i : ι), e (v i))) :
f = g

Two alternating maps indexed by a fintype are equal if they are equal when all arguments are distinct basis vectors.