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 ofR-linear alternating maps fromι → MtoN.f.map_eq_zero_of_eqexpresses thatfis zero when two inputs are equal.f.map_swapexpresses thatfis negated when two inputs are swapped.f.map_permexpresses howfvaries by a sign change under a permutation of its inputs.- An
AddCommMonoid,AddCommGroup, andModulestructure overAlternatingMaps that matches the definitions overMultilinearMaps. 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 byFin 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:
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
:
Type (max (max u_2 u_3) u_7)
- toFun : (ι → M) → N
- map_add' : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), MultilinearMap.toFun (↑s) (Function.update m i (x + y)) = MultilinearMap.toFun (↑s) (Function.update m i x) + MultilinearMap.toFun (↑s) (Function.update m i y)
- map_smul' : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), MultilinearMap.toFun (↑s) (Function.update m i (c • x)) = c • MultilinearMap.toFun (↑s) (Function.update m i x)
- map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → MultilinearMap.toFun (↑s) v = 0
The map is alternating: if
vhas two equal coordinates, thenf v = 0.
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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
{ι : Type u_7}
:
FunLike (AlternatingMap R M N ι) (ι → M) fun x => N
instance
AlternatingMap.coeFun
{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}
:
CoeFun (AlternatingMap R M N ι) fun x => (ι → M) → N
@[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 : AlternatingMap R M N ι)
:
f.toFun = ↑f
@[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 → MultilinearMap.toFun f v = 0)
:
↑{ toMultilinearMap := f, map_eq_zero_of_eq' := h } = ↑f
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 : 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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[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}
[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 FunLike.coe
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 : AlternatingMap R M N ι}
{g : AlternatingMap R M N ι}
:
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 : 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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
{ι : Type u_7}
{f : AlternatingMap R M N ι}
{g : AlternatingMap R M N ι}
:
instance
AlternatingMap.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}
:
Coe (AlternatingMap R M N ι) (MultilinearMap R (fun x => M) N)
@[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 : AlternatingMap R M N ι)
:
↑↑f = ↑f
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 AlternatingMap.toMultilinearMap
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 →
MultilinearMap.toFun
{ toFun := f, map_add' := fun [inst : DecidableEq ι] => h₁ fun a b => inst a b,
map_smul' := fun [inst : DecidableEq ι] => h₂ fun a b => inst a b }
v = 0)
:
↑{
toMultilinearMap :=
{ toFun := f, map_add' := fun [inst : DecidableEq ι] => h₁ fun a b => inst a b,
map_smul' := fun [inst : DecidableEq ι] => 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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
{ι : Type u_7}
(f : AlternatingMap R M N ι)
(v : ι → M)
[DecidableEq ι]
(i : ι)
(x : M)
(y : M)
:
↑f (Function.update v i (x + y)) = ↑f (Function.update v i x) + ↑f (Function.update v i y)
@[simp]
theorem
AlternatingMap.map_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' : AlternatingMap R M' N' ι)
(v' : ι → M')
[DecidableEq ι]
(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}
[Semiring R]
{M' : Type u_5}
[AddCommGroup M']
[Module R M']
{N' : Type u_6}
[AddCommGroup N']
[Module R N']
{ι : Type u_7}
(g' : AlternatingMap R M' N' ι)
(v' : ι → M')
[DecidableEq ι]
(i : ι)
(x : M')
:
↑g' (Function.update v' i (-x)) = -↑g' (Function.update v' i x)
@[simp]
theorem
AlternatingMap.map_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 : AlternatingMap R M N ι)
(v : ι → M)
[DecidableEq ι]
(i : ι)
(r : R)
(x : M)
:
↑f (Function.update v i (r • x)) = r • ↑f (Function.update v i x)
@[simp]
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 : 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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
{ι : Type u_7}
(f : AlternatingMap R M N ι)
[DecidableEq ι]
(m : ι → M)
(i : ι)
:
↑f (Function.update m i 0) = 0
@[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 : AlternatingMap R M N ι)
[Nonempty ι]
:
↑f 0 = 0
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 : AlternatingMap R M 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
instance
AlternatingMap.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]
:
SMul S (AlternatingMap R M N ι)
@[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 : AlternatingMap R M N ι)
{S : Type u_10}
[Monoid S]
[DistribMulAction S N]
[SMulCommClass R S N]
(c : S)
(m : ι → M)
:
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 : AlternatingMap R M N ι)
{S : Type u_10}
[Monoid S]
[DistribMulAction S N]
[SMulCommClass R S N]
(c : S)
:
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 : AlternatingMap R M N ι)
:
instance
AlternatingMap.isCentralScalar
{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 (AlternatingMap R M N ι)
@[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 : AlternatingMap R M N ι)
(g : AlternatingMap R M P ι)
(m : (i : ι) → (fun x => M) i)
:
↑(AlternatingMap.prod f g) m = (↑f m, ↑g m)
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 : 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}
[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 : AlternatingMap R M N ι)
(g : AlternatingMap R M P ι)
:
↑(AlternatingMap.prod f g) = MultilinearMap.prod ↑f ↑g
@[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 : ι') → AlternatingMap R M (N i) ι)
(m : (i : ι) → (fun x => M) i)
(i : ι')
:
↑(AlternatingMap.pi f) m i = ↑(f i) m
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 : ι') → 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}
[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 : ι') → AlternatingMap R M (N i) ι)
:
↑(AlternatingMap.pi f) = 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}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
(f : AlternatingMap R M₁ R ι)
(z : M₂)
:
∀ (a : (i : ι) → (fun x => M₁) i), ↑(AlternatingMap.smulRight f z) a = ↑f a • z
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 : 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}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
(f : AlternatingMap R M₁ R ι)
(z : M₂)
:
↑(AlternatingMap.smulRight f z) = MultilinearMap.smulRight (↑f) z
instance
AlternatingMap.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}
:
Add (AlternatingMap R M N ι)
@[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 : AlternatingMap R M N ι)
(f' : AlternatingMap R M N ι)
(v : ι → M)
:
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 : AlternatingMap R M N ι)
(f' : AlternatingMap R M N ι)
:
instance
AlternatingMap.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}
:
Zero (AlternatingMap R M N ι)
@[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
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
@[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' := (_ : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → MultilinearMap.toFun (↑0) v = 0) } = 0
instance
AlternatingMap.inhabited
{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 (AlternatingMap R M N ι)
instance
AlternatingMap.addCommMonoid
{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 (AlternatingMap R M N ι)
instance
AlternatingMap.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}
:
Neg (AlternatingMap R M N' ι)
@[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 : AlternatingMap R M N' ι)
(m : ι → M)
:
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 : AlternatingMap R M N' ι)
:
instance
AlternatingMap.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}
:
Sub (AlternatingMap R M N' ι)
@[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 : AlternatingMap R M N' ι)
(g₂ : AlternatingMap R M N' ι)
(m : ι → M)
:
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 : AlternatingMap R M N' ι)
(g₂ : AlternatingMap R M N' ι)
:
instance
AlternatingMap.addCommGroup
{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 (AlternatingMap R M N' ι)
instance
AlternatingMap.distribMulAction
{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 (AlternatingMap R M N ι)
instance
AlternatingMap.module
{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 (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}
[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 (AlternatingMap R M N ι)
@[simp]
theorem
AlternatingMap.ofSubsingleton_apply
(R : Type u_1)
[Semiring R]
(M : Type u_2)
[AddCommMonoid M]
[Module R M]
{ι : Type u_7}
[Subsingleton ι]
(i : ι)
(f : ι → M)
:
↑(AlternatingMap.ofSubsingleton R M i) f = Function.eval i f
def
AlternatingMap.ofSubsingleton
(R : Type u_1)
[Semiring R]
(M : Type u_2)
[AddCommMonoid M]
[Module R M]
{ι : Type u_7}
[Subsingleton ι]
(i : ι)
:
AlternatingMap R M M ι
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)
[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)
:
↑(AlternatingMap.constOfIsEmpty R M ι m) = Function.const (ι → M) m
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)
:
AlternatingMap R M N ι
The constant map is alternating when ι is empty.
Instances For
@[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 : AlternatingMap R M N ι)
(p : Submodule R N)
(h : ∀ (v : ι → M), ↑f v ∈ p)
(v : ι → M)
:
↑(↑(AlternatingMap.codRestrict f p h) v) = ↑f v
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 : AlternatingMap R M N ι)
(p : Submodule R N)
(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}
[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_10}
[AddCommMonoid N₂]
[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}
[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_10}
[AddCommMonoid N₂]
[Module R N₂]
(g : N →ₗ[R] N₂)
(f : AlternatingMap R M N ι)
:
↑(↑(LinearMap.compAlternatingMap g) f) = ↑g ∘ ↑f
@[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_10}
[AddCommMonoid N₂]
[Module R N₂]
(g : N →ₗ[R] N₂)
(f : AlternatingMap R M N ι)
(m : ι → M)
:
↑(↑(LinearMap.compAlternatingMap g) f) m = ↑g (↑f m)
theorem
LinearMap.smulRight_eq_comp
{R : Type u_11}
{M₁ : Type u_12}
{M₂ : Type u_13}
{ι : Type u_14}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
(f : AlternatingMap R M₁ R ι)
(z : M₂)
:
AlternatingMap.smulRight f z = ↑(LinearMap.compAlternatingMap (LinearMap.smulRight LinearMap.id z)) f
@[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 : AlternatingMap R M N ι)
(p : Submodule R N)
(h : ∀ (v : ι → M), ↑f v ∈ p)
:
↑(LinearMap.compAlternatingMap (Submodule.subtype p)) (AlternatingMap.codRestrict f p h) = f
@[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_10}
[AddCommMonoid N₂]
[Module R N₂]
(g : N →ₗ[R] N₂)
(f : AlternatingMap R M N ι)
(p : Submodule R N₂)
(h : ∀ (c : N), ↑g c ∈ p)
:
↑(LinearMap.compAlternatingMap (LinearMap.codRestrict p g h)) f = AlternatingMap.codRestrict (↑(LinearMap.compAlternatingMap g) f) p fun v => h (↑f v)
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 : 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}
[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 : AlternatingMap R M N ι)
(g : M₂ →ₗ[R] M)
:
↑(AlternatingMap.compLinearMap f g) = ↑f ∘ (fun x x_1 => x ∘ x_1) ↑g
@[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 : AlternatingMap R M N ι)
(g : M₂ →ₗ[R] M)
(v : ι → M₂)
:
↑(AlternatingMap.compLinearMap f g) v = ↑f fun i => ↑g (v i)
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 : 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}
[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)
:
@[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₁ : AlternatingMap R M N ι)
(f₂ : AlternatingMap R M N ι)
(g : M₂ →ₗ[R] M)
:
AlternatingMap.compLinearMap (f₁ + f₂) g = AlternatingMap.compLinearMap f₁ g + AlternatingMap.compLinearMap f₂ g
@[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 : AlternatingMap R M N ι)
:
@[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 : AlternatingMap R M N ι)
:
AlternatingMap.compLinearMap f LinearMap.id = f
Composing an alternating map with the identity linear map in each argument.
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 => AlternatingMap.compLinearMap g f
Composing with a surjective linear map is injective.
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₁ : AlternatingMap R M N ι)
(g₂ : AlternatingMap R M N ι)
:
AlternatingMap.compLinearMap g₁ f = AlternatingMap.compLinearMap g₂ f ↔ g₁ = g₂
@[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 : AlternatingMap R M N ι)
:
↑(AlternatingMap.domLCongr R N ι S e) f = AlternatingMap.compLinearMap f ↑(LinearEquiv.symm e)
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₂)
:
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)
[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]
:
AlternatingMap.domLCongr R N ι S (LinearEquiv.refl R M) = LinearEquiv.refl S (AlternatingMap R M N ι)
@[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₂)
:
LinearEquiv.symm (AlternatingMap.domLCongr R N ι S e) = AlternatingMap.domLCongr R N ι S (LinearEquiv.symm e)
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₃)
:
LinearEquiv.trans (AlternatingMap.domLCongr R N ι S e) (AlternatingMap.domLCongr R N ι S f) = AlternatingMap.domLCongr R N ι S (LinearEquiv.trans e f)
@[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 : AlternatingMap R M N ι)
(g : M₂ ≃ₗ[R] M)
:
AlternatingMap.compLinearMap f ↑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 #
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 : AlternatingMap R M N ι)
{α : Type u_12}
[DecidableEq ι]
(t : Finset α)
(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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
{ι : Type u_7}
(f : AlternatingMap R M N ι)
(v : ι → M)
[DecidableEq ι]
{i : ι}
{j : ι}
(hij : i ≠ j)
:
↑f (Function.update v i (v j)) = 0
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 : AlternatingMap R M N ι)
(v : ι → M)
[DecidableEq ι]
{i : ι}
{j : ι}
(hij : i ≠ j)
(m : M)
:
↑f (Function.update (Function.update v i m) j m) = 0
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 : AlternatingMap R M N ι)
(v : ι → M)
[DecidableEq ι]
{i : ι}
{j : ι}
(hij : i ≠ j)
:
↑f (v ∘ ↑(Equiv.swap i j)) + ↑f v = 0
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 : AlternatingMap R M N ι)
(v : ι → M)
[DecidableEq ι]
{i : ι}
{j : ι}
(hij : i ≠ j)
:
↑f v + ↑f (v ∘ ↑(Equiv.swap i j)) = 0
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 : AlternatingMap R M N' ι)
(v : ι → M)
[DecidableEq ι]
{i : ι}
{j : ι}
(hij : i ≠ j)
:
↑g (v ∘ ↑(Equiv.swap i j)) = -↑g v
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 : AlternatingMap R M N' ι)
[DecidableEq ι]
[Fintype ι]
(v : ι → M)
(σ : Equiv.Perm ι)
:
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 : AlternatingMap R M N' ι)
(v : ι → M)
[DecidableEq ι]
[Fintype ι]
(σ : Equiv.Perm ι)
:
@[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 : AlternatingMap R M N ι)
(v : ι' → M)
:
↑(AlternatingMap.domDomCongr σ f) v = ↑f (v ∘ ↑σ)
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 : 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}
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
{ι : Type u_7}
(f : AlternatingMap R M N ι)
:
AlternatingMap.domDomCongr (Equiv.refl ι) f = f
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 : AlternatingMap R M N ι)
:
AlternatingMap.domDomCongr (σ₁.trans σ₂) f = AlternatingMap.domDomCongr σ₂ (AlternatingMap.domDomCongr σ₁ f)
@[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}
(σ : ι ≃ ι')
:
AlternatingMap.domDomCongr σ 0 = 0
@[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 : AlternatingMap R M N ι)
(g : AlternatingMap R M N ι)
:
AlternatingMap.domDomCongr σ (f + g) = AlternatingMap.domDomCongr σ f + AlternatingMap.domDomCongr σ g
@[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 : AlternatingMap R M N ι)
:
AlternatingMap.domDomCongr σ (c • f) = c • AlternatingMap.domDomCongr σ f
@[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 : AlternatingMap R M N ι)
:
@[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 : AlternatingMap R M N ι')
:
↑(AddEquiv.symm (AlternatingMap.domDomCongrEquiv σ)) f = AlternatingMap.domDomCongr σ.symm f
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}
(σ : ι ≃ ι')
:
AlternatingMap R M N ι ≃+ AlternatingMap R M N ι'
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}
[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 : AlternatingMap R M N ι')
:
↑(LinearEquiv.symm (AlternatingMap.domDomLcongr S σ)) f = AlternatingMap.domDomCongr σ.symm f
@[simp]
theorem
AlternatingMap.domDomLcongr_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 : AlternatingMap R M N ι)
:
↑(AlternatingMap.domDomLcongr S σ) f = AlternatingMap.domDomCongr σ f
def
AlternatingMap.domDomLcongr
{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]
(σ : ι ≃ ι')
:
AlternatingMap R M N ι ≃ₗ[S] AlternatingMap R M N ι'
alternating_map.dom_dom_congr as a linear equivalence.
Instances For
@[simp]
theorem
AlternatingMap.domDomLcongr_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]
:
AlternatingMap.domDomLcongr S (Equiv.refl ι) = LinearEquiv.refl S (AlternatingMap R M N ι)
@[simp]
theorem
AlternatingMap.domDomLcongr_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]
(σ : ι ≃ ι')
:
@[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 : AlternatingMap R M N ι)
(g : AlternatingMap R M N ι)
:
AlternatingMap.domDomCongr σ f = AlternatingMap.domDomCongr σ g ↔ 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}
[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 : AlternatingMap R M N ι)
:
AlternatingMap.domDomCongr σ f = 0 ↔ f = 0
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 : AlternatingMap R M N' ι)
[Fintype ι]
[DecidableEq ι]
(σ : Equiv.Perm ι)
:
AlternatingMap.domDomCongr σ g = ↑Equiv.Perm.sign σ • g
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 : AlternatingMap R M N ι)
(σ : ι ≃ ι')
:
↑(AlternatingMap.domDomCongr σ f) = MultilinearMap.domDomCongr σ ↑f
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 : AlternatingMap K M N ι)
(v : ι → M)
(h : ¬LinearIndependent K v)
:
↑f v = 0
If the arguments are linearly dependent then the result is 0.
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 : AlternatingMap R M N (Fin (Nat.succ n)))
(m : Fin n → M)
(x : M)
(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.
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 : AlternatingMap R M N (Fin (Nat.succ 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.
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' →+ 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}
[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')
:
↑(↑MultilinearMap.alternatization m) = ↑(Finset.sum Finset.univ fun σ => ↑Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m)
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')
:
↑(↑MultilinearMap.alternatization m) = Finset.sum Finset.univ fun σ => ↑Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m
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)
:
↑(↑MultilinearMap.alternatization m) v = Finset.sum Finset.univ fun σ => ↑Equiv.Perm.sign σ • ↑(MultilinearMap.domDomCongr σ m) v
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 : AlternatingMap R M N' ι)
:
↑MultilinearMap.alternatization ↑a = Nat.factorial (Fintype.card ι) • 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}
[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 (LinearMap.compMultilinearMap g f) = ↑(LinearMap.compAlternatingMap g) (↑MultilinearMap.alternatization f)
Composition with a linear map before and after alternatization are equivalent.
@[inline, reducible]
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 : α ⊕ β)
:
Function.Involutive (SMul.smul (Equiv.swap 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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
(σ : Equiv.Perm.ModSumCongr ιa ι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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
(σ : Equiv.Perm (ιa ⊕ ιb))
:
AlternatingMap.domCoprod.summand a b (Quotient.mk'' σ) = ↑Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ (MultilinearMap.domCoprod ↑a ↑b)
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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
(σ : Equiv.Perm.ModSumCongr ιa ιb)
{v : ιa ⊕ ιb → Mᵢ}
{i : ιa ⊕ ιb}
{j : ιa ⊕ ιb}
(hv : v i = v j)
(hij : i ≠ j)
:
↑(AlternatingMap.domCoprod.summand a b σ) v + ↑(AlternatingMap.domCoprod.summand a b (Equiv.swap i j • σ)) 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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
(σ : Equiv.Perm.ModSumCongr ιa ιb)
{v : ιa ⊕ ιb → Mᵢ}
{i : ιa ⊕ ιb}
{j : ιa ⊕ ιb}
(hv : v i = v j)
(hij : i ≠ j)
:
Equiv.swap i j • σ = σ → ↑(AlternatingMap.domCoprod.summand a b σ) 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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
(v : ιa ⊕ ιb → Mᵢ)
:
↑(AlternatingMap.domCoprod a b) v = ↑(Finset.sum Finset.univ fun σ => AlternatingMap.domCoprod.summand a b σ) 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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
:
↑(AlternatingMap.domCoprod a b) = Finset.sum Finset.univ fun σ => AlternatingMap.domCoprod.summand a b σ
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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
:
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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
:
↑AlternatingMap.domCoprod' (a ⊗ₜ[R'] b) = AlternatingMap.domCoprod a 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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(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 • MultilinearMap.domCoprod (MultilinearMap.domDomCongr σa a) (MultilinearMap.domDomCongr σb 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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : MultilinearMap R' (fun x => Mᵢ) N₁)
(b : MultilinearMap R' (fun x => Mᵢ) N₂)
:
↑MultilinearMap.alternatization (MultilinearMap.domCoprod a b) = 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}
[CommSemiring R']
[AddCommGroup N₁]
[Module R' N₁]
[AddCommGroup N₂]
[Module R' N₂]
[AddCommMonoid Mᵢ]
[Module R' Mᵢ]
[DecidableEq ιa]
[DecidableEq ιb]
(a : AlternatingMap R' Mᵢ N₁ ιa)
(b : AlternatingMap R' Mᵢ N₂ ιb)
:
↑MultilinearMap.alternatization (MultilinearMap.domCoprod ↑a ↑b) = (Nat.factorial (Fintype.card ιa) * Nat.factorial (Fintype.card ιb)) • AlternatingMap.domCoprod a b
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}
[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 : AlternatingMap R' N₁ N₂ ι}
{g : AlternatingMap R' N₁ 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.
Currying #
@[simp]
theorem
AlternatingMap.curryLeft_apply_apply
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
(m : M'')
(v : Fin n → M'')
:
↑(↑(AlternatingMap.curryLeft f) m) v = ↑f (Matrix.vecCons m v)
def
AlternatingMap.curryLeft
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
:
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}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
:
@[simp]
theorem
AlternatingMap.curryLeft_add
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
(g : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
:
@[simp]
theorem
AlternatingMap.curryLeft_smul
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
(r : R')
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
:
AlternatingMap.curryLeft (r • f) = r • AlternatingMap.curryLeft f
@[simp]
theorem
AlternatingMap.curryLeftLinearMap_apply
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
:
↑AlternatingMap.curryLeftLinearMap f = AlternatingMap.curryLeft f
def
AlternatingMap.curryLeftLinearMap
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
:
AlternatingMap R' M'' N'' (Fin (Nat.succ n)) →ₗ[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}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
{n : ℕ}
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ (Nat.succ n))))
(m : M'')
:
↑(AlternatingMap.curryLeft (↑(AlternatingMap.curryLeft f) 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}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[AddCommMonoid N₂'']
[Module R' M'']
[Module R' N'']
[Module R' N₂'']
{n : ℕ}
(g : N'' →ₗ[R'] N₂'')
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
(m : M'')
:
↑(AlternatingMap.curryLeft (↑(LinearMap.compAlternatingMap g) f)) m = ↑(LinearMap.compAlternatingMap g) (↑(AlternatingMap.curryLeft f) m)
@[simp]
theorem
AlternatingMap.curryLeft_compLinearMap
{R' : Type u_10}
{M'' : Type u_11}
{M₂'' : Type u_12}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid M₂'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' M₂'']
[Module R' N'']
{n : ℕ}
(g : M₂'' →ₗ[R'] M'')
(f : AlternatingMap R' M'' N'' (Fin (Nat.succ n)))
(m : M₂'')
:
↑(AlternatingMap.curryLeft (AlternatingMap.compLinearMap f g)) m = AlternatingMap.compLinearMap (↑(AlternatingMap.curryLeft f) (↑g m)) g
@[simp]
theorem
AlternatingMap.constLinearEquivOfIsEmpty_apply
{ι : Type u_7}
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
[IsEmpty ι]
(m : N'')
:
↑AlternatingMap.constLinearEquivOfIsEmpty m = AlternatingMap.constOfIsEmpty R' M'' ι m
@[simp]
theorem
AlternatingMap.constLinearEquivOfIsEmpty_symm_apply
{ι : Type u_7}
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
[IsEmpty ι]
(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}
[CommSemiring R']
[AddCommMonoid M'']
[AddCommMonoid N'']
[Module R' M'']
[Module R' N'']
[IsEmpty ι]
:
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.