# Zulip Chat Archive

## Stream: FLT-regular

### Topic: finite_dimensional instance

#### Riccardo Brasca (Nov 17 2021 at 12:56):

@Anne Baanen noted that Lean didn't include the assumptions `[fintype S] [is_cyclotomic_extension S K L]`

in

```
instance finite_dimensional : finite_dimensional K L := sorry
```

so we were working with the assumption that any fields extension is finite :innocent:

This was an instance so it was really dangerous, but now everything seems OK. By the way, the linter says it is a dangerous instance

```
/- The `dangerous_instance` linter reports: -/
/- DANGEROUS INSTANCES FOUND.
These instances are recursive, and create a new type-class problem which will have metavariables.
Possible solution: remove the instance attribute or make it a local instance instead.
Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive. -/
#check @is_cyclotomic_extension.finite_dimensional /- The following arguments become metavariables. argument 1: (S : set ℕ+) -/
```

I am not sure I understand what this means, so I made it a lemma instead. Note that this means you may sometimes need

```
local attribute [instance] is_cyclotomic_extension.finite_dimensional
```

(this will give also separability).

#### Sebastien Gouezel (Nov 17 2021 at 13:10):

It means that in general Lean can not guess what `S`

should be, to apply this instance, so it can go crazy.

#### Anne Baanen (Nov 17 2021 at 13:30):

Would it make sense for `is_cyclotomic_extension S K L`

to have `S`

as an `out_param`

(or even a field of `is_cyclotomic`

)? That is, given `K`

and `L`

, is there a canonical choice of `S`

?

#### Anne Baanen (Nov 17 2021 at 13:32):

Probably not, since `L`

might have more roots than assumed by your lemma.

#### Riccardo Brasca (Nov 17 2021 at 13:32):

I don't think so: $\mathbb{Q}(\zeta_6)$ is both a third and a sixth cyclotomic extension

#### Anne Baanen (Nov 17 2021 at 13:35):

Right, so you probably don't want to write `[is_cyclotomic_extension K L] (h : n ∈ is_cyclotomic_extension.root_degrees)`

instead of `[is_cyclotomic_extension {n} K L]`

.

#### Anne Baanen (Nov 17 2021 at 13:35):

Where `root_degrees`

is the set of all `n`

such that `X^n - 1`

has a root in `L`

#### Anne Baanen (Nov 17 2021 at 13:40):

No, it'd be even more complicated since `is_cyclotomic_extension {n} K L`

also asserts that `L = K(ζₙ)`

.

#### Riccardo Brasca (Nov 17 2021 at 13:43):

Yes, `is_cyclotomic_extension S K L`

means that `L`

is the `K`

-extension given by all the `n`

-roots of unity, for all `n`

in `S`

. But given `L`

there is no way to recover `S`

(that is not unique).

#### Anne Baanen (Nov 17 2021 at 13:44):

Hmm, if are there no cases in practice where `S`

has to be infinite then we could make `[finite_dimensional K L]`

a parameter to `is_cyclotomic_extension`

. But there probably are :P

#### Anne Baanen (Nov 17 2021 at 13:45):

So you'd get:

```
class is_cyclotomic_extension (s : finset ℕ+) [finite_dimensional K L] : Prop :=
```

#### Riccardo Brasca (Nov 17 2021 at 13:47):

In this project there is no need for infinite `S`

, (even singletons are enough) but if we want the most general definition (to be used someday in mathlib) then infinite `S`

will be useful, for example the maximal abelian extension of `Q`

will be cyclotomic, and that's nice.

#### Riccardo Brasca (Nov 17 2021 at 13:49):

Especially @Filippo A. E. Nuccio will be not so happy if a cyclotomic extension has to be finite

#### Anne Baanen (Nov 17 2021 at 13:49):

Ok, I've run out of tricks to avoid making `is_cyclotomic_extension.finite_dimensional`

a lemma and `haveI`

'ing it back into the assumptions when needed.

#### Filippo A. E. Nuccio (Nov 17 2021 at 13:51):

Indeed, I won't be happy, especially if this will land in `mathlib`

: the cyclotomic extension $\mathbb{Q}(\zeta_{p^\infty})$ would not be a cyclotomic one...

#### Alex J. Best (Nov 17 2021 at 14:05):

We could just name it finite cyclotomic instead then? I'm guessing there will be lots of things which are only true for the $\mathbf Q(\zeta _n)$'s and not for the infinite extension, so we will need a distinction at some point?

#### Anne Baanen (Nov 17 2021 at 14:09):

So we would add a typeclass of the form `[finite_cyclotomic_extension (s : finset ℕ) K L]`

to abbreviate `[cyclotomic_extension (s : set ℕ) K L] (h : s.is_finite)`

?

#### Riccardo Brasca (Nov 17 2021 at 14:10):

We can have a class `is_cyclotomic_extension_finite`

or something similar: it is just `is_cyclotomic_extension`

plus `finite_dimensional`

#### Anne Baanen (Nov 17 2021 at 14:11):

The issue is that `is_cyclotomic_extension_finite`

would need `finite_dimensional`

as a parameter anyway, so it wouldn't help abbreviate much.

#### Anne Baanen (Nov 17 2021 at 14:13):

(Unless of course we add a feature to Lean that expands `[[is_cyclotomic_extension_finite s K L]]`

to something like `[field K] [field L] [algebra K L] [finite_dimensional K L] [fintype s] [is_cyclotomic_extension s K L]`

.)

#### Riccardo Brasca (Nov 17 2021 at 12:56):

@Anne Baanen noted that Lean didn't include the assumptions `[fintype S] [is_cyclotomic_extension S K L]`

in

```
instance finite_dimensional : finite_dimensional K L := sorry
```

so we were working with the assumption that any fields extension is finite :innocent:

This was an instance so it was really dangerous, but now everything seems OK. By the way, the linter says it is a dangerous instance

```
/- The `dangerous_instance` linter reports: -/
/- DANGEROUS INSTANCES FOUND.
These instances are recursive, and create a new type-class problem which will have metavariables.
Possible solution: remove the instance attribute or make it a local instance instead.
Currently this linter does not check whether the metavariables only occur in arguments marked with `out_param`, in which case this linter gives a false positive. -/
#check @is_cyclotomic_extension.finite_dimensional /- The following arguments become metavariables. argument 1: (S : set ℕ+) -/
```

I am not sure I understand what this means, so I made it a lemma instead. Note that this means you may sometimes need

```
local attribute [instance] is_cyclotomic_extension.finite_dimensional
```

(this will give also separability).

#### Sebastien Gouezel (Nov 17 2021 at 13:10):

It means that in general Lean can not guess what `S`

should be, to apply this instance, so it can go crazy.

#### Anne Baanen (Nov 17 2021 at 13:30):

Would it make sense for `is_cyclotomic_extension S K L`

to have `S`

as an `out_param`

(or even a field of `is_cyclotomic`

)? That is, given `K`

and `L`

, is there a canonical choice of `S`

?

#### Anne Baanen (Nov 17 2021 at 13:32):

Probably not, since `L`

might have more roots than assumed by your lemma.

#### Riccardo Brasca (Nov 17 2021 at 13:32):

I don't think so: $\mathbb{Q}(\zeta_6)$ is both a third and a sixth cyclotomic extension

#### Anne Baanen (Nov 17 2021 at 13:35):

Right, so you probably don't want to write `[is_cyclotomic_extension K L] (h : n ∈ is_cyclotomic_extension.root_degrees)`

instead of `[is_cyclotomic_extension {n} K L]`

.

#### Anne Baanen (Nov 17 2021 at 13:35):

Where `root_degrees`

is the set of all `n`

such that `X^n - 1`

has a root in `L`

#### Anne Baanen (Nov 17 2021 at 13:40):

No, it'd be even more complicated since `is_cyclotomic_extension {n} K L`

also asserts that `L = K(ζₙ)`

.

#### Riccardo Brasca (Nov 17 2021 at 13:43):

Yes, `is_cyclotomic_extension S K L`

means that `L`

is the `K`

-extension given by all the `n`

-roots of unity, for all `n`

in `S`

. But given `L`

there is no way to recover `S`

(that is not unique).

#### Anne Baanen (Nov 17 2021 at 13:44):

Hmm, if are there no cases in practice where `S`

has to be infinite then we could make `[finite_dimensional K L]`

a parameter to `is_cyclotomic_extension`

. But there probably are :P

#### Anne Baanen (Nov 17 2021 at 13:45):

So you'd get:

```
class is_cyclotomic_extension (s : finset ℕ+) [finite_dimensional K L] : Prop :=
```

#### Riccardo Brasca (Nov 17 2021 at 13:47):

In this project there is no need for infinite `S`

, (even singletons are enough) but if we want the most general definition (to be used someday in mathlib) then infinite `S`

will be useful, for example the maximal abelian extension of `Q`

will be cyclotomic, and that's nice.

#### Riccardo Brasca (Nov 17 2021 at 13:49):

Especially @Filippo A. E. Nuccio will be not so happy if a cyclotomic extension has to be finite

#### Anne Baanen (Nov 17 2021 at 13:49):

Ok, I've run out of tricks to avoid making `is_cyclotomic_extension.finite_dimensional`

a lemma and `haveI`

'ing it back into the assumptions when needed.

#### Filippo A. E. Nuccio (Nov 17 2021 at 13:51):

Indeed, I won't be happy, especially if this will land in `mathlib`

: the cyclotomic extension $\mathbb{Q}(\zeta_{p^\infty})$ would not be a cyclotomic one...

#### Alex J. Best (Nov 17 2021 at 14:05):

We could just name it finite cyclotomic instead then? I'm guessing there will be lots of things which are only true for the $\mathbf Q(\zeta _n)$'s and not for the infinite extension, so we will need a distinction at some point?

#### Anne Baanen (Nov 17 2021 at 14:09):

So we would add a typeclass of the form `[finite_cyclotomic_extension (s : finset ℕ) K L]`

to abbreviate `[cyclotomic_extension (s : set ℕ) K L] (h : s.is_finite)`

?

#### Riccardo Brasca (Nov 17 2021 at 14:10):

We can have a class `is_cyclotomic_extension_finite`

or something similar: it is just `is_cyclotomic_extension`

plus `finite_dimensional`

#### Anne Baanen (Nov 17 2021 at 14:11):

The issue is that `is_cyclotomic_extension_finite`

would need `finite_dimensional`

as a parameter anyway, so it wouldn't help abbreviate much.

#### Anne Baanen (Nov 17 2021 at 14:13):

(Unless of course we add a feature to Lean that expands `[[is_cyclotomic_extension_finite s K L]]`

to something like `[field K] [field L] [algebra K L] [finite_dimensional K L] [fintype s] [is_cyclotomic_extension s K L]`

.)

Last updated: Dec 20 2023 at 11:08 UTC