## 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