Notation for `multilinear_map`

Stream: general

[Eric Wieser]

Any ideas for notation for docs#multilinear_map? To make things confusing, we already have (⨂ i, M i) →ₗ[R] N for docs#linear_map over docs#pi_tensor_product, which is almost isomorphic; meanwhile, (Π i, M i) →ₗ[R] N is a linear map over a pi type, which has different properties.

I came up with Πₗ i, M i →ₗ[R] N but I think it's not a good idea. Here's a mwe for someone else to try similar ideas:

import linear_algebra.multilinear

notation `Πₗ ` binders `, ` m:(scoped:67 f, λ R, multilinear_map R f) `→ₗ[`R`]` N := m R N

example
  {ι R N : Type*} {M : ι → Type*}
  [semiring R] [∀ i, add_comm_monoid (M i)] [∀ i, semimodule R (M i)]
  [add_comm_monoid N] [semimodule R N] :
    Πₗ i, M i →ₗ[R] N :=
begin
  sorry
end

[Yury G. Kudryashov]

In case of continuous_multilinear_maps we only have notation for continuous_multilinear_map (λ i : fin n, E) F

[Eric Wieser]

What is that notation? I don't remember seeing it when I last looked at docs#continuous_multilinear_map

[Eric Wieser]

Ah, M [×n]→L[R] N

[Frédéric Dupuis]

How about something like (Π i, M i) →ₘₗ[R] N?

[Eric Wieser]

Notation can't start with ( unfortunately - so that would require some clever trickery to convert Π i, M i into λ i, M i

[Eric Wieser]

I can basically get that working with:

import linear_algebra.multilinear

abbreviation type_of.codomain {α : Type*} {β : α → Type*} (a : Π (i : α), β i) (i : α) : Type* :=
β i

notation A ` →ₗₘ[` R `] ` N := multilinear_map R (type_of.codomain (sorry : A)) N

variables {ι R M N : Type*} {Mᵢ : ι → Type*}
  [decidable_eq ι]
  [semiring R] [∀ i, add_comm_monoid (Mᵢ i)] [∀ i, semimodule R (Mᵢ i)]
  [add_comm_monoid M] [semimodule R M]
  [add_comm_monoid N] [semimodule R N]

example : (Π i, Mᵢ i) →ₗₘ[R] N :=
begin
  dunfold type_of.codomain, dsimp only,
  exact 0,
end

example : (ι → M) →ₗₘ[R] N :=
begin
  dunfold type_of.codomain, dsimp only,
  exact 0,
end

[Eric Wieser]

But I don't know how to eliminate the sorry in the notation

[Eric Wieser]

The typeof strategy doesn't work, because it requires me to construct a term of A to use even if one doesn't exist

[Eric Wieser]

Solved!

import linear_algebra.multilinear

inductive type_info (α : Type*)
| unit [] : type_info

abbreviation type_info.codomain {α : Type*} {β : α → Type*}
  (a : type_info (Π (i : α), β i)) : α → Type* := β

notation A ` →ₗₘ[` R `] ` N := multilinear_map R (type_info.codomain (type_info.unit A)) N

variables {ι R M N : Type*} {Mᵢ : ι → Type*}
  [decidable_eq ι]
  [semiring R] [∀ i, add_comm_monoid (Mᵢ i)] [∀ i, semimodule R (Mᵢ i)]
  [add_comm_monoid M] [semimodule R M]
  [add_comm_monoid N] [semimodule R N]

example : (Π i, Mᵢ i) →ₗₘ[R] N :=
begin
  dunfold type_info.codomain, dsimp only,
  exact 0,
end

example : (ι → M) →ₗₘ[R] N :=
begin
  dunfold type_info.codomain, dsimp only,
  exact 0,
end

[Eric Wieser]

#6152