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

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Eric Wieser]

Ah right, I see the mistake in my reasoning

[Eric Wieser]

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

[Anne Baanen]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Johan Commelin]

Sounds like dom_dom_congr then :oops:

[Eric Wieser]

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]

#5136