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

Stream: maths

[Eric Wieser]

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]

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]

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]

I think docs#multilinear_map.cons_smul will help here

[Eric Wieser]

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]

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]

Ah, attribute [simps] multilinear_curry_left_equiv makes substantial progress

[Anne Baanen]

How about this (some smaller holes left open):

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]

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]

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

[Anne Baanen]

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]

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]

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

[Eric Wieser]

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