# mathlib3documentation

linear_algebra.alternating

# Alternating Maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• alternating_map R M N ι is the space of R-linear alternating maps from ι → M to N.
• f.map_eq_zero_of_eq expresses that f is zero when two inputs are equal.
• f.map_swap expresses that f is negated when two inputs are swapped.
• f.map_perm expresses how f varies by a sign change under a permutation of its inputs.
• An add_comm_monoid, add_comm_group, and module structure over alternating_maps that matches the definitions over multilinear_maps.
• multilinear_map.dom_dom_congr, for permutating the elements within a family.
• multilinear_map.alternatization, which makes an alternating map out of a non-alternating one.
• alternating_map.dom_coprod, which behaves as a product between two alternating maps.
• alternating_map.curry_left, for binding the leftmost argument of an alternating map indexed by fin n.succ.

## 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:

• alternating_map.coe_add
• alternating_map.coe_zero
• alternating_map.coe_sub
• alternating_map.coe_neg
• alternating_map.coe_smul
def alternating_map.to_multilinear_map {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (self : N ι) :
(λ (i : ι), M) N

The multilinear map associated to an alternating map

structure alternating_map (R : Type u_1) [semiring R] (M : Type u_2) [ M] (N : Type u_3) [ N] (ι : Type u_7) :
Type (max u_2 u_3 u_7)
• to_fun : (Π (i : ι), (λ (i : ι), M) i) N
• map_add' : [_inst_1_1 : (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), self.to_fun i (x + y)) = self.to_fun i x) + self.to_fun i y)
• map_smul' : [_inst_1_1 : (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), self.to_fun i (c x)) = c self.to_fun i x)
• map_eq_zero_of_eq' : (v : ι M) (i j : ι), v i = v j i j self.to_fun v = 0

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

Instances for alternating_map

Basic coercion simp lemmas, largely copied from ring_hom and multilinear_map

@[protected, instance]
def alternating_map.fun_like {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
fun_like M N ι) M) (λ (_x : ι M), N)
Equations
@[protected, instance]
def alternating_map.has_coe_to_fun {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
has_coe_to_fun M N ι) (λ (_x : N ι), M) N)
Equations
@[simp]
theorem alternating_map.to_fun_eq_coe {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) :
@[simp]
theorem alternating_map.coe_mk {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : M) N) (h₁ : [_inst_1 : (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), f i (x + y)) = f i x) + f i y)) (h₂ : [_inst_1_1 : (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), f i (c x)) = c f i x)) (h₃ : (v : ι M) (i j : ι), v i = v j i j f 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {f g : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
@[simp, norm_cast]
theorem alternating_map.coe_inj {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {f g : N ι} :
f = g f = g
@[ext]
theorem alternating_map.ext {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {f f' : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {f g : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
has_coe M N ι) (λ (i : ι), M) N)
Equations
@[simp, norm_cast]
theorem alternating_map.coe_multilinear_map {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) :
theorem alternating_map.coe_multilinear_map_injective {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
@[simp]
theorem alternating_map.to_multilinear_map_eq_coe {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) :
@[simp]
theorem alternating_map.coe_multilinear_map_mk {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : M) N) (h₁ : [_inst_1 : (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), f i (x + y)) = f i x) + f i y)) (h₂ : [_inst_1_1 : (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), f i (c x)) = c f i x)) (h₃ : (v : ι M) (i j : ι), v i = v j i j f 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (v : ι M) [decidable_eq ι] (i : ι) (x y : M) :
f i (x + y)) = f i x) + f i y)
@[simp]
theorem alternating_map.map_sub {R : Type u_1} [semiring R] {M' : Type u_5} [add_comm_group M'] [ M'] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g' : M' N' ι) (v' : ι M') [decidable_eq ι] (i : ι) (x y : M') :
g' i (x - y)) = g' i x) - g' i y)
@[simp]
theorem alternating_map.map_neg {R : Type u_1} [semiring R] {M' : Type u_5} [add_comm_group M'] [ M'] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g' : M' N' ι) (v' : ι M') [decidable_eq ι] (i : ι) (x : M') :
g' i (-x)) = -g' i x)
@[simp]
theorem alternating_map.map_smul {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (v : ι M) [decidable_eq ι] (i : ι) (r : R) (x : M) :
f i (r x)) = r f i x)
@[simp]
theorem alternating_map.map_eq_zero_of_eq {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) [decidable_eq ι] (m : ι M) (i : ι) :
f i 0) = 0
@[simp]
theorem alternating_map.map_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) [nonempty ι] :
f 0 = 0
theorem alternating_map.map_eq_zero_of_not_injective {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (v : ι M) (hv : ¬) :
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_smul {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {S : Type u_10} [monoid S] [ N] [ N] :
M N ι)
Equations
@[simp]
theorem alternating_map.smul_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) {S : Type u_10} [monoid S] [ N] [ 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) {S : Type u_10} [monoid S] [ N] [ N] (c : S) :
(c f) = c f
theorem alternating_map.coe_fn_smul {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {S : Type u_10} [monoid S] [ N] [ N] (c : S) (f : N ι) :
(c f) = c f
@[protected, instance]
def alternating_map.is_central_scalar {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {S : Type u_10} [monoid S] [ N] [ N] [ N] :
M N ι)
@[simp]
theorem alternating_map.prod_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {P : Type u_4} [ P] {ι : Type u_7} (f : N ι) (g : P ι) (ᾰ : Π (i : ι), (λ (i : ι), M) i) :
(f.prod g) = (f ᾰ, g ᾰ)
def alternating_map.prod {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {P : Type u_4} [ P] {ι : Type u_7} (f : N ι) (g : P ι) :
(N × P) ι

The cartesian product of two alternating maps, as a multilinear map.

Equations
@[simp]
theorem alternating_map.coe_prod {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {P : Type u_4} [ P] {ι : Type u_7} (f : N ι) (g : P ι) :
(f.prod g) = f.prod g
@[simp]
theorem alternating_map.pi_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_7} {ι' : Type u_3} {N : ι' Type u_4} [Π (i : ι'), add_comm_monoid (N i)] [Π (i : ι'), (N i)] (f : Π (i : ι'), (N i) ι) (ᾰ : Π (i : ι), (λ (i : ι), M) i) (i : ι') :
i = (f i)
def alternating_map.pi {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_7} {ι' : Type u_3} {N : ι' Type u_4} [Π (i : ι'), add_comm_monoid (N i)] [Π (i : ι'), (N i)] (f : Π (i : ι'), (N i) ι) :
(Π (i : ι'), N i) ι

Combine a family of alternating maps with the same domain and codomains N i into an alternating map taking values in the space of functions Π i, N i.

Equations
@[simp]
theorem alternating_map.coe_pi {R : Type u_1} [semiring R] {M : Type u_2} [ M] {ι : Type u_7} {ι' : Type u_3} {N : ι' Type u_4} [Π (i : ι'), add_comm_monoid (N i)] [Π (i : ι'), (N i)] (f : Π (i : ι'), (N i) ι) :
= multilinear_map.pi (λ (a : ι'), (f a))
@[simp]
theorem alternating_map.smul_right_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (f : M₁ R ι) (z : M₂) (ᾰ : Π (i : ι), (λ (i : ι), M₁) i) :
(f.smul_right z) = f ᾰ z
def alternating_map.smul_right {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (f : M₁ R ι) (z : M₂) :
M₁ M₂ ι

Given an alternating R-multilinear map f taking values in R, f.smul_right z is the map sending m to f m • z.

Equations
@[simp]
theorem alternating_map.coe_smul_right {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (f : M₁ R ι) (z : M₂) :
@[protected, instance]
def alternating_map.has_add {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
Equations
@[simp]
theorem alternating_map.add_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f f' : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f f' : N ι) :
(f + f') = f + f'
@[protected, instance]
def alternating_map.has_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
has_zero M N ι)
Equations
@[simp]
theorem alternating_map.zero_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (v : ι M) :
0 v = 0
@[norm_cast]
theorem alternating_map.coe_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
0 = 0
@[protected, instance]
def alternating_map.inhabited {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
inhabited M N ι)
Equations
@[protected, instance]
def alternating_map.add_comm_monoid {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} :
Equations
@[protected, instance]
def alternating_map.has_neg {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} :
has_neg M N' ι)
Equations
@[simp]
theorem alternating_map.neg_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g : N' ι) (m : ι M) :
(-g) m = -g m
@[norm_cast]
theorem alternating_map.coe_neg {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g : N' ι) :
@[protected, instance]
def alternating_map.has_sub {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} :
has_sub M N' ι)
Equations
@[simp]
theorem alternating_map.sub_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g g₂ : 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} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g g₂ : N' ι) :
(g - g₂) = g - g₂
@[protected, instance]
def alternating_map.add_comm_group {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} :
Equations
@[protected, instance]
def alternating_map.distrib_mul_action {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {S : Type u_10} [monoid S] [ N] [ N] :
M N ι)
Equations
@[protected, instance]
def alternating_map.module {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {S : Type u_10} [semiring S] [ N] [ N] :
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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {S : Type u_10} [semiring S] [ N] [ N]  :
M N ι)
@[simp]
theorem alternating_map.of_subsingleton_apply (R : Type u_1) [semiring R] (M : Type u_2) [ M] {ι : Type u_7} [subsingleton ι] (i : ι) (f : Π (x : ι), (λ (i : ι), (λ (i : ι), M) i) x) :
f =
def alternating_map.of_subsingleton (R : Type u_1) [semiring R] (M : Type u_2) [ M] {ι : Type u_7} [subsingleton ι] (i : ι) :
M ι

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

Equations
def alternating_map.const_of_is_empty (R : Type u_1) [semiring R] (M : Type u_2) [ M] {N : Type u_3} [ N] (ι : Type u_7) [is_empty ι] (m : N) :
N ι

The constant map is alternating when ι is empty.

Equations
@[simp]
theorem alternating_map.const_of_is_empty_apply (R : Type u_1) [semiring R] (M : Type u_2) [ M] {N : Type u_3} [ N] (ι : Type u_7) [is_empty ι] (m : N) :
m) = function.const (Π (i : ι), (λ (i : ι), M) i) m
@[simp]
theorem alternating_map.cod_restrict_apply_coe {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (p : N) (h : (v : ι M), f v p) (v : Π (i : ι), (λ (i : ι), M) i) :
((f.cod_restrict p h) v) = f v
def alternating_map.cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (p : N) (h : (v : ι M), f v p) :
p ι

Restrict the codomain of an alternating map to a submodule.

Equations

### Composition with linear maps #

def linear_map.comp_alternating_map {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {N₂ : Type u_10} [add_comm_monoid N₂] [ N₂] (g : N →ₗ[R] N₂) :
N ι →+ 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {N₂ : Type u_10} [add_comm_monoid N₂] [ N₂] (g : N →ₗ[R] N₂) (f : N ι) :
@[simp]
theorem linear_map.comp_alternating_map_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {N₂ : Type u_10} [add_comm_monoid N₂] [ N₂] (g : N →ₗ[R] N₂) (f : N ι) (m : ι M) :
theorem linear_map.smul_right_eq_comp {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (f : M₁ R ι) (z : M₂) :
@[simp]
theorem linear_map.subtype_comp_alternating_map_cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (p : N) (h : (v : ι M), f v p) :
@[simp]
theorem linear_map.comp_alternating_map_cod_restrict {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {N₂ : Type u_10} [add_comm_monoid N₂] [ N₂] (g : N →ₗ[R] N₂) (f : N ι) (p : N₂) (h : (c : N), g c p) :
def alternating_map.comp_linear_map {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (f : N ι) (g : M₂ →ₗ[R] M) :
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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (f : N ι) (g : M₂ →ₗ[R] M) :
@[simp]
theorem alternating_map.comp_linear_map_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (f : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] {M₃ : Type u_11} [add_comm_monoid M₃] [ M₃] (f : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (g : M₂ →ₗ[R] M) :
= 0
@[simp]
theorem alternating_map.add_comp_linear_map {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (f₁ f₂ : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] [nonempty ι] (f : N ι) :
= 0
@[simp]
theorem alternating_map.comp_linear_map_id {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (f : M₂ →ₗ[R] M) (hf : function.surjective f) :
function.injective (λ (g : N ι), g.comp_linear_map 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (f : M₂ →ₗ[R] M) (hf : function.surjective f) (g₁ g₂ : 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} [ M] (N : Type u_3) [ N] (ι : Type u_7) {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (S : Type u_12) [semiring S] [ N] [ N] (e : M ≃ₗ[R] M₂) :
N ι ≃ₗ[S] M₂ N ι

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} [ M] (N : Type u_3) [ N] (ι : Type u_7) {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (S : Type u_12) [semiring S] [ N] [ N] (e : M ≃ₗ[R] M₂) (f : N ι) :
@[simp]
theorem alternating_map.dom_lcongr_refl (R : Type u_1) [semiring R] {M : Type u_2} [ M] (N : Type u_3) [ N] (ι : Type u_7) (S : Type u_12) [semiring S] [ N] [ N] :
S M) = M N ι)
@[simp]
theorem alternating_map.dom_lcongr_symm (R : Type u_1) [semiring R] {M : Type u_2} [ M] (N : Type u_3) [ N] (ι : Type u_7) {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (S : Type u_12) [semiring S] [ N] [ N] (e : M ≃ₗ[R] M₂) :
S e).symm = S e.symm
theorem alternating_map.dom_lcongr_trans (R : Type u_1) [semiring R] {M : Type u_2} [ M] (N : Type u_3) [ N] (ι : Type u_7) {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] {M₃ : Type u_11} [add_comm_monoid M₃] [ M₃] (S : Type u_12) [semiring S] [ N] [ N] (e : M ≃ₗ[R] M₂) (f : M₂ ≃ₗ[R] M₃) :
S e).trans S f) = S (e.trans f)
@[simp]
theorem alternating_map.comp_linear_equiv_eq_zero_iff {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {M₂ : Type u_10} [add_comm_monoid M₂] [ M₂] (f : N ι) (g : M₂ ≃ₗ[R] M) :
= 0 f = 0

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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) {α : Type u_4} [decidable_eq ι] (t : finset α) (i : ι) (g : α M) (m : ι M) :
f i (t.sum (λ (a : α), g a))) = t.sum (λ (a : α), f 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} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (v : ι M) [decidable_eq ι] {i j : ι} (hij : i j) :
f i (v j)) = 0
theorem alternating_map.map_update_update {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (v : ι M) [decidable_eq ι] {i j : ι} (hij : i j) (m : M) :
f (function.update i m) j m) = 0
theorem alternating_map.map_swap_add {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (v : ι M) [decidable_eq ι] {i j : ι} (hij : i j) :
f (v j)) + f v = 0
theorem alternating_map.map_add_swap {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) (v : ι M) [decidable_eq ι] {i j : ι} (hij : i j) :
f v + f (v j)) = 0
theorem alternating_map.map_swap {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g : N' ι) (v : ι M) [decidable_eq ι] {i j : ι} (hij : i j) :
g (v j)) = -g v
theorem alternating_map.map_perm {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g : N' ι) [decidable_eq ι] [fintype ι] (v : ι M) (σ : equiv.perm ι) :
g (v σ) = g v
theorem alternating_map.map_congr_perm {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g : N' ι) (v : ι M) [decidable_eq ι] [fintype ι] (σ : equiv.perm ι) :
g v = g (v σ)
@[simp]
theorem alternating_map.dom_dom_congr_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : N ι) (v : Π (i : ι'), (λ (i : ι'), M) i) :
= f (v σ)
def alternating_map.dom_dom_congr {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : N ι) :
N ι'

Transfer the arguments to a map along an equivalence between argument indices.

This is the alternating version of multilinear_map.dom_dom_congr.

Equations
@[simp]
theorem alternating_map.dom_dom_congr_refl {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (f : N ι) :
theorem alternating_map.dom_dom_congr_trans {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} {ι'' : Type u_9} (σ₁ : ι ι') (σ₂ : ι' ι'') (f : N ι) :
@[simp]
theorem alternating_map.dom_dom_congr_zero {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') :
@[simp]
theorem alternating_map.dom_dom_congr_add {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f g : N ι) :
@[simp]
theorem alternating_map.dom_dom_congr_smul {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} {S : Type u_4} [monoid S] [ N] [ N] (σ : ι ι') (c : S) (f : N ι) :
(c f) =
@[simp]
theorem alternating_map.dom_dom_congr_equiv_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : N ι) :
def alternating_map.dom_dom_congr_equiv {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') :
N ι ≃+ N ι'

alternating_map.dom_dom_congr as an equivalence.

This is declared separately because it does not work with dot notation.

Equations
@[simp]
theorem alternating_map.dom_dom_congr_equiv_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : N ι') :
def alternating_map.dom_dom_lcongr {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [semiring S] [ N] [ N] (σ : ι ι') :
N ι ≃ₗ[S] N ι'

alternating_map.dom_dom_congr as a linear equivalence.

Equations
@[simp]
theorem alternating_map.dom_dom_lcongr_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [semiring S] [ N] [ N] (σ : ι ι') (f : N ι) :
@[simp]
theorem alternating_map.dom_dom_lcongr_symm_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [semiring S] [ N] [ N] (σ : ι ι') (f : N ι') :
@[simp]
theorem alternating_map.dom_dom_lcongr_refl {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} (S : Type u_12) [semiring S] [ N] [ N] :
= M N ι)
@[simp]
theorem alternating_map.dom_dom_lcongr_to_add_equiv {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [semiring S] [ N] [ N] (σ : ι ι') :
@[simp]
theorem alternating_map.dom_dom_congr_eq_iff {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f g : N ι) :

The results of applying dom_dom_congr to two maps are equal if and only if those maps are.

@[simp]
theorem alternating_map.dom_dom_congr_eq_zero_iff {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : N ι) :
f = 0
theorem alternating_map.dom_dom_congr_perm {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} (g : N' ι) [fintype ι] [decidable_eq ι] (σ : equiv.perm ι) :
@[norm_cast]
theorem alternating_map.coe_dom_dom_congr {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {ι : Type u_7} {ι' : Type u_8} (f : N ι) (σ : ι ι') :
theorem alternating_map.map_linear_dependent {ι : Type u_7} {K : Type u_1} [ring K] {M : Type u_2} [ M] {N : Type u_3} [ N] (f : N ι) (v : ι M) (h : ¬) :
f v = 0

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

theorem alternating_map.map_vec_cons_add {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {n : } (f : N (fin n.succ)) (m : fin n M) (x y : M) :
f (matrix.vec_cons (x + y) m) = f m) + f m)

A version of multilinear_map.cons_add for alternating_map.

theorem alternating_map.map_vec_cons_smul {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N : Type u_3} [ N] {n : } (f : N (fin n.succ)) (m : fin n M) (c : R) (x : M) :
f (matrix.vec_cons (c x) m) = c f m)

A version of multilinear_map.cons_smul for alternating_map.

def multilinear_map.alternatization {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} [fintype ι] [decidable_eq ι] :
(λ (i : ι), M) N' →+ 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} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} [fintype ι] [decidable_eq ι] (m : (λ (i : ι), M) N') :
= (finset.univ.sum (λ (σ : ,
theorem multilinear_map.alternatization_coe {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} [fintype ι] [decidable_eq ι] (m : (λ (i : ι), M) N') :
= finset.univ.sum (λ (σ : ,
theorem multilinear_map.alternatization_apply {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} [fintype ι] [decidable_eq ι] (m : (λ (i : ι), M) N') (v : ι M) :
= finset.univ.sum (λ (σ : ,
theorem alternating_map.coe_alternatization {R : Type u_1} [semiring R] {M : Type u_2} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} [decidable_eq ι] [fintype ι] (a : 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} [ M] {N' : Type u_6} [add_comm_group N'] [ N'] {ι : Type u_7} {N'₂ : Type u_10} [add_comm_group N'₂] [ N'₂] [decidable_eq ι] [fintype ι] (g : N' →ₗ[R] N'₂) (f : (λ (_x : ι), M) N') :

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

@[reducible]
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_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : Mᵢ N₁ ιa) (b : Mᵢ N₂ ιb) (σ : ιb) :
(λ (_x : ιa ιb), Mᵢ) N₁ N₂)

summand used in alternating_map.dom_coprod

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

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_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : Mᵢ N₁ ιa) (b : Mᵢ N₂ ιb) (σ : ιb) {v : ιa ιb Mᵢ} {i j : ιa ιb} (hv : v i = v j) (hij : i j) :
j σ = σ v = 0

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_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : Mᵢ N₁ ιa) (b : Mᵢ N₂ ιb) :
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 linear_map.mul'.

Equations
@[simp]
theorem alternating_map.dom_coprod_apply {ιa : Type u_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : Mᵢ N₁ ιa) (b : Mᵢ N₂ ιb) (v : Π (i : ιa ιb), (λ (i : ιa ιb), Mᵢ) i) :
(a.dom_coprod b) v = (finset.univ.sum (λ (σ : ιb), v
theorem alternating_map.dom_coprod_coe {ιa : Type u_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : Mᵢ N₁ ιa) (b : Mᵢ N₂ ιb) :
(a.dom_coprod b) = finset.univ.sum (λ (σ : ιb),
def alternating_map.dom_coprod' {ιa : Type u_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] :
Mᵢ N₁ ιa) Mᵢ N₂ ιb) →ₗ[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_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : Mᵢ N₁ ιa) (b : Mᵢ N₂ ιb) :
theorem multilinear_map.dom_coprod_alternization_coe {ιa : Type u_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : (λ (_x : ιa), Mᵢ) N₁) (b : (λ (_x : ιb), Mᵢ) N₂) :
= finset.univ.sum (λ (σa : equiv.perm ιa), finset.univ.sum (λ (σb : equiv.perm ιb),

A helper lemma for multilinear_map.dom_coprod_alternization.

theorem multilinear_map.dom_coprod_alternization {ιa : Type u_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : (λ (_x : ιa), Mᵢ) N₁) (b : (λ (_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_10} {ιb : Type u_11} [fintype ιa] [fintype ιb] {R' : Type u_12} {Mᵢ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} [comm_semiring R'] [add_comm_group N₁] [module R' N₁] [add_comm_group N₂] [module R' N₂] [add_comm_monoid Mᵢ] [module R' Mᵢ] [decidable_eq ιa] [decidable_eq ιb] (a : Mᵢ N₁ ιa) (b : 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_7} {ι₁ : Type u_10} [finite ι] {R' : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13} [comm_semiring R'] [add_comm_monoid N₁] [add_comm_monoid N₂] [module R' N₁] [module R' N₂] {f g : N₁ N₂ ι} (e : basis ι₁ R' N₁) (h : (v : ι ι₁), f (λ (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.

### Currying #

def alternating_map.curry_left {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } (f : M'' N'' (fin n.succ)) :
M'' →ₗ[R'] M'' N'' (fin n)

Given an alternating map f in n+1 variables, split the first variable to obtain a linear map into alternating maps in n variables, given by x ↦ (m ↦ f (matrix.vec_cons x m)). It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.

This is multilinear_map.curry_left for alternating_map. See also alternating_map.curry_left_linear_map.

Equations
@[simp]
theorem alternating_map.curry_left_apply_apply {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } (f : M'' N'' (fin n.succ)) (m : M'') (v : Π (i : fin n), (λ (i : fin n), M'') i) :
((f.curry_left) m) v = f v)
@[simp]
theorem alternating_map.curry_left_zero {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } :
@[simp]
theorem alternating_map.curry_left_add {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } (f g : M'' N'' (fin n.succ)) :
(f + g).curry_left =
@[simp]
theorem alternating_map.curry_left_smul {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } (r : R') (f : M'' N'' (fin n.succ)) :
@[simp]
theorem alternating_map.curry_left_linear_map_apply {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } (f : M'' N'' (fin n.succ)) :
def alternating_map.curry_left_linear_map {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } :
M'' N'' (fin n.succ) →ₗ[R'] M'' →ₗ[R'] M'' N'' (fin n)

alternating_map.curry_left as a linear_map. This is a separate definition as dot notation does not work for this version.

Equations
@[simp]
theorem alternating_map.curry_left_same {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] {n : } (f : M'' N'' (fin n.succ.succ)) (m : M'') :

Currying with the same element twice gives the zero map.

@[simp]
theorem alternating_map.curry_left_comp_alternating_map {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} {N₂'' : Type u_14} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [add_comm_monoid N₂''] [module R' M''] [module R' N''] [module R' N₂''] {n : } (g : N'' →ₗ[R'] N₂'') (f : M'' N'' (fin n.succ)) (m : M'') :
@[simp]
theorem alternating_map.curry_left_comp_linear_map {R' : Type u_10} {M'' : Type u_11} {M₂'' : Type u_12} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid M₂''] [add_comm_monoid N''] [module R' M''] [module R' M₂''] [module R' N''] {n : } (g : M₂'' →ₗ[R'] M'') (f : M'' N'' (fin n.succ)) (m : M₂'') :
@[simp]
theorem alternating_map.const_linear_equiv_of_is_empty_symm_apply {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] [is_empty ι] (f : M'' N'' ι) :
def alternating_map.const_linear_equiv_of_is_empty {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] [is_empty ι] :
N'' ≃ₗ[R'] M'' N'' ι

The space of constant maps is equivalent to the space of maps that are alternating with respect to an empty family.

Equations
@[simp]
theorem alternating_map.const_linear_equiv_of_is_empty_apply {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [comm_semiring R'] [add_comm_monoid M''] [add_comm_monoid N''] [module R' M''] [module R' N''] [is_empty ι] (m : N'') :