# Zulip Chat Archive

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

Last updated: May 19 2021 at 02:10 UTC