Notation for span

Stream: general

[Heather Macbeth]

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]

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

[Adam Topaz]

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]

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]

@Thomas Browning probably knows :)

[Rob Lewis]

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

[Rob Lewis]

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

[Adam Topaz]

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]

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

[Heather Macbeth]

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]

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]

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]

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]

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

[Adam Topaz]

(assuming you're using vscode :smile:)

[Heather Macbeth]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Thomas Browning]

and it allowed for adjoining multiple elements at once

[Heather Macbeth]

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]

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

[Heather Macbeth]

Yup, #5538.

[Adam Topaz]

Great! Thanks :)