Zulip Chat Archive

Stream: general

Topic: Notation for span


Heather Macbeth (Dec 22 2020 at 23:18):

I would like to find some kind of notation for the span of a vector, really anything shorter than typing span ℝ {v} repeatedly. Can someone help me troubleshoot? I have tried

import linear_algebra.basic
import data.real.basic

infix `∙`:1000 := λ 𝕜 x, submodule.span 𝕜 {x}

notation `⟪`x`⟫_`𝕜  := submodule.span 𝕜 {x}

variables {E : Type*} [add_comm_group E] [module  E]

example (x y : E) (hy : y  (  x)) (hy' : y  x) : y = 0 := sorry

example (x y : E) (hy : y  x_ℝ) (hy' : y  x) : y = 0 := sorry

which give the errors, respectively,

failed to synthesize type class instance for
E : Type u_1,
_inst_1 : add_comm_group E,
_inst_2 : module ℝ E,
x y : E,
𝕜 : Type ?,
x : ?m_1
⊢ semiring 𝕜

(among others) and

don't know how to synthesize placeholder
context:
E : Type u_1,
_inst_1 : add_comm_group E,
_inst_2 : module ℝ E,
x y : E
⊢ Type ?

Heather Macbeth (Dec 22 2020 at 23:24):

(please ignore the dubious mathematics, I just want it to typecheck!)

Adam Topaz (Dec 22 2020 at 23:26):

This works:

import linear_algebra.basic
import data.real.basic


notation `⟪`x`⟫_`𝕜  := submodule.span 𝕜 (set.insert x )

variables {E : Type*} [add_comm_group E] [module  E]

example (x y : E) (hy : y   x _ℝ) (hy' : y  x) : y = 0 := sorry

Adam Topaz (Dec 22 2020 at 23:27):

I feel like there was a similar issue with similar notation around adjoining elements to fields in the work around Galois theory, but I don't remember how it was resolved.

Adam Topaz (Dec 22 2020 at 23:27):

@Thomas Browning probably knows :)

Rob Lewis (Dec 22 2020 at 23:28):

example (x y : E) (hy : y ∉ submodule.span ℝ {x}) (hy' : y ≠ x) : y = 0 := sorry doesn't work, no notation at all

Rob Lewis (Dec 22 2020 at 23:28):

It does seem to be because Lean doesn't pick up on {x} : set E

Adam Topaz (Dec 22 2020 at 23:29):

This also works:

import linear_algebra.basic
import data.real.basic


notation `⟪`x`⟫_`𝕜  := submodule.span 𝕜 {y | y = x}

variables {E : Type*} [add_comm_group E] [module  E]

example (x y : E) (hy : y   x _ℝ) (hy' : y  x) : y = 0 := sorry

Heather Macbeth (Dec 22 2020 at 23:33):

Thank you! What about the infix version, is there a way to get that working?

Heather Macbeth (Dec 22 2020 at 23:36):

Oh,

notation 𝕜`∙`x := submodule.span 𝕜 (set.insert x )

seems to work. Maybe it's just a peculiarity of the infix keyword that the other one didn't.

Heather Macbeth (Dec 22 2020 at 23:37):

At least, this works:

import linear_algebra.basic
import data.real.basic

notation 𝕜`∙`x := submodule.span 𝕜 (set.insert x )

variables {E : Type*} [add_comm_group E] [module  E]

example (x y : E) (hy : y  (  x)) (hy' : y  x) : y = 0 := sorry

Is there something I can do with priorities that will let me ditch the parentheses in (ℝ ∙ x)?

Adam Topaz (Dec 22 2020 at 23:39):

Maybe something like this?

import linear_algebra.basic
import data.real.basic

notation 𝕜`∙`:1000 x := submodule.span 𝕜 (set.insert x )

variables {E : Type*} [add_comm_group E] [module  E]

example (x y : E) (hy : y    x) (hy' : y  x) : y = 0 := sorry

Heather Macbeth (Dec 22 2020 at 23:40):

Awesome, thanks! One last question: is there a centralized list of unicode characters, so that I can find a dot character without any previous use in mathlib?

Adam Topaz (Dec 22 2020 at 23:45):

I think you have to look at the repo for the vscode extension.

Adam Topaz (Dec 22 2020 at 23:45):

(assuming you're using vscode :smile:)

Heather Macbeth (Dec 22 2020 at 23:46):

If I remember correctly, that lists all the unicode symbols that are taken. But how can I determine the complement? :)

Mario Carneiro (Dec 22 2020 at 23:55):

that list is not all taken characters, in fact most of them are free

Mario Carneiro (Dec 22 2020 at 23:55):

a better list would be #print notation with all of mathlib imported

Mario Carneiro (Dec 22 2020 at 23:56):

alternatively, if you are looking specifically for unicode characters, you can just use the list in the repo and grep for uses of each of them in mathlib

Thomas Browning (Dec 23 2020 at 02:10):

Here's what we used for adjoin:

/--
Variation on `set.insert` to enable good notation for adjoining elements to fields.
Used to preferentially use `singleton` rather than `insert` when adjoining one element.
-/
--this definition of notation is courtesy of Kyle Miller on zulip
class insert {α : Type*} (s : set α) :=
(insert : α  set α)

@[priority 1000]
instance insert_empty {α : Type*} : insert ( : set α) :=
{ insert := λ x, @singleton _ _ set.has_singleton x }

@[priority 900]
instance insert_nonempty {α : Type*} (s : set α) : insert s :=
{ insert := λ x, set.insert x s }

notation K`⟮`:std.prec.max_plus l:(foldr `, ` (h t, insert.insert t h) ) `⟯` := adjoin K l

Thomas Browning (Dec 23 2020 at 02:10):

This made it so that K(x) was definitionally equal to adjoin K {x}

Thomas Browning (Dec 23 2020 at 02:11):

and it allowed for adjoining multiple elements at once

Heather Macbeth (Dec 23 2020 at 07:19):

Another way to do the original problem, adapting a trick from the code @Thomas Browning posted:

import linear_algebra.basic
import data.real.basic

notation 𝕜`∙`:1000 x := submodule.span 𝕜 (@singleton _ _ set.has_singleton x)

variables {E : Type*} [add_comm_group E] [module  E]

example (x y : E) (hy : y  (  x)) (hy' : y  x) : y = 0 := sorry

Adam Topaz (Jan 14 2021 at 04:23):

@Heather Macbeth did your new notation for the span of a vector get merged into mathlib yet?

Heather Macbeth (Jan 14 2021 at 04:24):

Yup, #5538.

Adam Topaz (Jan 14 2021 at 04:24):

Great! Thanks :)


Last updated: Dec 20 2023 at 11:08 UTC