Stream: maths

Topic: Lean can't figure out type of {a}

Thomas Browning (Aug 21 2020 at 20:29):

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 (Aug 21 2020 at 20:30):

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

Thomas Browning (Aug 21 2020 at 20:31):

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

(deleted)

Thomas Browning (Aug 21 2020 at 20:31):

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

(deleted)

Thomas Browning (Aug 21 2020 at 20:32):

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 (Aug 21 2020 at 20:34):

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 (Aug 21 2020 at 20:34):

It's a hack:

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


(deleted)

Thomas Browning (Aug 21 2020 at 20:34):

Oh, it looks like that works!

Thomas Browning (Aug 21 2020 at 20:35):

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

Adam Topaz (Aug 21 2020 at 20:35):

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

Adam Topaz (Aug 21 2020 at 20:37):

@Mario Carneiro Do you have any suggestions?

Mario Carneiro (Aug 21 2020 at 20:38):

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

Thomas Browning (Aug 21 2020 at 20:38):

I think that I tried that

Thomas Browning (Aug 21 2020 at 20:39):

Yeah, that doesn't work unfortunately

Mario Carneiro (Aug 21 2020 at 20:40):

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

Mario Carneiro (Aug 21 2020 at 20:42):

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

Patrick Lutz (Aug 21 2020 at 20:42):

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 (Aug 21 2020 at 20:42):

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


Is that safe?

Mario Carneiro (Aug 21 2020 at 20:42):

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

Patrick Lutz (Aug 21 2020 at 20:43):

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 (Aug 21 2020 at 20:43):

You can make adjoin_simple reducible

Mario Carneiro (Aug 21 2020 at 20:43):

Or you can notate the type of α

Patrick Lutz (Aug 21 2020 at 20:43):

What do you mean?

Adam Topaz (Aug 21 2020 at 20:44):

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 (Aug 21 2020 at 20:45):

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 (Aug 21 2020 at 20:46):

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 (Aug 21 2020 at 20:47):

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 (Aug 21 2020 at 20:48):

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

Patrick Lutz (Aug 21 2020 at 20:48):

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 (Aug 21 2020 at 20:48):

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

Mario Carneiro (Aug 21 2020 at 20:49):

how about  F[(α)]

Mario Carneiro (Aug 21 2020 at 20:50):

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

Adam Topaz (Aug 21 2020 at 20:50):

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 (Aug 21 2020 at 20:51):

with unicode the Possibilities are Endless (TM)

Patrick Massot (Aug 21 2020 at 20:51):

Where are those zero-width unicode characters again?

Mario Carneiro (Aug 21 2020 at 20:51):

I recall seeing a talk about the mongolian vowel separator

Patrick Massot (Aug 21 2020 at 20:51):

In the perfectoid project we also used fancy parentheses.

Mario Carneiro (Aug 21 2020 at 20:52):

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

Patrick Massot (Aug 21 2020 at 20:52):

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

Patrick Massot (Aug 21 2020 at 20:53):

Those are not actual parentheses.

Adam Topaz (Aug 21 2020 at 20:53):

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

Patrick Massot (Aug 21 2020 at 20:55):

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 (Aug 21 2020 at 20:55):

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

Adam Topaz (Aug 21 2020 at 20:56):

F>>= a <<=?