Zulip Chat Archive

Stream: general

Topic: Notation for `multilinear_map`


view this post on Zulip Eric Wieser (Feb 09 2021 at 14:10):

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

view this post on Zulip Yury G. Kudryashov (Feb 09 2021 at 18:18):

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

view this post on Zulip Eric Wieser (Feb 09 2021 at 18:38):

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

view this post on Zulip Eric Wieser (Feb 09 2021 at 18:39):

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

view this post on Zulip Frédéric Dupuis (Feb 09 2021 at 19:00):

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

view this post on Zulip Eric Wieser (Feb 09 2021 at 22:09):

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

view this post on Zulip Eric Wieser (Feb 09 2021 at 22:42):

I can basically get that working with:

view this post on Zulip Eric Wieser (Feb 09 2021 at 22:42):

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

view this post on Zulip Eric Wieser (Feb 09 2021 at 22:43):

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

view this post on Zulip Eric Wieser (Feb 09 2021 at 22:52):

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

view this post on Zulip Eric Wieser (Feb 10 2021 at 08:49):

#6152


Last updated: May 11 2021 at 14:11 UTC