# Zulip Chat Archive

## 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)

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

(deleted)

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

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

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

(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 = β}
```

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

(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
```

#### Adam Topaz (Aug 21 2020 at 20:42):

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):

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 (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):

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 (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):

#### 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 <<=`

?

#### Kevin Buzzard (Aug 21 2020 at 21:18):

I think those might already be used for monads

#### Kevin Buzzard (Aug 21 2020 at 21:19):

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

Last updated: May 10 2021 at 06:13 UTC