Zulip Chat Archive

Stream: new members

Topic: Notation of linear_algebra.dual


view this post on Zulip Nicolò Cavalleri (Oct 28 2020 at 13:55):

I don't really understand this notation:

universes u v w
variables {K : Type u} {V : Type v} {ι : Type w} [decidable_eq ι]
variables [field K] [add_comm_group V] [vector_space K V]

local notation `V'` := dual K V

How can lean guess the field? Or is it assuming the field is always named K? In the latter case why is it a good notation?

view this post on Zulip Julian Berman (Oct 28 2020 at 14:06):

Won't it be because the vector space knows it

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:06):

This is just for V itself. E.g. you couldn't use the notation W' if W is some other vectorspace.

view this post on Zulip Reid Barton (Oct 28 2020 at 14:06):

right, it's not only "guessing" the field, but also the vector space

view this post on Zulip Nicolò Cavalleri (Oct 28 2020 at 14:09):

Oh right sorry so this is just meant to be an ad hoc notation

view this post on Zulip Nicolò Cavalleri (Oct 28 2020 at 14:09):

I mean it is local but still reported at the top of the file this is why I thought it was meant to be not so local

view this post on Zulip Nicolò Cavalleri (Oct 28 2020 at 14:11):

What do you think of the notation

localized "notation V `ᵛ` R := module.dual R V" in linear_algebra.dual

? I need to invent a short notation to be used in vector bundles and that is more standard

view this post on Zulip Adam Topaz (Oct 28 2020 at 14:17):

Wouldn't writing V ᵛ R be just as tedious as writing dual R V?

view this post on Zulip Reid Barton (Oct 28 2020 at 14:17):

I think we try to document local notation at the top of the file so that you can understand what is going on on line 600 by looking at line 10 and not having to find line 418 where the notation is defined.


Last updated: May 10 2021 at 17:39 UTC