Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Anne Baanen (Apr 08 2021 at 14:27):

I think docs#multilinear_map.cons_smul will help here

view this post on Zulip 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)

view this post on Zulip 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
``

view this post on Zulip Eric Wieser (Apr 08 2021 at 14:38):

Ah, attribute [simps] multilinear_curry_left_equiv makes substantial progress

view this post on Zulip Anne Baanen (Apr 08 2021 at 14:42):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 08 2021 at 14:54):

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

view this post on Zulip 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? :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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