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 permuting the elements within a family.
MultilinearMap.alternatization, which makes an alternating map out of a non-alternating one.
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:

source

structure AlternatingMap (R : Type u_1) [Semiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_7) extends MultilinearMap R (fun (x : ι) => M) N :

Type (max (max u_2 u_3) u_7)

An alternating map from ι → M to N, denoted M [⋀^ι]→ₗ[R] N, is a multilinear map that vanishes when two of its arguments are equal.

toFun : (ι → M) → N
map_update_add' [DecidableEq ι] (m : ι → M) (i : ι) (x y : M) : (↑self).toFun (Function.update m i (x + y)) = (↑self).toFun (Function.update m i x) + (↑self).toFun (Function.update m i y)
map_update_smul' [DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M) : (↑self).toFun (Function.update m i (c • x)) = c • (↑self).toFun (Function.update m i x)
map_eq_zero_of_eq' (v : ι → M) (i j : ι) : v i = v j → i ≠ j → (↑self).toFun v = 0
The map is alternating: if v has two equal coordinates, then f v = 0.

Instances For

source

def «term_[⋀^_]→ₗ[_]_» :

Lean.TrailingParserDescr

An alternating map from ι → M to N, denoted M [⋀^ι]→ₗ[R] N, is a multilinear map that vanishes when two of its arguments are equal.

Equations

One or more equations did not get rendered due to their size.

Instances For

Basic coercion simp lemmas, largely copied from RingHom and MultilinearMap

source

instance AlternatingMap.instFunLike {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

FunLike (M [⋀^ι]→ₗ[R] N) (ι → M) N

Equations

AlternatingMap.instFunLike = { coe := fun (f : M [⋀^ι]→ₗ[R] N) => (↑f).toFun, coe_injective' := ⋯ }

source

@[simp]

theorem AlternatingMap.toFun_eq_coe {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) :

(↑f).toFun = ⇑f

source

@[simp]

theorem AlternatingMap.coe_mk {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : MultilinearMap R (fun (x : ι) => M) N) (h : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f.toFun v = 0) :

⇑{ toMultilinearMap := f, map_eq_zero_of_eq' := h } = ⇑f

source

theorem AlternatingMap.congr_fun {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {f g : M [⋀^ι]→ₗ[R] N} (h : f = g) (x : ι → M) :

f x = g x

source

theorem AlternatingMap.congr_arg {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {x y : ι → M} (h : x = y) :

f x = f y

source

theorem AlternatingMap.coe_injective {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

Function.Injective DFunLike.coe

source

theorem AlternatingMap.coe_inj {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {f g : M [⋀^ι]→ₗ[R] N} :

⇑f = ⇑g ↔ f = g

source

theorem AlternatingMap.ext {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {f f' : M [⋀^ι]→ₗ[R] N} (H : ∀ (x : ι → M), f x = f' x) :

f = f'

source

theorem AlternatingMap.ext_iff {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {f f' : M [⋀^ι]→ₗ[R] N} :

f = f' ↔ ∀ (x : ι → M), f x = f' x

source

instance AlternatingMap.instCoe {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

Coe (M [⋀^ι]→ₗ[R] N) (MultilinearMap R (fun (x : ι) => M) N)

Equations

AlternatingMap.instCoe = { coe := fun (x : M [⋀^ι]→ₗ[R] N) => ↑x }

source

@[simp]

theorem AlternatingMap.coe_multilinearMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) :

⇑↑f = ⇑f

source

theorem AlternatingMap.coe_multilinearMap_injective {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

Function.Injective toMultilinearMap

source

theorem AlternatingMap.coe_multilinearMap_mk {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : (ι → M) → N) (h₁ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)) (h₂ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), f (Function.update m i (c • x)) = c • f (Function.update m i x)) (h₃ : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → { toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯ }.toFun v = 0) :

↑{ toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := h₃ } = { toFun := f, map_update_add' := h₁, map_update_smul' := h₂ }

Simp-normal forms of the structure fields #

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

source

@[simp]

theorem AlternatingMap.map_update_add {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) [DecidableEq ι] (i : ι) (x y : M) :

f (Function.update v i (x + y)) = f (Function.update v i x) + f (Function.update v i y)

source

@[simp]

theorem AlternatingMap.map_update_sub {R : Type u_1} [Semiring R] {M' : Type u_5} [AddCommGroup M'] [Module R M'] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g' : M' [⋀^ι]→ₗ[R] N') (v' : ι → M') [DecidableEq ι] (i : ι) (x y : M') :

g' (Function.update v' i (x - y)) = g' (Function.update v' i x) - g' (Function.update v' i y)

source

@[simp]

theorem AlternatingMap.map_update_neg {R : Type u_1} [Semiring R] {M' : Type u_5} [AddCommGroup M'] [Module R M'] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g' : M' [⋀^ι]→ₗ[R] N') (v' : ι → M') [DecidableEq ι] (i : ι) (x : M') :

g' (Function.update v' i (-x)) = -g' (Function.update v' i x)

source

@[simp]

theorem AlternatingMap.map_update_smul {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) [DecidableEq ι] (i : ι) (r : R) (x : M) :

f (Function.update v i (r • x)) = r • f (Function.update v i x)

source

theorem AlternatingMap.map_eq_zero_of_eq {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) {i j : ι} (h : v i = v j) (hij : i ≠ j) :

f v = 0

source

theorem AlternatingMap.map_coord_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {m : ι → M} (i : ι) (h : m i = 0) :

f m = 0

source

@[simp]

theorem AlternatingMap.map_update_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) [DecidableEq ι] (m : ι → M) (i : ι) :

f (Function.update m i 0) = 0

source

@[simp]

theorem AlternatingMap.map_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) [Nonempty ι] :

f 0 = 0

source

theorem AlternatingMap.map_eq_zero_of_not_injective {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) (hv : ¬Function.Injective v) :

f v = 0

Algebraic structure inherited from `MultilinearMap` #

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

source

instance AlternatingMap.instSMul {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] :

SMul S (M [⋀^ι]→ₗ[R] N)

Equations

AlternatingMap.instSMul = { smul := fun (c : S) (f : M [⋀^ι]→ₗ[R] N) => let __src := c • ↑f; { toMultilinearMap := __src, map_eq_zero_of_eq' := ⋯ } }

source

@[simp]

theorem AlternatingMap.smul_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {S : Type u_10} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (c : S) (m : ι → M) :

(c • f) m = c • f m

source

theorem AlternatingMap.coe_smul {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {S : Type u_10} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (c : S) :

↑(c • f) = c • ↑f

source

theorem AlternatingMap.coeFn_smul {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (c : S) (f : M [⋀^ι]→ₗ[R] N) :

⇑(c • f) = c • ⇑f

source

instance AlternatingMap.instSMulCommClass {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] {T : Type u_11} [Monoid T] [DistribMulAction T N] [SMulCommClass R T N] [SMulCommClass S T N] :

SMulCommClass S T (M [⋀^ι]→ₗ[R] N)

source

instance AlternatingMap.instIsCentralScalar {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] [DistribMulAction Sᵐᵒᵖ N] [IsCentralScalar S N] :

IsCentralScalar S (M [⋀^ι]→ₗ[R] N)

source

def AlternatingMap.prod {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {P : Type u_4} [AddCommMonoid P] [Module R P] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) :

M [⋀^ι]→ₗ[R] (N × P)

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

Equations

f.prod g = { toMultilinearMap := (↑f).prod ↑g, map_eq_zero_of_eq' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.prod_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {P : Type u_4} [AddCommMonoid P] [Module R P] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) (m : (i : ι) → (fun (x : ι) => M) i) :

(f.prod g) m = (f m, g m)

source

@[simp]

theorem AlternatingMap.coe_prod {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {P : Type u_4} [AddCommMonoid P] [Module R P] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (g : M [⋀^ι]→ₗ[R] P) :

↑(f.prod g) = (↑f).prod ↑g

source

def AlternatingMap.pi {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_7} {ι' : Type u_10} {N : ι' → Type u_11} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → M [⋀^ι]→ₗ[R] N i) :

M [⋀^ι]→ₗ[R] ((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

AlternatingMap.pi f = { toMultilinearMap := MultilinearMap.pi fun (a : ι') => ↑(f a), map_eq_zero_of_eq' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.pi_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_7} {ι' : Type u_10} {N : ι' → Type u_11} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → M [⋀^ι]→ₗ[R] N i) (m : (i : ι) → (fun (x : ι) => M) i) (i : ι') :

(pi f) m i = (f i) m

source

@[simp]

theorem AlternatingMap.coe_pi {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_7} {ι' : Type u_10} {N : ι' → Type u_11} [(i : ι') → AddCommMonoid (N i)] [(i : ι') → Module R (N i)] (f : (i : ι') → M [⋀^ι]→ₗ[R] N i) :

↑(pi f) = MultilinearMap.pi fun (a : ι') => ↑(f a)

source

def AlternatingMap.smulRight {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :

M₁ [⋀^ι]→ₗ[R] 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

f.smulRight z = { toMultilinearMap := (↑f).smulRight z, map_eq_zero_of_eq' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.smulRight_apply {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) (a✝ : (i : ι) → (fun (x : ι) => M₁) i) :

(f.smulRight z) a✝ = f a✝ • z

source

@[simp]

theorem AlternatingMap.coe_smulRight {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :

↑(f.smulRight z) = (↑f).smulRight z

source

instance AlternatingMap.instAdd {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

Add (M [⋀^ι]→ₗ[R] N)

Equations

AlternatingMap.instAdd = { add := fun (a b : M [⋀^ι]→ₗ[R] N) => let __src := ↑a + ↑b; { toMultilinearMap := __src, map_eq_zero_of_eq' := ⋯ } }

source

@[simp]

theorem AlternatingMap.add_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f f' : M [⋀^ι]→ₗ[R] N) (v : ι → M) :

(f + f') v = f v + f' v

source

theorem AlternatingMap.coe_add {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f f' : M [⋀^ι]→ₗ[R] N) :

↑(f + f') = ↑f + ↑f'

source

instance AlternatingMap.instZero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

Zero (M [⋀^ι]→ₗ[R] N)

Equations

AlternatingMap.instZero = { zero := let __src := 0; { toMultilinearMap := __src, map_eq_zero_of_eq' := ⋯ } }

source

@[simp]

theorem AlternatingMap.zero_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (v : ι → M) :

0 v = 0

source

theorem AlternatingMap.coe_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

↑0 = 0

source

@[simp]

theorem AlternatingMap.mk_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

{ toMultilinearMap := 0, map_eq_zero_of_eq' := ⋯ } = 0

source

instance AlternatingMap.instInhabited {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

Inhabited (M [⋀^ι]→ₗ[R] N)

Equations

AlternatingMap.instInhabited = { default := 0 }

source

instance AlternatingMap.instAddCommMonoid {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} :

AddCommMonoid (M [⋀^ι]→ₗ[R] N)

Equations

One or more equations did not get rendered due to their size.

source

instance AlternatingMap.instNeg {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} :

Neg (M [⋀^ι]→ₗ[R] N')

Equations

AlternatingMap.instNeg = { neg := fun (f : M [⋀^ι]→ₗ[R] N') => let __src := -↑f; { toMultilinearMap := __src, map_eq_zero_of_eq' := ⋯ } }

source

@[simp]

theorem AlternatingMap.neg_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (m : ι → M) :

(-g) m = -g m

source

theorem AlternatingMap.coe_neg {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') :

↑(-g) = -↑g

source

instance AlternatingMap.instSub {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} :

Sub (M [⋀^ι]→ₗ[R] N')

Equations

AlternatingMap.instSub = { sub := fun (f g : M [⋀^ι]→ₗ[R] N') => let __src := ↑f - ↑g; { toMultilinearMap := __src, map_eq_zero_of_eq' := ⋯ } }

source

@[simp]

theorem AlternatingMap.sub_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g g₂ : M [⋀^ι]→ₗ[R] N') (m : ι → M) :

(g - g₂) m = g m - g₂ m

source

theorem AlternatingMap.coe_sub {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g g₂ : M [⋀^ι]→ₗ[R] N') :

↑(g - g₂) = ↑g - ↑g₂

source

instance AlternatingMap.instAddCommGroup {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} :

AddCommGroup (M [⋀^ι]→ₗ[R] N')

Equations

One or more equations did not get rendered due to their size.

source

instance AlternatingMap.instDistribMulAction {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] :

DistribMulAction S (M [⋀^ι]→ₗ[R] N)

Equations

AlternatingMap.instDistribMulAction = { toSMul := AlternatingMap.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

source

instance AlternatingMap.instModule {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Semiring S] [Module S N] [SMulCommClass R S N] :

Module S (M [⋀^ι]→ₗ[R] N)

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

Equations

AlternatingMap.instModule = { toDistribMulAction := AlternatingMap.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

source

instance AlternatingMap.instNoZeroSMulDivisors {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Semiring S] [Module S N] [SMulCommClass R S N] [NoZeroSMulDivisors S N] :

NoZeroSMulDivisors S (M [⋀^ι]→ₗ[R] N)

source

def AlternatingMap.toMultilinearMapLM {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Semiring S] [Module S N] [SMulCommClass R S N] :

M [⋀^ι]→ₗ[R] N →ₗ[S] MultilinearMap R (fun (x : ι) => M) N

Embedding of alternating maps into multilinear maps as a linear map.

Equations

AlternatingMap.toMultilinearMapLM = { toFun := AlternatingMap.toMultilinearMap, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.toMultilinearMapLM_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} [Semiring S] [Module S N] [SMulCommClass R S N] (self : M [⋀^ι]→ₗ[R] N) :

toMultilinearMapLM self = ↑self

source

def AlternatingMap.ofSubsingleton (R : Type u_1) [Semiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] {ι : Type u_7} [Subsingleton ι] (i : ι) :

(M →ₗ[R] N) ≃ M [⋀^ι]→ₗ[R] N

The natural equivalence between linear maps from M to N and 1-multilinear alternating maps from M to N.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem AlternatingMap.ofSubsingleton_apply_apply (R : Type u_1) [Semiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] {ι : Type u_7} [Subsingleton ι] (i : ι) (f : M →ₗ[R] N) (x : ι → M) :

((ofSubsingleton R M N i) f) x = f (x i)

source

@[simp]

theorem AlternatingMap.ofSubsingleton_symm_apply_apply (R : Type u_1) [Semiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] {ι : Type u_7} [Subsingleton ι] (i : ι) (f : M [⋀^ι]→ₗ[R] N) (x : M) :

((ofSubsingleton R M N i).symm f) x = f fun (x_1 : ι) => x

source

def AlternatingMap.constOfIsEmpty (R : Type u_1) [Semiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_7) [IsEmpty ι] (m : N) :

M [⋀^ι]→ₗ[R] N

The constant map is alternating when ι is empty.

Equations

AlternatingMap.constOfIsEmpty R M ι m = { toFun := Function.const (ι → M) m, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.constOfIsEmpty_apply (R : Type u_1) [Semiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (ι : Type u_7) [IsEmpty ι] (m : N) :

⇑(constOfIsEmpty R M ι m) = Function.const (ι → M) m

source

def AlternatingMap.codRestrict {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ (v : ι → M), f v ∈ p) :

M [⋀^ι]→ₗ[R] ↥p

Restrict the codomain of an alternating map to a submodule.

Equations

f.codRestrict p h = { toFun := fun (v : ι → M) => ⟨f v, ⋯⟩, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.codRestrict_apply_coe {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ (v : ι → M), f v ∈ p) (v : ι → M) :

↑((f.codRestrict p h) v) = f v

Composition with linear maps #

source

def LinearMap.compAlternatingMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :

M [⋀^ι]→ₗ[R] N₂

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

Equations

g.compAlternatingMap f = { toMultilinearMap := g.compMultilinearMap ↑f, map_eq_zero_of_eq' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.coe_compAlternatingMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :

⇑(g.compAlternatingMap f) = ⇑g ∘ ⇑f

source

@[simp]

theorem LinearMap.compAlternatingMap_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (m : ι → M) :

(g.compAlternatingMap f) m = g (f m)

source

@[simp]

theorem LinearMap.compAlternatingMap_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (g : N →ₗ[R] N₂) :

g.compAlternatingMap 0 = 0

source

@[simp]

theorem LinearMap.zero_compAlternatingMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (f : M [⋀^ι]→ₗ[R] N) :

compAlternatingMap 0 f = 0

source

@[simp]

theorem LinearMap.compAlternatingMap_add {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (g : N →ₗ[R] N₂) (f₁ f₂ : M [⋀^ι]→ₗ[R] N) :

g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂

source

@[simp]

theorem LinearMap.add_compAlternatingMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (g₁ g₂ : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :

(g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f

source

@[simp]

theorem LinearMap.compAlternatingMap_smul {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] [Monoid S] [DistribMulAction S N] [DistribMulAction S N₂] [SMulCommClass R S N] [SMulCommClass R S N₂] [CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :

g.compAlternatingMap (s • f) = s • g.compAlternatingMap f

source

@[simp]

theorem LinearMap.smul_compAlternatingMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {S : Type u_10} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] [Monoid S] [DistribMulAction S N₂] [SMulCommClass R S N₂] (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :

(s • g).compAlternatingMap f = s • g.compAlternatingMap f

source

def LinearMap.compAlternatingMapₗ {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (S : Type u_10) {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] [Semiring S] [Module S N] [Module S N₂] [SMulCommClass R S N] [SMulCommClass R S N₂] [CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) :

M [⋀^ι]→ₗ[R] N →ₗ[S] M [⋀^ι]→ₗ[R] N₂

LinearMap.compAlternatingMap as an S-linear map.

Equations

LinearMap.compAlternatingMapₗ S g = { toFun := g.compAlternatingMap, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.compAlternatingMapₗ_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (S : Type u_10) {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] [Semiring S] [Module S N] [Module S N₂] [SMulCommClass R S N] [SMulCommClass R S N₂] [CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :

(compAlternatingMapₗ S g) f = g.compAlternatingMap f

source

theorem LinearMap.smulRight_eq_comp {R : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14} {ι : Type u_15} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂) :

f.smulRight z = (id.smulRight z).compAlternatingMap f

source

@[simp]

theorem LinearMap.subtype_compAlternatingMap_codRestrict {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N) (h : ∀ (v : ι → M), f v ∈ p) :

p.subtype.compAlternatingMap (f.codRestrict p h) = f

source

@[simp]

theorem LinearMap.compAlternatingMap_codRestrict {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {N₂ : Type u_11} [AddCommMonoid N₂] [Module R N₂] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N₂) (h : ∀ (c : N), g c ∈ p) :

(codRestrict p g h).compAlternatingMap f = (g.compAlternatingMap f).codRestrict p ⋯

source

def AlternatingMap.compLinearMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :

M₂ [⋀^ι]→ₗ[R] N

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

Equations

f.compLinearMap g = { toMultilinearMap := (↑f).compLinearMap fun (x : ι) => g, map_eq_zero_of_eq' := ⋯ }

Instances For

source

theorem AlternatingMap.coe_compLinearMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :

⇑(f.compLinearMap g) = ⇑f ∘ fun (x : ι → M₂) => ⇑g ∘ x

source

@[simp]

theorem AlternatingMap.compLinearMap_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) (v : ι → M₂) :

(f.compLinearMap g) v = f fun (i : ι) => g (v i)

source

theorem AlternatingMap.compLinearMap_assoc {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_11} [AddCommMonoid M₃] [Module R M₃] (f : M [⋀^ι]→ₗ[R] N) (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂) :

(f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂)

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

source

@[simp]

theorem AlternatingMap.zero_compLinearMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (g : M₂ →ₗ[R] M) :

compLinearMap 0 g = 0

source

@[simp]

theorem AlternatingMap.add_compLinearMap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (f₁ f₂ : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) :

(f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

source

@[simp]

theorem AlternatingMap.compLinearMap_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] [Nonempty ι] (f : M [⋀^ι]→ₗ[R] N) :

f.compLinearMap 0 = 0

source

@[simp]

theorem AlternatingMap.compLinearMap_id {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) :

f.compLinearMap LinearMap.id = f

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

source

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

Function.Injective fun (g : M [⋀^ι]→ₗ[R] N) => g.compLinearMap f

Composing with a surjective linear map is injective.

source

theorem AlternatingMap.compLinearMap_inj {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (f : M₂ →ₗ[R] M) (hf : Function.Surjective ⇑f) (g₁ g₂ : M [⋀^ι]→ₗ[R] N) :

g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂

source

theorem AlternatingMap.ext_ring {N : Type u_3} [AddCommMonoid N] {ι : Type u_7} {R : Type u_12} [CommSemiring R] [Module R N] [Finite ι] ⦃f g : R [⋀^ι]→ₗ[R] N⦄ (h : (f fun (x : ι) => 1) = g fun (x : ι) => 1) :

f = g

If two R-alternating maps from R are equal on 1, then they are equal.

This is the alternating version of LinearMap.ext_ring.

source

theorem AlternatingMap.ext_ring_iff {N : Type u_3} [AddCommMonoid N] {ι : Type u_7} {R : Type u_12} [CommSemiring R] [Module R N] [Finite ι] {f g : R [⋀^ι]→ₗ[R] N} :

f = g ↔ (f fun (x : ι) => 1) = g fun (x : ι) => 1

source

instance AlternatingMap.uniqueOfCommRing {N : Type u_3} [AddCommMonoid N] {ι : Type u_7} {R : Type u_12} [CommSemiring R] [Module R N] [Finite ι] [Nontrivial ι] :

Unique (R [⋀^ι]→ₗ[R] N)

The only R-alternating map from two or more copies of R is the zero map.

Equations

AlternatingMap.uniqueOfCommRing = { toInhabited := AlternatingMap.instInhabited, uniq := ⋯ }

source

def AlternatingMap.domLCongr (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (e : M ≃ₗ[R] M₂) :

M [⋀^ι]→ₗ[R] N ≃ₗ[S] M₂ [⋀^ι]→ₗ[R] N

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

This is AlternatingMap.compLinearMap as an isomorphism, and the alternating version of LinearEquiv.multilinearMapCongrLeft. It could also have been called LinearEquiv.alternatingMapCongrLeft.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem AlternatingMap.domLCongr_apply (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (e : M ≃ₗ[R] M₂) (f : M [⋀^ι]→ₗ[R] N) :

(domLCongr R N ι S e) f = f.compLinearMap ↑e.symm

source

@[simp]

theorem AlternatingMap.domLCongr_refl (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_7) (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] :

domLCongr R N ι S (LinearEquiv.refl R M) = LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N)

source

@[simp]

theorem AlternatingMap.domLCongr_symm (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (e : M ≃ₗ[R] M₂) :

(domLCongr R N ι S e).symm = domLCongr R N ι S e.symm

source

theorem AlternatingMap.domLCongr_trans (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_7) {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_11} [AddCommMonoid M₃] [Module R M₃] (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (e : M ≃ₗ[R] M₂) (f : M₂ ≃ₗ[R] M₃) :

domLCongr R N ι S e ≪≫ₗ domLCongr R N ι S f = domLCongr R N ι S (e ≪≫ₗ f)

source

@[simp]

theorem AlternatingMap.compLinearEquiv_eq_zero_iff {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {M₂ : Type u_10} [AddCommMonoid M₂] [Module R M₂] (f : M [⋀^ι]→ₗ[R] N) (g : M₂ ≃ₗ[R] M) :

f.compLinearMap ↑g = 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 `MultilinearMap` #

source

theorem AlternatingMap.map_update_sum {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {α : Type u_12} [DecidableEq ι] (t : Finset α) (i : ι) (g : α → M) (m : ι → M) :

f (Function.update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, 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.

source

theorem AlternatingMap.map_update_self {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) [DecidableEq ι] {i j : ι} (hij : i ≠ j) :

f (Function.update v i (v j)) = 0

source

theorem AlternatingMap.map_update_update {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) [DecidableEq ι] {i j : ι} (hij : i ≠ j) (m : M) :

f (Function.update (Function.update v i m) j m) = 0

source

theorem AlternatingMap.map_swap_add {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) [DecidableEq ι] {i j : ι} (hij : i ≠ j) :

f (v ∘ ⇑(Equiv.swap i j)) + f v = 0

source

theorem AlternatingMap.map_add_swap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M) [DecidableEq ι] {i j : ι} (hij : i ≠ j) :

f v + f (v ∘ ⇑(Equiv.swap i j)) = 0

source

theorem AlternatingMap.map_swap {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (v : ι → M) [DecidableEq ι] {i j : ι} (hij : i ≠ j) :

g (v ∘ ⇑(Equiv.swap i j)) = -g v

source

theorem AlternatingMap.map_perm {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [DecidableEq ι] [Fintype ι] (v : ι → M) (σ : Equiv.Perm ι) :

g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v

source

theorem AlternatingMap.map_congr_perm {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (v : ι → M) [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) :

g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ)

source

def AlternatingMap.domDomCongr {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) :

M [⋀^ι']→ₗ[R] N

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

This is the alternating version of MultilinearMap.domDomCongr.

Equations

AlternatingMap.domDomCongr σ f = { toFun := fun (v : ι' → M) => f (v ∘ ⇑σ), map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.domDomCongr_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) (v : ι' → M) :

(domDomCongr σ f) v = f (v ∘ ⇑σ)

source

@[simp]

theorem AlternatingMap.domDomCongr_refl {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) :

domDomCongr (Equiv.refl ι) f = f

source

theorem AlternatingMap.domDomCongr_trans {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} {ι'' : Type u_9} (σ₁ : ι ≃ ι') (σ₂ : ι' ≃ ι'') (f : M [⋀^ι]→ₗ[R] N) :

domDomCongr (σ₁.trans σ₂) f = domDomCongr σ₂ (domDomCongr σ₁ f)

source

@[simp]

theorem AlternatingMap.domDomCongr_zero {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') :

domDomCongr σ 0 = 0

source

@[simp]

theorem AlternatingMap.domDomCongr_add {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) :

domDomCongr σ (f + g) = domDomCongr σ f + domDomCongr σ g

source

@[simp]

theorem AlternatingMap.domDomCongr_smul {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} {S : Type u_12} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (σ : ι ≃ ι') (c : S) (f : M [⋀^ι]→ₗ[R] N) :

domDomCongr σ (c • f) = c • domDomCongr σ f

source

def AlternatingMap.domDomCongrEquiv {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') :

M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N

AlternatingMap.domDomCongr as an equivalence.

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

Equations

AlternatingMap.domDomCongrEquiv σ = { toFun := AlternatingMap.domDomCongr σ, invFun := AlternatingMap.domDomCongr σ.symm, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.domDomCongrEquiv_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) :

(domDomCongrEquiv σ) f = domDomCongr σ f

source

@[simp]

theorem AlternatingMap.domDomCongrEquiv_symm_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι']→ₗ[R] N) :

(domDomCongrEquiv σ).symm f = domDomCongr σ.symm f

source

def AlternatingMap.domDomCongrₗ {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (σ : ι ≃ ι') :

M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι']→ₗ[R] N

AlternatingMap.domDomCongr as a linear equivalence.

Equations

AlternatingMap.domDomCongrₗ S σ = { toFun := AlternatingMap.domDomCongr σ, map_add' := ⋯, map_smul' := ⋯, invFun := AlternatingMap.domDomCongr σ.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem AlternatingMap.domDomCongrₗ_symm_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (σ : ι ≃ ι') (f : M [⋀^ι']→ₗ[R] N) :

(domDomCongrₗ S σ).symm f = domDomCongr σ.symm f

source

@[simp]

theorem AlternatingMap.domDomCongrₗ_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) :

(domDomCongrₗ S σ) f = domDomCongr σ f

source

@[simp]

theorem AlternatingMap.domDomCongrₗ_refl {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] :

domDomCongrₗ S (Equiv.refl ι) = LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N)

source

@[simp]

theorem AlternatingMap.domDomCongrₗ_toAddEquiv {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [Semiring S] [Module S N] [SMulCommClass R S N] (σ : ι ≃ ι') :

↑(domDomCongrₗ S σ) = domDomCongrEquiv σ

source

@[simp]

theorem AlternatingMap.domDomCongr_eq_iff {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f g : M [⋀^ι]→ₗ[R] N) :

domDomCongr σ f = domDomCongr σ g ↔ f = g

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

source

@[simp]

theorem AlternatingMap.domDomCongr_eq_zero_iff {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) :

domDomCongr σ f = 0 ↔ f = 0

source

theorem AlternatingMap.domDomCongr_perm {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) :

domDomCongr σ g = Equiv.Perm.sign σ • g

source

theorem AlternatingMap.coe_domDomCongr {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_7} {ι' : Type u_8} (f : M [⋀^ι]→ₗ[R] N) (σ : ι ≃ ι') :

↑(domDomCongr σ f) = MultilinearMap.domDomCongr σ ↑f

source

theorem AlternatingMap.map_linearDependent {ι : Type u_7} {K : Type u_12} [Ring K] {M : Type u_13} [AddCommGroup M] [Module K M] {N : Type u_14} [AddCommGroup N] [Module K N] [NoZeroSMulDivisors K N] (f : M [⋀^ι]→ₗ[K] N) (v : ι → M) (h : ¬LinearIndependent K v) :

f v = 0

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

source

theorem AlternatingMap.map_vecCons_add {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M) :

f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)

A version of MultilinearMap.cons_add for AlternatingMap.

source

theorem AlternatingMap.map_vecCons_smul {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (c : R) (x : M) :

f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)

A version of MultilinearMap.cons_smul for AlternatingMap.

source

def MultilinearMap.alternatization {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [Fintype ι] [DecidableEq ι] :

MultilinearMap R (fun (x : ι) => M) N' →+ M [⋀^ι]→ₗ[R] N'

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MultilinearMap.alternatization_def {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (m : MultilinearMap R (fun (x : ι) => M) N') :

⇑(alternatization m) = ⇑(∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • domDomCongr σ m)

source

theorem MultilinearMap.alternatization_coe {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (m : MultilinearMap R (fun (x : ι) => M) N') :

↑(alternatization m) = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • domDomCongr σ m

source

theorem MultilinearMap.alternatization_apply {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (m : MultilinearMap R (fun (x : ι) => M) N') (v : ι → M) :

(alternatization m) v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • (domDomCongr σ m) v

source

theorem AlternatingMap.coe_alternatization {R : Type u_1} [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N' : Type u_6} [AddCommGroup N'] [Module R N'] {ι : Type u_7} [DecidableEq ι] [Fintype ι] (a : M [⋀^ι]→ₗ[R] N') :

MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a

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

source

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

MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f)

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

source

theorem Module.Basis.ext_alternating {ι : Type u_7} {ι₁ : Type u_10} [Finite ι] {R' : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13} [CommSemiring R'] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R' N₁] [Module R' N₂] {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁) (h : ∀ (v : ι → ι₁), Function.Injective 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.

source

def LinearEquiv.alternatingMapCongrRight {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} {N₂'' : Type u_14} [CommSemiring R'] [AddCommMonoid M''] [AddCommMonoid N''] [AddCommMonoid N₂''] [Module R' M''] [Module R' N''] [Module R' N₂''] (e : N'' ≃ₗ[R'] N₂'') :

M'' [⋀^ι]→ₗ[R'] N'' ≃ₗ[R'] M'' [⋀^ι]→ₗ[R'] N₂''

An isomorphism of multilinear maps given an isomorphism between their codomains.

This is Linear.compAlternatingMap as an isomorphism, and the alternating version of LinearEquiv.multilinearMapCongrRight.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem LinearEquiv.alternatingMapCongrRight_apply_apply {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} {N₂'' : Type u_14} [CommSemiring R'] [AddCommMonoid M''] [AddCommMonoid N''] [AddCommMonoid N₂''] [Module R' M''] [Module R' N''] [Module R' N₂''] (e : N'' ≃ₗ[R'] N₂'') (f : M'' [⋀^ι]→ₗ[R'] N'') (a✝ : (i : ι) → (fun (x : ι) => M'') i) :

(e.alternatingMapCongrRight f) a✝ = e (f a✝)

source

@[simp]