Alternating Maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We construct the bundled function alternating_map, which extends multilinear_map with all the
arguments of the same type.
Main definitions #
alternating_map R M N ιis the space 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
add_comm_monoid,add_comm_group, andmodulestructure overalternating_maps that matches the definitions overmultilinear_maps. multilinear_map.dom_dom_congr, for permutating the elements within a family.multilinear_map.alternatization, which makes an alternating map out of a non-alternating one.alternating_map.dom_coprod, which behaves as a product between two alternating maps.alternating_map.curry_left, for binding the leftmost argument of an alternating map indexed byfin n.succ.
Implementation notes #
alternating_map is defined in terms of map_eq_zero_of_eq, as this is easier to work with than
using map_swap as a definition, and does not require has_neg N.
alternating_maps are provided with a coercion to multilinear_map, along with a set of
norm_cast lemmas that act on the algebraic structure:
def
alternating_map.to_multilinear_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(self : alternating_map R M N ι) :
multilinear_map R (λ (i : ι), M) N
The multilinear map associated to an alternating map
structure
alternating_map
(R : Type u_1)
[semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
(N : Type u_3)
[add_comm_monoid N]
[module R N]
(ι : Type u_7) :
Type (max u_2 u_3 u_7)
- to_fun : (Π (i : ι), (λ (i : ι), M) i) → N
- map_add' : ∀ [_inst_1_1 : decidable_eq ι] (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), self.to_fun (function.update m i (x + y)) = self.to_fun (function.update m i x) + self.to_fun (function.update m i y)
- map_smul' : ∀ [_inst_1_1 : decidable_eq ι] (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), self.to_fun (function.update m i (c • x)) = c • self.to_fun (function.update m i x)
- map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → self.to_fun v = 0
An alternating map is a multilinear map that vanishes when two of its arguments are equal.
Instances for alternating_map
- alternating_map.has_sizeof_inst
- alternating_map.fun_like
- alternating_map.has_coe_to_fun
- alternating_map.multilinear_map.has_coe
- alternating_map.has_smul
- alternating_map.is_central_scalar
- alternating_map.has_add
- alternating_map.has_zero
- alternating_map.inhabited
- alternating_map.add_comm_monoid
- alternating_map.has_neg
- alternating_map.has_sub
- alternating_map.add_comm_group
- alternating_map.distrib_mul_action
- alternating_map.module
- alternating_map.no_zero_smul_divisors
Basic coercion simp lemmas, largely copied from ring_hom and multilinear_map
@[protected, instance]
def
alternating_map.fun_like
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
fun_like (alternating_map R M N ι) (ι → M) (λ (_x : ι → M), N)
Equations
@[protected, instance]
def
alternating_map.has_coe_to_fun
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
has_coe_to_fun (alternating_map R M N ι) (λ (_x : alternating_map R M N ι), (ι → M) → N)
Equations
@[simp]
theorem
alternating_map.to_fun_eq_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι) :
@[simp]
theorem
alternating_map.coe_mk
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : (ι → M) → N)
(h₁ : ∀ [_inst_1 : decidable_eq ι] (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), f (function.update m i (x + y)) = f (function.update m i x) + f (function.update m i y))
(h₂ : ∀ [_inst_1_1 : decidable_eq ι] (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), f (function.update m i (c • x)) = c • f (function.update m i x))
(h₃ : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0) :
theorem
alternating_map.congr_fun
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{f g : alternating_map R M N ι}
(h : f = g)
(x : ι → M) :
theorem
alternating_map.congr_arg
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
{x y : ι → M}
(h : x = y) :
theorem
alternating_map.coe_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
@[simp, norm_cast]
theorem
alternating_map.coe_inj
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{f g : alternating_map R M N ι} :
@[ext]
theorem
alternating_map.ext
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{f f' : alternating_map R M N ι}
(H : ∀ (x : ι → M), ⇑f x = ⇑f' x) :
f = f'
theorem
alternating_map.ext_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{f g : alternating_map R M N ι} :
@[protected, instance]
def
alternating_map.multilinear_map.has_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
has_coe (alternating_map R M N ι) (multilinear_map R (λ (i : ι), M) N)
Equations
- alternating_map.multilinear_map.has_coe = {coe := λ (x : alternating_map R M N ι), x.to_multilinear_map}
@[simp, norm_cast]
theorem
alternating_map.coe_multilinear_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι) :
theorem
alternating_map.coe_multilinear_map_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
@[simp]
theorem
alternating_map.to_multilinear_map_eq_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι) :
f.to_multilinear_map = ↑f
@[simp]
theorem
alternating_map.coe_multilinear_map_mk
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : (ι → M) → N)
(h₁ : ∀ [_inst_1 : decidable_eq ι] (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (x y : (λ (i : ι), M) i), f (function.update m i (x + y)) = f (function.update m i x) + f (function.update m i y))
(h₂ : ∀ [_inst_1_1 : decidable_eq ι] (m : Π (i : ι), (λ (i : ι), M) i) (i : ι) (c : R) (x : (λ (i : ι), M) i), f (function.update m i (c • x)) = c • f (function.update m i x))
(h₃ : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0) :
Simp-normal forms of the structure fields #
These are expressed in terms of ⇑f instead of f.to_fun.
@[simp]
theorem
alternating_map.map_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
[decidable_eq ι]
(i : ι)
(x y : M) :
⇑f (function.update v i (x + y)) = ⇑f (function.update v i x) + ⇑f (function.update v i y)
@[simp]
theorem
alternating_map.map_sub
{R : Type u_1}
[semiring R]
{M' : Type u_5}
[add_comm_group M']
[module R M']
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g' : alternating_map R M' N' ι)
(v' : ι → M')
[decidable_eq ι]
(i : ι)
(x y : M') :
⇑g' (function.update v' i (x - y)) = ⇑g' (function.update v' i x) - ⇑g' (function.update v' i y)
@[simp]
theorem
alternating_map.map_neg
{R : Type u_1}
[semiring R]
{M' : Type u_5}
[add_comm_group M']
[module R M']
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g' : alternating_map R M' N' ι)
(v' : ι → M')
[decidable_eq ι]
(i : ι)
(x : M') :
⇑g' (function.update v' i (-x)) = -⇑g' (function.update v' i x)
@[simp]
theorem
alternating_map.map_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
[decidable_eq ι]
(i : ι)
(r : R)
(x : M) :
⇑f (function.update v i (r • x)) = r • ⇑f (function.update v i x)
@[simp]
theorem
alternating_map.map_eq_zero_of_eq
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
{i j : ι}
(h : v i = v j)
(hij : i ≠ j) :
theorem
alternating_map.map_coord_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
{m : ι → M}
(i : ι)
(h : m i = 0) :
@[simp]
theorem
alternating_map.map_update_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
[decidable_eq ι]
(m : ι → M)
(i : ι) :
⇑f (function.update m i 0) = 0
@[simp]
theorem
alternating_map.map_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
[nonempty ι] :
theorem
alternating_map.map_eq_zero_of_not_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
(hv : ¬function.injective v) :
Algebraic structure inherited from multilinear_map #
alternating_map carries the same add_comm_monoid, add_comm_group, and module structure
as multilinear_map
@[protected, instance]
def
alternating_map.has_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{S : Type u_10}
[monoid S]
[distrib_mul_action S N]
[smul_comm_class R S N] :
has_smul S (alternating_map R M N ι)
Equations
- alternating_map.has_smul = {smul := λ (c : S) (f : alternating_map R M N ι), {to_fun := (c • ↑f).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}}
@[simp]
theorem
alternating_map.smul_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
{S : Type u_10}
[monoid S]
[distrib_mul_action S N]
[smul_comm_class R S N]
(c : S)
(m : ι → M) :
@[norm_cast]
theorem
alternating_map.coe_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
{S : Type u_10}
[monoid S]
[distrib_mul_action S N]
[smul_comm_class R S N]
(c : S) :
theorem
alternating_map.coe_fn_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{S : Type u_10}
[monoid S]
[distrib_mul_action S N]
[smul_comm_class R S N]
(c : S)
(f : alternating_map R M N ι) :
@[protected, instance]
def
alternating_map.is_central_scalar
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{S : Type u_10}
[monoid S]
[distrib_mul_action S N]
[smul_comm_class R S N]
[distrib_mul_action Sᵐᵒᵖ N]
[is_central_scalar S N] :
is_central_scalar S (alternating_map R M N ι)
@[simp]
theorem
alternating_map.prod_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{P : Type u_4}
[add_comm_monoid P]
[module R P]
{ι : Type u_7}
(f : alternating_map R M N ι)
(g : alternating_map R M P ι)
(ᾰ : Π (i : ι), (λ (i : ι), M) i) :
def
alternating_map.prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{P : Type u_4}
[add_comm_monoid P]
[module R P]
{ι : Type u_7}
(f : alternating_map R M N ι)
(g : alternating_map R M P ι) :
alternating_map R M (N × P) ι
The cartesian product of two alternating maps, as a multilinear map.
Equations
- f.prod g = {to_fun := (f.to_multilinear_map.prod g.to_multilinear_map).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
@[simp]
theorem
alternating_map.coe_prod
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{P : Type u_4}
[add_comm_monoid P]
[module R P]
{ι : Type u_7}
(f : alternating_map R M N ι)
(g : alternating_map R M P ι) :
@[simp]
theorem
alternating_map.pi_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{ι : Type u_7}
{ι' : Type u_3}
{N : ι' → Type u_4}
[Π (i : ι'), add_comm_monoid (N i)]
[Π (i : ι'), module R (N i)]
(f : Π (i : ι'), alternating_map R M (N i) ι)
(ᾰ : Π (i : ι), (λ (i : ι), M) i)
(i : ι') :
⇑(alternating_map.pi f) ᾰ i = ⇑(f i) ᾰ
def
alternating_map.pi
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{ι : Type u_7}
{ι' : Type u_3}
{N : ι' → Type u_4}
[Π (i : ι'), add_comm_monoid (N i)]
[Π (i : ι'), module R (N i)]
(f : Π (i : ι'), alternating_map R M (N i) ι) :
alternating_map 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.
Equations
- alternating_map.pi f = {to_fun := (multilinear_map.pi (λ (a : ι'), (f a).to_multilinear_map)).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
@[simp]
theorem
alternating_map.coe_pi
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{ι : Type u_7}
{ι' : Type u_3}
{N : ι' → Type u_4}
[Π (i : ι'), add_comm_monoid (N i)]
[Π (i : ι'), module R (N i)]
(f : Π (i : ι'), alternating_map R M (N i) ι) :
↑(alternating_map.pi f) = multilinear_map.pi (λ (a : ι'), ↑(f a))
@[simp]
theorem
alternating_map.smul_right_apply
{R : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{ι : Type u_4}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(f : alternating_map R M₁ R ι)
(z : M₂)
(ᾰ : Π (i : ι), (λ (i : ι), M₁) i) :
⇑(f.smul_right z) ᾰ = ⇑f ᾰ • z
def
alternating_map.smul_right
{R : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{ι : Type u_4}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(f : alternating_map R M₁ R ι)
(z : M₂) :
alternating_map 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.
Equations
- f.smul_right z = {to_fun := (f.to_multilinear_map.smul_right z).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
@[simp]
theorem
alternating_map.coe_smul_right
{R : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{ι : Type u_4}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(f : alternating_map R M₁ R ι)
(z : M₂) :
↑(f.smul_right z) = ↑f.smul_right z
@[protected, instance]
def
alternating_map.has_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
has_add (alternating_map R M N ι)
Equations
- alternating_map.has_add = {add := λ (a b : alternating_map R M N ι), {to_fun := (↑a + ↑b).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}}
@[simp]
theorem
alternating_map.add_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f f' : alternating_map R M N ι)
(v : ι → M) :
@[norm_cast]
theorem
alternating_map.coe_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f f' : alternating_map R M N ι) :
@[protected, instance]
def
alternating_map.has_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
has_zero (alternating_map R M N ι)
Equations
- alternating_map.has_zero = {zero := {to_fun := 0.to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}}
@[simp]
theorem
alternating_map.zero_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(v : ι → M) :
@[norm_cast]
theorem
alternating_map.coe_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
@[protected, instance]
def
alternating_map.inhabited
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
inhabited (alternating_map R M N ι)
Equations
@[protected, instance]
def
alternating_map.add_comm_monoid
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7} :
add_comm_monoid (alternating_map R M N ι)
Equations
- alternating_map.add_comm_monoid = function.injective.add_comm_monoid coe_fn alternating_map.coe_injective alternating_map.add_comm_monoid._proof_2 alternating_map.add_comm_monoid._proof_3 alternating_map.add_comm_monoid._proof_4
@[protected, instance]
def
alternating_map.has_neg
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7} :
has_neg (alternating_map R M N' ι)
Equations
- alternating_map.has_neg = {neg := λ (f : alternating_map R M N' ι), {to_fun := (-↑f).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}}
@[simp]
theorem
alternating_map.neg_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g : alternating_map R M N' ι)
(m : ι → M) :
@[norm_cast]
theorem
alternating_map.coe_neg
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g : alternating_map R M N' ι) :
@[protected, instance]
def
alternating_map.has_sub
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7} :
has_sub (alternating_map R M N' ι)
Equations
- alternating_map.has_sub = {sub := λ (f g : alternating_map R M N' ι), {to_fun := (↑f - ↑g).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}}
@[simp]
theorem
alternating_map.sub_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g g₂ : alternating_map R M N' ι)
(m : ι → M) :
@[norm_cast]
theorem
alternating_map.coe_sub
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g g₂ : alternating_map R M N' ι) :
@[protected, instance]
def
alternating_map.add_comm_group
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7} :
add_comm_group (alternating_map R M N' ι)
Equations
- alternating_map.add_comm_group = function.injective.add_comm_group coe_fn alternating_map.add_comm_group._proof_3 alternating_map.add_comm_group._proof_4 alternating_map.add_comm_group._proof_5 alternating_map.add_comm_group._proof_6 alternating_map.add_comm_group._proof_7 alternating_map.add_comm_group._proof_8 alternating_map.add_comm_group._proof_9
@[protected, instance]
def
alternating_map.distrib_mul_action
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{S : Type u_10}
[monoid S]
[distrib_mul_action S N]
[smul_comm_class R S N] :
distrib_mul_action S (alternating_map R M N ι)
Equations
- alternating_map.distrib_mul_action = {to_mul_action := {to_has_smul := alternating_map.has_smul _inst_14, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}
@[protected, instance]
def
alternating_map.module
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{S : Type u_10}
[semiring S]
[module S N]
[smul_comm_class R S N] :
module S (alternating_map R M N ι)
The space of multilinear maps over an algebra over R is a module over R, for the pointwise
addition and scalar multiplication.
Equations
- alternating_map.module = {to_distrib_mul_action := alternating_map.distrib_mul_action _inst_14, add_smul := _, zero_smul := _}
@[protected, instance]
def
alternating_map.no_zero_smul_divisors
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{S : Type u_10}
[semiring S]
[module S N]
[smul_comm_class R S N]
[no_zero_smul_divisors S N] :
no_zero_smul_divisors S (alternating_map R M N ι)
@[simp]
theorem
alternating_map.of_subsingleton_apply
(R : Type u_1)
[semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
{ι : Type u_7}
[subsingleton ι]
(i : ι)
(f : Π (x : ι), (λ (i : ι), (λ (i : ι), M) i) x) :
⇑(alternating_map.of_subsingleton R M i) f = function.eval i f
def
alternating_map.of_subsingleton
(R : Type u_1)
[semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
{ι : Type u_7}
[subsingleton ι]
(i : ι) :
alternating_map R M M ι
The evaluation map from ι → M to M at a given i is alternating when ι is subsingleton.
Equations
- alternating_map.of_subsingleton R M i = {to_fun := function.eval i, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
def
alternating_map.const_of_is_empty
(R : Type u_1)
[semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
(ι : Type u_7)
[is_empty ι]
(m : N) :
alternating_map R M N ι
The constant map is alternating when ι is empty.
Equations
- alternating_map.const_of_is_empty R M ι m = {to_fun := function.const (Π (i : ι), (λ (i : ι), M) i) m, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
@[simp]
theorem
alternating_map.const_of_is_empty_apply
(R : Type u_1)
[semiring R]
(M : Type u_2)
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
(ι : Type u_7)
[is_empty ι]
(m : N) :
⇑(alternating_map.const_of_is_empty R M ι m) = function.const (Π (i : ι), (λ (i : ι), M) i) m
@[simp]
theorem
alternating_map.cod_restrict_apply_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(p : submodule R N)
(h : ∀ (v : ι → M), ⇑f v ∈ p)
(v : Π (i : ι), (λ (i : ι), M) i) :
↑(⇑(f.cod_restrict p h) v) = ⇑f v
def
alternating_map.cod_restrict
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(p : submodule R N)
(h : ∀ (v : ι → M), ⇑f v ∈ p) :
alternating_map R M ↥p ι
Restrict the codomain of an alternating map to a submodule.
Equations
- f.cod_restrict p h = {to_fun := λ (v : Π (i : ι), (λ (i : ι), M) i), ⟨⇑f v, _⟩, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
Composition with linear maps #
def
linear_map.comp_alternating_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{N₂ : Type u_10}
[add_comm_monoid N₂]
[module R N₂]
(g : N →ₗ[R] N₂) :
alternating_map R M N ι →+ alternating_map R M N₂ ι
Composing a alternating map with a linear map on the left gives again an alternating map.
Equations
- g.comp_alternating_map = {to_fun := λ (f : alternating_map R M N ι), {to_fun := (g.comp_multilinear_map ↑f).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}, map_zero' := _, map_add' := _}
@[simp]
theorem
linear_map.coe_comp_alternating_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{N₂ : Type u_10}
[add_comm_monoid N₂]
[module R N₂]
(g : N →ₗ[R] N₂)
(f : alternating_map R M N ι) :
@[simp]
theorem
linear_map.comp_alternating_map_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{N₂ : Type u_10}
[add_comm_monoid N₂]
[module R N₂]
(g : N →ₗ[R] N₂)
(f : alternating_map R M N ι)
(m : ι → M) :
theorem
linear_map.smul_right_eq_comp
{R : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{ι : Type u_4}
[comm_semiring R]
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(f : alternating_map R M₁ R ι)
(z : M₂) :
f.smul_right z = ⇑((linear_map.id.smul_right z).comp_alternating_map) f
@[simp]
theorem
linear_map.subtype_comp_alternating_map_cod_restrict
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(p : submodule R N)
(h : ∀ (v : ι → M), ⇑f v ∈ p) :
⇑(p.subtype.comp_alternating_map) (f.cod_restrict p h) = f
@[simp]
theorem
linear_map.comp_alternating_map_cod_restrict
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{N₂ : Type u_10}
[add_comm_monoid N₂]
[module R N₂]
(g : N →ₗ[R] N₂)
(f : alternating_map R M N ι)
(p : submodule R N₂)
(h : ∀ (c : N), ⇑g c ∈ p) :
⇑((linear_map.cod_restrict p g h).comp_alternating_map) f = (⇑(g.comp_alternating_map) f).cod_restrict p _
def
alternating_map.comp_linear_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(f : alternating_map R M N ι)
(g : M₂ →ₗ[R] M) :
alternating_map R M₂ N ι
Composing a alternating map with the same linear map on each argument gives again an alternating map.
Equations
- f.comp_linear_map g = {to_fun := (↑f.comp_linear_map (λ (_x : ι), g)).to_fun, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
theorem
alternating_map.coe_comp_linear_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(f : alternating_map R M N ι)
(g : M₂ →ₗ[R] M) :
⇑(f.comp_linear_map g) = ⇑f ∘ function.comp ⇑g
@[simp]
theorem
alternating_map.comp_linear_map_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(f : alternating_map R M N ι)
(g : M₂ →ₗ[R] M)
(v : ι → M₂) :
⇑(f.comp_linear_map g) v = ⇑f (λ (i : ι), ⇑g (v i))
theorem
alternating_map.comp_linear_map_assoc
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
{M₃ : Type u_11}
[add_comm_monoid M₃]
[module R M₃]
(f : alternating_map R M N ι)
(g₁ : M₂ →ₗ[R] M)
(g₂ : M₃ →ₗ[R] M₂) :
(f.comp_linear_map g₁).comp_linear_map g₂ = f.comp_linear_map (g₁.comp g₂)
Composing an alternating map twice with the same linear map in each argument is the same as composing with their composition.
@[simp]
theorem
alternating_map.zero_comp_linear_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(g : M₂ →ₗ[R] M) :
0.comp_linear_map g = 0
@[simp]
theorem
alternating_map.add_comp_linear_map
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(f₁ f₂ : alternating_map R M N ι)
(g : M₂ →ₗ[R] M) :
(f₁ + f₂).comp_linear_map g = f₁.comp_linear_map g + f₂.comp_linear_map g
@[simp]
theorem
alternating_map.comp_linear_map_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
[nonempty ι]
(f : alternating_map R M N ι) :
f.comp_linear_map 0 = 0
@[simp]
theorem
alternating_map.comp_linear_map_id
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι) :
Composing an alternating map with the identity linear map in each argument.
theorem
alternating_map.comp_linear_map_injective
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(f : M₂ →ₗ[R] M)
(hf : function.surjective ⇑f) :
function.injective (λ (g : alternating_map R M N ι), g.comp_linear_map f)
Composing with a surjective linear map is injective.
theorem
alternating_map.comp_linear_map_inj
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(f : M₂ →ₗ[R] M)
(hf : function.surjective ⇑f)
(g₁ g₂ : alternating_map R M N ι) :
g₁.comp_linear_map f = g₂.comp_linear_map f ↔ g₁ = g₂
def
alternating_map.dom_lcongr
(R : Type u_1)
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(N : Type u_3)
[add_comm_monoid N]
[module R N]
(ι : Type u_7)
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(e : M ≃ₗ[R] M₂) :
alternating_map R M N ι ≃ₗ[S] alternating_map R M₂ N ι
Construct a linear equivalence between maps from a linear equivalence between domains.
Equations
- alternating_map.dom_lcongr R N ι S e = {to_fun := λ (f : alternating_map R M N ι), f.comp_linear_map ↑(e.symm), map_add' := _, map_smul' := _, inv_fun := λ (g : alternating_map R M₂ N ι), g.comp_linear_map ↑e, left_inv := _, right_inv := _}
@[simp]
theorem
alternating_map.dom_lcongr_apply
(R : Type u_1)
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(N : Type u_3)
[add_comm_monoid N]
[module R N]
(ι : Type u_7)
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(e : M ≃ₗ[R] M₂)
(f : alternating_map R M N ι) :
⇑(alternating_map.dom_lcongr R N ι S e) f = f.comp_linear_map ↑(e.symm)
@[simp]
theorem
alternating_map.dom_lcongr_refl
(R : Type u_1)
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(N : Type u_3)
[add_comm_monoid N]
[module R N]
(ι : Type u_7)
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N] :
alternating_map.dom_lcongr R N ι S (linear_equiv.refl R M) = linear_equiv.refl S (alternating_map R M N ι)
@[simp]
theorem
alternating_map.dom_lcongr_symm
(R : Type u_1)
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(N : Type u_3)
[add_comm_monoid N]
[module R N]
(ι : Type u_7)
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(e : M ≃ₗ[R] M₂) :
(alternating_map.dom_lcongr R N ι S e).symm = alternating_map.dom_lcongr R N ι S e.symm
theorem
alternating_map.dom_lcongr_trans
(R : Type u_1)
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
(N : Type u_3)
[add_comm_monoid N]
[module R N]
(ι : Type u_7)
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
{M₃ : Type u_11}
[add_comm_monoid M₃]
[module R M₃]
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(e : M ≃ₗ[R] M₂)
(f : M₂ ≃ₗ[R] M₃) :
(alternating_map.dom_lcongr R N ι S e).trans (alternating_map.dom_lcongr R N ι S f) = alternating_map.dom_lcongr R N ι S (e.trans f)
@[simp]
theorem
alternating_map.comp_linear_equiv_eq_zero_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{M₂ : Type u_10}
[add_comm_monoid M₂]
[module R M₂]
(f : alternating_map R M N ι)
(g : M₂ ≃ₗ[R] M) :
f.comp_linear_map ↑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 multilinear_map #
theorem
alternating_map.map_update_sum
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
{α : Type u_4}
[decidable_eq ι]
(t : finset α)
(i : ι)
(g : α → M)
(m : ι → M) :
⇑f (function.update m i (t.sum (λ (a : α), g a))) = t.sum (λ (a : α), ⇑f (function.update m i (g a)))
Theorems specific to alternating maps #
Various properties of reordered and repeated inputs which follow from
alternating_map.map_eq_zero_of_eq.
theorem
alternating_map.map_update_self
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
[decidable_eq ι]
{i j : ι}
(hij : i ≠ j) :
⇑f (function.update v i (v j)) = 0
theorem
alternating_map.map_update_update
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
[decidable_eq ι]
{i j : ι}
(hij : i ≠ j)
(m : M) :
⇑f (function.update (function.update v i m) j m) = 0
theorem
alternating_map.map_swap_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
[decidable_eq ι]
{i j : ι}
(hij : i ≠ j) :
theorem
alternating_map.map_add_swap
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι)
(v : ι → M)
[decidable_eq ι]
{i j : ι}
(hij : i ≠ j) :
theorem
alternating_map.map_swap
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g : alternating_map R M N' ι)
(v : ι → M)
[decidable_eq ι]
{i j : ι}
(hij : i ≠ j) :
theorem
alternating_map.map_perm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g : alternating_map R M N' ι)
[decidable_eq ι]
[fintype ι]
(v : ι → M)
(σ : equiv.perm ι) :
theorem
alternating_map.map_congr_perm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g : alternating_map R M N' ι)
(v : ι → M)
[decidable_eq ι]
[fintype ι]
(σ : equiv.perm ι) :
@[simp]
theorem
alternating_map.dom_dom_congr_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι')
(f : alternating_map R M N ι)
(v : Π (i : ι'), (λ (i : ι'), M) i) :
def
alternating_map.dom_dom_congr
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι')
(f : alternating_map R M N ι) :
alternating_map R M N ι'
Transfer the arguments to a map along an equivalence between argument indices.
This is the alternating version of multilinear_map.dom_dom_congr.
@[simp]
theorem
alternating_map.dom_dom_congr_refl
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(f : alternating_map R M N ι) :
alternating_map.dom_dom_congr (equiv.refl ι) f = f
theorem
alternating_map.dom_dom_congr_trans
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
{ι'' : Type u_9}
(σ₁ : ι ≃ ι')
(σ₂ : ι' ≃ ι'')
(f : alternating_map R M N ι) :
alternating_map.dom_dom_congr (σ₁.trans σ₂) f = alternating_map.dom_dom_congr σ₂ (alternating_map.dom_dom_congr σ₁ f)
@[simp]
theorem
alternating_map.dom_dom_congr_zero
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι') :
@[simp]
theorem
alternating_map.dom_dom_congr_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι')
(f g : alternating_map R M N ι) :
@[simp]
theorem
alternating_map.dom_dom_congr_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
{S : Type u_4}
[monoid S]
[distrib_mul_action S N]
[smul_comm_class R S N]
(σ : ι ≃ ι')
(c : S)
(f : alternating_map R M N ι) :
alternating_map.dom_dom_congr σ (c • f) = c • alternating_map.dom_dom_congr σ f
@[simp]
theorem
alternating_map.dom_dom_congr_equiv_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι')
(f : alternating_map R M N ι) :
def
alternating_map.dom_dom_congr_equiv
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι') :
alternating_map R M N ι ≃+ alternating_map R M N ι'
alternating_map.dom_dom_congr as an equivalence.
This is declared separately because it does not work with dot notation.
Equations
- alternating_map.dom_dom_congr_equiv σ = {to_fun := alternating_map.dom_dom_congr σ, inv_fun := alternating_map.dom_dom_congr σ.symm, left_inv := _, right_inv := _, map_add' := _}
@[simp]
theorem
alternating_map.dom_dom_congr_equiv_symm_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι')
(f : alternating_map R M N ι') :
def
alternating_map.dom_dom_lcongr
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(σ : ι ≃ ι') :
alternating_map R M N ι ≃ₗ[S] alternating_map R M N ι'
alternating_map.dom_dom_congr as a linear equivalence.
Equations
- alternating_map.dom_dom_lcongr S σ = {to_fun := alternating_map.dom_dom_congr σ, map_add' := _, map_smul' := _, inv_fun := alternating_map.dom_dom_congr σ.symm, left_inv := _, right_inv := _}
@[simp]
theorem
alternating_map.dom_dom_lcongr_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(σ : ι ≃ ι')
(f : alternating_map R M N ι) :
@[simp]
theorem
alternating_map.dom_dom_lcongr_symm_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(σ : ι ≃ ι')
(f : alternating_map R M N ι') :
⇑((alternating_map.dom_dom_lcongr S σ).symm) f = alternating_map.dom_dom_congr σ.symm f
@[simp]
theorem
alternating_map.dom_dom_lcongr_refl
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N] :
alternating_map.dom_dom_lcongr S (equiv.refl ι) = linear_equiv.refl S (alternating_map R M N ι)
@[simp]
theorem
alternating_map.dom_dom_lcongr_to_add_equiv
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(S : Type u_12)
[semiring S]
[module S N]
[smul_comm_class R S N]
(σ : ι ≃ ι') :
@[simp]
theorem
alternating_map.dom_dom_congr_eq_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι')
(f g : alternating_map R M N ι) :
alternating_map.dom_dom_congr σ f = alternating_map.dom_dom_congr σ g ↔ f = g
The results of applying dom_dom_congr to two maps are equal if and only if those maps are.
@[simp]
theorem
alternating_map.dom_dom_congr_eq_zero_iff
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(σ : ι ≃ ι')
(f : alternating_map R M N ι) :
alternating_map.dom_dom_congr σ f = 0 ↔ f = 0
theorem
alternating_map.dom_dom_congr_perm
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
(g : alternating_map R M N' ι)
[fintype ι]
[decidable_eq ι]
(σ : equiv.perm ι) :
@[norm_cast]
theorem
alternating_map.coe_dom_dom_congr
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{ι : Type u_7}
{ι' : Type u_8}
(f : alternating_map R M N ι)
(σ : ι ≃ ι') :
theorem
alternating_map.map_linear_dependent
{ι : Type u_7}
{K : Type u_1}
[ring K]
{M : Type u_2}
[add_comm_group M]
[module K M]
{N : Type u_3}
[add_comm_group N]
[module K N]
[no_zero_smul_divisors K N]
(f : alternating_map K M N ι)
(v : ι → M)
(h : ¬linear_independent K v) :
If the arguments are linearly dependent then the result is 0.
theorem
alternating_map.map_vec_cons_add
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{n : ℕ}
(f : alternating_map R M N (fin n.succ))
(m : fin n → M)
(x y : M) :
⇑f (matrix.vec_cons (x + y) m) = ⇑f (matrix.vec_cons x m) + ⇑f (matrix.vec_cons y m)
A version of multilinear_map.cons_add for alternating_map.
theorem
alternating_map.map_vec_cons_smul
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N : Type u_3}
[add_comm_monoid N]
[module R N]
{n : ℕ}
(f : alternating_map R M N (fin n.succ))
(m : fin n → M)
(c : R)
(x : M) :
⇑f (matrix.vec_cons (c • x) m) = c • ⇑f (matrix.vec_cons x m)
A version of multilinear_map.cons_smul for alternating_map.
def
multilinear_map.alternatization
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
[fintype ι]
[decidable_eq ι] :
multilinear_map R (λ (i : ι), M) N' →+ alternating_map R M N' ι
Produce an alternating_map out of a multilinear_map, by summing over all argument
permutations.
Equations
- multilinear_map.alternatization = {to_fun := λ (m : multilinear_map R (λ (i : ι), M) N'), {to_fun := ⇑(finset.univ.sum (λ (σ : equiv.perm ι), ⇑equiv.perm.sign σ • multilinear_map.dom_dom_congr σ m)), map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}, map_zero' := _, map_add' := _}
theorem
multilinear_map.alternatization_def
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
[fintype ι]
[decidable_eq ι]
(m : multilinear_map R (λ (i : ι), M) N') :
⇑(⇑multilinear_map.alternatization m) = ⇑(finset.univ.sum (λ (σ : equiv.perm ι), ⇑equiv.perm.sign σ • multilinear_map.dom_dom_congr σ m))
theorem
multilinear_map.alternatization_coe
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
[fintype ι]
[decidable_eq ι]
(m : multilinear_map R (λ (i : ι), M) N') :
↑(⇑multilinear_map.alternatization m) = finset.univ.sum (λ (σ : equiv.perm ι), ⇑equiv.perm.sign σ • multilinear_map.dom_dom_congr σ m)
theorem
multilinear_map.alternatization_apply
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
[fintype ι]
[decidable_eq ι]
(m : multilinear_map R (λ (i : ι), M) N')
(v : ι → M) :
⇑(⇑multilinear_map.alternatization m) v = finset.univ.sum (λ (σ : equiv.perm ι), ⇑equiv.perm.sign σ • ⇑(multilinear_map.dom_dom_congr σ m) v)
theorem
alternating_map.coe_alternatization
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
[decidable_eq ι]
[fintype ι]
(a : alternating_map R M N' ι) :
Alternatizing a multilinear map that is already alternating results in a scale factor of n!,
where n is the number of inputs.
theorem
linear_map.comp_multilinear_map_alternatization
{R : Type u_1}
[semiring R]
{M : Type u_2}
[add_comm_monoid M]
[module R M]
{N' : Type u_6}
[add_comm_group N']
[module R N']
{ι : Type u_7}
{N'₂ : Type u_10}
[add_comm_group N'₂]
[module R N'₂]
[decidable_eq ι]
[fintype ι]
(g : N' →ₗ[R] N'₂)
(f : multilinear_map R (λ (_x : ι), M) N') :
Composition with a linear map before and after alternatization are equivalent.
@[reducible]
Elements which are considered equivalent if they differ only by swaps within α or β
theorem
equiv.perm.mod_sum_congr.swap_smul_involutive
{α : Type u_1}
{β : Type u_2}
[decidable_eq (α ⊕ β)]
(i j : α ⊕ β) :
def
alternating_map.dom_coprod.summand
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb)
(σ : equiv.perm.mod_sum_congr ιa ιb) :
multilinear_map R' (λ (_x : ιa ⊕ ιb), Mᵢ) (tensor_product R' N₁ N₂)
summand used in alternating_map.dom_coprod
Equations
- alternating_map.dom_coprod.summand a b σ = quotient.lift_on' σ (λ (σ : equiv.perm (ιa ⊕ ιb)), ⇑equiv.perm.sign σ • multilinear_map.dom_dom_congr σ (↑a.dom_coprod ↑b)) _
theorem
alternating_map.dom_coprod.summand_mk'
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb)
(σ : equiv.perm (ιa ⊕ ιb)) :
theorem
alternating_map.dom_coprod.summand_add_swap_smul_eq_zero
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb)
(σ : equiv.perm.mod_sum_congr ιa ιb)
{v : ιa ⊕ ιb → Mᵢ}
{i j : ιa ⊕ ιb}
(hv : v i = v j)
(hij : i ≠ j) :
⇑(alternating_map.dom_coprod.summand a b σ) v + ⇑(alternating_map.dom_coprod.summand a b (equiv.swap i j • σ)) v = 0
Swapping elements in σ with equal values in v results in an addition that cancels
theorem
alternating_map.dom_coprod.summand_eq_zero_of_smul_invariant
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb)
(σ : equiv.perm.mod_sum_congr ιa ιb)
{v : ιa ⊕ ιb → Mᵢ}
{i j : ιa ⊕ ιb}
(hv : v i = v j)
(hij : i ≠ j) :
equiv.swap i j • σ = σ → ⇑(alternating_map.dom_coprod.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.
def
alternating_map.dom_coprod
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb) :
alternating_map R' Mᵢ (tensor_product R' N₁ N₂) (ιa ⊕ ιb)
Like multilinear_map.dom_coprod, but ensures the result is also alternating.
Note that this is usually defined (for instance, as used in Proposition 22.24 in [GQ11])
over integer indices ιa = fin n and ιb = fin m, as
$$
(f \wedge g)(u_1, \ldots, u_{m+n}) =
\sum_{\operatorname{shuffle}(m, n)} \operatorname{sign}(\sigma)
f(u_{\sigma(1)}, \ldots, u_{\sigma(m)}) g(u_{\sigma(m+1)}, \ldots, u_{\sigma(m+n)}),
$$
where $\operatorname{shuffle}(m, n)$ consists of all permutations of $[1, m+n]$ such that
$\sigma(1) < \cdots < \sigma(m)$ and $\sigma(m+1) < \cdots < \sigma(m+n)$.
Here, we generalize this by replacing:
- the product in the sum with a tensor product
- the filtering of $[1, m+n]$ to shuffles with an isomorphic quotient
- the additions in the subscripts of $\sigma$ with an index of type
sum
The specialized version can be obtained by combining this definition with fin_sum_fin_equiv and
linear_map.mul'.
Equations
- a.dom_coprod b = {to_fun := λ (v : Π (i : ιa ⊕ ιb), (λ (i : ιa ⊕ ιb), Mᵢ) i), ⇑(finset.univ.sum (λ (σ : equiv.perm.mod_sum_congr ιa ιb), alternating_map.dom_coprod.summand a b σ)) v, map_add' := _, map_smul' := _, map_eq_zero_of_eq' := _}
@[simp]
theorem
alternating_map.dom_coprod_apply
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb)
(v : Π (i : ιa ⊕ ιb), (λ (i : ιa ⊕ ιb), Mᵢ) i) :
⇑(a.dom_coprod b) v = ⇑(finset.univ.sum (λ (σ : equiv.perm.mod_sum_congr ιa ιb), alternating_map.dom_coprod.summand a b σ)) v
theorem
alternating_map.dom_coprod_coe
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb) :
↑(a.dom_coprod b) = finset.univ.sum (λ (σ : equiv.perm.mod_sum_congr ιa ιb), alternating_map.dom_coprod.summand a b σ)
def
alternating_map.dom_coprod'
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb] :
tensor_product R' (alternating_map R' Mᵢ N₁ ιa) (alternating_map R' Mᵢ N₂ ιb) →ₗ[R'] alternating_map R' Mᵢ (tensor_product R' N₁ N₂) (ιa ⊕ ιb)
A more bundled version of alternating_map.dom_coprod that maps
((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.
Equations
- alternating_map.dom_coprod' = tensor_product.lift (linear_map.mk₂ R' alternating_map.dom_coprod alternating_map.dom_coprod'._proof_7 alternating_map.dom_coprod'._proof_8 alternating_map.dom_coprod'._proof_9 alternating_map.dom_coprod'._proof_10)
@[simp]
theorem
alternating_map.dom_coprod'_apply
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb) :
⇑alternating_map.dom_coprod' (a ⊗ₜ[R'] b) = a.dom_coprod b
theorem
multilinear_map.dom_coprod_alternization_coe
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : multilinear_map R' (λ (_x : ιa), Mᵢ) N₁)
(b : multilinear_map R' (λ (_x : ιb), Mᵢ) N₂) :
↑(⇑multilinear_map.alternatization a).dom_coprod ↑(⇑multilinear_map.alternatization b) = finset.univ.sum (λ (σa : equiv.perm ιa), finset.univ.sum (λ (σb : equiv.perm ιb), ⇑equiv.perm.sign σa • ⇑equiv.perm.sign σb • (multilinear_map.dom_dom_congr σa a).dom_coprod (multilinear_map.dom_dom_congr σb b)))
A helper lemma for multilinear_map.dom_coprod_alternization.
theorem
multilinear_map.dom_coprod_alternization
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : multilinear_map R' (λ (_x : ιa), Mᵢ) N₁)
(b : multilinear_map R' (λ (_x : ιb), Mᵢ) N₂) :
Computing the multilinear_map.alternatization of the multilinear_map.dom_coprod is the same
as computing the alternating_map.dom_coprod of the multilinear_map.alternatizations.
theorem
multilinear_map.dom_coprod_alternization_eq
{ιa : Type u_10}
{ιb : Type u_11}
[fintype ιa]
[fintype ιb]
{R' : Type u_12}
{Mᵢ : Type u_13}
{N₁ : Type u_14}
{N₂ : Type u_15}
[comm_semiring R']
[add_comm_group N₁]
[module R' N₁]
[add_comm_group N₂]
[module R' N₂]
[add_comm_monoid Mᵢ]
[module R' Mᵢ]
[decidable_eq ιa]
[decidable_eq ιb]
(a : alternating_map R' Mᵢ N₁ ιa)
(b : alternating_map R' Mᵢ N₂ ιb) :
⇑multilinear_map.alternatization (↑a.dom_coprod ↑b) = ((fintype.card ιa).factorial * (fintype.card ιb).factorial) • a.dom_coprod b
Taking the multilinear_map.alternatization of the multilinear_map.dom_coprod of two
alternating_maps gives a scaled version of the alternating_map.coprod of those maps.
theorem
basis.ext_alternating
{ι : Type u_7}
{ι₁ : Type u_10}
[finite ι]
{R' : Type u_11}
{N₁ : Type u_12}
{N₂ : Type u_13}
[comm_semiring R']
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[module R' N₁]
[module R' N₂]
{f g : alternating_map R' N₁ N₂ ι}
(e : basis ι₁ R' N₁)
(h : ∀ (v : ι → ι₁), function.injective v → ⇑f (λ (i : ι), ⇑e (v i)) = ⇑g (λ (i : ι), ⇑e (v i))) :
f = g
Two alternating maps indexed by a fintype are equal if they are equal when all arguments
are distinct basis vectors.
Currying #
def
alternating_map.curry_left
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ}
(f : alternating_map R' M'' N'' (fin n.succ)) :
M'' →ₗ[R'] alternating_map R' M'' N'' (fin n)
Given an alternating map f in n+1 variables, split the first variable to obtain
a linear map into alternating maps in n variables, given by x ↦ (m ↦ f (matrix.vec_cons x m)).
It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.
This is multilinear_map.curry_left for alternating_map. See also
alternating_map.curry_left_linear_map.
@[simp]
theorem
alternating_map.curry_left_apply_apply
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ}
(f : alternating_map R' M'' N'' (fin n.succ))
(m : M'')
(v : Π (i : fin n), (λ (i : fin n), M'') i) :
⇑(⇑(f.curry_left) m) v = ⇑f (matrix.vec_cons m v)
@[simp]
theorem
alternating_map.curry_left_zero
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ} :
0.curry_left = 0
@[simp]
theorem
alternating_map.curry_left_add
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ}
(f g : alternating_map R' M'' N'' (fin n.succ)) :
(f + g).curry_left = f.curry_left + g.curry_left
@[simp]
theorem
alternating_map.curry_left_smul
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ}
(r : R')
(f : alternating_map R' M'' N'' (fin n.succ)) :
(r • f).curry_left = r • f.curry_left
@[simp]
theorem
alternating_map.curry_left_linear_map_apply
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ}
(f : alternating_map R' M'' N'' (fin n.succ)) :
def
alternating_map.curry_left_linear_map
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ} :
alternating_map R' M'' N'' (fin n.succ) →ₗ[R'] M'' →ₗ[R'] alternating_map R' M'' N'' (fin n)
alternating_map.curry_left as a linear_map. This is a separate definition as dot notation
does not work for this version.
Equations
- alternating_map.curry_left_linear_map = {to_fun := λ (f : alternating_map R' M'' N'' (fin n.succ)), f.curry_left, map_add' := _, map_smul' := _}
@[simp]
theorem
alternating_map.curry_left_same
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
{n : ℕ}
(f : alternating_map R' M'' N'' (fin n.succ.succ))
(m : M'') :
⇑((⇑(f.curry_left) m).curry_left) m = 0
Currying with the same element twice gives the zero map.
@[simp]
theorem
alternating_map.curry_left_comp_alternating_map
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
{N₂'' : Type u_14}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[add_comm_monoid N₂'']
[module R' M'']
[module R' N'']
[module R' N₂'']
{n : ℕ}
(g : N'' →ₗ[R'] N₂'')
(f : alternating_map R' M'' N'' (fin n.succ))
(m : M'') :
⇑((⇑(g.comp_alternating_map) f).curry_left) m = ⇑(g.comp_alternating_map) (⇑(f.curry_left) m)
@[simp]
theorem
alternating_map.curry_left_comp_linear_map
{R' : Type u_10}
{M'' : Type u_11}
{M₂'' : Type u_12}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid M₂'']
[add_comm_monoid N'']
[module R' M'']
[module R' M₂'']
[module R' N'']
{n : ℕ}
(g : M₂'' →ₗ[R'] M'')
(f : alternating_map R' M'' N'' (fin n.succ))
(m : M₂'') :
⇑((f.comp_linear_map g).curry_left) m = (⇑(f.curry_left) (⇑g m)).comp_linear_map g
@[simp]
theorem
alternating_map.const_linear_equiv_of_is_empty_symm_apply
{ι : Type u_7}
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
[is_empty ι]
(f : alternating_map R' M'' N'' ι) :
def
alternating_map.const_linear_equiv_of_is_empty
{ι : Type u_7}
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
[is_empty ι] :
N'' ≃ₗ[R'] alternating_map R' M'' N'' ι
The space of constant maps is equivalent to the space of maps that are alternating with respect to an empty family.
Equations
- alternating_map.const_linear_equiv_of_is_empty = {to_fun := alternating_map.const_of_is_empty R' M'' ι _inst_21, map_add' := _, map_smul' := _, inv_fun := λ (f : alternating_map R' M'' N'' ι), ⇑f 0, left_inv := _, right_inv := _}
@[simp]
theorem
alternating_map.const_linear_equiv_of_is_empty_apply
{ι : Type u_7}
{R' : Type u_10}
{M'' : Type u_11}
{N'' : Type u_13}
[comm_semiring R']
[add_comm_monoid M'']
[add_comm_monoid N'']
[module R' M'']
[module R' N'']
[is_empty ι]
(m : N'') :