Stream: Is there code for X?

Topic: If f is a multilinear map then λ v, f (v ∘ σ) is too

Eric Wieser (Nov 26 2020 at 10:43):

That is, if I have a multilinear map of n inputs, I can turn it into a multilinear map over m inputs by "wiring up" the inputs however I like

Reid Barton (Nov 26 2020 at 12:01):

This isn't true unless σ is a bijection (and so n = m)

Eric Wieser (Nov 26 2020 at 12:16):

Ah right, I see the mistake in my reasoning

Eric Wieser (Nov 26 2020 at 12:20):

Does this exist for σ : A ≃ B then? If not, what would be a good name? multilinear_map.comp_domain f σ?

Anne Baanen (Nov 26 2020 at 12:29):

Maybe even multilinear_map.congr_domain, since the result is an equiv between maps in n inputs and maps in m inputs

Eric Wieser (Nov 26 2020 at 12:42):

I thought about that too. (to be clear, as Reid points out this is an equiv between maps with inputs of type A and B, not with different numbers of inputs)

Eric Wieser (Nov 26 2020 at 12:43):

Also note that we have docs#finsupp.dom_congr, in case we want precedent in the naming

Eric Wieser (Nov 26 2020 at 12:43):

Ah, here's the concern - this is a congruence in the domain of the domain, not in the domain itself

Johan Commelin (Nov 26 2020 at 12:44):

Sounds like dom_dom_congr then :oops:

Eric Wieser (Nov 27 2020 at 17:49):

lemma function.update_comp_equiv {α β α' : Sort*} [decidable_eq α'] [decidable_eq α] (f : α  β) (g : α'  α)
(a : α) (v : β) :
(function.update f a v)  g = function.update (f  g) (g.symm a) v :=
by {rw [function.update_comp _ (g.injective), g.apply_symm_apply]}

lemma function.update_comp_equiv_apply {α β α' : Sort*} [decidable_eq α'] [decidable_eq α] (f : α  β) (g : α'  α)
(a : α) (v : β) (a' : α') :
(function.update f a v) (g a') = function.update (f  g) (g.symm a) v a' :=
congr_fun (function.update_comp_equiv f g a v) a'

def multilinear_map.dom_dom_congr (m : multilinear_map R (λ i : ι, M) N) (σ : equiv.perm ι) :
multilinear_map R (λ i : ι, M) N :=
{ to_fun := λ v, m (λ i, v (σ i)),
map_add' := λ v i a b, by { simp_rw function.update_comp_equiv_apply v, rw m.map_add, },
map_smul' := λ v i a b, by { simp_rw function.update_comp_equiv_apply v, rw m.map_smul, }, }

Should I be using a congr-like name for those function lemmas? Do they belong in equiv instead?

Eric Wieser (Nov 27 2020 at 18:47):

#5136

Last updated: May 19 2021 at 02:10 UTC