## Stream: maths

### Topic: multilinear_map: f (c • x) = c ^ fintype.card ι • f x

#### Eric Wieser (Apr 08 2021 at 14:19):

We have a result like this already at docs#matrix.det_smul. However, this should generalize to all multilinear_maps.

I can't work out how to perform the necessary induction to do so. Can anyone help? I'm stuck on this sorry

import linear_algebra.multilinear

variables {R : Type*} {N₁ : Type*} {N : Type*}
variables [comm_semiring R] [add_comm_monoid N₁] [semimodule R N₁] [add_comm_monoid N] [semimodule R N]

lemma multilinear_map.map_smul_pi_fin_aux {n : ℕ}
(c : R) (f : multilinear_map R (λ (i : fin n), N₁) N) :
f.comp_linear_map (λ (i : fin n), linear_map.lsmul R N₁ c) =
c ^ n • f :=
begin
ext, simp,
sorry,
end


which is enough to prove the more general result

lemma multilinear_map.map_smul_pi {ι : Type*} [fintype ι] [decidable_eq ι]
(c : R) (f : multilinear_map R (λ i : ι, N₁) N) (x : Π i : ι, N₁):
f (c • x) = c ^ fintype.card ι • f x :=
begin
suffices h : f.comp_linear_map (λ (i : ι), linear_map.lsmul R N₁ c) =
c ^ fintype.card ι • f,
{ have := multilinear_map.congr_fun h x,
simp at this,
exact this, },
obtain ⟨e⟩ := (fintype.equiv_fin ι).nonempty,
apply (multilinear_map.dom_dom_congr_linear_equiv N₁ N R R e).injective,
rw [linear_equiv.map_smul, ←multilinear_map.map_smul_pi_fin_aux],
ext,
simp,
end


#### Anne Baanen (Apr 08 2021 at 14:25):

Presumably we want induction on n, and then show a multilinear map on fin (n + 1) → N is like a linear map in N and a multilinear map on fin n → N.

#### Anne Baanen (Apr 08 2021 at 14:26):

Base case:

import linear_algebra.multilinear

variables {R : Type*} {N₁ : Type*} {N : Type*}
variables [comm_semiring R] [add_comm_monoid N₁] [semimodule R N₁] [add_comm_monoid N] [semimodule R N]

lemma multilinear_map.map_smul_pi_fin_aux {n : ℕ}
(c : R) (f : multilinear_map R (λ (i : fin n), N₁) N) :
f.comp_linear_map (λ (i : fin n), linear_map.lsmul R N₁ c) =
c ^ n • f :=
begin
induction n,
{ ext,
simp only [multilinear_map.comp_linear_map_apply, one_smul, linear_map.lsmul_apply, pow_zero],
congr }, -- fin 0 → N is a subsingleton, so congr gets rid of it
sorry
end


#### Anne Baanen (Apr 08 2021 at 14:27):

I think docs#multilinear_map.cons_smul will help here

#### Eric Wieser (Apr 08 2021 at 14:29):

That sounds like a reasonable approach - the other I can think of is to incrementally replace x with update x i (c • x)

#### Eric Wieser (Apr 08 2021 at 14:36):

This makes some progress, but I can't work how to clean up, I think we're missing some simp lemmas:

lemma multilinear_map.map_smul_pi_fin_aux {n : ℕ}
(c : R) (f : multilinear_map R (λ (i : fin n), N₁) N) :
f.comp_linear_map (λ (i : fin n), linear_map.lsmul R N₁ c) =
c ^ n • f :=
begin
induction n with n ih,
{ext, simp [subsingleton.elim (λ (i : fin 0), c • x i) x] },
apply (multilinear_curry_left_equiv R (λ _, N₁) N).symm.injective,
ext1,
rw [linear_equiv.map_smul, pow_succ', mul_smul, linear_map.smul_apply],
rw ←ih,
ext1,
simp [multilinear_curry_left_equiv],
sorry,
end



#### Eric Wieser (Apr 08 2021 at 14:38):

Ah, attribute [simps] multilinear_curry_left_equiv makes substantial progress

#### Anne Baanen (Apr 08 2021 at 14:42):

lemma multilinear_map.map_smul_pi_fin_aux {n : ℕ}
(c : R) (f : multilinear_map R (λ (i : fin n), N₁) N) :
f.comp_linear_map (λ (i : fin n), linear_map.lsmul R N₁ c) =
c ^ n • f :=
begin
ext x,
simp only [multilinear_map.comp_linear_map_apply, linear_map.lsmul_apply, multilinear_map.smul_apply],
conv_lhs { simp [← pi.smul_apply] },
induction n with n ih,
{ simp only [one_smul, pow_zero],
congr }, -- fin 0 → N is a subsingleton, so congr gets rid of it
set g : multilinear_map R (λ (i : fin n), N₁) N := (multilinear_curry_left_equiv _ _ _).symm f (x 0),
have hfg : ∀ y, f (fin.cons (x 0) y) = g y := _,
set y : fin n → N₁ := x ∘ fin.succ,
have hxy : x = fin.cons (x 0) y := _,
have hxy' : c • x = fin.cons (c • x 0) (c • y) := _,
have hfg' : f x = g y := _,
rw [hxy', multilinear_map.cons_smul, hfg, ih g y, pow_succ, mul_smul, hfg'],
all_goals { sorry },
end


#### Anne Baanen (Apr 08 2021 at 14:49):

Done!

import linear_algebra.multilinear

variables {R : Type*} {N₁ : Type*} {N : Type*}
variables [comm_semiring R] [add_comm_monoid N₁] [semimodule R N₁] [add_comm_monoid N] [semimodule R N]

attribute [simps] multilinear_curry_left_equiv

lemma multilinear_map.map_smul_pi_fin_aux {n : ℕ}
(c : R) (f : multilinear_map R (λ (i : fin n), N₁) N) :
f.comp_linear_map (λ (i : fin n), linear_map.lsmul R N₁ c) =
c ^ n • f :=
begin
ext x,
simp only [multilinear_map.comp_linear_map_apply, linear_map.lsmul_apply, multilinear_map.smul_apply],
conv_lhs { simp [← pi.smul_apply] },
induction n with n ih,
{ simp only [one_smul, pow_zero],
congr }, -- fin 0 → N is a subsingleton, so congr gets rid of it
set g : multilinear_map R (λ (i : fin n), N₁) N := (multilinear_curry_left_equiv _ _ _).symm f (x 0),
have hfg : ∀ y, f (fin.cons (x 0) y) = g y := λ y, by simp [g],
set y : fin n → N₁ := x ∘ fin.succ,
have hxy : x = fin.cons (x 0) y := by { ext i, refine fin.cases _ _ i; simp },
have hxy' : c • x = fin.cons (c • x 0) (c • y) := by { ext i, refine fin.cases _ _ i; simp },
have hfg' : f x = g y := by rw [hxy, hfg (x ∘ fin.succ)],
rw [hxy', multilinear_map.cons_smul, hfg, ih g y, pow_succ, mul_smul, hfg'],
end


#### Eric Wieser (Apr 08 2021 at 14:54):

Oops, I think this already exists as docs#multilinear_map.map_smul_univ

#### Anne Baanen (Apr 08 2021 at 14:55):

Well, at least we found out that attribute [simps] multilinear_curry_left_equiv should be added. Do you want to make the PR? :)

#### Yury G. Kudryashov (Apr 08 2021 at 15:12):

While ι = fin n is the most important case for a multilinear_map, general lemmas should deal with any {ι : Type*} [fintype ι] when possible. E.g., in this case it's better to do induction on s : finset ι in f (s.piecewise (c • m) m) = c ^ s.card • f m, see docs#multilinear_map.map_piecewise_smul

#### Eric Wieser (Apr 08 2021 at 15:13):

@Yury, see the original post - i used the fin case as a stepping stone to prove the fintype case

#### Eric Wieser (Apr 08 2021 at 15:14):

Eric Wieser said:

That sounds like a reasonable approach - the other I can think of is to incrementally replace x with update x i (c • x)

I guess this is the finset approach Yury G. Kudryashov describes, as opposed to the currying approach Anne Baanen described

Last updated: May 09 2021 at 09:11 UTC