Lean can't figure out type of {a}

Stream: maths

[Thomas Browning]

So we've been working with adjoining elements to fields:

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S)

def adjoin_simple (α : E) : set E := adjoin F {α}

--this is fine
example (α : E) (x : F) : algebra_map F E x ∈ (adjoin_simple F α) := sorry

--this is also fine
example (α : E) (x : F) : algebra_map F E x ∈ adjoin F ({α} : set E) := sorry

--this doesn't work
example (α : E) (x : F) : algebra_map F E x ∈ adjoin F {α} := sorry

but lean sometimes has trouble figuring out that if α : E then {α} : set E

How can we fix this?

[Adam Topaz]

You can always tell lean explicitly ({a} : set E).

[Thomas Browning]

The problem is when we try to define notation (give me a sec)

[Thomas Browning]

(deleted)

[Thomas Browning]

We would really like to get notation F[alpha] to work

[Thomas Browning]

(deleted)

[Thomas Browning]

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S)

def adjoin_simple (α : E) : set E := adjoin F {α}

--this is fine
example (α : E) (x : F) : algebra_map F E x ∈ (adjoin_simple F α) := sorry

--this is also fine
example (α : E) (x : F) : algebra_map F E x ∈ adjoin F ({α} : set E) := sorry

--this doesn't work
example (α : E) (x : F) : algebra_map F E x ∈ adjoin F {α} := sorry

notation K`[`:std.prec.max_plus β`]` := adjoin K {β}

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x ∈ F[α] := sorry

--this works because it knows that F[α] is supposed to be in set E
example (α : E) (x : F) : F[α] = adjoin_simple F α := sorry

[Thomas Browning]

so the notation sometimes works when it already knows that F[α] is supposed to be in set E, but we would like this sort of notation to work more generally

[Adam Topaz]

It's a hack:

notation K`[`:std.prec.max_plus β`]` := adjoin K {x | x = β}

[Thomas Browning]

(deleted)

[Thomas Browning]

Oh, it looks like that works!

[Thomas Browning]

Is there any downside or is that hack as good as it looks?

[Adam Topaz]

Yeah, but someone who actually know how to write notation would give you a better answer :)

[Adam Topaz]

@Mario Carneiro Do you have any suggestions?

[Mario Carneiro]

Have you tried notation K`[`:std.prec.max_plus β`]` := adjoin K ({β} : set _)?

[Thomas Browning]

I think that I tried that

[Thomas Browning]

Yeah, that doesn't work unfortunately

[Mario Carneiro]

Oh, I see the problem now. Yeah you should make the notation unfold to adjoin_simple

[Mario Carneiro]

it's generally a bad idea to have notations unfold to things other than constant applied to variables

[Patrick Lutz]

Mario Carneiro said:

Oh, I see the problem now. Yeah you should make the notation unfold to adjoin_simple

We want to remove adjoin_simple

[Adam Topaz]

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S)

def adjoin_simple (α : E) : set E := adjoin F ({α} : set _)

notation K`[`:std.prec.max_plus β`]` := adjoin_simple K β

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x ∈ F[α] := sorry

[Adam Topaz]

Is that safe?

[Mario Carneiro]

Unfortunately lean has limited capacity to perform rewriting as part of notation expansion

[Patrick Lutz]

Adam Topaz said:

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S)

def adjoin_simple (α : E) : set E := adjoin F ({α} : set _)

notation K`[`:std.prec.max_plus β`]` := adjoin_simple K β

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x ∈ F[α] := sorry

Yeah, that's what we were doing before. But we kind of want to remove adjoin_simple

[Mario Carneiro]

You can make adjoin_simple reducible

[Mario Carneiro]

Or you can notate the type of α

[Patrick Lutz]

What do you mean?

[Adam Topaz]

import field_theory.subfield
import ring_theory.algebra

variables (F : Type*) [field F] {E : Type*} [field E] [algebra F E] (S : set E)

def adjoin : set E := field.closure (set.range (algebra_map F E) ∪ S)

@[reducible]
def adjoin_simple (α : E) : set E := adjoin F ({α} : set _)

notation K`[`:std.prec.max_plus β`]` := adjoin_simple K β

--how can we get this to work?
example (α : E) (x : F) : algebra_map F E x ∈ F[α] := sorry

[Mario Carneiro]

or

notation K`[`:std.prec.max_plus β`:`E`]` := adjoin K ({β} : set E)

example (α : E) (x : F) : algebra_map F E x ∈ F[α:E] := sorry

[Adam Topaz]

By the way, from a mathematical point of view, this is confusing notation since $K[\alpha]$ usually denotes the algebra generated by $\alpha$ and not the field generated by $\alpha$, but I guess (...) doesn't work with notation?

[Mario Carneiro]

aha:

notation K`[`:std.prec.max_plus β`]` :=
adjoin K (@singleton _ _ set.has_singleton β)

example (α : E) (x : F) : algebra_map F E x ∈ F[α] := sorry

[Adam Topaz]

Now how can we change [..] to (..)?

[Patrick Lutz]

Adam Topaz said:

By the way, from a mathematical point of view, this is confusing notation since $K[\alpha]$ usually denotes the algebra generated by $\alpha$ and not the field generated by $\alpha$, but I guess (...) doesn't work with notation?

Yeah, parentheses don't seem to work well in notation for some reason

[Patrick Lutz]

We're open to other suggestions for notation though (besides square brackets)

[Mario Carneiro]

how about F[(α)]

[Mario Carneiro]

you can also do funny things like F-(α)- as long as it doesn't begin with ( or end with )

[Adam Topaz]

Mario Carneiro said:

you can also do funny things like F-(α)- as long as it doesn't begin with ( or end with )

That looks awful!

[Mario Carneiro]

with unicode the Possibilities are Endless (TM)

[Patrick Massot]

Where are those zero-width unicode characters again?

[Mario Carneiro]

I recall seeing a talk about the mongolian vowel separator

[Patrick Massot]

In the perfectoid project we also used fancy parentheses.

[Mario Carneiro]

which is one of the few space characters that went through multiple character classes over the different unicode standards

[Patrick Massot]

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/Spa/localization_Huber.lean#L28

[Patrick Massot]

Those are not actual parentheses.

[Adam Topaz]

My vscode doesn't like that (I think I'm missing some fonts :( )

[Patrick Massot]

That's one of the many reason why this isn't such a great idea (and it would probably not go through mathlib review).

[Mario Carneiro]

personally I greatly prefer "ascii art" to this kind of thing

[Adam Topaz]

F>>= a <<=?

[Kevin Buzzard]

I think those might already be used for monads

[Kevin Buzzard]

I would use four characters, then you'll be fine