Cyclotomic fields

Stream: maths

[Riccardo Brasca]

@Eric Rodriguez If you want refactor the definition of cyclotomic polynomials pleas go ahead.
But the current API should suffice to prove that the splitting field of cyclotomic n Z is the same as the splitting field of X^n-1. We know that the roots if cyclotomic n Z (in C) are the primitive roots of unity.

[Riccardo Brasca]

Are you planning to do some Galois theory after that?

[Eric Rodriguez]

Yes, that's the plan. I was hoping to get some more general results (I think they're equal if X^n-1 is separable in R) but I'm not averse to the specialised results if that's what's easiest, too

[Riccardo Brasca]

Oh yes, I mean in characteristic 0.

[Riccardo Brasca]

In any case we know that cyclotomic n Z is irreducible and we know its roots, so mathematically there is not a lot to do, but of course in Lean the story is different. But I think that if there is something missing is rather about splitting fields in general than about cyclotomic polynomials. (Of course there a lot of missing results about cyclotomic polynomial, but for Galois theory what we have should suffice).

[Riccardo Brasca]

I am asking because I think that a very very interesting middle sized project is Fermat Last Theorem for regular primes. I don't know if someone else is working on it, but if this is not the case I would like to think about it.

[Antoine Chambert-Loir]

Could one define the cyclotomic polynomials as the unique sequence $(\Phi_n)$ of monic polynomials with integer coefficients characterized by the formula $T^n-1=\prod_{d\mid n} \Phi_d$ holds?

[Kevin Buzzard]

you'd have to simultaneously make the definition and the proof that polynomials exist which satisfy the property, but this can be done

[Kevin Buzzard]

Alternatively you could define them to be "Phi(n) is T^n-1/prod_{d|n, d<n}Phi(d) if this is a polynomial, and 37 otherwise" and then prove later on that none of them are 37

[Riccardo Brasca]

This is essentially what Johan was proposing. But let me stress that we already have a definition, and a pretty good API (up to irreducibility). I maybe chose the wrong definition at the beginning, going through the complex numbers, but before thinking about alternative definitions we should ask ourselves if it is worth the effort of reproving all the results.

[Kevin Buzzard]

actually I think Phi(0) might be 37

[Riccardo Brasca]

We already add this discussion one year ago :). Currently cyclotomic 0 R = 1.

[Kevin Buzzard]

but it doesn't have degree phi(0)=2 ;-)

[Riccardo Brasca]

docs#polynomial.degree_cyclotomic says it's true for all n, so I think 0.totient = 0.

[Yaël Dillies]

That makes sense from my point of view, as no element strictly smaller than 0 is coprime with 0.

[Riccardo Brasca]

BTW, what I was proposing to get rid of the use of complex numbers in much simpler than redoing everything: it suffices to have a char 0 field with all the primitive roots of unity (like Q bar). I should check, but maybe we can even use a different field for every n, and then the splitting field of X^n-1 would be enough.

[Riccardo Brasca]

Of course this not for any mathematical reasons, it is just to avoid having import analysis.complex.roots_of_unity at the beginning of a morally "algebraic" file.

[Kevin Buzzard]

So we're saying there are three approaches. There's a totally "hands-on" approach where you define Phi_n recursively in $\Z[X]$, there's an approach via Galois theory where you work in the splitting field of $X^n-1$ (so it imports a whole bunch of algebra files) and there's an approach via using the complex numbers (where you import some analysis files). The "hands-on" approach will need very few imports but you might have to work hard and I guess it's not clear whether there's any point in doing so just to shorten the import tree -- you would be making mathlib more incomprehensible. The approach via splitting fields -- you won't have to import the complex numbers and a proof that they're algebraically closed (actually no, you only need a basic theory of roots of unity which is much easier), but you will have to import quite a bit of field theory.

[Riccardo Brasca]

For those that are not following the flt-regular stream: we are discussing about the definition of cyclotomic extensions/fields. We want a super general definition, even if of course we are going to work in a much more specific case. Does anyone have in mind something called "cyclotomic extension" that is not captured by the following?

import field_theory.splitting_field
import data.pnat.basic

class is_cyclotomic_extension (K L : Type*) [field K] [field L] [algebra K L] (S : set pnat) :=
(splits (a : pnat) (ha : a ∈ S) : polynomial.splits (algebra_map K L) (polynomial.X^(a : ℕ) - 1))
(adjoint_roots : algebra.adjoin K { b : L | ∃ a : pnat, a ∈ S ∧ b^(a : ℕ) = 1 } = ⊤) -- or some other equivalent condition

[Filippo A. E. Nuccio]

Do you really want to restrict to field K and field L? It might be useful to say that $\mathbb{Z}[\zeta_n]$ is a cyclotomic extension.

[Riccardo Brasca]

docs#polynomial.splits is for fields. But don't worry, we have docs#integral_closure.is_integral_closure for that.

[Riccardo Brasca]

So the idea is to have cyclotomic extensions of fields and their ring of integers (of course with the lemma that says it's enough add a primitive root of unity).

[Filippo A. E. Nuccio]

Yes, I know the integral_closure business; but I am wondering if it is reasonable to impose that a "cyclotomic algebra tower" be only defined for fields.

[Filippo A. E. Nuccio]

(deleted)

[Riccardo Brasca]

Well, to be honest I am not even sure what that notation means. In real math, when we write $\mathbb{Z}[\alpha]$ we often mean the ring of integers of $\mathbb{Q}(\alpha)$.

[Riccardo Brasca]

We rarely speak about the subalgebra generated by $\alpha$, unless it is already integrally closed

[Filippo A. E. Nuccio]

No, I am not so sure; $\mathbb{Z}[\sqrt{5}]$ is a very honest order in $\mathbb{Q}(\sqrt{5})$

[Riccardo Brasca]

OK, probably I rarely use that :innocent:

[Riccardo Brasca]

But what definition do you propose? We cannot say that a polynomial is split over a ring

[Filippo A. E. Nuccio]

I think it would be a problem to only have full rings of integers; for instance, if one day we develop global CFT, it would be important to develop general orders.

[Riccardo Brasca]

Wait, maybe the condition splits is useless

[Filippo A. E. Nuccio]

We can say it splits over a domain, where there are at most as many roots as the degree?

[Riccardo Brasca]

I mean that I don't want to do the refactor

[Filippo A. E. Nuccio]

I understand, and it makes sense.

[Filippo A. E. Nuccio]

But indeed, do you need the splitting condition? For instance, we define ring of integers for every field (including positive char!, or the reals) as the integral closure of $\mathbb{Z}$. It might be disgusting, but you do not need any finiteness condition on it.

[Filippo A. E. Nuccio]

Can't you define a Prop called contains_nth_root_of_one by saying that $\Phi_n$ has at least one root, and then define that an algebra tower $A/B$ is cyclotomic if the Prop is satisfied?

[Riccardo Brasca]

Is it OK in characteristic $p$ for $\Phi_p$?

[Riccardo Brasca]

Yes, it seems it is

[Riccardo Brasca]

class is_cyclotomic_extension (K L : Type*) [comm_ring K] [ring L] [algebra K L] (S : set pnat) :=
(ex_root (a : pnat) (ha : a ∈ S) : ∃ r : L, polynomial.aeval r (polynomial.cyclotomic a K) = 0)
(adjoint_roots : algebra.adjoin K { b : L | ∃ a : pnat, a ∈ S ∧ b^(↑a : ℕ) = 1 } = ⊤)

[Riccardo Brasca]

Do we say that $\mathbb{F}_p$ is the $p$-th cyclotomic extension of $\mathbb{F}_p$?

[Eric Rodriguez]

Riccardo Brasca said:

Do we say that $\mathbb{F}_p$ is the $p$-th cyclotomic extension of $\mathbb{F}_p$?

Yes, I think this is what was suggested earlier

[Filippo A. E. Nuccio]

Why not? I think it is better to add a lemma saying that "nothing happens" rather than adding a constraint.

[Riccardo Brasca]

Ah, I am stupid, this is always the extension generated by the primitive $p$-th roots of unity (there are no primitive $p$-th roots of unity in $\mathbb{F}_p$, so that's OK)

[Filippo A. E. Nuccio]

Well, I wanted to add a :+1: but certainly don't want to agree on your "I am stupid"... :wink:

[Filippo A. E. Nuccio]

What I like of the above definition is that it also allows for infinite cyclotomic extensions, because you do not require that S is a finset. Indeed, when we will do Iwasawa theory, it will be important to have the cyclotomic $\mathbb{Z}_p$-extension at our disposal.

[Filippo A. E. Nuccio]

By the way, I have been thinking about the (S : set pnat) business. I am wondering if it would not be more appropriate to let S be a sub-lattice of pnat (or of nat) when the (positive) naturals are ordered by division. This would allow to use Galois connections to state the theorem that the $n$-th cyclotomic field is contained in the $m$-th whenever $n\mid m$. Otherwise, the result becomes a bit painful to state (divisibility is always defined in nat but "often" means nothing) and more painful to prove: whereas Galois connections are really natural and cute (@Patrick Massot and @Yaël Dillies , dont' you agree ? :wink: )

[Yaël Dillies]

They really are cute! But how do you state that S is a sublattice?

[Yaël Dillies]

Unless I misunderstood, does that mean we should define a type synonym for any type where division makes sense?

[Yaël Dillies]

Then S : set (div_order nat) or S : set (div_order pnat) would be more appropriate.

[Yaël Dillies]

However we'll need to quotient by the units to even get a partial order...

[Filippo A. E. Nuccio]

You are right. What I had in mind is that it is useful to be sure that S is itself a (div)-lattice. So, for instance, rather than considering the singleton a : set nat one should consider the lattice of all divisors of a. They give rise to the same cyclotomic extension, but with the Galois connection bonus.

[Filippo A. E. Nuccio]

And as long as nat is concerned, there are not so many units...

[Filippo A. E. Nuccio]

At any rate, it is vital to wait for @Riccardo Brasca 's opinion on all this, since he is the one defining cyclotomic extensions.

[Kevin Buzzard]

I don't immediately see how to use Galois connections because we don't have a type of all cyclotomic fields

[Filippo A. E. Nuccio]

Not yet, but this was Riccardo's project, to define them. And my point was whether it is better to attach a cyclotomic field to a subset of nat or to some sort of division-lattice in it, so that we can later state the existence of a Galois connection.

[Kevin Buzzard]

If we defined a choice of $\overline{\mathbb{Q}}$ (e.g. the subfield of $\mathbb{C}$) then we could define cyclotomic fields as subfields of this, and also define $Gal(\overline{\mathbb{Q}}/\mathbb{Q})$.

[Kevin Buzzard]

After all, we defined $\mathbb{C}$ and that has automorphisms

[Filippo A. E. Nuccio]

My experience with Dededind domains would rather suggest to keep everything moving, so defining a predicate is_cyclotomic_extension L K to say that L is obtained by adjoining the root of a cyclotomic polynomial to K whatever K is.

[Johan Commelin]

I agree that it's not clear that Galois connections can be used here. Basically, we would need to define

def lattice_of_cyclotomic_fields := _

But I don't think it will be very nice to work with terms of that type.

[Filippo A. E. Nuccio]

Hmm...I see what you mean, but coming from the Iwasawa-theoretic perspective, this would seem quite reasonable to me. The way Iwasawa theory attaches gadgets (class groups, ell. curves or cohomology thereof) to "layers" in cyclotomic extensions seems to be described pretty well as a Galois connection

lattice_of_cyclotomic_fields -> bleah

I might not see some hidden problem, though.

[Johan Commelin]

In Iwasawa theory, is this an honest lattice, or is it a category (with Galois groups as automorphism groups for the object = cyclotomic fields).

[Johan Commelin]

Because maybe we should use (adjoint) functors instead of Galois connections.

[Filippo A. E. Nuccio]

I would really think that it is a honest lattice; but may be I should better understand when is it better to speak in terms of lattices and when in terms of categories. In #docs.galois_connection I read "A Galois connection is a pair of functions l and u satisfying l a ≤ b ↔ a ≤ u b. They are special cases of adjoint functors in category theory, but do not depend on the category theory library in mathlib." and I have the feeling that the whole machinery of category theory would not be very useful in practice for Iwasawa theory.

[Johan Commelin]

So all fields are embedded in a fixed algebraic closure? And you don't consider different embeddings?

[Filippo A. E. Nuccio]

Indeed, it never happened to me to consider different embeddings while doing Iwasawa theory...

[Kevin Buzzard]

Cyclotomic extensions are abelian extensions, so the subtle problem of whether a number field should be regarded as coming with a fixed embedding into the complexes is reduced to the simpler problem of understanding their Galois groups

[Kevin Buzzard]

Filippo might never have changed his embedding into the complexes but will have considered the Galois group of a cyclotomic field over Q

[Filippo A. E. Nuccio]

Sure I did! At any rate, I would be happy in general to get a clearer picture on when are Galois connections/insertions the best choice as opposed to categorical adjunctions.

[Adam Topaz]

In the other stream I originally had in mind to use truncation_sets for S (which might additionally be closed under lcm). What do you think about that idea?

[Adam Topaz]

Another issue in positive characteristic is that you can add as many powers of p as you like without changing the property

[Filippo A. E. Nuccio]

Do you mean truncated sets?

[Filippo A. E. Nuccio]

Concerning positive char, I agree that nothing happens, but what is the problem in the definition?

[Adam Topaz]

Oh I mean truncation sets in the sense of, e.g., http://math.uchicago.edu/~drinfeld/Seminar-2019/Witt_vectors/Hesselholt%20on%20Witt%20vectors.pdf

[Filippo A. E. Nuccio]

Oh, great. I was not aware of this notion. Sure, it makes sense and really goes in the direction I had in mind.

[Filippo A. E. Nuccio]

I confess I still somewhat feel that setting up Galois would make Iwasawa-theory life easy: for instance, you could say that the assignment $n \mapsto \mathcal{C}_n$ is a Galois connection where $\mathcal{C}_n$ is a group (e.g. the class group) attached to the field of degree $p^n$ in a cyclotomic tower.

[Filippo A. E. Nuccio]

A part from this, I think it would be important to allow for infinite truncation sets.

[Adam Topaz]

For sure. I don't want any finiteness restriction on S

[Adam Topaz]

There should be something like a Galois connection btw. Maybe just an adjunction between the lattice of truncation sets and the category of cyclotomic extensions (which is not a lattice since there are automorphisms).

[Filippo A. E. Nuccio]

Ah, I see the business with lattices and categories, now: thanks!

[Adam Topaz]

You probably can use the category of all algebras over the base field. The functor in one direction takes a set S and gives the cyclotomic extension associated to it, and in the other direction you take an algebra and send it to the set S of all n such that X^n-1 splits in the algebra.

[Filippo A. E. Nuccio]

Truncation sets might indeed be the right context!

[Filippo A. E. Nuccio]

Yes, it seems to make sense.

[Filippo A. E. Nuccio]

The only problem is that "the cyclotomic extensions associated to it" does not quite exist, right? One needs to pick up an alg closed field - or something like that.

[Filippo A. E. Nuccio]

I would rather consider the category of all $K$-subalgebras in a $K$-algebra $L$, and let $L$ vary.

[Riccardo Brasca]

I am not ignoring your messages, and your help is really appreciated. I will read everything after having fixed a problem with the current def

[Adam Topaz]

@Filippo A. E. Nuccio you are right, to define the functor from S to algebras, it might be easier to choose an algebraic closure and work inside there.

[Kevin Buzzard]

Filippo A. E. Nuccio said:

Ah, I see the business with lattices and categories, now: thanks!

Categories in Lean have two universes associated with them -- the universe where the objects live and the universe where the morphisms live. If you imagine a category where morphisms live in Prop then you get exactly a preorder :-)

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Filippo A. E. Nuccio said:

Ah, I see the business with lattices and categories, now: thanks!

Categories in Lean have two universes associated with them -- the universe where the objects live and the universe where the morphisms live. If you imagine a category where morphisms live in Prop then you get exactly a preorder :-)

Oh, this is very nice a description indeed! Thanks.

[Kevin Buzzard]

and then all the adjoint functor stuff just precisely translates into Galois connections in this special case.

[Kevin Buzzard]

Unfortunately my memory was that Scott once tried to let categories have Props as morphisms but things didn't work out for some reason, so he changed them all back to types.

[Filippo A. E. Nuccio]

Ah, I see. But as long as preorders exist, we can call these special categories that way...

[Kevin Buzzard]

For some reason, quiver is allowed to have Hom sets in Prop, but not category_struct (see the "v+1" in that definition)

[Kevin Buzzard]

However it's still a cool mental model to have :-)

[Riccardo Brasca]

Late to the party, but currently we have a characteristic predicate

universes u v

variables (S : set ℕ+) (A : Type u) (B : Type v) [comm_ring A] [comm_ring B] [algebra A B]

class is_cyclotomic_extension :=
( ex_root (a : ℕ+) (ha : a ∈ S) : ∃ r : B, aeval r (cyclotomic a A) = 0 )
( adjoint_roots : ∀ x, x ∈ adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } )

[Riccardo Brasca]

And a "model"

@[derive [field, algebra K]]
def cyclotomic_field : Type w := (cyclotomic n K).splitting_field

lemma is_cyclotomic_extension : is_cyclotomic_extension {n} K (cyclotomic_field n K) := sorry

defined over a field K for S a singleton.

[Adam Topaz]

Just playing around with this idea @Filippo A. E. Nuccio:

import field_theory.is_alg_closed.algebraic_closure
import field_theory.adjoin
import algebra.category.Algebra.basic
import category_theory.category.preorder
import field_theory.splitting_field

universe u
variables (F : Type u) [field F]

open category_theory

noncomputable theory

structure FieldExtension :=
(K : Type u)
[str : field K]
[alg : algebra F K]

namespace FieldExtension

variables (K : FieldExtension F)

instance has_coe_to_sort : has_coe_to_sort (FieldExtension F) Type* := ⟨λ K, K.K⟩

instance : field K := K.str
instance : algebra F K := K.alg

instance : category (FieldExtension F) :=
{ hom := λ K L, K →ₐ[F] L,
  id := λ K, alg_hom.id _ _,
  comp := λ A B C f g, g.comp f }

variable {F}

def of (E : Type u) [field E] [algebra F E] : FieldExtension F := ⟨E⟩

def ι (K : FieldExtension F) : F →+* K := algebra_map _ _

end FieldExtension
open polynomial

def to_set : FieldExtension F ⥤ (set pnat) :=
{ obj := λ A, { n | splits A.ι (X^(n : ℕ)-1) },
  map := λ A B f, hom_of_le $ λ x hx, begin
    have : B.ι = ring_hom.comp f.to_ring_hom A.ι,
    { ext t,
      exact (f.commutes t).symm },
    rw this,
    apply splits_comp_of_splits,
    exact hx,
  end }

def to_algebra : (set pnat) ⥤ FieldExtension F :=
let Fbar := algebraic_closure F in
{ obj := λ S, FieldExtension.of $
    intermediate_field.adjoin F {x : Fbar | ∃ (n : ℕ+) (hn : n ∈ S), x^(n : ℕ) = 1},
  map := λ S T f, subalgebra.inclusion $ intermediate_field.adjoin.mono _ _ _ $ begin
    rintros x ⟨n,hn,hx⟩,
    refine ⟨n, le_of_hom f hn, hx⟩,
  end,
  map_id' := begin
    intros S,
    ext t,
    simpa,
  end,
  map_comp' := begin
    intros A B C i j,
    ext t,
    simpa,
  end }

I wanted to prove the adjunction as well, but I have to go teach :expressionless:

[Filippo A. E. Nuccio]

Very nice!

[Riccardo Brasca]

I guess we can have some interplay with a more down to Earth interpretation, right? Like group and Group and so on.

[Riccardo Brasca]

I agree that such an abstract approach can be useful sometimes, but what will happen when we have to prove that (1-z)^p =... or a similar very very concrete result? Of course it will be provable, at end the objects are the same, but I am afraid it will be annoying.

[Riccardo Brasca]

It seems that it's enough to prove something like is_cyclotomic_extension S K (to_algebra S) to make the link between the categorical def and the "concrete" one.

[Antoine Chambert-Loir]

Riccardo Brasca said:

Well, to be honest I am not even sure what that notation means. In real math, when we write $\mathbb{Z}[\alpha]$ we often mean the ring of integers of $\mathbb{Q}(\alpha)$.

To be honest, I've never seen any use of this convention, and I would not recommend it.

[Antoine Chambert-Loir]

Riccardo Brasca said:

But what definition do you propose? We cannot say that a polynomial is split over a ring

If the polynomial is monic, it may sense to say that it factors as a product of monic terms of degree 1 .

Moreover, the book Modern Computer Algebra by von zur Gathen and Gerhard, ISBN: 0-521-82646-2, defines the splitting algebra $S$ of a monic degree $n$ polynomial $P\in R[T]$ as the algebra generated by $n$ indeterminates $a_1,\dots,a_n$ quotiented by the relations that say that $P=(T-a_1)\dots (T-a_n)$. This algebra is free of rank $n!$ over $R$, it has an action of the symmetric group $\mathfrak S_n$. If $R$ is a field, then this algebra is artinian, the symmetric group acts transitively on the set of maximal ideals, the residue fields are splitting extensions of $P$., and the fixator of any maximal ideal in $\mathfrak S_n$ is “the” Galois group of $P$.

[Riccardo Brasca]

It surely makes sense mathematically. I meant it's not in mathlib, and I prefer not spending two months in writing 100 stupid lemmas about a new notion if it's possible

[Yaël Dillies]

Well, isn't that the point of those big projects? :stuck_out_tongue:

[Antoine Chambert-Loir]

Riccardo Brasca said:

It surely makes sense mathematically. I meant it's not in mathlib, and I prefer not spending two months in writing 100 stupid lemmas about a new notion if it's possible

I don't know whether it is useful to include it in mathlib, and I don't claim somebody should.
I just claim this is a meaningful mathematical notion, and having it in mind may be useful to think about the topic.

[Riccardo Brasca]

Sure, I completely agree!

[Eric Wieser]

Am I correct in reading the above as a proposed more general definition of docs#polynomial.splitting_field? Or is it a separate concept?

[Adam Topaz]

@Eric Wieser Antoine's suggestion won't quite generalize the splitting field, but it's related. If you apply that construction in the case where the base is a field, and mod out by some maximal ideal, you would indeed get "the" splitting field (rather, "a" splitting field).

[Adam Topaz]

One point where I think this construction could be very useful is in generalizing docs#polynomial.splits

[Adam Topaz]

I.e. we could say that a polynomial f : R[X] splits w.r.t $\iota : R \to S$ if $\iota$ factors through the algebra in question.

[Antoine Chambert-Loir]

Eric Wieser said:

Am I correct in reading the above as a proposed more general definition of docs#polynomial.splitting_field? Or is it a separate concept?

It is a separate, but related, concept. If you apply the “splitting algebra” to a separable polynomial over a field, you get a separable algebra which is a product of fields, all isomorphic to the splitting field extension. If the polynomial is not separable, the algebra you get may not be a field, it may have nilpotent elements. (Already for $P=T^2$, what you get is $k[a,b]/(a+b,ab)=k[a]/(a^2)$.)

[Riccardo Brasca]

After some weeks working on the flt-regular project, we realized that the definition of is_cyclotomic_extension we are using is maybe too general. The definition is basically "generated by the roots of the n-th cyclotomic polynomial". You can have a look at #10849 or at the full project if you are curious.

The problem is that, for example, the $5$ cyclotomic extension of $\mathbb{F}_5$ is trivial, and in practice it is not true that we have n-th primitive roots of unity in a n-th cyclotomic extension. The math is clear (I even have a Lean proof the following): if $L/K$ is a $n$-th cyclotomic extension and $n \neq 0$ in $K$ then everything is OK, but if $K$ is of characteristic $p > 0$ and $n = p^s m$ with $p$ and $m$ coprime, then we only have $m$-th primitive roots of unity in $L$.

My question is what can we do in Lean? Having hn : (↑n : _) ≠ 0 is getting annoying, and in practice, for flt-regular, we are only interested in the char_zero case. Of course char_p cyclotomic extensions are interesting, but maybe not the $p$-th cyclotomic extension of $\mathbb{F}_p$. I am thinking about adding to the definition of is_cyclotomic_extension the condition that (↑n : _) ≠ 0. What do you think?

[Riccardo Brasca]

I don't see a way of using efficiently TC resolution here, but it's maybe my fault.

[Eric Rodriguez]

(related discussion here)

[Riccardo Brasca]

To give a more explicit example, consider the following: let B be an A-algbra with [is_cyclotomic_extension n A B] for a given n. Let foo be the theorem that says that, if [is_domain B] and (↑n : B) ≠ 0 then there is a primitive n-th root of unity in B. We want also a bar theorem that, if [is_domain B] [char_zero B] gives the same result as foo, without having to prove (↑n : B) ≠ 0 manually.

[Riccardo Brasca]

Of course we can just prove both foo and bar, but we would like to avoid to duplicate all the theorems with (↑n : B) ≠ 0.

[Adam Topaz]

Maybe the definition of "primitive root of unity" should be changed?

[Adam Topaz]

What definition is currently being used?

[Riccardo Brasca]

The definition looks perfectly fine to me, it's just that there are no $5$-th primitive roots of unity if a field of chracteristic $5$.

[Riccardo Brasca]

The multiplicative order of a primitive n-th root of unity is n.

[Riccardo Brasca]

I mean, this is essentially the definition.

[Adam Topaz]

Well, I would argue that $1$ is a primitive 5th root of unity in a field of characteristic $5$ :)

[Adam Topaz]

But that doesn't satisfy docs#is_primitive_root.

[Riccardo Brasca]

1 ^ 1 = 1 but 5 ∣ 1 is false.

[Adam Topaz]

yeah, of course, so one could change the second condition in that def

[Eric Rodriguez]

are you then saying a primitive root should by definition be a root of the nth cyclotomic poly?

[Adam Topaz]

I guess so, yeah.

[Riccardo Brasca]

But cyclotomic polynomials are defined using primitive roots...

[Riccardo Brasca]

I know they can be defined directly, but I don't think we want to do such a refactor

[Riccardo Brasca]

@Eric Rodriguez what do you think about having results with(↑n : _) ≠ 0 as an explicit assumption (so no fact) and duplicate them in the char_zero case? Maybe at the end of the day the duplicated code is not that much...

[Riccardo Brasca]

For flt-regular we will very quickly specialize to Q, so it doesn't really matter

[Eric Rodriguez]

I still think it may be helpful to have the ne-zero classes that I outlined in the linked thread; TC can then deal with everything (hopefully) - there should only be this new class, and no_smul_zero_divisors involved. That also seems like a decent solution, though; who deals with charp and char zero at the same time without getting headaches ;b

[Yaël Dillies]

Sounds easy enough that abbreviating the appropriate fact and maybe writing some quick API (to avoid always going down to fact.out) should do the job.

[Eric Rodriguez]

we can't have (global) fact instances, Yael

[Eric Rodriguez]

at least, we shouldn't because it slows down TC; but a couple of cases seem to have done it regardless

[Yaël Dillies]

Then don't make it an abbreviation but instead a proper class.

[Riccardo Brasca]

Do you mean something like

class test (R : Type*) [semiring R] (n : ℕ) : Prop :=
(out : ((n : R) ≠ 0))

?

[Eric Rodriguez]

I had N+ in mind, but I think this is better because we can just provide an easy-to-use instance for N+

[Riccardo Brasca]

class test (R : Type*) [semiring R] (n : ℕ) : Prop :=
(out : ((n : R) ≠ 0))

instance foo (R : Type*) [semiring R] [char_zero R] (n : ℕ+) : test R n :=
⟨nat.cast_ne_zero.2 n.pos.ne'⟩

seems to work

[Riccardo Brasca]

If there are no TC resolution problems I propose this way

[Eric Rodriguez]

any idea where in mathlib this could be placed?

[Yaël Dillies]

Close to docs#char_zero?

[Yaël Dillies]

Actually, this is a very sense-making typeclass that can probably be used in many places where we had previously used char_zero.

[Yaël Dillies]

Typically for docs#nat.asc_factorial, docs#pochhammer...

[Yaël Dillies]

char_not_dvd_class?

[Kevin Buzzard]

I have never heard of the phrase "cyclotomic extension" being used to describe anything other than extensions of number fields and p-adic fields BTW

[Yaël Dillies]

To be honest, I have been looking for that typeclass quite a few times already and wondered why we weren't needing it. I guess we actually do!

[Kevin Buzzard]

This "n!=0 in the ground field" thing comes up a lot in representation theory of finite groups too (you often average some construction in the field over the elements of the group)

[Riccardo Brasca]

Time to sleep for me, but it seems we all agree about this new typeclass :)
@Kevin Buzzard I agree about "cyclotomic extension" being used only in characteristic zero, but the mathlib mafia forced us to write the most general definition...

[Alex J. Best]

I'm slightly conflicted about this all now, on the one hand its always nice to get results for free, and it would occasionally be helpful perhaps to reduce cyclotomic rings modulo primes and still have some results.
Buut I really feel like all these weird facts floating around causes unnecessary difficultly / complication for flt-regular at this point.
That said it certainly seems a characteristic not n typeclass is useful, certainly the char_not 2 version will be!

[Adam Topaz]

I think the correct class should be defined around is_unit n. That's a condition that pops up a lot in practice.. much more than the condition that n is nonzero

[Eric Rodriguez]

Isn't that just invertible? This wouldn't work for our use case, as we lifted a couple results through the fraction field, and so we require n ≠ 0 for things in an arbitrary integral domain

[Kevin Buzzard]

For rep theory of finite groups invertible is exactly what you need -- it's not just that the order is nonzero but that you can divide by it.

[Eric Rodriguez]

I began work on the foo typeclass in branch#foo_typeclass... name suggestions, lemma suggestions, and commits not only welcome, but much encouraged ;D

[Eric Rodriguez]

the file is currently src/algebra/foo.lean

[Riccardo Brasca]

Eric Rodriguez said:

I began work on the foo typeclass in branch#foo_typeclass... name suggestions, lemma suggestions, and commits not only welcome, but much encouraged ;D

Can you open a WIP PR so we can comment there?

[Riccardo Brasca]

Concerning n ≠ 0 or invertible, if someone really need invertiblethey can create another class bar, and we can provide an insance of bar having foo and field. I can be wrong, but I have the impression that, when invertible is needed people are working over a field, so this would be enough.

[Damiano Testa]

I agree that most of the times, the ground ring is a field. However, I have sometimes used rings such as $\mathbb{Z}[\frac{1}{2}]$ to explicitly assume that 2 was invertible, but still work over a Dedekind domain.

[Damiano Testa]

The solution of using two typeclasses, one where it is enough to assume that n is non-zero and one where you explicitly invert it, seems good to me, though.

[Damiano Testa]

In the specific context of modular curves of given level $N$, it is quite common to work over $\mathbb{Z}[\frac{1}{N}]$. I find that this is a situation where the two points of view mentioned above (cyclotomic-like stuff and modular/non-modular representation theory) come together.

[Damiano Testa]

Having said that, it is probably reasonable to not develop the whole theory in this generality right now!

[Riccardo Brasca]

Indeed we morally already have the class with $N$ invertible: it is the same as $\mathbb{Z}[1/N]$-algebras.

[Riccardo Brasca]

But I don't know if this can help

[Johan Commelin]

@Riccardo Brasca It wasn't clear to me from your message above whether you know this, but docs#invertible already exists. So we don't need "another class bar".

[Johan Commelin]

But maybe you meant something else with that bar?

[Riccardo Brasca]

We need (n : R) ≠ 0), that is not the same since we also want to work integrally, but this probably gives a good API to generalize, thanks!!

[Johan Commelin]

Right, but that's already your foo class, right? So I didn't understand what you wanted from the bar class.

[Riccardo Brasca]

Yes yes, I was talking about bar without knowing docs#invertible exists

[Johan Commelin]

Ok, gotcha.

[Riccardo Brasca]

Having

instance ne.fact_coe (K R : Type*) (n : ℕ+) [field K] [ring R] [nontrivial R] [algebra K R]
  [hK : fact (((n : ℕ) : K) ≠ 0)] : fact (((n : ℕ) : R) ≠ 0) :=
⟨by simpa using (function.injective.ne (algebra_map K R).injective hK.out)⟩

instance ne.fact_char_zero (K : Type*) (n : ℕ+) [field K] [char_zero K] :
  fact (((n : ℕ) : K) ≠ 0) := ⟨nat.cast_ne_zero.mpr n.pos.ne'⟩

here makes the linter unhappy

/- The `fails_quickly` linter reports: -/
/- TYPE CLASS SEARCHES TIMED OUT.
The following instances are part of a loop, or an excessively long search.
It is common that the loop occurs in a different class than the one flagged below,
but usually an instance that is part of the loop is also flagged.

I tried to debug the error but I don't see where I am creating a loop. Any idea?

[Yaël Dillies]

Might be fails_quickly having too low of a time-out

[Riccardo Brasca]

The linter suggest what to do, here, but for all the flagged instance I just get a timeout, no errors.

[Riccardo Brasca]

I just realized I have no idea how to run the linter locally...is it a scropt somewhere?

[Riccardo Brasca]

I know about #lint at the ed of a file, I am talking about the global linter

[Riccardo Brasca]

Ah, it's probably lean --run scripts/lint_project.lean or something similar

[Eric Rodriguez]

#11033 is the PR; my first run failed pretty badly, I'm going to try take more of a look today

[Eric Rodriguez]

Also, what does it mean by "R is a metavariable"? I thought I was being clever with my char-zero typeclass

[Yaël Dillies]

It means it can't be inferred from context usually. Try using out_param and summoning @Anne Baanen

[Riccardo Brasca]

Looking at docs#invertible, it seems that they decided to not have any global instance. Everything is a def, and instances can be activated when needed.

[Anne Baanen]

Yaël Dillies said:

It means it can't be inferred from context usually. Try using out_param and summoning Anne Baanen

Indeed. The rule is that any parameter to the instance must be an [instance parameter] itself, be inferrable from the goal (i.e. appear after the :), or an out_param.

[Anne Baanen]

However, in this case you can't make S an out_param to foo because it is not uniquely determined by the other parameters to foo.

[Anne Baanen]

Does the argument order matter? I would prefer foo n R, but not sure what TC prefers.

Since n depends on R, the parameters have to stay in that order according to type theory. Although I guess you could use notation `foo` n R := foo_class R n.

My suggestion would be to define class foo {R : Type*} [has_zero R] (n : R) := (out : n ≠ 0) instead, because then you can write foo (n : R).

[Riccardo Brasca]

I tested in flt-regular the strategy of having lemmas instead of instances, and using local attribute [instance] when needed. It seems to work well.

[Eric Rodriguez]

If that's what invertible does, as well, then that seems very reasonable.

[Antoine Chambert-Loir]

Riccardo Brasca said:

After some weeks working on the flt-regular project, we realized that the definition of is_cyclotomic_extension we are using is maybe too general. The definition is basically "generated by the roots of the n-th cyclotomic polynomial". You can have a look at #10849 or at the full project if you are curious.

Sorry to come after the battle, but why such a definition?

Compare with the definition of a solvable-by-radicals extension: you ask that it is generated (inductively) by elements $a$ some positive power of which belong to the base field. Here, I'd say a cyclotomic extension is generated by elements some (strictly positive) power of which is 1. Cyclotomic of cyclotomic is cyclotomic (so I did not define the stuff inductively).

It's easy to refine the definition to ask that the exponents belong to a given subset of $\mathbf N$.

If the base is a field and the extension is finitely generated, you can prove that it is generated by a single root of unity (which is primitive of some order).

If the base is an integrally closed domain, you can prove that its integral closure in a cyclotomic extension of the fraction field is a cyclotomic extension. This amounts to the property that the ring of integers of $\mathbf Q(\zeta_n)$ is $\mathbf Z[\zeta_n]$ (and some limit arguments in the general case).

[Eric Rodriguez]

Antoine Chambert-Loir said:

Riccardo Brasca said:

After some weeks working on the flt-regular project, we realized that the definition of is_cyclotomic_extension we are using is maybe too general. The definition is basically "generated by the roots of the n-th cyclotomic polynomial". You can have a look at #10849 or at the full project if you are curious.

Sorry to come after the battle, but why such a definition?

Compare with the definition of a solvable-by-radicals extension: you ask that it is generated (inductively) by elements $a$ some positive power of which belong to the base field. Here, I'd say a cyclotomic extension is generated by elements some (strictly positive) power of which is 1. Cyclotomic of cyclotomic is cyclotomic (so I did not define the stuff inductively).

It's easy to refine the definition to ask that the exponents belong to a given subset of $\mathbf N$.

If the base is a field and the extension is finitely generated, you can prove that it is generated by a single root of unity (which is primitive of some order).

If the base is an integrally closed domain, you can prove that its integral closure in a cyclotomic extension of the fraction field is a cyclotomic extension. This amounts to the property that the ring of integers of $\mathbf Q(\zeta_n)$ is $\mathbf Z[\zeta_n]$ (and some limit arguments in the general case).

sorry just copying this to make it easier to read. Zulip needs double $s for LaTeX, for some reason

[Eric Rodriguez]

I'm confused how you'd want to state this that's fundamentally different to our definition; our definition is a) we have all nth roots for n in S : set pnat, and b) algebra.adjoin K {these nth roots} = \top.

[Johan Commelin]

I think Antoine wants to avoid mentioning n in the type. @Antoine Chambert-Loir do I understand that correctly?
You want something like

def is_cyclotomic (A B : Type*) [comm_ring A] [comm_ring B] [algebra A B] : Prop :=
∃ s : set B,
  (subalgebra.span A s = ⊤) ∧
  (∀ b ∈ s, ∃ n > 0, b ^ n = 1)

[Will Sawin]

This definition would be different in that it would allow for cyclotomic extensions of infinite degree.

[Adam Topaz]

The definition proposed in #10849 allows for infinite extensions as well.

[Adam Topaz]

But to build on Johan's def above, you can just say that the algebra is generated by the set of roots of unity contained in the algebra. No set needed.

[Antoine Chambert-Loir]

Exactly. And probably something like is_elementarily_cyclotomic where the set s is replaced by a single element b: B.

[Adam Topaz]

One argument to have a set as a parameter is to obtain some sort of adjunction between the lattice of subsets of Nat and the lattice of cyclotomic extensions. But it seems this just complicates things for the FLT project.

[Kevin Buzzard]

You have to be careful here because cyclotomic extensions are only unique up to non-unique isomorphism, so it's not clear to me that they even form a partial order -- there is some automorphism group complicating the picture in my head, at least

[Adam Topaz]

My second lattice should have been category, sorry :grinning_face_with_smiling_eyes:

[Eric Rodriguez]

There's no real complication for the FLT - if we wanted just to prove FLT, we could specialise every result to Q and all of our issues vanish. But we are trying to prove every result at a reasonable level of generality

[Kevin Buzzard]

If we're going for is_cyclotomic_extension, meaning \exists S : set nat, is_S_cyclotomic as a predicate on K-fields or whatever then yeah this looks to me like a category

[Adam Topaz]

You don't even need to restrict the category of algebras. Given a set S, associate the distinguished cyclotomic extension associated to S, constructed in some way. Given an algebra B, construct the set of all n such that the nth cyclotomic poly splits on B. These should be adjoint functors, I think.

[Antoine Chambert-Loir]

Is it so clear that there is such a “distinguished” cyclotomic extension associated to a set S ? I am not sure. Even if S = {n}, the only canonical stuff would be $R[T]/(T^n-1)$, but you could also consider $R[T]/(\Phi_n)$, or $R[T]/(P)$, for some factor of $T^n-1$, even not necessarily irreducible. If you fix a universal algebra in which everything is supposed to live (an algebraic closure), then OK.

[Adam Topaz]

You're right, "distinguished" was not the right word. One just has to come up with some construction (e.g. work inside a chosen algebraically closed extension)

[Kevin Buzzard]

This is all exactly the same as localisation. There's no distinguished localization R S but there is is_localization R S A if A is an R-algebra.

[Kevin Buzzard]

similarly for algebraic_closure and is_algebraic_closure

[Kevin Buzzard]

(the latter apparently doesn't exist)

[Adam Topaz]

I think it does? docs#is_algebraic_closure

[Yaël Dillies]

docs#is_alg_closure

[Kevin Buzzard]

If you fixed an algebraic closure and let all your fields be subfields of that, it would be analogous to the trick they use in the odd order Coq proof where all their groups are subgroups of a big group, i.e. all terms not types

[Kevin Buzzard]

So there is a relative theory one can define (cyclotomic S : subalgebra K L) and an absolute theory defined with models (cyclotomic' S K : Type) and also an absolute theory defined by the universal property (is_cyclotomic S K E with [algebra K E])

[Riccardo Brasca]

Thanks for all the comments.
To be honest I don't think it is worth to fundamentally change the current definition unless it's clear that things will really improve. Our current definition seems to work pretty well, for example we have a sorry free computation of the discriminant in of a p-th cyclotomic extension of the rationals. The only problem so far is that we have this annoying assumption ((n : ℕ) : _) ≠ 0 lying around. It is just an annoyance, the proofs work. I proposed to change the definition just to include this condition, but the new idea using a class seems very promising.

[Riccardo Brasca]

Just a couple of comments:

• is_cyclotomic_extension is definitely needed, cyclotomic_extension is not enough (we have both, and all the theorems use is_cyclotomic_extension).
• I have the impression that forgetting the n (or S) complicates things a little, if we want to say that the discriminant of what we currently call is_cyclotomic_extension p Q L is p^... we have to say something about, for example, the degree of a cyclotomic extension of Q and it seems unnatural.

[Riccardo Brasca]

At the end of the day what we want is that our definition (assuming it is the obvious one for Q and for finite fields in the separable case) is flexible enough to allow us to do some serious math, and the only way to find out is to test it. The computation of the discriminant is currently very similar to the pen and paper proof (except for some combinatoric nightmares unrelated to cyclotomic extensions) and I take this as a very good sign.

[Riccardo Brasca]

Having said this, merry Christmas to everybody !

[Johan Commelin]

I think that one of the benefits of the ∃ s, ... predicate is that the type becomes simpler. So Lean cannot get confused about different n or s working for the same field extension, because all this data is now hidden in a Prop.
But like Riccardo says, this comes at a cost: you now have to work harder to get access to that data.