# Documentation

Mathlib.LinearAlgebra.Alternating

# Alternating Maps #

We construct the bundled function AlternatingMap, which extends MultilinearMap with all the arguments of the same type.

## Main definitions #

• AlternatingMap 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 AddCommMonoid, AddCommGroup, and Module structure over AlternatingMaps that matches the definitions over MultilinearMaps.
• MultilinearMap.domDomCongr, for permutating the elements within a family.
• MultilinearMap.alternatization, which makes an alternating map out of a non-alternating one.
• AlternatingMap.domCoprod, which behaves as a product between two alternating maps.
• AlternatingMap.curryLeft, for binding the leftmost argument of an alternating map indexed by Fin n.succ.

## Implementation notes #

AlternatingMap 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 Neg N.

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

• AlternatingMap.coe_add
• AlternatingMap.coe_zero
• AlternatingMap.coe_sub
• AlternatingMap.coe_neg
• AlternatingMap.coe_smul
structure AlternatingMap (R : Type u_1) [] (M : Type u_2) [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_7) extends :
Type (max (max u_2 u_3) u_7)

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

Instances For

Basic coercion simp lemmas, largely copied from RingHom and MultilinearMap

instance AlternatingMap.funLike {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
FunLike (AlternatingMap R M N ι) (ιM) fun x => N
instance AlternatingMap.coeFun {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
CoeFun (AlternatingMap R M N ι) fun x => (ιM) → N
@[simp]
theorem AlternatingMap.toFun_eq_coe {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) :
f.toFun = f
@[simp]
theorem AlternatingMap.coe_mk {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : MultilinearMap R (fun x => M) N) (h : ∀ (v : ιM) (i j : ι), v i = v ji j) :
{ toMultilinearMap := f, map_eq_zero_of_eq' := h } = f
theorem AlternatingMap.congr_fun {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {f : AlternatingMap R M N ι} {g : AlternatingMap R M N ι} (h : f = g) (x : ιM) :
f x = g x
theorem AlternatingMap.congr_arg {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) {x : ιM} {y : ιM} (h : x = y) :
f x = f y
theorem AlternatingMap.coe_injective {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
Function.Injective FunLike.coe
theorem AlternatingMap.coe_inj {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {f : AlternatingMap R M N ι} {g : AlternatingMap R M N ι} :
f = g f = g
theorem AlternatingMap.ext {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {f : AlternatingMap R M N ι} {f' : AlternatingMap R M N ι} (H : ∀ (x : ιM), f x = f' x) :
f = f'
theorem AlternatingMap.ext_iff {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {f : AlternatingMap R M N ι} {g : AlternatingMap R M N ι} :
f = g ∀ (x : ιM), f x = g x
instance AlternatingMap.coe {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
Coe (AlternatingMap R M N ι) (MultilinearMap R (fun x => M) N)
@[simp]
theorem AlternatingMap.coe_multilinearMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) :
f = f
theorem AlternatingMap.coe_multilinearMap_injective {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
Function.Injective AlternatingMap.toMultilinearMap
theorem AlternatingMap.coe_multilinearMap_mk {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : (ιM) → N) (h₁ : ∀ [inst : ] (m : ιM) (i : ι) (x y : M), f (Function.update m i (x + y)) = f () + f ()) (h₂ : ∀ [inst : ] (m : ιM) (i : ι) (c : R) (x : M), f (Function.update m i (c x)) = c f ()) (h₃ : ∀ (v : ιM) (i j : ι), v i = v ji jMultilinearMap.toFun { toFun := f, map_add' := fun [inst : ] => h₁ fun a b => inst a b, map_smul' := fun [inst : ] => h₂ fun a b => inst a b } v = 0) :
{ toMultilinearMap := { toFun := f, map_add' := fun [inst : ] => h₁ fun a b => inst a b, map_smul' := fun [inst : ] => h₂ fun a b => inst a b }, map_eq_zero_of_eq' := h₃ } = { toFun := f, map_add' := h₁, map_smul' := h₂ }

### Simp-normal forms of the structure fields #

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

@[simp]
theorem AlternatingMap.map_add {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) [] (i : ι) (x : M) (y : M) :
f (Function.update v i (x + y)) = f () + f ()
@[simp]
theorem AlternatingMap.map_sub {R : Type u_1} [] {M' : Type u_5} [] [Module R M'] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g' : AlternatingMap R M' N' ι) (v' : ιM') [] (i : ι) (x : M') (y : M') :
g' (Function.update v' i (x - y)) = g' (Function.update v' i x) - g' (Function.update v' i y)
@[simp]
theorem AlternatingMap.map_neg {R : Type u_1} [] {M' : Type u_5} [] [Module R M'] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g' : AlternatingMap R M' N' ι) (v' : ιM') [] (i : ι) (x : M') :
g' (Function.update v' i (-x)) = -g' (Function.update v' i x)
@[simp]
theorem AlternatingMap.map_smul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) [] (i : ι) (r : R) (x : M) :
f (Function.update v i (r x)) = r f ()
@[simp]
theorem AlternatingMap.map_eq_zero_of_eq {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) {i : ι} {j : ι} (h : v i = v j) (hij : i j) :
f v = 0
theorem AlternatingMap.map_coord_zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) {m : ιM} (i : ι) (h : m i = 0) :
f m = 0
@[simp]
theorem AlternatingMap.map_update_zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) [] (m : ιM) (i : ι) :
f () = 0
@[simp]
theorem AlternatingMap.map_zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) [] :
f 0 = 0
theorem AlternatingMap.map_eq_zero_of_not_injective {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) (hv : ) :
f v = 0

### Algebraic structure inherited from MultilinearMap#

AlternatingMap carries the same AddCommMonoid, AddCommGroup, and Module structure as MultilinearMap

instance AlternatingMap.smul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {S : Type u_10} [] [] [] :
SMul S (AlternatingMap R M N ι)
@[simp]
theorem AlternatingMap.smul_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) {S : Type u_10} [] [] [] (c : S) (m : ιM) :
↑(c f) m = c f m
theorem AlternatingMap.coe_smul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) {S : Type u_10} [] [] [] (c : S) :
↑(c f) = c f
theorem AlternatingMap.coeFn_smul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {S : Type u_10} [] [] [] (c : S) (f : AlternatingMap R M N ι) :
↑(c f) = c f
instance AlternatingMap.isCentralScalar {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {S : Type u_10} [] [] [] [] [] :
@[simp]
theorem AlternatingMap.prod_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {P : Type u_4} [] [Module R P] {ι : Type u_7} (f : AlternatingMap R M N ι) (g : AlternatingMap R M P ι) (m : (i : ι) → (fun x => M) i) :
↑() m = (f m, g m)
def AlternatingMap.prod {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {P : Type u_4} [] [Module R P] {ι : Type u_7} (f : AlternatingMap R M N ι) (g : AlternatingMap R M P ι) :
AlternatingMap R M (N × P) ι

The cartesian product of two alternating maps, as an alternating map.

Instances For
@[simp]
theorem AlternatingMap.coe_prod {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {P : Type u_4} [] [Module R P] {ι : Type u_7} (f : AlternatingMap R M N ι) (g : AlternatingMap R M P ι) :
↑() =
@[simp]
theorem AlternatingMap.pi_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_7} {ι' : Type u_10} {N : ι'Type u_11} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → AlternatingMap R M (N i) ι) (m : (i : ι) → (fun x => M) i) (i : ι') :
↑() m i = ↑(f i) m
def AlternatingMap.pi {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_7} {ι' : Type u_10} {N : ι'Type u_11} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → AlternatingMap R M (N i) ι) :
AlternatingMap R M ((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.

Instances For
@[simp]
theorem AlternatingMap.coe_pi {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_7} {ι' : Type u_10} {N : ι'Type u_11} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → AlternatingMap R M (N i) ι) :
↑() = MultilinearMap.pi fun a => ↑(f a)
@[simp]
theorem AlternatingMap.smulRight_apply {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [] [] [] [Module R M₁] [Module R M₂] (f : AlternatingMap R M₁ R ι) (z : M₂) :
∀ (a : (i : ι) → (fun x => M₁) i), ↑() a = f a z
def AlternatingMap.smulRight {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [] [] [] [Module R M₁] [Module R M₂] (f : AlternatingMap R M₁ R ι) (z : M₂) :
AlternatingMap R 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.

Instances For
@[simp]
theorem AlternatingMap.coe_smulRight {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [] [] [] [Module R M₁] [Module R M₂] (f : AlternatingMap R M₁ R ι) (z : M₂) :
↑() =
instance AlternatingMap.add {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
Add (AlternatingMap R M N ι)
@[simp]
theorem AlternatingMap.add_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (f' : AlternatingMap R M N ι) (v : ιM) :
↑(f + f') v = f v + f' v
theorem AlternatingMap.coe_add {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (f' : AlternatingMap R M N ι) :
↑(f + f') = f + f'
instance AlternatingMap.zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
Zero (AlternatingMap R M N ι)
@[simp]
theorem AlternatingMap.zero_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (v : ιM) :
0 v = 0
theorem AlternatingMap.coe_zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
0 = 0
@[simp]
theorem AlternatingMap.mk_zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
{ toMultilinearMap := 0, map_eq_zero_of_eq' := (_ : ∀ (v : ιM) (i j : ι), v i = v ji jMultilinearMap.toFun (0) v = 0) } = 0
instance AlternatingMap.inhabited {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
instance AlternatingMap.addCommMonoid {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} :
instance AlternatingMap.neg {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} :
Neg (AlternatingMap R M N' ι)
@[simp]
theorem AlternatingMap.neg_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) (m : ιM) :
↑(-g) m = -g m
theorem AlternatingMap.coe_neg {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) :
↑(-g) = -g
instance AlternatingMap.sub {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} :
Sub (AlternatingMap R M N' ι)
@[simp]
theorem AlternatingMap.sub_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) (g₂ : AlternatingMap R M N' ι) (m : ιM) :
↑(g - g₂) m = g m - g₂ m
theorem AlternatingMap.coe_sub {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) (g₂ : AlternatingMap R M N' ι) :
↑(g - g₂) = g - g₂
instance AlternatingMap.addCommGroup {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} :
instance AlternatingMap.distribMulAction {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {S : Type u_10} [] [] [] :
instance AlternatingMap.module {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {S : Type u_10} [] [Module S N] [] :
Module S (AlternatingMap 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.

instance AlternatingMap.noZeroSMulDivisors {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {S : Type u_10} [] [Module S N] [] [] :
@[simp]
theorem AlternatingMap.ofSubsingleton_apply (R : Type u_1) [] (M : Type u_2) [] [Module R M] {ι : Type u_7} [] (i : ι) (f : ιM) :
↑() f =
def AlternatingMap.ofSubsingleton (R : Type u_1) [] (M : Type u_2) [] [Module R M] {ι : Type u_7} [] (i : ι) :

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

Instances For
@[simp]
theorem AlternatingMap.constOfIsEmpty_apply (R : Type u_1) [] (M : Type u_2) [] [Module R M] {N : Type u_3} [] [Module R N] (ι : Type u_7) [] (m : N) :
↑() = Function.const (ιM) m
def AlternatingMap.constOfIsEmpty (R : Type u_1) [] (M : Type u_2) [] [Module R M] {N : Type u_3} [] [Module R N] (ι : Type u_7) [] (m : N) :

The constant map is alternating when ι is empty.

Instances For
@[simp]
theorem AlternatingMap.codRestrict_apply_coe {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (p : ) (h : ∀ (v : ιM), f v p) (v : ιM) :
↑(↑() v) = f v
def AlternatingMap.codRestrict {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (p : ) (h : ∀ (v : ιM), f v p) :
AlternatingMap R M { x // x p } ι

Restrict the codomain of an alternating map to a submodule.

Instances For

### Composition with linear maps #

def LinearMap.compAlternatingMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {N₂ : Type u_10} [] [Module R N₂] (g : N →ₗ[R] N₂) :
AlternatingMap R M N ι →+ AlternatingMap R M N₂ ι

Composing an alternating map with a linear map on the left gives again an alternating map.

Instances For
@[simp]
theorem LinearMap.coe_compAlternatingMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {N₂ : Type u_10} [] [Module R N₂] (g : N →ₗ[R] N₂) (f : AlternatingMap R M N ι) :
↑() = g f
@[simp]
theorem LinearMap.compAlternatingMap_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {N₂ : Type u_10} [] [Module R N₂] (g : N →ₗ[R] N₂) (f : AlternatingMap R M N ι) (m : ιM) :
↑() m = g (f m)
theorem LinearMap.smulRight_eq_comp {R : Type u_11} {M₁ : Type u_12} {M₂ : Type u_13} {ι : Type u_14} [] [] [] [Module R M₁] [Module R M₂] (f : AlternatingMap R M₁ R ι) (z : M₂) :
@[simp]
theorem LinearMap.subtype_compAlternatingMap_codRestrict {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (p : ) (h : ∀ (v : ιM), f v p) :
= f
@[simp]
theorem LinearMap.compAlternatingMap_codRestrict {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {N₂ : Type u_10} [] [Module R N₂] (g : N →ₗ[R] N₂) (f : AlternatingMap R M N ι) (p : Submodule R N₂) (h : ∀ (c : N), g c p) :
↑() f = AlternatingMap.codRestrict () p fun v => h (f v)
def AlternatingMap.compLinearMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (f : AlternatingMap R M N ι) (g : M₂ →ₗ[R] M) :
AlternatingMap R M₂ N ι

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

Instances For
theorem AlternatingMap.coe_compLinearMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (f : AlternatingMap R M N ι) (g : M₂ →ₗ[R] M) :
↑() = f (fun x x_1 => x x_1) g
@[simp]
theorem AlternatingMap.compLinearMap_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (f : AlternatingMap R M N ι) (g : M₂ →ₗ[R] M) (v : ιM₂) :
↑() v = f fun i => g (v i)
theorem AlternatingMap.compLinearMap_assoc {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] {M₃ : Type u_11} [] [Module R M₃] (f : AlternatingMap 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 AlternatingMap.zero_compLinearMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (g : M₂ →ₗ[R] M) :
@[simp]
theorem AlternatingMap.add_compLinearMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (f₁ : AlternatingMap R M N ι) (f₂ : AlternatingMap R M N ι) (g : M₂ →ₗ[R] M) :
@[simp]
theorem AlternatingMap.compLinearMap_zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] [] (f : AlternatingMap R M N ι) :
@[simp]
theorem AlternatingMap.compLinearMap_id {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) :

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

theorem AlternatingMap.compLinearMap_injective {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (f : M₂ →ₗ[R] M) (hf : ) :

Composing with a surjective linear map is injective.

theorem AlternatingMap.compLinearMap_inj {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (f : M₂ →ₗ[R] M) (hf : ) (g₁ : AlternatingMap R M N ι) (g₂ : AlternatingMap R M N ι) :
g₁ = g₂
@[simp]
theorem AlternatingMap.domLCongr_apply (R : Type u_1) [] {M : Type u_2} [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [] [Module R M₂] (S : Type u_12) [] [Module S N] [] (e : M ≃ₗ[R] M₂) (f : AlternatingMap R M N ι) :
↑() f =
def AlternatingMap.domLCongr (R : Type u_1) [] {M : Type u_2} [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [] [Module R M₂] (S : Type u_12) [] [Module S N] [] (e : M ≃ₗ[R] M₂) :
AlternatingMap R M N ι ≃ₗ[S] AlternatingMap R M₂ N ι

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

Instances For
@[simp]
theorem AlternatingMap.domLCongr_refl (R : Type u_1) [] {M : Type u_2} [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_7) (S : Type u_12) [] [Module S N] [] :
@[simp]
theorem AlternatingMap.domLCongr_symm (R : Type u_1) [] {M : Type u_2} [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [] [Module R M₂] (S : Type u_12) [] [Module S N] [] (e : M ≃ₗ[R] M₂) :
theorem AlternatingMap.domLCongr_trans (R : Type u_1) [] {M : Type u_2} [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [] [Module R M₂] {M₃ : Type u_11} [] [Module R M₃] (S : Type u_12) [] [Module S N] [] (e : M ≃ₗ[R] M₂) (f : M₂ ≃ₗ[R] M₃) :
@[simp]
theorem AlternatingMap.compLinearEquiv_eq_zero_iff {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [] [Module R M₂] (f : AlternatingMap R M N ι) (g : M₂ ≃ₗ[R] M) :
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 MultilinearMap#

theorem AlternatingMap.map_update_sum {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) {α : Type u_12} [] (t : ) (i : ι) (g : αM) (m : ιM) :
f (Function.update m i (Finset.sum t fun a => g a)) = Finset.sum t fun a => f (Function.update m i (g a))

### Theorems specific to alternating maps #

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

theorem AlternatingMap.map_update_self {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) [] {i : ι} {j : ι} (hij : i j) :
f (Function.update v i (v j)) = 0
theorem AlternatingMap.map_update_update {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) [] {i : ι} {j : ι} (hij : i j) (m : M) :
f (Function.update () j m) = 0
theorem AlternatingMap.map_swap_add {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) [] {i : ι} {j : ι} (hij : i j) :
f (v ↑()) + f v = 0
theorem AlternatingMap.map_add_swap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) (v : ιM) [] {i : ι} {j : ι} (hij : i j) :
f v + f (v ↑()) = 0
theorem AlternatingMap.map_swap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) (v : ιM) [] {i : ι} {j : ι} (hij : i j) :
g (v ↑()) = -g v
theorem AlternatingMap.map_perm {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) [] [] (v : ιM) (σ : ) :
g (v σ) = Equiv.Perm.sign σ g v
theorem AlternatingMap.map_congr_perm {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) (v : ιM) [] [] (σ : ) :
g v = Equiv.Perm.sign σ g (v σ)
@[simp]
theorem AlternatingMap.domDomCongr_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : AlternatingMap R M N ι) (v : ι'M) :
↑() v = f (v σ)
def AlternatingMap.domDomCongr {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : AlternatingMap R M N ι) :
AlternatingMap R M N ι'

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

This is the alternating version of MultilinearMap.domDomCongr.

Instances For
@[simp]
theorem AlternatingMap.domDomCongr_refl {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (f : AlternatingMap R M N ι) :
theorem AlternatingMap.domDomCongr_trans {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} {ι'' : Type u_9} (σ₁ : ι ι') (σ₂ : ι' ι'') (f : AlternatingMap R M N ι) :
AlternatingMap.domDomCongr (σ₁.trans σ₂) f =
@[simp]
theorem AlternatingMap.domDomCongr_zero {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') :
@[simp]
theorem AlternatingMap.domDomCongr_add {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : AlternatingMap R M N ι) (g : AlternatingMap R M N ι) :
@[simp]
theorem AlternatingMap.domDomCongr_smul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} {S : Type u_12} [] [] [] (σ : ι ι') (c : S) (f : AlternatingMap R M N ι) :
@[simp]
theorem AlternatingMap.domDomCongrEquiv_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : AlternatingMap R M N ι) :
@[simp]
theorem AlternatingMap.domDomCongrEquiv_symm_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : AlternatingMap R M N ι') :
def AlternatingMap.domDomCongrEquiv {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') :

AlternatingMap.domDomCongr as an equivalence.

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

Instances For
@[simp]
theorem AlternatingMap.domDomLcongr_symm_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [] [Module S N] [] (σ : ι ι') (f : AlternatingMap R M N ι') :
↑() f = AlternatingMap.domDomCongr σ.symm f
@[simp]
theorem AlternatingMap.domDomLcongr_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [] [Module S N] [] (σ : ι ι') (f : AlternatingMap R M N ι) :
def AlternatingMap.domDomLcongr {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [] [Module S N] [] (σ : ι ι') :

alternating_map.dom_dom_congr as a linear equivalence.

Instances For
@[simp]
theorem AlternatingMap.domDomLcongr_refl {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} (S : Type u_12) [] [Module S N] [] :
@[simp]
theorem AlternatingMap.domDomLcongr_toAddEquiv {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [] [Module S N] [] (σ : ι ι') :
@[simp]
theorem AlternatingMap.domDomCongr_eq_iff {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : AlternatingMap R M N ι) (g : AlternatingMap R M N ι) :
f = g

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

@[simp]
theorem AlternatingMap.domDomCongr_eq_zero_iff {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ι') (f : AlternatingMap R M N ι) :
f = 0
theorem AlternatingMap.domDomCongr_perm {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} (g : AlternatingMap R M N' ι) [] [] (σ : ) :
= Equiv.Perm.sign σ g
theorem AlternatingMap.coe_domDomCongr {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_7} {ι' : Type u_8} (f : AlternatingMap R M N ι) (σ : ι ι') :
theorem AlternatingMap.map_linearDependent {ι : Type u_7} {K : Type u_12} [Ring K] {M : Type u_13} [] [Module K M] {N : Type u_14} [] [Module K N] [] (f : AlternatingMap K M N ι) (v : ιM) (h : ) :
f v = 0

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

theorem AlternatingMap.map_vecCons_add {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {n : } (f : AlternatingMap R M N (Fin ())) (m : Fin nM) (x : M) (y : M) :
f (Matrix.vecCons (x + y) m) = f () + f ()

A version of MultilinearMap.cons_add for AlternatingMap.

theorem AlternatingMap.map_vecCons_smul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {n : } (f : AlternatingMap R M N (Fin ())) (m : Fin nM) (c : R) (x : M) :
f (Matrix.vecCons (c x) m) = c f ()

A version of MultilinearMap.cons_smul for AlternatingMap.

def MultilinearMap.alternatization {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} [] [] :
MultilinearMap R (fun x => M) N' →+ AlternatingMap R M N' ι

Produce an AlternatingMap out of a MultilinearMap, by summing over all argument permutations.

Instances For
theorem MultilinearMap.alternatization_def {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} [] [] (m : MultilinearMap R (fun x => M) N') :
↑(MultilinearMap.alternatization m) = ↑(Finset.sum Finset.univ fun σ => Equiv.Perm.sign σ )
theorem MultilinearMap.alternatization_coe {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} [] [] (m : MultilinearMap R (fun x => M) N') :
↑(MultilinearMap.alternatization m) = Finset.sum Finset.univ fun σ => Equiv.Perm.sign σ
theorem MultilinearMap.alternatization_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} [] [] (m : MultilinearMap R (fun x => M) N') (v : ιM) :
↑(MultilinearMap.alternatization m) v = Finset.sum Finset.univ fun σ => Equiv.Perm.sign σ ↑() v
theorem AlternatingMap.coe_alternatization {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} [] [] (a : AlternatingMap R M N' ι) :
MultilinearMap.alternatization a =

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

theorem LinearMap.compMultilinearMap_alternatization {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N' : Type u_6} [] [Module R N'] {ι : Type u_7} {N'₂ : Type u_10} [AddCommGroup N'₂] [Module R N'₂] [] [] (g : N' →ₗ[R] N'₂) (f : MultilinearMap R (fun x => M) N') :
MultilinearMap.alternatization () = ↑() (MultilinearMap.alternatization f)

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

@[inline, reducible]
abbrev Equiv.Perm.ModSumCongr (α : Type u_16) (β : Type u_17) :
Type (max u_16 u_17)

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

Instances For
theorem Equiv.Perm.ModSumCongr.swap_smul_involutive {α : Type u_16} {β : Type u_17} [DecidableEq (α β)] (i : α β) (j : α β) :
def AlternatingMap.domCoprod.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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) (σ : ) :
MultilinearMap R' (fun x => Mᵢ) (TensorProduct R' N₁ N₂)

summand used in AlternatingMap.domCoprod

Instances For
theorem AlternatingMap.domCoprod.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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) (σ : Equiv.Perm (ιa ιb)) :
= Equiv.Perm.sign σ
theorem AlternatingMap.domCoprod.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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) (σ : ) {v : ιa ιbMᵢ} {i : ιa ιb} {j : ιa ιb} (hv : v i = v j) (hij : i j) :
↑() v + ↑(AlternatingMap.domCoprod.summand a b ( σ)) v = 0

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

theorem AlternatingMap.domCoprod.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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) (σ : ) {v : ιa ιbMᵢ} {i : ιa ιb} {j : ιa ιb} (hv : v i = v j) (hij : i j) :
σ = σ↑() v = 0

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

@[simp]
theorem AlternatingMap.domCoprod_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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) (v : ιa ιbMᵢ) :
↑() v = ↑(Finset.sum Finset.univ fun σ => ) v
def AlternatingMap.domCoprod {ι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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) :
AlternatingMap R' Mᵢ (TensorProduct R' N₁ N₂) (ιa ιb)

Like MultilinearMap.domCoprod, but ensures the result is also alternating.

Note that this is usually defined (for instance, as used in Proposition 22.24 in [Gallier2011Notes]) 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 finSumFinEquiv and LinearMap.mul'.

Instances For
theorem AlternatingMap.domCoprod_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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) :
↑() = Finset.sum Finset.univ fun σ =>
def AlternatingMap.domCoprod' {ι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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] :
TensorProduct R' (AlternatingMap R' Mᵢ N₁ ιa) (AlternatingMap R' Mᵢ N₂ ιb) →ₗ[R'] AlternatingMap R' Mᵢ (TensorProduct R' N₁ N₂) (ιa ιb)

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

Instances For
@[simp]
theorem AlternatingMap.domCoprod'_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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) :
AlternatingMap.domCoprod' (a ⊗ₜ[R'] b) =
theorem MultilinearMap.domCoprod_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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : MultilinearMap R' (fun x => Mᵢ) N₁) (b : MultilinearMap R' (fun x => Mᵢ) N₂) :
MultilinearMap.domCoprod ↑(MultilinearMap.alternatization a) ↑(MultilinearMap.alternatization b) = Finset.sum Finset.univ fun σa => Finset.sum Finset.univ fun σb => Equiv.Perm.sign σa Equiv.Perm.sign σb

A helper lemma for MultilinearMap.domCoprod_alternization.

theorem MultilinearMap.domCoprod_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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : MultilinearMap R' (fun x => Mᵢ) N₁) (b : MultilinearMap R' (fun x => Mᵢ) N₂) :
MultilinearMap.alternatization () = AlternatingMap.domCoprod (MultilinearMap.alternatization a) (MultilinearMap.alternatization b)

Computing the MultilinearMap.alternatization of the MultilinearMap.domCoprod is the same as computing the AlternatingMap.domCoprod of the MultilinearMap.alternatizations.

theorem MultilinearMap.domCoprod_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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : AlternatingMap R' Mᵢ N₁ ιa) (b : AlternatingMap R' Mᵢ N₂ ιb) :
MultilinearMap.alternatization () = ()

Taking the MultilinearMap.alternatization of the MultilinearMap.domCoprod of two AlternatingMaps gives a scaled version of the AlternatingMap.coprod of those maps.

theorem Basis.ext_alternating {ι : Type u_7} {ι₁ : Type u_10} [] {R' : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13} [] [] [] [Module R' N₁] [Module R' N₂] {f : AlternatingMap R' N₁ N₂ ι} {g : AlternatingMap R' N₁ N₂ ι} (e : Basis ι₁ R' N₁) (h : ∀ (v : ιι₁), (f fun i => e (v i)) = g fun 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 #

@[simp]
theorem AlternatingMap.curryLeft_apply_apply {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } (f : AlternatingMap R' M'' N'' (Fin ())) (m : M'') (v : Fin nM'') :
↑(↑() m) v = f ()
def AlternatingMap.curryLeft {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } (f : AlternatingMap R' M'' N'' (Fin ())) :
M'' →ₗ[R'] AlternatingMap 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.vecCons 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 MultilinearMap.curryLeft for AlternatingMap. See also AlternatingMap.curryLeftLinearMap.

Instances For
@[simp]
theorem AlternatingMap.curryLeft_zero {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } :
@[simp]
theorem AlternatingMap.curryLeft_add {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } (f : AlternatingMap R' M'' N'' (Fin ())) (g : AlternatingMap R' M'' N'' (Fin ())) :
@[simp]
theorem AlternatingMap.curryLeft_smul {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } (r : R') (f : AlternatingMap R' M'' N'' (Fin ())) :
@[simp]
theorem AlternatingMap.curryLeftLinearMap_apply {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } (f : AlternatingMap R' M'' N'' (Fin ())) :
AlternatingMap.curryLeftLinearMap f =
def AlternatingMap.curryLeftLinearMap {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } :
AlternatingMap R' M'' N'' (Fin ()) →ₗ[R'] M'' →ₗ[R'] AlternatingMap R' M'' N'' (Fin n)

AlternatingMap.curryLeft as a LinearMap. This is a separate definition as dot notation does not work for this version.

Instances For
@[simp]
theorem AlternatingMap.curryLeft_same {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] {n : } (f : AlternatingMap R' M'' N'' (Fin (Nat.succ ()))) (m : M'') :
↑() m = 0

Currying with the same element twice gives the zero map.

@[simp]
theorem AlternatingMap.curryLeft_compAlternatingMap {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} {N₂'' : Type u_14} [] [] [] [AddCommMonoid N₂''] [Module R' M''] [Module R' N''] [Module R' N₂''] {n : } (g : N'' →ₗ[R'] N₂'') (f : AlternatingMap R' M'' N'' (Fin ())) (m : M'') :
↑() m = ↑() (↑() m)
@[simp]
theorem AlternatingMap.curryLeft_compLinearMap {R' : Type u_10} {M'' : Type u_11} {M₂'' : Type u_12} {N'' : Type u_13} [] [] [AddCommMonoid M₂''] [] [Module R' M''] [Module R' M₂''] [Module R' N''] {n : } (g : M₂'' →ₗ[R'] M'') (f : AlternatingMap R' M'' N'' (Fin ())) (m : M₂'') :
= AlternatingMap.compLinearMap (↑() (g m)) g
@[simp]
theorem AlternatingMap.constLinearEquivOfIsEmpty_apply {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] [] (m : N'') :
AlternatingMap.constLinearEquivOfIsEmpty m =
@[simp]
theorem AlternatingMap.constLinearEquivOfIsEmpty_symm_apply {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] [] (f : AlternatingMap R' M'' N'' ι) :
↑(LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty) f = f 0
def AlternatingMap.constLinearEquivOfIsEmpty {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} [] [] [] [Module R' M''] [Module R' N''] [] :
N'' ≃ₗ[R'] AlternatingMap R' M'' N'' ι

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

Instances For