finite_dimensional instance

Stream: FLT-regular

[Riccardo Brasca]

@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]

It means that in general Lean can not guess what S should be, to apply this instance, so it can go crazy.

[Anne Baanen]

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]

Probably not, since L might have more roots than assumed by your lemma.

[Riccardo Brasca]

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

[Anne Baanen]

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]

Where root_degrees is the set of all n such that X^n - 1 has a root in L

[Anne Baanen]

No, it'd be even more complicated since is_cyclotomic_extension {n} K L also asserts that L = K(ζₙ).

[Riccardo Brasca]

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]

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]

So you'd get:

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

[Riccardo Brasca]

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]

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

[Anne Baanen]

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]

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]

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]

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]

We can have a class is_cyclotomic_extension_finite or something similar: it is just is_cyclotomic_extension plus finite_dimensional

[Anne Baanen]

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]

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

@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]

It means that in general Lean can not guess what S should be, to apply this instance, so it can go crazy.

[Anne Baanen]

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]

Probably not, since L might have more roots than assumed by your lemma.

[Riccardo Brasca]

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

[Anne Baanen]

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]

Where root_degrees is the set of all n such that X^n - 1 has a root in L

[Anne Baanen]

No, it'd be even more complicated since is_cyclotomic_extension {n} K L also asserts that L = K(ζₙ).

[Riccardo Brasca]

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]

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]

So you'd get:

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

[Riccardo Brasca]

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]

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

[Anne Baanen]

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]

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]

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]

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]

We can have a class is_cyclotomic_extension_finite or something similar: it is just is_cyclotomic_extension plus finite_dimensional

[Anne Baanen]

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]

(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].)