Cyclotomic field defn

Stream: FLT-regular

[Eric Rodriguez]

I noticed this project so far is working with adjoin_root cyclotomic. I wonder if instead, X^n-1.splitting_fieldis a better option. I think the second option is better suited to Galois theory (as then the .galhas good defeq) and also easier to generalise to other fields. (it works for all fields with n ≠ 0, whilst I think this one may not)

[Chris Birkbeck]

I'm not sure how much Galois theory this project would strictly need. That said, maybe for more general things it would be good to have something that plays well with Galois theory.

[Eric Rodriguez]

Yeah, the gal stuff I didn't mean for the project specifically, but just for general usage

[Alex J. Best]

I hit some issues I didn't understand with the splitting field definition (see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/synthesized.20type.20class.20instance.20is.20not.20definitionally.20equal/near/258373075)

[Alex J. Best]

That said we should definitely provide an instance of is_splitting_field for our field, would that be sufficient for the gal defeq or no?

[Eric Rodriguez]

.gal is defined as _.splitting_field alg_equiv[polynomial's base ring] _.splitting_field so no; we wouldn't have that the automorphisms are the same, although maybe a nice stopgap is to just provide the alg_equiv between the two and work with that

[Eric Rodriguez]

For non Q rings its also nontrivial to show that the cyclotomic splf is the same as the X^n-1 splf; so that's another thing to consider (I spent a while on this)

[Thomas Browning]

When proving abel-ruffini, I think we did things in terms of X ^ n - 1, and it seemed to work fine. I would suggest making a definition cyclotomic_field n = (X ^ n - 1).splitting_field.

[Thomas Browning]

With regards to Galois theory, polynomial.gal is not what you should be using. We did most Galois theory in terms of arbitrary normal separable field extensions (see galois.lean).

[Thomas Browning]

In particular, a result like "the Galois group of $\mathbb{Q}(\zeta_n)/\mathbb{Q}$ is $(\mathbb{Z}/n\mathbb{Z})^\times$" should be phrased in terms of E ≃ₐ[F] E, rather than (X ^ n - 1).gal.

[Eric Rodriguez]

What is the point of polynomial.gal then?

[Thomas Browning]

Mostly, it's for when you're just interested in Galois groups of polynomials, rather than Galois groups of field extensions more generally. We used it for proving abel-ruffini.

[Riccardo Brasca]

Well, if we are not able to prove is_splitting_field then it means something is missing the cyclotomic polynomial API, or somewhere else. And the whole API for splitting fields should use is_splitting_field.

[Riccardo Brasca]

I am almost tempted to have is_cyclotomic_field

[Johan Commelin]

That would just be is_splitting_field (X ^ n - 1) right? I think that should suffice (at least for now).

[Riccardo Brasca]

Yes, sure

[Riccardo Brasca]

Let me try

[Riccardo Brasca]

OK, is_cyclotomic_field seems to work. But now we have the problem for cyclotomic_ring...

[Chris Birkbeck]

the definition of zeta' in cyclotomic_units seems to now be broken.

[Johan Commelin]

Do we already have some sort of is_ring_of_integers?

[Johan Commelin]

@Anne Baanen I forgot the status...

[Riccardo Brasca]

Chris Birkbeck said:

the definition of zeta' in cyclotomic_units seems to now be broken.

I am fixing it

[Alex J. Best]

Johan Commelin said:

Do we already have some sort of is_ring_of_integers?

I guess something like [is_fraction_ring S L] [is_dedekind_domain S] takes that role?

[Thomas Browning]

Could we just use ring_of_integers, and prove that ring_of_integers equals algebra.adjoin?

[Riccardo Brasca]

Well, the point is that if we use is_cyclotomic_fields (that is nothing else than is_splitting_field) we probably want a characteristic predicate also for the ring of integers.

[Riccardo Brasca]

It seems to me we have to decide how to write things before going on writing lemmas. If we change the basic definition then refactoring everything is going to be rather painful.

Let's start with the cyclotomic field. The most "clean" way I see is to define

class is_cyclotomic_field : Prop := (out : is_splitting_field ℚ K (X ^ n - 1))

for (K : Type*) [field K] [char_zero K]. Of course we can have the explicit model

def cyclotomic_field [fact (0 < n)] : Type* := adjoin_root (cyclotomic n ℚ)

instance : is_cyclotomic_field n (cyclotomic_field n) := sorry

[Riccardo Brasca]

Then everything is stated using (K : Type*) [field K] [char_zero K] [is_cyclotomic_field p K], for example

def zeta' : K :=
classical.some (exists_root_of_splits (algebra_map ℚ K) (is_splitting_field.splits _ _)
  (degree_cyclotomic_pos p ℚ hn.out).ne.symm)

[Riccardo Brasca]

The point of taking this approach is that the definition of cyclotomic_field doesn't matter, it is the fact that it has the is_cyclotomic_field instance that makes everything working.

[Alex J. Best]

Yeah as long as we stick to a reasonable API it doesn't make too much difference which definition we end up using i hope

[Alex J. Best]

And I think it's hard to make decisions about what actual definitions to use without trying them and seeing what goes right and wrong

[Riccardo Brasca]

Ah, we have docs#is_integral_closure!

[Riccardo Brasca]

So I suggest we try to use characteristic predicates everywhere. If at some point it becomes to complicated we can always start using the explicit models, but going the other way is going to be painful

[Eric Rodriguez]

I know this isn't the focus of this project, but I really don't want to have multiple defns all over the place, so:
https://kconrad.math.uconn.edu/blurbs/galoistheory/cyclotomic.pdf suggests that cyclotomic fields works over char p in some cases. I think if we're defining this this way, it may be easier to say that is_cyclotomic_field n means that the nth roots of unity are full, which gives us zeta automatically (#9778 or #9779, can't remember).

[Eric Rodriguez]

The current way, the definition does not work for char p cyclotomic extensions

[Eric Rodriguez]

Oh, I just realised what the second condition actually meant in is_splitting_field (which is totally sensible of course).

[Eric Rodriguez]

Still, the current defn of the predicate isn't good either

[Riccardo Brasca]

I don't understand which definition you propose. You say "is_cyclotomic_field n means that the nth roots of unity are full", but this is satisfied by, for example, the complex numbers. We need in a way or in another specify that it is the splitting field, and not bigger.

[Riccardo Brasca]

And this seems annoying to treat uniformly in char 0 and char p

[Adam Topaz]

Generally a field extension $L|K$ is called "cyclotomic" if it is "generated" by roots of unity.

[Riccardo Brasca]

Yeah, sure, but we want something like the n-th cyclotomic field...

[Adam Topaz]

What's the problem with char p?

[Adam Topaz]

The p-cyclotomic extension of a field $K$ of characteristic $p$ is $K$ itself.

[Riccardo Brasca]

I mean, if I want to use is_splitting_field

[Riccardo Brasca]

I need a base field

[Eric Rodriguez]

What about is_cyclotomic_extension F K n?

[Riccardo Brasca]

Defined using is_splitting_field?

[Thomas Browning]

meaning?

class is_cyclotomic_extension :=
(out : is_splitting_field F K (X ^ n - 1))

[Riccardo Brasca]

We will probably need some abbreviation to avoid writing Q everywhere, but why not

[Adam Topaz]

Thomas Browning said:

meaning?

class is_cyclotomic_extension :=
(out : is_splitting_field F K (X ^ n - 1))

You can even just do

abbreviation  is_cyclotomic_extension := ...

[Riccardo Brasca]

I am done for today, but the basic definitions (for fields) are in src/number_theory/cyclotomic/field/basic.lean. If someone wants to generalize these to is_cyclotomic_extension F n please go ahead. Just be sure to provide the relevant instances, even only in char 0 (sorry as proof is perfectly fine of course).

[Riccardo Brasca]

src/number_theory/cyclotomic/ring/ is for the ring of integers, it contains the statement

lemma eq_adjoin : cyclotomic_ring n =
  algebra.adjoin ℤ {adjoin_root.root (cyclotomic n ℚ)} := sorry

that should be generalized to any R [is_cyclotomic_ring R K].

[Thomas Browning]

Could I have permission to push? (username tb65536)

[Eric Rodriguez]

I'd also like it (although I won't for a bit) [user: ericrbg]

[Scott Morrison]

@Thomas Browning, @Eric Rodriguez, I've sent an invitation with write access.

[Adam Topaz]

Just thinking out loud about defining cyclotomic extensions which will include the infinite case as well. Here's one proposal

import field_theory.splitting_field
import data.pnat.basic

structure truncation_set :=
(S : set pnat)
(div (a b) : a ∈ S → b ∣ a → b ∈ S)

instance truncation_set.has_mem : has_mem pnat truncation_set := ⟨λ a S, a ∈ S.S⟩

class is_cyclotomic_extension (K L : Type*) [field K] [field L] [algebra K L] (S : truncation_set) :=
(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

Note that truncation sets also show up in the theory of big Witt vectors, so it wouldn't hurt to have that definition anyway :)

[Thomas Browning]

If you're dealing with cyclotomic extensions, it seems like you should be looking at subsets of the integers closed under multiplication and taking divisors? (i.e., pick an enatfor each prime).

[Adam Topaz]

Why closed under multiplication?

[Adam Topaz]

With the truncation set approach, I can consider the set {1,5} to consider $K(\mu_5)$, I can consider all powers of 5 to consider $K(\mu_{5^\infty})$, etc

[Alex J. Best]

@Thomas Browning I don't think making is_cyclotomic_field an abbreviation is looking like a good idea, it causes a typeclass loop according to #lint.

[Thomas Browning]

Adam Topaz said:

Why closed under multiplication?

Sorry, I meant closed under lcm.

[Thomas Browning]

Alex J. Best said:

Thomas Browning I don't think making is_cyclotomic_field an abbreviation is looking like a good idea, it causes a typeclass loop according to #lint.

Ah, thanks for pointing this out. I'll push a fix (unless someone gets to it before me)

[Adam Topaz]

Sure, adding a condition saying closed under lcm should be fine. I think if you take the lcm closure T of a truncation set S, then the projection W_T to W_S on big Witt vectors is an isomorphism.

[Thomas Browning]

I feel like this is some sort of "completion" of the divisibility poset (you can "go off to infinity" at any subset of primes). Is there a way to generalize this precisely?

[Riccardo Brasca]

I like Adam's idea. Indeed infinite cyclotomic extensions are more common than char p cyclotomic extensions (at least in what I do). The definition makes sense even for an arbitrary S : set pnat, right? We can have something like is_truncation_set, to use this assumption.

[Riccardo Brasca]

In this way the definition is really super general, and we can always add other conditions later on.

[Chris Birkbeck]

I agree infinite cyclotomic extensions would be great.

[Riccardo Brasca]

And it seems to me S : set nat is fine... if S = {0} we get L = K

[Riccardo Brasca]

This is of course mathematically irrelevant, but usually working with nat is easier than working with pnat.

[Riccardo Brasca]

It seems the most general definition is

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

It makes sense in any characteristic and it allows base ring (instead of a base field) and infinite extensions. Maybe it's more elegant to use root_of_unity in the second condition, but this is only a personal taste.

[Riccardo Brasca]

I don't see any real problem with nat instead of pnat (and I prefer working with nat, the API is better). Does someone see a reason to prefer pnat?

[Adam Topaz]

The definition you wrote won't work with Nat if S contains 0

[Adam Topaz]

The second condition would reduce to saying that L is generated by L

[Johan Commelin]

Hmm, that's a good point (-;

[Adam Topaz]

And the first condition would reduce to saying that Phi_0 which is the constant 1 has a root, which cannot hold in a nontrivial ring

[Riccardo Brasca]

Ah ops, I checked the first one with X^n -1

[Riccardo Brasca]

Well, maybe it is still OK, there no S-extensions if S contains 0, do we care?

[Adam Topaz]

I would prefer pnat tbh. Yes the API is less developed, but in my mind pnat is fundamentally multiplicative whereas Nat is additive. The cyclotomic theory is essentially multiplicative in nature, so it makes sense to me to use pnat

[Riccardo Brasca]

OK, let's try pnat.

[Adam Topaz]

With Nat and 0 in S, the trivial algebra would be cyclotomic :rofl:

[Riccardo Brasca]

Don't tell our colleagues that we really spend time thinking about the $0$-th cyclotomic extension of the trivial ring.

[Riccardo Brasca]

import ring_theory.polynomial.cyclotomic

variables (K L : Type*) [comm_ring K] [comm_ring L] [is_domain L] [algebra K L]

class is_cyclotomic_extension (S : set ℕ+) :=
(ex_root (a : ℕ+) (ha : a ∈ S) : ∃ r : L, polynomial.aeval r (polynomial.cyclotomic a K) = 0)
(adjoint_roots : algebra.adjoin K (set.Union (λ (i : S), ((primitive_roots i L) : set L))) = ⊤)

If there is anyone among you that believes this definition should not take place, speak now or forever hold your peace.

[Chris Birkbeck]

I'm happy with that.

[Johan Commelin]

@Riccardo Brasca I think you can use nicer notation for that union, hopefully.

[Johan Commelin]

Doesn't something like ⋃ i ∈ S, primitive_roots i L work?

[Johan Commelin]

Anyway, probably one of the first things after this definition will be some lemmas that give equivalent statements (e.g. using roots_of_unity instead of primitive_roots). All those versions will probably be useful in the end.

[Adam Topaz]

What's the benefit of using primitive roots as opposed to all nth roots of unity?

[Adam Topaz]

I feel like checking for all roots would be easier, so it might make sense to have that as the constructor

[Riccardo Brasca]

⋃ i ∈ S, (primitive_roots ↑i L) : set L this works. I used primitive roots because roots_of_unity is a subgroup of units of L, so there are even more coercions

[Riccardo Brasca]

but it's doable of course. I think that it's better to use one of them rather than saying manually "roots of X^n-1"

[Johan Commelin]

Maybe the constructor should just use {b : L | ∃ i ∈ S, ... }.

[Johan Commelin]

And then a lemma can say: ooh, in fact you can use a primitive root of unity

[Riccardo Brasca]

Exactly the opposite of what I was thinking, but I trust you guys more than myself :grinning_face_with_smiling_eyes:

[Riccardo Brasca]

So this one?

import ring_theory.polynomial.cyclotomic

variables (K L : Type*) [comm_ring K] [ring L] [algebra K L]

class is_cyclotomic_extension (S : set ℕ+) :=
(ex_root (a : ℕ+) (ha : a ∈ S) : ∃ r : L, polynomial.aeval r (polynomial.cyclotomic a K) = 0)
(adjoint_roots : algebra.adjoin K {b : L | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1} = ⊤)

[Adam Topaz]

That looks good to me!

[Adam Topaz]

I guess this would imply L is commutative. Do we want to infer a comm_ring instance from this or just assume commutativity from the start?

[Johan Commelin]

Should it be phrased as ⊤ ≤ _? Because that's easier to verify?

[Johan Commelin]

Or even just: ∀ x : L, x ∈ algebra.adjoin ...

[Johan Commelin]

Then proofs don't need to start with rw eq_top_iff

[Riccardo Brasca]

Adam Topaz said:

I guess this would imply L is commutative. Do we want to infer a comm_ring instance from this or just assume commutativity from the start?

Good question. We cannot add ... : comm_ring R := sorry, right? Because a priori there could be a diamond for the two ring structures... and I don't want to prove it now if it is more than 5 minutes.

[Johan Commelin]

I wouldn't worry about this for now.

[Johan Commelin]

Just assume commutativity.

[Adam Topaz]

I agree we should just assume commutativity! But I also don't think proving it as an instance would cause a diamond since the ring structure would come from the given ring structure of L.

[Adam Topaz]

It might be a diamond, but the two ring instances would be defeq

[Riccardo Brasca]

Sure, but if our proof is sorry then Lean cannot know the two structure are defeq. But let's just assume commutativity.

[Adam Topaz]

Oh, I see. but if you write

instance [is_cyclotomic_extension K L S] : comm_ring L :=
{ mul_comm' := sorry,
.. (infer_instance : ring L) }

then it should be okay, right?

[Adam Topaz]

Anyway, all rings are commutative so why do we even care ;)

[Riccardo Brasca]

I've never used abbreviation, is this what we want?

variables (S : set ℕ+) (K : Type*) [field K] [char_zero K]

abbreviation is_cyclotomic_extension_rat := is_cyclotomic_extension S ℚ K
``

[Johan Commelin]

_rat is longer than ℚ . So I think I wouldn't bother.

[Riccardo Brasca]

good point

[Thomas Browning]

Here's a worry: If we use an infinite S (e.g., all positive integers), then will algebra.adjoin give us the whole cyclotomic field, or only a subalgebra?

[Riccardo Brasca]

We get the extension generated by all roots of unity.

[Thomas Browning]

Is it obvious that $\mathbb{Q}[\zeta_1,\zeta_2,\ldots]=\mathbb{Q}(\zeta_1,\zeta_2,\ldots)$ (algebra adjoin vs field adjoin)?

[Riccardo Brasca]

Yes, any element is in a finitely generated subalgebra, so you don't have to worry about infinitely many generators.

[Riccardo Brasca]

So we now have a very general definition is_cyclotomic_extension. I don't see how to write down an explicit model in the same degree of generality. For example we can take the splitting field of the cyclotomic polynomials, but this works only over fields and for S a singleton.

[Johan Commelin]

But that doesn't matter right?

[Johan Commelin]

You just setup the API as general as possible. And at the end of your project you specialize to $ℚ(ζ_p)$.

[Thomas Browning]

Riccardo Brasca said:

So we now have a very general definition is_cyclotomic_extension. I don't see how to write down an explicit model in the same degree of generality. For example we can take the splitting field of the cyclotomic polynomials, but this works only over fields and for S a singleton.

You could work in an algebraic closure and take a sup of subalgebras or intermediate fields.

[Riccardo Brasca]

Mmh.. yes, it should be enoug. Once we have $\mathbb{Q}(\zeta_n)$ we can say that algebra.adjoin ℤ ζ is a cyclotomic extension

[Riccardo Brasca]

Where ζ is inside $\mathbb{Q}(\zeta_n)$

[Thomas Browning]

If we really want to be fancy, we could build the infinite cyclotomic extension and take fixed fields by closed subgroups of the Galois group $\widehat{\mathbb{Z}}^\times$. This would also give us the $\mathbb{Z}_p$ from Iwasawa theory.

[Thomas Browning]

(although Lean doesn't know this version of the Galois correspondence yet)

[Adam Topaz]

Thomas Browning said:

If we really want to be fancy, we could build the infinite cyclotomic extension and take fixed fields by closed subgroups of the Galois group $\widehat{\mathbb{Z}}^\times$. This would also give us the $\mathbb{Z}_p$ from Iwasawa theory.

This is where one would have to worry about characteristic...

[Johan Commelin]

@Riccardo Brasca Right, so you will need an instance for $ℚ(ζ_n)$. But that should suffice. (Ok, and maybe for the integral version.)

[Thomas Browning]

Could you do both simultaneously with adjoin_root?

[Adam Topaz]

One question is this: Given a positive integer $n$, should we prove a cyclotomic instance for $S = \{n\}$ or for $S$ the divisors of $n$?

[Thomas Browning]

Adam Topaz said:

One question is this: Given a positive integer $n$, should we prove a cyclotomic instance for $S = \{n\}$ or for $S$ the divisors of $n$?

If we view S as saying "what roots of unity you want to adjoin", then I think {n} is more natural and less cumbersome?

[Riccardo Brasca]

My question is exactly what is (in Lean) the integral version. Over a field we can use splitting_field and we are good. The problem with adjoin_root is that it add the root even if it is already there.

[Thomas Browning]

Would taking an arbitrary irreducible factor of the cyclotomic polynomial work?

[Riccardo Brasca]

It is by def the quotient of the polynomial ring by the polynomial. So if we don't have irreducibility this is very badly behaved

[Riccardo Brasca]

No, we want all the roots

[Thomas Browning]

Could you define some weird induction thing that takes a polynomial, pulls off an irreducible factor and applies adjoin_root, and repeats?

[Thomas Browning]

This might even generalize the splitting field construction

[Johan Commelin]

For the integral version, can't you use integral closure, or algebra.adjoin?

[Riccardo Brasca]

Well, you are proposing to generalize splitting_field to rings. This is surely possible in some sense, but I am afraid it's going to be a lot of work.

Maybe the best thing is, for domains, to just consider algebra.adjoin R T, where T is the set of roots of unity in the field of fraction

[Riccardo Brasca]

Yes exactly, having the field we can work there

[Riccardo Brasca]

people are against using integral_closure since in general the thing is not integrally closed (it is for Z).

[Riccardo Brasca]

I think I wrote down the relevant definitions. They are in number_theory/cyclotomic/basic. I am going to stop for today, but the idea is to get rid of number_theory/cyclotomic/field/basic and number_theory/cyclotomic/ring/basic, so if someone wants to modify the other files please go ahead. It should be easy.

[Riccardo Brasca]

In number_theory/cyclotomic/basic there a lot of sorry, most of them are instances.

[Riccardo Brasca]

I think that using abbreviation/notation or whatever instead of def some of them will become automatic, but in any case the majority should be easy.

[Chris Birkbeck]

Awesome!

[Chris Birkbeck]

So I was just trying to get the class_group stuff working with the new cyclotomic definition, but it gives me an error I'd not seen before maximum class-instance resolution depth has been reached . What does this mean?

[Riccardo Brasca]

It means there is a cycle of instances

[Riccardo Brasca]

Where is it?

[Chris Birkbeck]

aha, I tried the set_option trace.class_instances true but I cant really interpret the output to see the problem. (Sorry I'm still quite new at this!)

[Chris Birkbeck]

I pushed the changes if you want to see the error for yourself

[Riccardo Brasca]

I've never understood the output if set_option trace.class_instances true: the problem is surely written, but it is too long to read.

[Riccardo Brasca]

I suggest we try to have master compiling without errors all the time. But we can of course use other branches to play with errors

[Riccardo Brasca]

But no problem for your commit :)

[Chris Birkbeck]

Ah sure that's probably a good idea! :)

[Chris Birkbeck]

Looking at the output it seems something happen here [class_instances] cached instance for field ℚ rat.field

[Riccardo Brasca]

I've probably missed something about the new open command, but I don't understand how Lean find cyclotomic_ring that is now called something like new_cyclotomic_field.cyclotomic_ring

[Chris Birkbeck]

Oh I added the open new_cyclotomic_field I thought it would just mean I dont have to type new_cyclotomic_field.cyclotomic_ring everytime.

[Riccardo Brasca]

There is no open here or am I blind?

[Riccardo Brasca]

But let me check the real error

[Chris Birkbeck]

Oh wait, maybe I pushed the wrong thing.

[Chris Birkbeck]

Yes I forgot to hit save before pushing, sorry!

[Riccardo Brasca]

I get an invalid namespace name 'new_cyclotomic_field' error.

[Chris Birkbeck]

Yeah, did you delete that namespace?

[Riccardo Brasca]

I didn't touch the namespace, there is something I don't understand. Let me see what really does the new open.

[Chris Birkbeck]

No I can see in your commit that you removed the that namespace from cyclotomic/basic

[Chris Birkbeck]

But either way, thats not the problem. the class instance thing is still there.

[Riccardo Brasca]

Ah ops, I messed up. Let's fix this, since there are two cyclotomic_ring and I want to be sure Lean is working with the good one.

[Riccardo Brasca]

So,

instance a : is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ) := sorry

noncomputable instance class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite
    ℤ (cyclotomic_ring n ℤ ℚ) ℚ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _,

end

complains with

failed to synthesize type class instance for
n : ℕ+
⊢ is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)

This usually means there is a diamond somewhere.

[Riccardo Brasca]

Can you check that all the instances I wrote in number_theory/cyclotomic/basic are good? For example that I didn't write algebra field ring instead of algebra ring field. I am checking them too, but two pairs of eyes are better.

[Riccardo Brasca]

Mmh,

instance cyclotomic_ring_int_is_integral_closure :
  is_integral_closure (cyclotomic_ring n A K) A (cyclotomic_field n K) := sorry

noncomputable instance class_group.fintype_of_cyclotomic_ring (n : ℕ+) [euclidean_domain A] :
  fintype (class_group (cyclotomic_ring n A K) (cyclotomic_field n K)) :=
begin
  letI : algebra A K := infer_instance,
  refine @class_group.fintype_of_admissible_of_finite
    A (cyclotomic_ring n A K) K (cyclotomic_field n K)
    _ _ _ _ _ _ _ _ _ _ _
    _ _ _ _ _ _ _ _ _ _,

end

says

failed to synthesize type class instance for
A : Type u_1,
K : Type u_2,
_inst_1 : comm_ring A,
_inst_2 : field K,
_inst_3 : is_domain A,
_inst_4 : algebra A K,
_inst_5 : is_fraction_ring A K,
n : ℕ+,
_inst_6 : euclidean_domain A,
_inst : algebra A K := infer_instance
⊢ algebra A K

I don't understand.

[Riccardo Brasca]

Lean wants

@algebra.{u_1 u_2} A K (@comm_ring.to_comm_semiring.{u_1} A (@euclidean_domain.to_comm_ring.{u_1} A _inst_6))
    (@ring.to_semiring.{u_2} K (@division_ring.to_ring.{u_2} K (@field.to_division_ring.{u_2} K _inst_2)))

and we have

@algebra.{u_1 u_2} A K (@comm_ring.to_comm_semiring.{u_1} A _inst_1)
    (@ring.to_semiring.{u_2} K (@division_ring.to_ring.{u_2} K (@field.to_division_ring.{u_2} K

[Riccardo Brasca]

I have to stop for a couple of hours, but something is confusing me. It seems there a diamond here, but it's strange nobody found it before.

[Riccardo Brasca]

Oh, OK, I see

[Riccardo Brasca]

euclidean_domain does not need ring

[Riccardo Brasca]

Bu the other problem is still there

[Alex J. Best]

There is the algebra Q diamond and the rat field diamond, both of which will likely continue to cause us issues

[Chris Birkbeck]

Sorry I was away talking to a student.
Riccardo Brasca said:

Can you check that all the instances I wrote in number_theory/cyclotomic/basic are good? For example that I didn't write algebra field ring instead of algebra ring field. I am checking them too, but two pairs of eyes are better.

Sorry I was afk talking to a student. I'll have a look now.

[Chris Birkbeck]

I have a noob question. What is a diamond? Is it when something can inherit the same properties from two different sources?

[Kevin Buzzard]

Right -- it's when you suddenly find that you have two instances of e.g. [algebra ℤ R] which are perhaps propositionally equal but not definitionally equal, because Lean mananged to find two ring homomorphisms from the integers to R in its type class system.

[Kevin Buzzard]

This is an issue because type class inference relies on definitional equality to work, basically, so diamonds can cause obscure/hard-to-diagnose errors.

[Kevin Buzzard]

The famous example, the one which really made me understand diamonds, is that metric spaces and topological spaces are classes in Lean, and there's an instance which takes a metric space to a topological space, and an instance which takes two metric spaces and returns a metric space structure on the product, with the L^2 norm say ($d((x_1,y_1),(x_2,y_2)):=\sqrt{(d(x_1,y_1)^2+d(x_2,y_2)^2}$) and there's an instance which takes two topological spaces and returns a topological space structure on the product.

[Kevin Buzzard]

This gives a diamond! Because if you start with two metric spaces, then the product topology coming from the topologies has a basis which are "rectangles" (i.e. of the form $U\times V$) whereas the topology coming from the metric has a basis which are "discs" (i.e. distance from a fixed point is $<r$).

[Kevin Buzzard]

It's a theorem that these two topologies are the same, but the proof is certainly not rfl!

[Chris Birkbeck]

Aha that makes perfect sense, thank you!

[Kevin Buzzard]

Even if you make the metric on the product equal to the sup norm you still don't get rfl for your proof that the two topologies coincide, because one is "basis generated by products of all open sets" and the other is "basis generated by products of all open balls"

[Kevin Buzzard]

The astonishing fix for this diamond, I think due to Johannes Hoelzl, is to make the topology part of the definition of a metric space!

[Kevin Buzzard]

So a metric space in Lean is [what you think a metric space is] + [a topology] + [a proof that the topology is equal to the one induced by the metric]

[Kevin Buzzard]

and then in the instance which defines a metric on the product of two metric spaces, you define the topology to be the product topology, and then you insert the proof that the metric product induces the product topology in the definition of the instance. This trivially fixes the diamond.

[Kevin Buzzard]

If you've ever looked at the definition of a group in mathlib recently, you'll see that it contains a map $\mathbb{Z}\times G\to G$ and a proof that this map sends $(n,g)$ to $g^n$, and this random extra field is there for the same sort of reason.

[Chris Birkbeck]

Ok great, I'll add diamonds to my list of things to worry about :)

[Johan Commelin]

Chris Birkbeck said:

I have a noob question. What is a diamond? Is it when something can inherit the same properties from two different sources?

Since yesterday we have a new way to answer this question! Meet our glossary :octopus:
https://leanprover-community.github.io/glossary.html#diamond

[Chris Birkbeck]

Johan Commelin said:

Chris Birkbeck said:

I have a noob question. What is a diamond? Is it when something can inherit the same properties from two different sources?

Since yesterday we have a new way to answer this question! Meet our glossary :octopus:
https://leanprover-community.github.io/glossary.html#diamond

Oh this is great! thank you

[Johan Commelin]

Credits to Julian Berman for writing it!

[Kevin Buzzard]

I think that a mathematician would understand my explanation better than Julian's, because they would know a lot more about topological spaces than about terms and types. I should PR an extension of the explanation with the example maybe (when I'm out of teaching hell next week)

[Johan Commelin]

Yeah, maybe the extended explanation can be written up somewhere (a gist?) and then we link to that?

[Johan Commelin]

I guess the glossary should try to be concise, and link to other places for details.

[Kevin Buzzard]

Gotcha

[Johan Commelin]

In fact, the "See Also" part already links to the forgetful inheritance discussion from the mathlib paper.

[Johan Commelin]

Which contains your metric space example.

[Riccardo Brasca]

@Chris Birkbeck I am back at the computer. The diamond I was talking was completely my fault, I had [ring A] [euclidean_domain A], so there were two structures of ring on A, and that confused Lean. Now I have euclidean_domain A but I still get the maximum class-instance resolution. Let's see what's wrong

[Chris Birkbeck]

Kevin Buzzard said:

I think that a mathematician would understand my explanation better than Julian's, because they would know a lot more about topological spaces than about terms and types. I should PR an extension of the explanation with the example maybe (when I'm out of teaching hell next week)

I agree with this. I understand the topology example much more than the typeclass description.

[Chris Birkbeck]

I'm not sure if this helps, but we get the same error if we try and do instance : number_field ℚ := infer_instance

[Chris Birkbeck]

It seems cyclotomic.basic.number_field is what causes it to break

[Riccardo Brasca]

Yes, there is something strange. But

import number_theory.cyclotomic.basic
import number_theory.class_number.finite
import number_theory.class_number.admissible_abs

open algebra polynomial

variable (n : ℕ+)

instance : is_fraction_ring
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field := sorry

noncomputable example :
  fintype (class_group
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field) :=
begin
  have sepKL : is_separable ℚ (cyclotomic n ℚ).splitting_field := sorry,
  haveI iicSRL : is_integral_closure
    (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1}) ℤ
    (cyclotomic n ℚ).splitting_field := sorry,
  refine @class_group.fintype_of_admissible_of_finite ℤ
    (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
    ℚ (cyclotomic n ℚ).splitting_field _ _ _
    _ _ _ _ _ _ _ _ _ _ _ _ _ _ absolute_value.abs_is_admissible _ _ _,

end

works.

[Riccardo Brasca]

I've unfolded the def by hand.

[Riccardo Brasca]

Ah, in

@[derive [comm_ring]]
def cyclotomic_ring : Type* := adjoin A { b : K | b ^ (n : ℕ) = 1 }

K should be cyclotomic_field {n} K!

[Riccardo Brasca]

I am pushing this, that in any case fix a mistake

[Riccardo Brasca]

So,

import ring_theory.polynomial.cyclotomic
import number_theory.class_number.finite
import number_theory.class_number.admissible_abs

open algebra polynomial

variable (n : ℕ+)

instance : is_fraction_ring
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field := sorry

noncomputable example :
  fintype (class_group
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field) :=
begin
  haveI iicSRL : is_integral_closure
    (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1}) ℤ
    (cyclotomic n ℚ).splitting_field := sorry,
  exact class_group.fintype_of_admissible_of_finite ℚ (cyclotomic n ℚ).splitting_field
    absolute_value.abs_is_admissible,
end

works perfectly. But if I add import number_theory.cyclotomic.basic I get the error. So now it's just a matter of bisecting the file to see what causes the problem.

[Riccardo Brasca]

I found the culprit! It's

instance number_field [is_cyclotomic_extension S K L] [number_field K] : number_field L := sorry

And once you know it, the reason is clear: if K is a number field then L is, but I think we know that subfields of number fields are number fields, so Lean goes back to K and then again to L and so on.

[Chris Birkbeck]

Aha this is what it seemed like when I did this instance : number_field ℚ := infer_instance experiment. But I don't know how to fix it.

[Riccardo Brasca]

It has to be a lemma, not an instance.

[Riccardo Brasca]

But we have another problem, and this time it really seems a diamond.

[Chris Birkbeck]

Riccardo Brasca said:

It has to be a lemma, not an instance.

Ahh ok.

[Chris Birkbeck]

Riccardo Brasca said:

But we have another problem, and this time it really seems a diamond.

Oh no

[Riccardo Brasca]

This

noncomputable instance class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  have h : is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ) := infer_instance,
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  _
  _ _ _ _ _ _ _ _ _,

end

fails with

failed to synthesize type class instance for
n : ℕ+,
h : is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)
⊢ is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)

And if you try to put h insted of the isolated underscore, there is a giant type mismatch at application error.

[Yakov Pechersky]

(deleted)

[Riccardo Brasca]

I wanted to see the two types, that's why I used have.

[Riccardo Brasca]

So h has type

  @is_scalar_tower ℤ ℚ (@cyclotomic_field n ℚ rat.field)
    (@sub_neg_monoid.has_scalar_int ℚ (@add_group.to_sub_neg_monoid ℚ rat.add_group))
    (@smul_with_zero.to_has_scalar ℚ (@cyclotomic_field n ℚ rat.field)
       (@mul_zero_class.to_has_zero ℚ
          (@mul_zero_one_class.to_mul_zero_class ℚ
             (@monoid_with_zero.to_mul_zero_one_class ℚ
                (@semiring.to_monoid_with_zero ℚ
                   (@comm_semiring.to_semiring ℚ
                      (@comm_ring.to_comm_semiring ℚ
                         (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field))))))))
       (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
          (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
             (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                   (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                      (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                         (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                            (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                               (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                  (@cyclotomic_field.field n ℚ rat.field))))))))))
       (@mul_action_with_zero.to_smul_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
          (@semiring.to_monoid_with_zero ℚ
             (@comm_semiring.to_semiring ℚ
                (@comm_ring.to_comm_semiring ℚ
                   (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field)))))
          (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
             (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
                (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                   (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                      (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                         (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                            (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                               (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                                  (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                     (@cyclotomic_field.field n ℚ rat.field))))))))))
          (@module.to_mul_action_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
             (@comm_semiring.to_semiring ℚ
                (@comm_ring.to_comm_semiring ℚ
                   (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field))))
             (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                   (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                      (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                         (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                            (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                               (@cyclotomic_field.field n ℚ rat.field)))))))
             (@algebra.to_module ℚ (@cyclotomic_field n ℚ rat.field)
                (@comm_ring.to_comm_semiring ℚ
                   (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field)))
                (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                   (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                      (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                         (@cyclotomic_field.field n ℚ rat.field))))
                (@cyclotomic_field.algebra n ℚ rat.field)))))
    (@sub_neg_monoid.has_scalar_int (@cyclotomic_field n ℚ rat.field)
       (@add_group.to_sub_neg_monoid (@cyclotomic_field n ℚ rat.field)
          (@add_comm_group.to_add_group (@cyclotomic_field n ℚ rat.field)
             (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                   (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                      (@cyclotomic_field.field n ℚ rat.field)))))))

[Riccardo Brasca]

And the type Lean wants is so long I cannot post here :upside_down:

[Riccardo Brasca]

But it must come from the def of cyclotomic_field n ℚ, so it's fixable I hope.

[Riccardo Brasca]

I've managed to reduce the size of the error, now the two types are almost readable. It's the error in this file.

[Riccardo Brasca]

@add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _ has type

  @is_scalar_tower ℤ ℚ (@cyclotomic_field n ℚ rat.field)
    (@sub_neg_monoid.has_scalar_int ℚ
       (@add_group.to_sub_neg_monoid ℚ
          (@add_comm_group.to_add_group ℚ
             (@ring.to_add_comm_group ℚ
                (@normed_ring.to_ring ℚ
                   (@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field)))))))
    (@smul_with_zero.to_has_scalar ℚ (@cyclotomic_field n ℚ rat.field)
       (@mul_zero_class.to_has_zero ℚ
          (@mul_zero_one_class.to_mul_zero_class ℚ
             (@monoid_with_zero.to_mul_zero_one_class ℚ
                (@semiring.to_monoid_with_zero ℚ
                   (@ring.to_semiring ℚ
                      (@normed_ring.to_ring ℚ
                         (@normed_comm_ring.to_normed_ring ℚ
                            (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))))))
       (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
          (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
             (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                (@add_comm_group.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                   (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                      (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                         (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                            (@cyclotomic_field.field n ℚ rat.field))))))))
       (@mul_action_with_zero.to_smul_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
          (@semiring.to_monoid_with_zero ℚ
             (@ring.to_semiring ℚ
                (@normed_ring.to_ring ℚ
                   (@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field)))))
          (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
             (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
                (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                   (@add_comm_group.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                      (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                         (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                            (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                               (@cyclotomic_field.field n ℚ rat.field))))))))
          (@module.to_mul_action_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
             (@ring.to_semiring ℚ
                (@normed_ring.to_ring ℚ
                   (@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
             (@add_comm_group.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                   (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                      (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                         (@cyclotomic_field.field n ℚ rat.field)))))
             (@algebra.to_module ℚ (@cyclotomic_field n ℚ rat.field) rat.comm_semiring
                (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                   (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                      (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                         (@cyclotomic_field.field n ℚ rat.field))))
                (@cyclotomic_field.algebra n ℚ rat.field)))))
    (@sub_neg_monoid.has_scalar_int (@cyclotomic_field n ℚ rat.field)
       (@add_group.to_sub_neg_monoid (@cyclotomic_field n ℚ rat.field)
          (@add_comm_group.to_add_group (@cyclotomic_field n ℚ rat.field)
             (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                   (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                      (@cyclotomic_field.field n ℚ rat.field)))))))

[Riccardo Brasca]

The actual type is still too big to fit in Zulip...

[Marc Masdeu]

Kevin Buzzard said:

I think that a mathematician would understand my explanation better than Julian's, because they would know a lot more about topological spaces than about terms and types. I should PR an extension of the explanation with the example maybe (when I'm out of teaching hell next week)

Isn't this explanation what's in https://leanprover-community.github.io/mathlib_docs/notes.html#forgetful%20inheritance ?

[Kevin Buzzard]

yeah I didn't click through :-)

[Kevin Buzzard]

The diamond error is that Lean is failing to solve

smul_with_zero.to_has_scalar = sub_neg_monoid.has_scalar_int

[Riccardo Brasca]

Ah, thank's!! How did you find it?

[Kevin Buzzard]

noncomputable lemma class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  (by convert @add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _)
  _ _ _ _ _ _ _ _ _,

end

[Kevin Buzzard]

I'm still thinking about it

[Kevin Buzzard]

I am quite confused because

example : (smul_with_zero.to_has_scalar : has_scalar ℤ (cyclotomic_field n ℚ)) = sub_neg_monoid.has_scalar_int :=
begin
  refl,
end

works

[Riccardo Brasca]

Ah, in any case super nice trick using convert to reduce the size of the output.

[Kevin Buzzard]

We've definitely still not got to the bottom of this

[Kevin Buzzard]

noncomputable lemma class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  (by {convert @add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _, sorry})
  _ _ _ _ _ _ _ _ _,
end

That tactic actually compiles without errors, leaving two goals.

[Riccardo Brasca]

The two goals are OK

[Kevin Buzzard]

One is absolute value ℤ ℤ -- so Lean is not inferring it

[Kevin Buzzard]

But the goal before the sorry is not being closed with refl

[Riccardo Brasca]

import number_theory.cyclotomic.basic
import number_theory.class_number.finite
import number_theory.class_number.admissible_abs

variable (n : ℕ+)

section finiteness

open new_cyclotomic_field

--set_option pp.all true

local attribute [-instance] smul_with_zero.to_has_scalar

noncomputable lemma class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  (by {convert @add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _, sorry})
  _ _ _ _ _ absolute_value.abs_is_admissible _ _ _,
end

end finiteness

[Kevin Buzzard]

oh nice! Indeed I'd just discovered that the instance of smul_with_zero.to_has_scalar in the term was not the one that type class inference was discovering.

[Riccardo Brasca]

But the sorry is still there, I have to think about it.

[Johan Commelin]

Uuughh, this all looks really ugly. I'm cheering you on from the side. The joys of spelunking through the depths of mathlibs algebra hierarchy.

[Kevin Buzzard]

My understanding so far is that Riccardo has managed to get type class inference to create a term of type has_scalar ℤ (cyclotomic_field n ℚ) which is not defeq to (smul_with_zero.to_has_scalar : has_scalar ℤ (cyclotomic_field n ℚ))

[Riccardo Brasca]

I agree that it's probably my fault, but I thought that all Z-action were defeq, we did a huge refactor to have this, didn't we?

[Riccardo Brasca]

The definition of cyclotomic_field n K is

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

[Kevin Buzzard]

heh :-) certainly not all int actions are defeq, but somehow the idea is supposed to be that we only ever let Lean see the defeq ones :-)

[Johan Commelin]

That smul_wth_zero must be coming from an "ugly" place, I guess.

[Riccardo Brasca]

@smul_with_zero.to_has_scalar ℤ (@cyclotomic_field n ℚ rat.field)
      (@mul_zero_class.to_has_zero ℤ
         (@mul_zero_one_class.to_mul_zero_class ℤ
            (@monoid_with_zero.to_mul_zero_one_class ℤ
               (@semiring.to_monoid_with_zero ℤ
                  (@comm_semiring.to_semiring ℤ
                     (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain)))))))
      (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
         (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
            (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
               (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                  (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                     (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                        (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                           (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                              (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                 (@cyclotomic_field.field n ℚ rat.field))))))))))
      (@mul_action_with_zero.to_smul_with_zero ℤ (@cyclotomic_field n ℚ rat.field)
         (@semiring.to_monoid_with_zero ℤ
            (@comm_semiring.to_semiring ℤ
               (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain))))
         (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
            (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
               (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                  (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                     (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                        (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                           (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                              (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                                 (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                    (@cyclotomic_field.field n ℚ rat.field))))))))))
         (@module.to_mul_action_with_zero ℤ (@cyclotomic_field n ℚ rat.field)
            (@comm_semiring.to_semiring ℤ
               (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain)))
            (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
               (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                  (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                     (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                        (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                           (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                              (@cyclotomic_field.field n ℚ rat.field)))))))
            (@algebra.to_module ℤ (@cyclotomic_field n ℚ rat.field)
               (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain))
               (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                  (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                     (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                        (@cyclotomic_field.field n ℚ rat.field))))
               (@new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ int.comm_ring rat.field _
                  (@algebra_int ℚ (@ordered_ring.to_ring ℚ rat.ordered_ring))
                  rat.is_fraction_ring)))) =
    @sub_neg_monoid.has_scalar_int (@cyclotomic_field n ℚ rat.field)
      (@add_group.to_sub_neg_monoid (@cyclotomic_field n ℚ rat.field)
         (@add_comm_group.to_add_group (@cyclotomic_field n ℚ rat.field)
            (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
               (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                  (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                     (@cyclotomic_field.field n ℚ rat.field))))))

Very good

[Kevin Buzzard]

The bad instance is coming from algebra.to_has_scalar

[Riccardo Brasca]

Yes, I just arrived to the conclusion that the problem is the Z-algebra structure on the cyclotomic field.

[Riccardo Brasca]

Let me check where it comes from.

[Chris Birkbeck]

Does it come from cyclotomic_field_algebra?

[Kevin Buzzard]

Yes, the bad instance has new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ in it

[Riccardo Brasca]

It's

instance cyclotomic_field_algebra : algebra A (cyclotomic_field n K) :=
((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra

[Chris Birkbeck]

Maybe for it doesn't like that its a composition when defined for Z?

[Riccardo Brasca]

Can it be universe related:

example : (new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ) =
  algebra ℤ (cyclotomic_field n ℚ) := sorry

is not happy with

type mismatch at application
  new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ = algebra ℤ (cyclotomic_field n ℚ)
term
  algebra ℤ (cyclotomic_field n ℚ)
has type
  Type : Type 1
but is expected to have type
  algebra ℤ (cyclotomic_field n ℚ) : Type

[Kevin Buzzard]

that's some type error, you have (term) = (type of the term)

[Kevin Buzzard]

But this works :-/

noncomputable def foo : algebra ℤ (cyclotomic_field n ℚ) := infer_instance
example : new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ = foo n := rfl

[Kevin Buzzard]

oh but that's just because type class inference finds precisely this term

[Kevin Buzzard]

so here's the problem:

-- this is `new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ`
noncomputable def foo : algebra ℤ (cyclotomic_field n ℚ) := by show_term {apply_instance}
-- remove the instance
local attribute [-instance] new_cyclotomic_field.cyclotomic_field_algebra
-- still works, now `algebra_int`
noncomputable def bar : algebra ℤ (cyclotomic_field n ℚ) := by show_term {apply_instance}
-- but they're not defeq
example : foo n = bar n := rfl -- fails

[Kevin Buzzard]

The new instance new_cyclotomic_field.cyclotomic_field_algebra is giving a non-defeq $\Z$-algebra structure

[Chris Birkbeck]

Yeah it must be because its defined as a composition

[Riccardo Brasca]

Oh gosh, thank you

[Chris Birkbeck]

or not, I dont know

[Riccardo Brasca]

In any case this is a problem that we have to solve

[Riccardo Brasca]

Let me see if I have enough time

[Kevin Buzzard]

example (A K L : Type) [comm_ring A] [field K] [field L] [algebra A K] [algebra K L] : algebra A L :=
infer_instance -- fails

Is this expected to fail? (i.e. do I need more imports?) I thought it would be worth looking at how analogues of cyclotomic_field_algebra are defined in mathlib.

[Johan Commelin]

@Kevin Buzzard Yes, that's supposed to fail. You need to use scalar towers.

[Johan Commelin]

Lean cannot guess which K it should be looking for.

[Adam Topaz]

I thought that was the whole point of scalar towers?

[Kevin Buzzard]

So the issue is that if A is the integers and if algebra A K is the instance discovered by type class inference (algebra_int) then we wantalgebra A L to end up also being defeq to this instance.

[Kevin Buzzard]

Right now this fails (of course):

example (K L : Type) [field K] [field L] [algebra K L] :
  (int.cast_ring_hom L : ℤ →+* L) = (algebra_map K L).comp (int.cast_ring_hom K) := rfl -- fails

because the RHS has got some random _inst_3 in it. So

instance cyclotomic_field_algebra : algebra A (cyclotomic_field n K) :=
((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra

will always cause trouble if A = ℤ

[Johan Commelin]

I'm actually surprised that we haven't hit this issue earlier...

[Johan Commelin]

There are tons of instance : algebra A blabla in mathlib. But blabla will always already have an algebra ℤ blabla instance coming from algebra_int.

[Adam Topaz]

maybe algebra_int shouldn't be an instance?

[Kevin Buzzard]

algebra_int has priority 99, perhaps this helps (by which I mean perhaps this is why we didn't run into it before)

[Johan Commelin]

Yeah, maybe. Having algebra_int not be an instance is quite disappointing though.

[Adam Topaz]

The alternative is to have all algebra A B instances extend is_scalar_tower \Z A B or something like that?

[Kevin Buzzard]

That feels very much like how we have solved previous problems of this nature

[Johan Commelin]

Does that even help? You would get an is_scalar_tower ℤ ℤ B, which shows that the two scalar actions are propeq. But they still wouldn't be defeq.

[Adam Topaz]

sigh

[Riccardo Brasca]

I have to stop, but I agree with Johan that it is strange we never encountered this before.

[Johan Commelin]

Maybe this is why:

src/ring_theory/subsemiring.lean
842-/-- The action by a subsemiring is the action by the underlying semiring. -/
843-instance [add_comm_monoid α] [module R' α] (S : subsemiring R') : module S α :=
844:{ smul := (•), .. module.comp_hom _ S.subtype }

src/algebra/module/basic.lean
107-@[reducible] def module.comp_hom [semiring S] (f : S →+* R) :
108-  module S M :=
109:{ smul := has_scalar.comp.smul f,

src/group_theory/group_action/defs.lean
169-  an additive action of `N` on `α` "-/]
170-def comp (g : N → M) : has_scalar N α :=
171:{ smul := has_scalar.comp.smul g }
--
309-@[reducible, to_additive] def comp_hom [monoid N] (g : N →* M) :
310-  mul_action N α :=
311:{ smul := has_scalar.comp.smul g,
--
396-@[reducible] def distrib_mul_action.comp_hom [monoid N] (f : N →* M) :
397-  distrib_mul_action N A :=
398:{ smul := has_scalar.comp.smul f,
--
476-@[reducible] def mul_distrib_mul_action.comp_hom [monoid N] (f : N →* M) :
477-  mul_distrib_mul_action N A :=
478:{ smul := has_scalar.comp.smul f,

[Johan Commelin]

All these examples use .comp for the definition of smul. But they are all defs.

[Kevin Buzzard]

i.e. none of them are instances

[Johan Commelin]

There is also

288-instance lift2_alg {F : intermediate_field K L} {E : intermediate_field F L} : algebra K E :=
289-{ to_fun := (algebra_map F E).comp (algebra_map K F),
290-  map_zero' := ((algebra_map F E).comp (algebra_map K F)).map_zero,
291-  map_one' := ((algebra_map F E).comp (algebra_map K F)).map_one,
292-  map_add' := ((algebra_map F E).comp (algebra_map K F)).map_add,
293-  map_mul' := ((algebra_map F E).comp (algebra_map K F)).map_mul,
294:  smul := λ a b, (((algebra_map F E).comp (algebra_map K F)) a) * b,

So maybe we can construct a problem there when K = ℚ.

[Kevin Buzzard]

rat.algebra_rat is indeed an instance (every char 0 division ring is a Q-algebra)

[Johan Commelin]

So

instance cyclotomic_field_algebra : algebra A (cyclotomic_field n K) :=
((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra

is evil. Right? What are the assumption on A and K here?

[Johan Commelin]

I should clone the repo.

[Chris Birkbeck]

We have [is_domain A] [algebra A K] [is_fraction_ring A K]

[Riccardo Brasca]

K is the fraction field

[Johan Commelin]

Aha. Then I guess we should just make this a def. And provide the relevant is_scalar_tower instances for it (after making it an instance locally).

[Johan Commelin]

Do you think you will need this as an instance a lot?

[Riccardo Brasca]

We are going to work with Z, so a def is perfectly fine

[Johan Commelin]

Certainly, when you specialize to ℤ and ℚ, you can give the "correct" instance, which doesn't cause a diamond.

[Riccardo Brasca]

The definition is much more general than what we need

[Johan Commelin]

Right, that's what I suspected.

[Eric Wieser]

Skimming this thread, I'd claim any algebra instance created with (x.comp y).to_algebra will turn out to be evil

[Kevin Buzzard]

However mathematicians want to say "B is an A-algebra and C is a B-algebra so C is obviously an A-algebra"

[Kevin Buzzard]

because if everything is a commutative ring then "B is an A-algebra" is just code for f : A ->+* B

[Riccardo Brasca]

There is no problem in changing the definition, but I don't see how to get rid of the diamond

[Eric Wieser]

Kevin Buzzard said:

However mathematicians want to say "B is an A-algebra and C is a B-algebra so C is obviously an A-algebra"

That's incompatible with the design currently used by mathlib, which is to say "B is an A-algebra, C is a B-algebra, C is an A-algebra in the obvious way", where the last part is is_scalar_tower A B C.

[Eric Wieser]

I'll try a PR to intermediate_field.lift2_alg to fix the smul-diamond.

[Kevin Buzzard]

But using is_scalar_tower isn't going to fix the diamond, right?

[Eric Wieser]

It fixes one of the two diamonds

[Eric Wieser]

(the one in smul but not the one in algebra_map)

[Eric Wieser]

Done: #10012. It's great when the fix is to delete code! replace actual proofs with "we already proved this"

[Eric Wieser]

At a glance I think this fixes the problem at the top of the thread, since it was a diamond in has_scalar not algebra_map

[Riccardo Brasca]

So, I made cyclotomic_field_algebra a lemma instead of an instance. We can just put

local attribute [instance] new_cyclotomic_field.cyclotomic_field_algebra

if we need it.

[Riccardo Brasca]

Now this is one is solved, the same thing happens with the other is_scalar_tower is docs#class_group.fintype_of_admissible_of_finite, but it is surely the same diamond.

[Riccardo Brasca]

number_theory/cyclotomic/class_group finally compiles without errors :grinning:

[Riccardo Brasca]

Thanks to everybody!

[Riccardo Brasca]

I will try this afternoon to make number_theory/cyclotomic/cyclotomic_units using the new definition.

[Eric Wieser]

I think #10019 might solve some more algebra issues, but I might need to change splitting_field too

[Riccardo Brasca]

Thanks! In any case we can work without the algebra instance (over Z), and have it later.

[Riccardo Brasca]

I don't think we need cyclotomic fields over anything than Q for this project.

[Eric Wieser]

Looking more closely at new_cyclotomic_field.cyclotomic_field_algebra, the diamond is caused by the nasty recursion stuff going on to define the field instance

[Eric Wieser]

The field.zsmul that appears in that recursion is not defeq to the algebra.smul that appears in the algebra recursion

[Eric Wieser]

Here's an example of how recursors can create diamonds:

variables {α β : Type*} (f0 : α) (fs : ℕ → α → α) (g0 : β) (gs : ℕ → β → β)

def rec1 : ℕ → α × β
| 0 := (f0, g0)
| (n + 1) := (fs n (rec1 n).1, gs n (rec1 n).2)

def rec2 : ℕ → α × β
| n := (nat.rec_on n f0 fs, nat.rec_on n g0 gs)

-- not definitionally equal
example (n : ℕ) : rec1 f0 fs g0 gs n = rec2 f0 fs g0 gs n := rfl

-- but equal nonetheless
lemma rec1_eq_rec2 : Π n, rec1 f0 fs g0 gs n = rec2 f0 fs g0 gs n
| 0 := rfl
| (n + 1) := begin
  have := rec1_eq_rec2 n,
  dsimp [rec1, rec2, ←nat.succ_eq_add_one],
  rw this,
  refl,
end

[Chris Birkbeck]

Sorry, I've been afk all day today (and will be on most Thursdays), but I'll try and catch-up on all this today/tomorrow :)

[Eric Wieser]

The replacement for lift_alg2 is merged, did it make any difference?

[Chris Birkbeck]

it's working now! edit: no its not. I hadn't read all the messages :(

[Chris Birkbeck]

Thank you!

[Riccardo Brasca]

You should make the two def an instance to check if it's really working. I can do this tomorrow

[Chris Birkbeck]

Oh no you're right. I made them instances and its complaining about is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)

[Eric Rodriguez]

i just pushed some old work that I did on cyclotomic things, maybe it can give some inspiration for figuring out the general proofs for is_cyclotomic_extension {n} A B

[Eric Rodriguez]

I was looking and thinking, and I think the best way to go about getting any primitive root (at which point the API is good enough for us to do pretty much whatever) is through finding that the cardinality of the roots of unity set is n. I think my specialized argument works, mostly, apart from it requires that X^n-1 splits, whilst we "only" have that there is a root of cyclotomic n F.

We definitely need to assume that our cyclotomic extension is normal, because otherwise we get to the weird Frobenius-y counterexamples, which leads to my final question: do we have a maths-proof that if cyclotomic n F splits, then so does X ^ n - 1? It seems perfectly reasonable to me, but every proof that I'd think of assumes we have a prim-root of unity.

[Riccardo Brasca]

In ready_for_mathlib/cyclotomic there is

lemma is_root_cyclotomic_iff {n : ℕ} {R : Type*} [comm_ring R] [is_domain R] {μ : R}
  : is_primitive_root μ n ↔ is_root (cyclotomic n R) μ := sorry

It shouldn't be difficult.

[Eric Rodriguez]

char_zero simplifies it (it's wrong for some charp; φ₄ ∈ F₂[x], for example) but I don't think it's as trivial as it seems mathematically

[Riccardo Brasca]

Ahahah, yes, that is obviously false, one needs to assume $n \neq 0$ in the base ring.

[Riccardo Brasca]

A simple proof is: let $a$ be a root, then $a^n = 1$ (since $\psi_n$ divides $X^n-1$) so $a$ is a $n$-th root of unity. If $a^m=1$ with $m < n$, then we obtain a repeated root of $X^n-1$, that is impossible.

[Riccardo Brasca]

I used a similar strategy to prove the irreducibility, so all of these is doable without too much effort even in Lean.

[Riccardo Brasca]

To obtain the repeated root we write $X^n-1 = \Psi_n \prod_{i | n, i < n}\Psi_i$, and $X^m-1$ appears in the second product.

[Riccardo Brasca]

Even better: we prove first of all that $a$ is a $n$-th root of unity iff it is the root of some $\Psi_i$ with $i|n$ (this is trivial since we have the product formula). Then it's clear that we obtain a double root.

[Eric Rodriguez]

Ooh, I was looking at the product formula for cyclotomic', which requires a primitive root to be there. Woop! That's good news :) ill try work on this soon

[Eric Rodriguez]

(also #9779 ever relevant...)

[Riccardo Brasca]

cyclotomic' is just implementation, it should never be used unless something is missing in the API for cyclotomic. But then one should add it :)

[Riccardo Brasca]

Ah yes, if we now squarefreeness over any ring even better! For fields it's already there

[Riccardo Brasca]

But docs#polynomial.separable.squarefree is over a field, so one has to generalize this too

[Riccardo Brasca]

I will not have time tomorrow, but I can write all the details on Friday.

[Riccardo Brasca]

@Eric Rodriguez Did you make any progress on the roots of cyclotomic polynomials?

[Riccardo Brasca]

I see you did :)

[Eric Rodriguez]

It's now done!! :) Proof could use with a bit of neatening up but I will do that when I'm not on a potato laptop ;b

[Riccardo Brasca]

Very nice! The only place you uses a field rather than a domain is docs#polynomial.separable.squarefree right?

[Eric Rodriguez]

Yes! And that's actually just too strong of a requirement, too:

import field_theory.separable

variables {F : Type*} [comm_ring F] [is_domain F]

open polynomial
open_locale classical

lemma multiplicity_le_one_of_separable {p q : polynomial F} (hq : ¬ is_unit q)
  (hsep : separable p) : multiplicity q p ≤ 1 :=
begin
  contrapose! hq,
  apply is_unit_of_self_mul_dvd_separable hsep,
  rw ← sq,
  apply multiplicity.pow_dvd_of_le_multiplicity,
  simpa only [nat.cast_one, nat.cast_bit0] using enat.add_one_le_of_lt hq
end

lemma separable.squarefree {p : polynomial F}  (hsep : separable p) : squarefree p :=
begin
  rw multiplicity.squarefree_iff_multiplicity_le_one p,
  intro f,
  by_cases hunit : is_unit f,
  { exact or.inr hunit },
  exact or.inl (multiplicity_le_one_of_separable hunit hsep)
end

[Eric Rodriguez]

oh, maybe it's a bit more dependent on it thinking about it, but I think it just takes replacing ↑n ≠ 0 to is_unit n, possibly

[Riccardo Brasca]

We don't want is_unit n (this is false in the ring of integers), ↑n ≠ 0 is perfect I think.

[Riccardo Brasca]

The main application for us will be the ring of integers in some cyclotomic field

[Riccardo Brasca]

Feel free to add your generalization of separable.squarefree to the project!

[Eric Rodriguez]

the state of the art so far is docs#polynomial.separable_X_pow_sub_C_unit, I've not given much thought to the separability/squarefreeness of X^n-1 in general rings; that's the main issue

[Eric Rodriguez]

it's just the same as the usual code with the typeclasses updated ^^ I will refactor mathlib soon instead

[Riccardo Brasca]

Ah, in docs#polynomial.separable_X_pow_sub_C_unit there is hn : is_unit ↑n...

[Riccardo Brasca]

So we really need fields

[Riccardo Brasca]

We can probably "cheat" using the field of fraction: a root of the cyclotomic polynomial over a domain is a primitive root when considered in in the field of fraction, so it is a primitive root even in the domain.

[Eric Rodriguez]

oh... so it turns out we reinvented the wheel! (EDIT:) docs#polynomial.order_of_root_cyclotomic_eq. The proof looks pretty identical to my proof, too

[Eric Rodriguez]

(yes, it's currently only for zmod, but I assume that's just what was needed)

[Riccardo Brasca]

Oh, and I even wrote that proof!

[Eric Rodriguez]

I'm having a jaunt at all this right now, and I'm just considering how to structure the basic.lean. I think for splitting_field_cyclotomic and most things after it it'll be nice to have the defn of zeta', which is currently in cyclotomic_units (we now get that it's a primitive root for "free"). however, this proof is limited (currently) to fields; is the correct approach to use the localization trick to generalize this result to comm_rings, and then use that there? or just sorry that proof for now, copy everything in, and try work on everything else? it does move it a lot earlier in the import hierarchy

[Riccardo Brasca]

I think it's false for a general ring, but we want it for a domain. The proof using the field of fraction should be easy, right?

[Riccardo Brasca]

But I agree that zeta' should be available as soon as possible

[Eric Rodriguez]

OK, my today has been taken up with the separable generalization, which is now finished: #10337. will be back to flt in a bit :)

[Riccardo Brasca]

I think the definition of is_cyclotomic_extension will not change anymore (at least not in the near future), so it's probably a good idea to finish the basic API and open a PR. I will start working on the sorry in number_theory/cyclotomic/basic, but if you think you have basic results/definition somewhere else (like for example the definition of zeta') don't hesitate to move them to basic.

[Chris Birkbeck]

Awesome. I'm super busy this week, but I should have lots more time for this next week, so I can help with these sorrys (if any remain!)

[Eric Rodriguez]

i've finally had some time to look at some things, but I think this is the sort of thing where I'd want people's inputs. Firstly, I think n : R ≠ 0 will be pretty important for the basic cyclotomic theory, so I propose carrying around in a fact. Everyone accept this as ok?

[Eric Rodriguez]

Secondly, there's a TC timeout in cyclotomic_units:182 - do we worry about it now? Or until we unsorry instances? I don't know how to debug such things

[Riccardo Brasca]

Using := by convert ... instead of := ... seems to fix the timeout for me. I didn't investigate why.

[Eric Rodriguez]

What do you think of the fact idea?

[Kevin Buzzard]

My student Ashvni has been working with p-adic stuff and told me yesterday that fact p.prime drove her nuts :-) In the definition of the p-adic numbers the decision was made to make p the parameter rather than hp : prime p, so what we write in lean corresponds to what we write in papers, but it also makes things quite inconvenient in practice apparently. On the other hand we used facts quite a bit in the perfectoid project. @Johan Commelin did facts drive you nuts? Don't forget the alternative, which is just to carry hn : n ≠ 0 around by hand

[Johan Commelin]

We didn't use fact in the perfectoid project. Do you mean LTE?

[Johan Commelin]

I found the facts quite convenient. Certainly fact p.prime has been quite pleasant to use for me.

[Johan Commelin]

What exactly are the problems that Ashvni is hitting?

[Riccardo Brasca]

@Eric Rodriguez I don't have any strong opinion about your fact idea, but it is surely true that n : R ≠ 0 is needed in a lot of places. In my opinion we should try to keep things as modular as possible, so we should have a subfolder of the (nonexistent) number_theory/cyclotomic folder called separable (or whatever) where we put all the results that need n : R ≠ 0. We should try to see if having the assumption as fact really reduces what we have to write.

[Johan Commelin]

Here is one reason why fact is sometimes a powerful tool: before we used fact we had two separate types zmod and zmodp. The latter was only defined for primes, and it carried a field instance. But with fact we could unify these, and now zmod n has a ring instance, but in the presence of fact p.prime then zmod p will also have a field instance.

[Alex J. Best]

Yes, this is a very important feature of fact, I think the annoyance comes when you have to things that are based on fact and things that just use a regular hypothesis. You have to start writing out everywhere, not so bad, but also take care that tactics can see the fact. For instance library_searhc

import data.nat.prime

lemma a {p : ℕ} [fact p.prime] : 2 ≤ p :=
begin
  library_search, --fails

end


lemma b {p : ℕ} (hp : p.prime) : 2 ≤ p :=
begin
  library_search, --works

end

[Alex J. Best]

I'm not sure if the intended use of fact is to make the hypotheses regular parameters and do haveI : fact p.prime := hp when you know you are going to need it, or to make the hypotheses facts and use have hp : p.prime := fact.out when you want the actual thing

[Johan Commelin]

My rule of thumb is: if you would start the LaTeX version of the file with "For the rest of this paper, we fix a prime number p", then you use fact. But if you are working with various prime numbers, or various types of prime numbers, then regular parameters is probably better.

[Alex J. Best]

Yeah for the library as it is right now you really do need both, so you have to convert between the two at some point

[Johan Commelin]

Note that you can also assume [hp : fact p.prime]. Then hp.1 is a term of type p.prime. Which works quite smoothly, I think.

[Alex J. Best]

But in my example you still have to either know the lemma library searched for, or ahead of time add the line have := hp.1 to your context for every fact

[Johan Commelin]

Or fix library_search :rofl:

[Alex J. Best]

You have to make a lot of other tactics fact aware too though!

[Alex J. Best]

Like assumption for instance

[Johan Commelin]

Ooh, sure, if you want interop with all tactics.

[Johan Commelin]

I was thinking of the discussion that extracts proof fields out of structures, before running a tactic such as library_search.

[Alex J. Best]

Well I would just love all the benefits of fact without having to modify my proofs and habits, at least thats what gets to me about it

[Alex J. Best]

Yeah it would be nice to have a "unfact" tactic, but its still unfortunate to run it at all

[Riccardo Brasca]

I will not have time to work on this during the weekend, but if someone wants to contribute I am stuck at (this is in number_theory/cyclotomic/basic)

lemma union_left [h : is_cyclotomic_extension T A B] (hS : S ⊆ T) :
  is_cyclotomic_extension S A (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }) :=
begin
  refine ⟨λ n hn, _, λ b, _⟩,
  { obtain ⟨b, hb⟩ := ((iff _ _ _).1 h).1 n (hS hn),
    refine ⟨⟨b, subset_adjoin ⟨n, hn, _⟩⟩, _⟩,
    { rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← is_root.def] at hb,
      suffices : (X ^ (n : ℕ) - 1).is_root b,
      { simpa [sub_eq_zero] using this },
      rw [← (eq_cyclotomic_iff n.pos _).1 rfl],
      exact root_mul_right_of_is_root _ hb },
      rwa [← subalgebra.coe_eq_zero, aeval_subalgebra_coe, subtype.coe_mk] },
  { sorry }
end

The goal is

...
b: ↥(adjoin A {b : B | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1})
⊢ b ∈ adjoin A {b : ↥(adjoin A {b : B | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1}) | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1}

I didn't tried hard, but working with subtypes is annoying! One this is done (or maybe a better reformulation?) the ending the proof of

lemma finite [h₁ : fintype S] [h₂ : is_cyclotomic_extension S A B] : finite A B

should be easy.

[Eric Rodriguez]

this is such a pesky goal...

[Riccardo Brasca]

I agree... But I don't see a better formulation of the result, that is meaningful

[Yakov Pechersky]

You should be able to say "cases b with b hb" to destruct the subtype

[Riccardo Brasca]

I have to sleep now, but that seems to help, thank you!

[Riccardo Brasca]

Is someone working on the last sorrys in number_theory/cyclotomic/basic? If not I will try to work on them tomorrow.
Once these sorrys are done I think we can PR the definition.

[Chris Birkbeck]

So I had said I was going to help with these, but I've had less time than I thought, so haven't been able to look at this :(

[Chris Birkbeck]

Sorry!

[Riccardo Brasca]

No problem!

[Eric Rodriguez]

Yes, I was going to work on them,but I got distracted by the cyclotomic positive proof and degree applications... Hopefully I'll give them a look tonight!

[Riccardo Brasca]

I've proved four sorrys. Now all the basic facts about is_cyclotomic_extension are sorry free. Any ideas on something basic missing? Otherwise would just go for a PR and see what people think about this.

[Chris Birkbeck]

Go for it :) I guess we'll find out later on what other things we need (if any).

[Eric Rodriguez]

I just uploaded a proof that cyclotomic_field n K is a cyclotomic extension (which is pretty much previous work refactored a bit). this approach currently doesn't scale to cyclotomic_ring, and I don't see an obvious workaround; I'm not too versed in no_smul_divisors and such like, but what we need is that the algebra_map K (cyclotomic_ring n K) is injective (which morally it is as it's morally the inclusion map), but I don't see an obvious way to prove that from what we have about algebras and such, e.g. by sidetracking through the fraction ring. If I don't come up with a better solution by tomorrow, I'm just going to sprinkle some char_zero and work on actual FLT instead of side-tracking myself about char-p cyclotomic extensions of domains...

[Riccardo Brasca]

Great work! I am still quite busy this week, but I will try to have a look. I am not completely sure we will need that cyclotomic_ring is a cyclotomic extension, maybe knowing that its field of fraction is cyclotomic_field will be enough.

[Eric Rodriguez]

I've just bumped again, if anyone has time please check I've not moved things wrongly.

[Alex J. Best]

I also tried to bump today, and made basically the same changes as you so mostly LGTM.
However one difference is I came to the conclusion that we should just assume

instance is_cyclotomic_extension [char_zero K] :

as IMO it is way too unwieldy to keep this fact about nested coes floating around, what do you think? For this project I don't think we will need this theory for positive characteristic (though it might be handy), but if we do need it I think we should worry about the extension to that case then rather than having this extra TC now.

[Alex J. Best]

I think the instance is still true if the characteristic divides n right? its just the proof is very annoying

[Eric Rodriguez]

I don't know the proof if the fact isn't true; it's definitely a completely different route to get there, though (I thought I found some counterexamples in Sage a couple days ago, but it was just a off-by-one error instead of anything real). But yea, I definitely think we should have that instance and forget about non-char zero. I added a fact that implies it, but maybe it's better to make my current instance a def and make a char_zero instance for now

[Riccardo Brasca]

Which result are you talking about?

[Riccardo Brasca]

In any case I am pretty sure that for this project char_zero is enough.

[Eric Rodriguez]

Whether cyclotomic_field is actually a cyclotomic extension in the case where is_root_cyclotomic_iff doesn't apply

[Riccardo Brasca]

I think this is true because if F is a field of characteristic p and n = m * p ^ s, with p that does not divide m, then cyclotomic n F = (cyclotomic m F) ^(p^s - p^(s-1)), but we don't have this result yet

[Riccardo Brasca]

Sorry for my long absence, I was super busy lately. I am preparing a PR with a definition of cyclotomic field, so this will be fixed once and for all.

[Riccardo Brasca]

#10849

[Eric Rodriguez]

sorry for always posting here when I make minimal progress; we're close to finishing off the proof of cyclotomic_ring being a cyclotomic extension; I'm once again stuck on proving things are non-zero... if people want to take a look, that's there, else hopefully I'll wake up with inspiration into how to turn algebra_map K (cyclotomic_ring n K) being injective into subalgebra.inclusion \bot (cyclotomic_ring n K) being injective (which is already in the library). Considering I always seem to work on the boring stuff lately, is there any other part of the proof people would like me to help out with instead? I'm happy to help anywhere^^

[Riccardo Brasca]

Having a look now

[Riccardo Brasca]

This is indeed quite annoying, but I will do it.

[Riccardo Brasca]

If you are looking for something slightly more interesting, there is zeta'.embeddings_equiv_primitive_roots in src/number_theory/cyclotomic/cyclotomic_units.lean.

[Riccardo Brasca]

This is false in general, but true over ℚ, that is enough for us

[Riccardo Brasca]

It probable makes sense to think a little bit to a more general version

[Riccardo Brasca]

Injectivity of algebra_map A (cyclotomic_ring n A K) is done.

[Riccardo Brasca]

Now the only sorry left in src/ready_for_mathlib/cyclotomic/basic.lean is

is_fraction_ring (cyclotomic_ring n A K) (cyclotomic_field n K)

I am not sure we need this now, so I made it a lemma, just to bu sure it's not used automatically somewhere

[Riccardo Brasca]

Ops, we already use it... so let me prove the instance

[Riccardo Brasca]

@Eric Rodriguez I see we are working on the same proof... no problem of course.
Have you any idea for surj?

[Riccardo Brasca]

It seems the only nontrivial statement for is_fraction_ring...

[Riccardo Brasca]

Ops, you finished eq_iff_exists, and your proof is better than mine :)

[Eric Rodriguez]

I'm currently thinking of getting the power basis for cyclotomic_field; hopefully that then just lets us use the existing fraction_ring instance to do everything else

[Eric Rodriguez]

I think it's in ring_theory.adjoin.basis or something

[Riccardo Brasca]

Using that cyclotomic_field n K is adjoin K ... I think we can do it with algebra.adjoin_induction without too much trouble

[Riccardo Brasca]

Currently we know this if (((n : ℕ) : A) ≠ 0, but sooner or later we will remove this

[Eric Rodriguez]

The proof of the cyclotomic power thing doesn't seem too bad, just mildly irritating, too. I think Alex's homogenization+factorization stuff will come in handy there

[Alex J. Best]

What's the cyclotomic power thing?

[Eric Rodriguez]

ɸ_{np^k}(x) = ɸₙ(x^p^k)/ɸₙ(x^p^(k-1)) modulo off by one errors

[Riccardo Brasca]

Nonsense

[Riccardo Brasca]

My math proof consists of going to C, where everything splits, and comparing the roots (with multiplicity)

[Alex J. Best]

That does seem annoying, well I hope it helps but it still seems tricky yes

[Riccardo Brasca]

In any case we don't need it

[Alex J. Best]

I thought it was helpful to get rid of some of the char_zero assumptions (or p \ne 0 in K)?

[Riccardo Brasca]

I don't see where we need it, but of course it would be nice to do everything in full generality.

Having this assumption seems to me a good compromise since I will be very easy to remove it when someone will prove the full result

[Riccardo Brasca]

src/ready_for_mathlib/cyclotomic/basic.lean is finally sorry free.

[Riccardo Brasca]

The proof of

is_fraction_ring (cyclotomic_ring n A K) (cyclotomic_field n K)

is not that nice, but at least it works

[Riccardo Brasca]

I've PRed more basic properties of cyclotomic extensions in #11264.

[Eric Rodriguez]

by the way, the algebra_rat diamond came up again when doing the galois proof. was fairly easy to get round when I realised it happened. I'm now going to re-fix ne_zero and then get some sleep

[Eric Rodriguez]

I noticed this project so far is working with adjoin_root cyclotomic. I wonder if instead, X^n-1.splitting_fieldis a better option. I think the second option is better suited to Galois theory (as then the .galhas good defeq) and also easier to generalise to other fields. (it works for all fields with n ≠ 0, whilst I think this one may not)

[Chris Birkbeck]

I'm not sure how much Galois theory this project would strictly need. That said, maybe for more general things it would be good to have something that plays well with Galois theory.

[Eric Rodriguez]

Yeah, the gal stuff I didn't mean for the project specifically, but just for general usage

[Alex J. Best]

I hit some issues I didn't understand with the splitting field definition (see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/synthesized.20type.20class.20instance.20is.20not.20definitionally.20equal/near/258373075)

[Alex J. Best]

That said we should definitely provide an instance of is_splitting_field for our field, would that be sufficient for the gal defeq or no?

[Eric Rodriguez]

.gal is defined as _.splitting_field alg_equiv[polynomial's base ring] _.splitting_field so no; we wouldn't have that the automorphisms are the same, although maybe a nice stopgap is to just provide the alg_equiv between the two and work with that

[Eric Rodriguez]

For non Q rings its also nontrivial to show that the cyclotomic splf is the same as the X^n-1 splf; so that's another thing to consider (I spent a while on this)

[Thomas Browning]

When proving abel-ruffini, I think we did things in terms of X ^ n - 1, and it seemed to work fine. I would suggest making a definition cyclotomic_field n = (X ^ n - 1).splitting_field.

[Thomas Browning]

With regards to Galois theory, polynomial.gal is not what you should be using. We did most Galois theory in terms of arbitrary normal separable field extensions (see galois.lean).

[Thomas Browning]

In particular, a result like "the Galois group of $\mathbb{Q}(\zeta_n)/\mathbb{Q}$ is $(\mathbb{Z}/n\mathbb{Z})^\times$" should be phrased in terms of E ≃ₐ[F] E, rather than (X ^ n - 1).gal.

[Eric Rodriguez]

What is the point of polynomial.gal then?

[Thomas Browning]

Mostly, it's for when you're just interested in Galois groups of polynomials, rather than Galois groups of field extensions more generally. We used it for proving abel-ruffini.

[Riccardo Brasca]

Well, if we are not able to prove is_splitting_field then it means something is missing the cyclotomic polynomial API, or somewhere else. And the whole API for splitting fields should use is_splitting_field.

[Riccardo Brasca]

I am almost tempted to have is_cyclotomic_field

[Johan Commelin]

That would just be is_splitting_field (X ^ n - 1) right? I think that should suffice (at least for now).

[Riccardo Brasca]

Yes, sure

[Riccardo Brasca]

Let me try

[Riccardo Brasca]

OK, is_cyclotomic_field seems to work. But now we have the problem for cyclotomic_ring...

[Chris Birkbeck]

the definition of zeta' in cyclotomic_units seems to now be broken.

[Johan Commelin]

Do we already have some sort of is_ring_of_integers?

[Johan Commelin]

@Anne Baanen I forgot the status...

[Riccardo Brasca]

Chris Birkbeck said:

the definition of zeta' in cyclotomic_units seems to now be broken.

I am fixing it

[Alex J. Best]

Johan Commelin said:

Do we already have some sort of is_ring_of_integers?

I guess something like [is_fraction_ring S L] [is_dedekind_domain S] takes that role?

[Thomas Browning]

Could we just use ring_of_integers, and prove that ring_of_integers equals algebra.adjoin?

[Riccardo Brasca]

Well, the point is that if we use is_cyclotomic_fields (that is nothing else than is_splitting_field) we probably want a characteristic predicate also for the ring of integers.

[Riccardo Brasca]

It seems to me we have to decide how to write things before going on writing lemmas. If we change the basic definition then refactoring everything is going to be rather painful.

Let's start with the cyclotomic field. The most "clean" way I see is to define

class is_cyclotomic_field : Prop := (out : is_splitting_field ℚ K (X ^ n - 1))

for (K : Type*) [field K] [char_zero K]. Of course we can have the explicit model

def cyclotomic_field [fact (0 < n)] : Type* := adjoin_root (cyclotomic n ℚ)

instance : is_cyclotomic_field n (cyclotomic_field n) := sorry

[Riccardo Brasca]

Then everything is stated using (K : Type*) [field K] [char_zero K] [is_cyclotomic_field p K], for example

def zeta' : K :=
classical.some (exists_root_of_splits (algebra_map ℚ K) (is_splitting_field.splits _ _)
  (degree_cyclotomic_pos p ℚ hn.out).ne.symm)

[Riccardo Brasca]

The point of taking this approach is that the definition of cyclotomic_field doesn't matter, it is the fact that it has the is_cyclotomic_field instance that makes everything working.

[Alex J. Best]

Yeah as long as we stick to a reasonable API it doesn't make too much difference which definition we end up using i hope

[Alex J. Best]

And I think it's hard to make decisions about what actual definitions to use without trying them and seeing what goes right and wrong

[Riccardo Brasca]

Ah, we have docs#is_integral_closure!

[Riccardo Brasca]

So I suggest we try to use characteristic predicates everywhere. If at some point it becomes to complicated we can always start using the explicit models, but going the other way is going to be painful

[Eric Rodriguez]

I know this isn't the focus of this project, but I really don't want to have multiple defns all over the place, so:
https://kconrad.math.uconn.edu/blurbs/galoistheory/cyclotomic.pdf suggests that cyclotomic fields works over char p in some cases. I think if we're defining this this way, it may be easier to say that is_cyclotomic_field n means that the nth roots of unity are full, which gives us zeta automatically (#9778 or #9779, can't remember).

[Eric Rodriguez]

The current way, the definition does not work for char p cyclotomic extensions

[Eric Rodriguez]

Oh, I just realised what the second condition actually meant in is_splitting_field (which is totally sensible of course).

[Eric Rodriguez]

Still, the current defn of the predicate isn't good either

[Riccardo Brasca]

I don't understand which definition you propose. You say "is_cyclotomic_field n means that the nth roots of unity are full", but this is satisfied by, for example, the complex numbers. We need in a way or in another specify that it is the splitting field, and not bigger.

[Riccardo Brasca]

And this seems annoying to treat uniformly in char 0 and char p

[Adam Topaz]

Generally a field extension $L|K$ is called "cyclotomic" if it is "generated" by roots of unity.

[Riccardo Brasca]

Yeah, sure, but we want something like the n-th cyclotomic field...

[Adam Topaz]

What's the problem with char p?

[Adam Topaz]

The p-cyclotomic extension of a field $K$ of characteristic $p$ is $K$ itself.

[Riccardo Brasca]

I mean, if I want to use is_splitting_field

[Riccardo Brasca]

I need a base field

[Eric Rodriguez]

What about is_cyclotomic_extension F K n?

[Riccardo Brasca]

Defined using is_splitting_field?

[Thomas Browning]

meaning?

class is_cyclotomic_extension :=
(out : is_splitting_field F K (X ^ n - 1))

[Riccardo Brasca]

We will probably need some abbreviation to avoid writing Q everywhere, but why not

[Adam Topaz]

Thomas Browning said:

meaning?

class is_cyclotomic_extension :=
(out : is_splitting_field F K (X ^ n - 1))

You can even just do

abbreviation  is_cyclotomic_extension := ...

[Riccardo Brasca]

I am done for today, but the basic definitions (for fields) are in src/number_theory/cyclotomic/field/basic.lean. If someone wants to generalize these to is_cyclotomic_extension F n please go ahead. Just be sure to provide the relevant instances, even only in char 0 (sorry as proof is perfectly fine of course).

[Riccardo Brasca]

src/number_theory/cyclotomic/ring/ is for the ring of integers, it contains the statement

lemma eq_adjoin : cyclotomic_ring n =
  algebra.adjoin ℤ {adjoin_root.root (cyclotomic n ℚ)} := sorry

that should be generalized to any R [is_cyclotomic_ring R K].

[Thomas Browning]

Could I have permission to push? (username tb65536)

[Eric Rodriguez]

I'd also like it (although I won't for a bit) [user: ericrbg]

[Scott Morrison]

@Thomas Browning, @Eric Rodriguez, I've sent an invitation with write access.

[Adam Topaz]

Just thinking out loud about defining cyclotomic extensions which will include the infinite case as well. Here's one proposal

import field_theory.splitting_field
import data.pnat.basic

structure truncation_set :=
(S : set pnat)
(div (a b) : a ∈ S → b ∣ a → b ∈ S)

instance truncation_set.has_mem : has_mem pnat truncation_set := ⟨λ a S, a ∈ S.S⟩

class is_cyclotomic_extension (K L : Type*) [field K] [field L] [algebra K L] (S : truncation_set) :=
(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

Note that truncation sets also show up in the theory of big Witt vectors, so it wouldn't hurt to have that definition anyway :)

[Thomas Browning]

If you're dealing with cyclotomic extensions, it seems like you should be looking at subsets of the integers closed under multiplication and taking divisors? (i.e., pick an enatfor each prime).

[Adam Topaz]

Why closed under multiplication?

[Adam Topaz]

With the truncation set approach, I can consider the set {1,5} to consider $K(\mu_5)$, I can consider all powers of 5 to consider $K(\mu_{5^\infty})$, etc

[Alex J. Best]

@Thomas Browning I don't think making is_cyclotomic_field an abbreviation is looking like a good idea, it causes a typeclass loop according to #lint.

[Thomas Browning]

Adam Topaz said:

Why closed under multiplication?

Sorry, I meant closed under lcm.

[Thomas Browning]

Alex J. Best said:

Thomas Browning I don't think making is_cyclotomic_field an abbreviation is looking like a good idea, it causes a typeclass loop according to #lint.

Ah, thanks for pointing this out. I'll push a fix (unless someone gets to it before me)

[Adam Topaz]

Sure, adding a condition saying closed under lcm should be fine. I think if you take the lcm closure T of a truncation set S, then the projection W_T to W_S on big Witt vectors is an isomorphism.

[Thomas Browning]

I feel like this is some sort of "completion" of the divisibility poset (you can "go off to infinity" at any subset of primes). Is there a way to generalize this precisely?

[Riccardo Brasca]

I like Adam's idea. Indeed infinite cyclotomic extensions are more common than char p cyclotomic extensions (at least in what I do). The definition makes sense even for an arbitrary S : set pnat, right? We can have something like is_truncation_set, to use this assumption.

[Riccardo Brasca]

In this way the definition is really super general, and we can always add other conditions later on.

[Chris Birkbeck]

I agree infinite cyclotomic extensions would be great.

[Riccardo Brasca]

And it seems to me S : set nat is fine... if S = {0} we get L = K

[Riccardo Brasca]

This is of course mathematically irrelevant, but usually working with nat is easier than working with pnat.

[Riccardo Brasca]

It seems the most general definition is

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

It makes sense in any characteristic and it allows base ring (instead of a base field) and infinite extensions. Maybe it's more elegant to use root_of_unity in the second condition, but this is only a personal taste.

[Riccardo Brasca]

I don't see any real problem with nat instead of pnat (and I prefer working with nat, the API is better). Does someone see a reason to prefer pnat?

[Adam Topaz]

The definition you wrote won't work with Nat if S contains 0

[Adam Topaz]

The second condition would reduce to saying that L is generated by L

[Johan Commelin]

Hmm, that's a good point (-;

[Adam Topaz]

And the first condition would reduce to saying that Phi_0 which is the constant 1 has a root, which cannot hold in a nontrivial ring

[Riccardo Brasca]

Ah ops, I checked the first one with X^n -1

[Riccardo Brasca]

Well, maybe it is still OK, there no S-extensions if S contains 0, do we care?

[Adam Topaz]

I would prefer pnat tbh. Yes the API is less developed, but in my mind pnat is fundamentally multiplicative whereas Nat is additive. The cyclotomic theory is essentially multiplicative in nature, so it makes sense to me to use pnat

[Riccardo Brasca]

OK, let's try pnat.

[Adam Topaz]

With Nat and 0 in S, the trivial algebra would be cyclotomic :rofl:

[Riccardo Brasca]

Don't tell our colleagues that we really spend time thinking about the $0$-th cyclotomic extension of the trivial ring.

[Riccardo Brasca]

import ring_theory.polynomial.cyclotomic

variables (K L : Type*) [comm_ring K] [comm_ring L] [is_domain L] [algebra K L]

class is_cyclotomic_extension (S : set ℕ+) :=
(ex_root (a : ℕ+) (ha : a ∈ S) : ∃ r : L, polynomial.aeval r (polynomial.cyclotomic a K) = 0)
(adjoint_roots : algebra.adjoin K (set.Union (λ (i : S), ((primitive_roots i L) : set L))) = ⊤)

If there is anyone among you that believes this definition should not take place, speak now or forever hold your peace.

[Chris Birkbeck]

I'm happy with that.

[Johan Commelin]

@Riccardo Brasca I think you can use nicer notation for that union, hopefully.

[Johan Commelin]

Doesn't something like ⋃ i ∈ S, primitive_roots i L work?

[Johan Commelin]

Anyway, probably one of the first things after this definition will be some lemmas that give equivalent statements (e.g. using roots_of_unity instead of primitive_roots). All those versions will probably be useful in the end.

[Adam Topaz]

What's the benefit of using primitive roots as opposed to all nth roots of unity?

[Adam Topaz]

I feel like checking for all roots would be easier, so it might make sense to have that as the constructor

[Riccardo Brasca]

⋃ i ∈ S, (primitive_roots ↑i L) : set L this works. I used primitive roots because roots_of_unity is a subgroup of units of L, so there are even more coercions

[Riccardo Brasca]

but it's doable of course. I think that it's better to use one of them rather than saying manually "roots of X^n-1"

[Johan Commelin]

Maybe the constructor should just use {b : L | ∃ i ∈ S, ... }.

[Johan Commelin]

And then a lemma can say: ooh, in fact you can use a primitive root of unity

[Riccardo Brasca]

Exactly the opposite of what I was thinking, but I trust you guys more than myself :grinning_face_with_smiling_eyes:

[Riccardo Brasca]

So this one?

import ring_theory.polynomial.cyclotomic

variables (K L : Type*) [comm_ring K] [ring L] [algebra K L]

class is_cyclotomic_extension (S : set ℕ+) :=
(ex_root (a : ℕ+) (ha : a ∈ S) : ∃ r : L, polynomial.aeval r (polynomial.cyclotomic a K) = 0)
(adjoint_roots : algebra.adjoin K {b : L | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1} = ⊤)

[Adam Topaz]

That looks good to me!

[Adam Topaz]

I guess this would imply L is commutative. Do we want to infer a comm_ring instance from this or just assume commutativity from the start?

[Johan Commelin]

Should it be phrased as ⊤ ≤ _? Because that's easier to verify?

[Johan Commelin]

Or even just: ∀ x : L, x ∈ algebra.adjoin ...

[Johan Commelin]

Then proofs don't need to start with rw eq_top_iff

[Riccardo Brasca]

Adam Topaz said:

I guess this would imply L is commutative. Do we want to infer a comm_ring instance from this or just assume commutativity from the start?

Good question. We cannot add ... : comm_ring R := sorry, right? Because a priori there could be a diamond for the two ring structures... and I don't want to prove it now if it is more than 5 minutes.

[Johan Commelin]

I wouldn't worry about this for now.

[Johan Commelin]

Just assume commutativity.

[Adam Topaz]

I agree we should just assume commutativity! But I also don't think proving it as an instance would cause a diamond since the ring structure would come from the given ring structure of L.

[Adam Topaz]

It might be a diamond, but the two ring instances would be defeq

[Riccardo Brasca]

Sure, but if our proof is sorry then Lean cannot know the two structure are defeq. But let's just assume commutativity.

[Adam Topaz]

Oh, I see. but if you write

instance [is_cyclotomic_extension K L S] : comm_ring L :=
{ mul_comm' := sorry,
.. (infer_instance : ring L) }

then it should be okay, right?

[Adam Topaz]

Anyway, all rings are commutative so why do we even care ;)

[Riccardo Brasca]

I've never used abbreviation, is this what we want?

variables (S : set ℕ+) (K : Type*) [field K] [char_zero K]

abbreviation is_cyclotomic_extension_rat := is_cyclotomic_extension S ℚ K

[Johan Commelin]

_rat is longer than ℚ . So I think I wouldn't bother.

[Riccardo Brasca]

good point

[Thomas Browning]

Here's a worry: If we use an infinite S (e.g., all positive integers), then will algebra.adjoin give us the whole cyclotomic field, or only a subalgebra?

[Riccardo Brasca]

We get the extension generated by all roots of unity.

[Thomas Browning]

Is it obvious that $\mathbb{Q}[\zeta_1,\zeta_2,\ldots]=\mathbb{Q}(\zeta_1,\zeta_2,\ldots)$ (algebra adjoin vs field adjoin)?

[Riccardo Brasca]

Yes, any element is in a finitely generated subalgebra, so you don't have to worry about infinitely many generators.

[Riccardo Brasca]

So we now have a very general definition is_cyclotomic_extension. I don't see how to write down an explicit model in the same degree of generality. For example we can take the splitting field of the cyclotomic polynomials, but this works only over fields and for S a singleton.

[Johan Commelin]

But that doesn't matter right?

[Johan Commelin]

You just setup the API as general as possible. And at the end of your project you specialize to $ℚ(ζ_p)$.

[Thomas Browning]

Riccardo Brasca said:

So we now have a very general definition is_cyclotomic_extension. I don't see how to write down an explicit model in the same degree of generality. For example we can take the splitting field of the cyclotomic polynomials, but this works only over fields and for S a singleton.

You could work in an algebraic closure and take a sup of subalgebras or intermediate fields.

[Riccardo Brasca]

Mmh.. yes, it should be enoug. Once we have $\mathbb{Q}(\zeta_n)$ we can say that algebra.adjoin ℤ ζ is a cyclotomic extension

[Riccardo Brasca]

Where ζ is inside $\mathbb{Q}(\zeta_n)$

[Thomas Browning]

If we really want to be fancy, we could build the infinite cyclotomic extension and take fixed fields by closed subgroups of the Galois group $\widehat{\mathbb{Z}}^\times$. This would also give us the $\mathbb{Z}_p$ from Iwasawa theory.

[Thomas Browning]

(although Lean doesn't know this version of the Galois correspondence yet)

[Adam Topaz]

Thomas Browning said:

If we really want to be fancy, we could build the infinite cyclotomic extension and take fixed fields by closed subgroups of the Galois group $\widehat{\mathbb{Z}}^\times$. This would also give us the $\mathbb{Z}_p$ from Iwasawa theory.

This is where one would have to worry about characteristic...

[Johan Commelin]

@Riccardo Brasca Right, so you will need an instance for $ℚ(ζ_n)$. But that should suffice. (Ok, and maybe for the integral version.)

[Thomas Browning]

Could you do both simultaneously with adjoin_root?

[Adam Topaz]

One question is this: Given a positive integer $n$, should we prove a cyclotomic instance for $S = \{n\}$ or for $S$ the divisors of $n$?

[Thomas Browning]

Adam Topaz said:

One question is this: Given a positive integer $n$, should we prove a cyclotomic instance for $S = \{n\}$ or for $S$ the divisors of $n$?

If we view S as saying "what roots of unity you want to adjoin", then I think {n} is more natural and less cumbersome?

[Riccardo Brasca]

My question is exactly what is (in Lean) the integral version. Over a field we can use splitting_field and we are good. The problem with adjoin_root is that it add the root even if it is already there.

[Thomas Browning]

Would taking an arbitrary irreducible factor of the cyclotomic polynomial work?

[Riccardo Brasca]

It is by def the quotient of the polynomial ring by the polynomial. So if we don't have irreducibility this is very badly behaved

[Riccardo Brasca]

No, we want all the roots

[Thomas Browning]

Could you define some weird induction thing that takes a polynomial, pulls off an irreducible factor and applies adjoin_root, and repeats?

[Thomas Browning]

This might even generalize the splitting field construction

[Johan Commelin]

For the integral version, can't you use integral closure, or algebra.adjoin?

[Riccardo Brasca]

Well, you are proposing to generalize splitting_field to rings. This is surely possible in some sense, but I am afraid it's going to be a lot of work.

Maybe the best thing is, for domains, to just consider algebra.adjoin R T, where T is the set of roots of unity in the field of fraction

[Riccardo Brasca]

Yes exactly, having the field we can work there

[Riccardo Brasca]

people are against using integral_closure since in general the thing is not integrally closed (it is for Z).

[Riccardo Brasca]

I think I wrote down the relevant definitions. They are in number_theory/cyclotomic/basic. I am going to stop for today, but the idea is to get rid of number_theory/cyclotomic/field/basic and number_theory/cyclotomic/ring/basic, so if someone wants to modify the other files please go ahead. It should be easy.

[Riccardo Brasca]

In number_theory/cyclotomic/basic there a lot of sorry, most of them are instances.

[Riccardo Brasca]

I think that using abbreviation/notation or whatever instead of def some of them will become automatic, but in any case the majority should be easy.

[Chris Birkbeck]

Awesome!

[Chris Birkbeck]

So I was just trying to get the class_group stuff working with the new cyclotomic definition, but it gives me an error I'd not seen before maximum class-instance resolution depth has been reached . What does this mean?

[Riccardo Brasca]

It means there is a cycle of instances

[Riccardo Brasca]

Where is it?

[Chris Birkbeck]

aha, I tried the set_option trace.class_instances true but I cant really interpret the output to see the problem. (Sorry I'm still quite new at this!)

[Chris Birkbeck]

I pushed the changes if you want to see the error for yourself

[Riccardo Brasca]

I've never understood the output if set_option trace.class_instances true: the problem is surely written, but it is too long to read.

[Riccardo Brasca]

I suggest we try to have master compiling without errors all the time. But we can of course use other branches to play with errors

[Riccardo Brasca]

But no problem for your commit :)

[Chris Birkbeck]

Ah sure that's probably a good idea! :)

[Chris Birkbeck]

Looking at the output it seems something happen here [class_instances] cached instance for field ℚ rat.field

[Riccardo Brasca]

I've probably missed something about the new open command, but I don't understand how Lean find cyclotomic_ring that is now called something like new_cyclotomic_field.cyclotomic_ring

[Chris Birkbeck]

Oh I added the open new_cyclotomic_field I thought it would just mean I dont have to type new_cyclotomic_field.cyclotomic_ring everytime.

[Riccardo Brasca]

There is no open here or am I blind?

[Riccardo Brasca]

But let me check the real error

[Chris Birkbeck]

Oh wait, maybe I pushed the wrong thing.

[Chris Birkbeck]

Yes I forgot to hit save before pushing, sorry!

[Riccardo Brasca]

I get an invalid namespace name 'new_cyclotomic_field' error.

[Chris Birkbeck]

Yeah, did you delete that namespace?

[Riccardo Brasca]

I didn't touch the namespace, there is something I don't understand. Let me see what really does the new open.

[Chris Birkbeck]

No I can see in your commit that you removed the that namespace from cyclotomic/basic

[Chris Birkbeck]

But either way, thats not the problem. the class instance thing is still there.

[Riccardo Brasca]

Ah ops, I messed up. Let's fix this, since there are two cyclotomic_ring and I want to be sure Lean is working with the good one.

[Riccardo Brasca]

So,

instance a : is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ) := sorry

noncomputable instance class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite
    ℤ (cyclotomic_ring n ℤ ℚ) ℚ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _,

end

complains with

failed to synthesize type class instance for
n : ℕ+
⊢ is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)

This usually means there is a diamond somewhere.

[Riccardo Brasca]

Can you check that all the instances I wrote in number_theory/cyclotomic/basic are good? For example that I didn't write algebra field ring instead of algebra ring field. I am checking them too, but two pairs of eyes are better.

[Riccardo Brasca]

Mmh,

instance cyclotomic_ring_int_is_integral_closure :
  is_integral_closure (cyclotomic_ring n A K) A (cyclotomic_field n K) := sorry

noncomputable instance class_group.fintype_of_cyclotomic_ring (n : ℕ+) [euclidean_domain A] :
  fintype (class_group (cyclotomic_ring n A K) (cyclotomic_field n K)) :=
begin
  letI : algebra A K := infer_instance,
  refine @class_group.fintype_of_admissible_of_finite
    A (cyclotomic_ring n A K) K (cyclotomic_field n K)
    _ _ _ _ _ _ _ _ _ _ _
    _ _ _ _ _ _ _ _ _ _,

end

says

failed to synthesize type class instance for
A : Type u_1,
K : Type u_2,
_inst_1 : comm_ring A,
_inst_2 : field K,
_inst_3 : is_domain A,
_inst_4 : algebra A K,
_inst_5 : is_fraction_ring A K,
n : ℕ+,
_inst_6 : euclidean_domain A,
_inst : algebra A K := infer_instance
⊢ algebra A K

I don't understand.

[Riccardo Brasca]

Lean wants

@algebra.{u_1 u_2} A K (@comm_ring.to_comm_semiring.{u_1} A (@euclidean_domain.to_comm_ring.{u_1} A _inst_6))
    (@ring.to_semiring.{u_2} K (@division_ring.to_ring.{u_2} K (@field.to_division_ring.{u_2} K _inst_2)))

and we have

@algebra.{u_1 u_2} A K (@comm_ring.to_comm_semiring.{u_1} A _inst_1)
    (@ring.to_semiring.{u_2} K (@division_ring.to_ring.{u_2} K (@field.to_division_ring.{u_2} K

[Riccardo Brasca]

I have to stop for a couple of hours, but something is confusing me. It seems there a diamond here, but it's strange nobody found it before.

[Riccardo Brasca]

Oh, OK, I see

[Riccardo Brasca]

euclidean_domain does not need ring

[Riccardo Brasca]

Bu the other problem is still there

[Alex J. Best]

There is the algebra Q diamond and the rat field diamond, both of which will likely continue to cause us issues

[Chris Birkbeck]

Sorry I was away talking to a student.
Riccardo Brasca said:

Can you check that all the instances I wrote in number_theory/cyclotomic/basic are good? For example that I didn't write algebra field ring instead of algebra ring field. I am checking them too, but two pairs of eyes are better.

Sorry I was afk talking to a student. I'll have a look now.

[Chris Birkbeck]

I have a noob question. What is a diamond? Is it when something can inherit the same properties from two different sources?

[Kevin Buzzard]

Right -- it's when you suddenly find that you have two instances of e.g. [algebra ℤ R] which are perhaps propositionally equal but not definitionally equal, because Lean mananged to find two ring homomorphisms from the integers to R in its type class system.

[Kevin Buzzard]

This is an issue because type class inference relies on definitional equality to work, basically, so diamonds can cause obscure/hard-to-diagnose errors.

[Kevin Buzzard]

The famous example, the one which really made me understand diamonds, is that metric spaces and topological spaces are classes in Lean, and there's an instance which takes a metric space to a topological space, and an instance which takes two metric spaces and returns a metric space structure on the product, with the L^2 norm say ($d((x_1,y_1),(x_2,y_2)):=\sqrt{(d(x_1,y_1)^2+d(x_2,y_2)^2}$) and there's an instance which takes two topological spaces and returns a topological space structure on the product.

[Kevin Buzzard]

This gives a diamond! Because if you start with two metric spaces, then the product topology coming from the topologies has a basis which are "rectangles" (i.e. of the form $U\times V$) whereas the topology coming from the metric has a basis which are "discs" (i.e. distance from a fixed point is $<r$).

[Kevin Buzzard]

It's a theorem that these two topologies are the same, but the proof is certainly not rfl!

[Chris Birkbeck]

Aha that makes perfect sense, thank you!

[Kevin Buzzard]

Even if you make the metric on the product equal to the sup norm you still don't get rfl for your proof that the two topologies coincide, because one is "basis generated by products of all open sets" and the other is "basis generated by products of all open balls"

[Kevin Buzzard]

The astonishing fix for this diamond, I think due to Johannes Hoelzl, is to make the topology part of the definition of a metric space!

[Kevin Buzzard]

So a metric space in Lean is [what you think a metric space is] + [a topology] + [a proof that the topology is equal to the one induced by the metric]

[Kevin Buzzard]

and then in the instance which defines a metric on the product of two metric spaces, you define the topology to be the product topology, and then you insert the proof that the metric product induces the product topology in the definition of the instance. This trivially fixes the diamond.

[Kevin Buzzard]

If you've ever looked at the definition of a group in mathlib recently, you'll see that it contains a map $\mathbb{Z}\times G\to G$ and a proof that this map sends $(n,g)$ to $g^n$, and this random extra field is there for the same sort of reason.

[Chris Birkbeck]

Ok great, I'll add diamonds to my list of things to worry about :)

[Johan Commelin]

Chris Birkbeck said:

I have a noob question. What is a diamond? Is it when something can inherit the same properties from two different sources?

Since yesterday we have a new way to answer this question! Meet our glossary :octopus:
https://leanprover-community.github.io/glossary.html#diamond

[Chris Birkbeck]

Johan Commelin said:

Chris Birkbeck said:

I have a noob question. What is a diamond? Is it when something can inherit the same properties from two different sources?

Since yesterday we have a new way to answer this question! Meet our glossary :octopus:
https://leanprover-community.github.io/glossary.html#diamond

Oh this is great! thank you

[Johan Commelin]

Credits to Julian Berman for writing it!

[Kevin Buzzard]

I think that a mathematician would understand my explanation better than Julian's, because they would know a lot more about topological spaces than about terms and types. I should PR an extension of the explanation with the example maybe (when I'm out of teaching hell next week)

[Johan Commelin]

Yeah, maybe the extended explanation can be written up somewhere (a gist?) and then we link to that?

[Johan Commelin]

I guess the glossary should try to be concise, and link to other places for details.

[Kevin Buzzard]

Gotcha

[Johan Commelin]

In fact, the "See Also" part already links to the forgetful inheritance discussion from the mathlib paper.

[Johan Commelin]

Which contains your metric space example.

[Riccardo Brasca]

@Chris Birkbeck I am back at the computer. The diamond I was talking was completely my fault, I had [ring A] [euclidean_domain A], so there were two structures of ring on A, and that confused Lean. Now I have euclidean_domain A but I still get the maximum class-instance resolution. Let's see what's wrong

[Chris Birkbeck]

Kevin Buzzard said:

I think that a mathematician would understand my explanation better than Julian's, because they would know a lot more about topological spaces than about terms and types. I should PR an extension of the explanation with the example maybe (when I'm out of teaching hell next week)

I agree with this. I understand the topology example much more than the typeclass description.

[Chris Birkbeck]

I'm not sure if this helps, but we get the same error if we try and do instance : number_field ℚ := infer_instance

[Chris Birkbeck]

It seems cyclotomic.basic.number_field is what causes it to break

[Riccardo Brasca]

Yes, there is something strange. But

import number_theory.cyclotomic.basic
import number_theory.class_number.finite
import number_theory.class_number.admissible_abs

open algebra polynomial

variable (n : ℕ+)

instance : is_fraction_ring
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field := sorry

noncomputable example :
  fintype (class_group
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field) :=
begin
  have sepKL : is_separable ℚ (cyclotomic n ℚ).splitting_field := sorry,
  haveI iicSRL : is_integral_closure
    (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1}) ℤ
    (cyclotomic n ℚ).splitting_field := sorry,
  refine @class_group.fintype_of_admissible_of_finite ℤ
    (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
    ℚ (cyclotomic n ℚ).splitting_field _ _ _
    _ _ _ _ _ _ _ _ _ _ _ _ _ _ absolute_value.abs_is_admissible _ _ _,

end

works.

[Riccardo Brasca]

I've unfolded the def by hand.

[Riccardo Brasca]

Ah, in

@[derive [comm_ring]]
def cyclotomic_ring : Type* := adjoin A { b : K | b ^ (n : ℕ) = 1 }

K should be cyclotomic_field {n} K!

[Riccardo Brasca]

I am pushing this, that in any case fix a mistake

[Riccardo Brasca]

So,

import ring_theory.polynomial.cyclotomic
import number_theory.class_number.finite
import number_theory.class_number.admissible_abs

open algebra polynomial

variable (n : ℕ+)

instance : is_fraction_ring
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field := sorry

noncomputable example :
  fintype (class_group
  (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1})
  (cyclotomic n ℚ).splitting_field) :=
begin
  haveI iicSRL : is_integral_closure
    (adjoin ℤ {b : (cyclotomic n ℚ).splitting_field | b ^ (n : ℕ) = 1}) ℤ
    (cyclotomic n ℚ).splitting_field := sorry,
  exact class_group.fintype_of_admissible_of_finite ℚ (cyclotomic n ℚ).splitting_field
    absolute_value.abs_is_admissible,
end

works perfectly. But if I add import number_theory.cyclotomic.basic I get the error. So now it's just a matter of bisecting the file to see what causes the problem.

[Riccardo Brasca]

I found the culprit! It's

instance number_field [is_cyclotomic_extension S K L] [number_field K] : number_field L := sorry

And once you know it, the reason is clear: if K is a number field then L is, but I think we know that subfields of number fields are number fields, so Lean goes back to K and then again to L and so on.

[Chris Birkbeck]

Aha this is what it seemed like when I did this instance : number_field ℚ := infer_instance experiment. But I don't know how to fix it.

[Riccardo Brasca]

It has to be a lemma, not an instance.

[Riccardo Brasca]

But we have another problem, and this time it really seems a diamond.

[Chris Birkbeck]

Riccardo Brasca said:

It has to be a lemma, not an instance.

Ahh ok.

[Chris Birkbeck]

Riccardo Brasca said:

But we have another problem, and this time it really seems a diamond.

Oh no

[Riccardo Brasca]

This

noncomputable instance class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  have h : is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ) := infer_instance,
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  _
  _ _ _ _ _ _ _ _ _,

end

fails with

failed to synthesize type class instance for
n : ℕ+,
h : is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)
⊢ is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)

And if you try to put h insted of the isolated underscore, there is a giant type mismatch at application error.

[Yakov Pechersky]

(deleted)

[Riccardo Brasca]

I wanted to see the two types, that's why I used have.

[Riccardo Brasca]

So h has type

  @is_scalar_tower ℤ ℚ (@cyclotomic_field n ℚ rat.field)
    (@sub_neg_monoid.has_scalar_int ℚ (@add_group.to_sub_neg_monoid ℚ rat.add_group))
    (@smul_with_zero.to_has_scalar ℚ (@cyclotomic_field n ℚ rat.field)
       (@mul_zero_class.to_has_zero ℚ
          (@mul_zero_one_class.to_mul_zero_class ℚ
             (@monoid_with_zero.to_mul_zero_one_class ℚ
                (@semiring.to_monoid_with_zero ℚ
                   (@comm_semiring.to_semiring ℚ
                      (@comm_ring.to_comm_semiring ℚ
                         (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field))))))))
       (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
          (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
             (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                   (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                      (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                         (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                            (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                               (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                  (@cyclotomic_field.field n ℚ rat.field))))))))))
       (@mul_action_with_zero.to_smul_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
          (@semiring.to_monoid_with_zero ℚ
             (@comm_semiring.to_semiring ℚ
                (@comm_ring.to_comm_semiring ℚ
                   (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field)))))
          (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
             (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
                (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                   (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                      (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                         (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                            (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                               (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                                  (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                     (@cyclotomic_field.field n ℚ rat.field))))))))))
          (@module.to_mul_action_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
             (@comm_semiring.to_semiring ℚ
                (@comm_ring.to_comm_semiring ℚ
                   (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field))))
             (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                   (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                      (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                         (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                            (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                               (@cyclotomic_field.field n ℚ rat.field)))))))
             (@algebra.to_module ℚ (@cyclotomic_field n ℚ rat.field)
                (@comm_ring.to_comm_semiring ℚ
                   (@euclidean_domain.to_comm_ring ℚ (@field.to_euclidean_domain ℚ rat.field)))
                (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                   (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                      (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                         (@cyclotomic_field.field n ℚ rat.field))))
                (@cyclotomic_field.algebra n ℚ rat.field)))))
    (@sub_neg_monoid.has_scalar_int (@cyclotomic_field n ℚ rat.field)
       (@add_group.to_sub_neg_monoid (@cyclotomic_field n ℚ rat.field)
          (@add_comm_group.to_add_group (@cyclotomic_field n ℚ rat.field)
             (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                   (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                      (@cyclotomic_field.field n ℚ rat.field)))))))

[Riccardo Brasca]

And the type Lean wants is so long I cannot post here :upside_down:

[Riccardo Brasca]

But it must come from the def of cyclotomic_field n ℚ, so it's fixable I hope.

[Riccardo Brasca]

I've managed to reduce the size of the error, now the two types are almost readable. It's the error in this file.

[Riccardo Brasca]

@add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _ has type

  @is_scalar_tower ℤ ℚ (@cyclotomic_field n ℚ rat.field)
    (@sub_neg_monoid.has_scalar_int ℚ
       (@add_group.to_sub_neg_monoid ℚ
          (@add_comm_group.to_add_group ℚ
             (@ring.to_add_comm_group ℚ
                (@normed_ring.to_ring ℚ
                   (@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field)))))))
    (@smul_with_zero.to_has_scalar ℚ (@cyclotomic_field n ℚ rat.field)
       (@mul_zero_class.to_has_zero ℚ
          (@mul_zero_one_class.to_mul_zero_class ℚ
             (@monoid_with_zero.to_mul_zero_one_class ℚ
                (@semiring.to_monoid_with_zero ℚ
                   (@ring.to_semiring ℚ
                      (@normed_ring.to_ring ℚ
                         (@normed_comm_ring.to_normed_ring ℚ
                            (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))))))
       (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
          (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
             (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                (@add_comm_group.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                   (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                      (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                         (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                            (@cyclotomic_field.field n ℚ rat.field))))))))
       (@mul_action_with_zero.to_smul_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
          (@semiring.to_monoid_with_zero ℚ
             (@ring.to_semiring ℚ
                (@normed_ring.to_ring ℚ
                   (@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field)))))
          (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
             (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
                (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                   (@add_comm_group.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                      (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                         (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                            (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                               (@cyclotomic_field.field n ℚ rat.field))))))))
          (@module.to_mul_action_with_zero ℚ (@cyclotomic_field n ℚ rat.field)
             (@ring.to_semiring ℚ
                (@normed_ring.to_ring ℚ
                   (@normed_comm_ring.to_normed_ring ℚ (@normed_field.to_normed_comm_ring ℚ rat.normed_field))))
             (@add_comm_group.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                   (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                      (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                         (@cyclotomic_field.field n ℚ rat.field)))))
             (@algebra.to_module ℚ (@cyclotomic_field n ℚ rat.field) rat.comm_semiring
                (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                   (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                      (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                         (@cyclotomic_field.field n ℚ rat.field))))
                (@cyclotomic_field.algebra n ℚ rat.field)))))
    (@sub_neg_monoid.has_scalar_int (@cyclotomic_field n ℚ rat.field)
       (@add_group.to_sub_neg_monoid (@cyclotomic_field n ℚ rat.field)
          (@add_comm_group.to_add_group (@cyclotomic_field n ℚ rat.field)
             (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
                (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                   (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                      (@cyclotomic_field.field n ℚ rat.field)))))))

[Riccardo Brasca]

The actual type is still too big to fit in Zulip...

[Marc Masdeu]

Kevin Buzzard said:

I think that a mathematician would understand my explanation better than Julian's, because they would know a lot more about topological spaces than about terms and types. I should PR an extension of the explanation with the example maybe (when I'm out of teaching hell next week)

Isn't this explanation what's in https://leanprover-community.github.io/mathlib_docs/notes.html#forgetful%20inheritance ?

[Kevin Buzzard]

yeah I didn't click through :-)

[Kevin Buzzard]

The diamond error is that Lean is failing to solve

smul_with_zero.to_has_scalar = sub_neg_monoid.has_scalar_int

[Riccardo Brasca]

Ah, thank's!! How did you find it?

[Kevin Buzzard]

noncomputable lemma class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  (by convert @add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _)
  _ _ _ _ _ _ _ _ _,

end

[Kevin Buzzard]

I'm still thinking about it

[Kevin Buzzard]

I am quite confused because

example : (smul_with_zero.to_has_scalar : has_scalar ℤ (cyclotomic_field n ℚ)) = sub_neg_monoid.has_scalar_int :=
begin
  refl,
end

works

[Riccardo Brasca]

Ah, in any case super nice trick using convert to reduce the size of the output.

[Kevin Buzzard]

We've definitely still not got to the bottom of this

[Kevin Buzzard]

noncomputable lemma class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  (by {convert @add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _, sorry})
  _ _ _ _ _ _ _ _ _,
end

That tactic actually compiles without errors, leaving two goals.

[Riccardo Brasca]

The two goals are OK

[Kevin Buzzard]

One is absolute value ℤ ℤ -- so Lean is not inferring it

[Kevin Buzzard]

But the goal before the sorry is not being closed with refl

[Riccardo Brasca]

import number_theory.cyclotomic.basic
import number_theory.class_number.finite
import number_theory.class_number.admissible_abs

variable (n : ℕ+)

section finiteness

open new_cyclotomic_field

--set_option pp.all true

local attribute [-instance] smul_with_zero.to_has_scalar

noncomputable lemma class_group.fintype_of_cyclotomic_ring (n : ℕ+) :
  fintype (class_group (cyclotomic_ring n ℤ ℚ) (cyclotomic_field n ℚ)) :=
begin
  refine @class_group.fintype_of_admissible_of_finite ℤ _ ℚ (cyclotomic_field n ℚ)
  _ _ _ _ _ _ _ _ _ _ _
  (by {convert @add_comm_group.int_is_scalar_tower ℚ (cyclotomic_field n ℚ) _ _ _, sorry})
  _ _ _ _ _ absolute_value.abs_is_admissible _ _ _,
end

end finiteness

[Kevin Buzzard]

oh nice! Indeed I'd just discovered that the instance of smul_with_zero.to_has_scalar in the term was not the one that type class inference was discovering.

[Riccardo Brasca]

But the sorry is still there, I have to think about it.

[Johan Commelin]

Uuughh, this all looks really ugly. I'm cheering you on from the side. The joys of spelunking through the depths of mathlibs algebra hierarchy.

[Kevin Buzzard]

My understanding so far is that Riccardo has managed to get type class inference to create a term of type has_scalar ℤ (cyclotomic_field n ℚ) which is not defeq to (smul_with_zero.to_has_scalar : has_scalar ℤ (cyclotomic_field n ℚ))

[Riccardo Brasca]

I agree that it's probably my fault, but I thought that all Z-action were defeq, we did a huge refactor to have this, didn't we?

[Riccardo Brasca]

The definition of cyclotomic_field n K is

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

[Kevin Buzzard]

heh :-) certainly not all int actions are defeq, but somehow the idea is supposed to be that we only ever let Lean see the defeq ones :-)

[Johan Commelin]

That smul_wth_zero must be coming from an "ugly" place, I guess.

[Riccardo Brasca]

@smul_with_zero.to_has_scalar ℤ (@cyclotomic_field n ℚ rat.field)
      (@mul_zero_class.to_has_zero ℤ
         (@mul_zero_one_class.to_mul_zero_class ℤ
            (@monoid_with_zero.to_mul_zero_one_class ℤ
               (@semiring.to_monoid_with_zero ℤ
                  (@comm_semiring.to_semiring ℤ
                     (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain)))))))
      (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
         (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
            (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
               (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                  (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                     (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                        (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                           (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                              (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                 (@cyclotomic_field.field n ℚ rat.field))))))))))
      (@mul_action_with_zero.to_smul_with_zero ℤ (@cyclotomic_field n ℚ rat.field)
         (@semiring.to_monoid_with_zero ℤ
            (@comm_semiring.to_semiring ℤ
               (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain))))
         (@add_zero_class.to_has_zero (@cyclotomic_field n ℚ rat.field)
            (@add_monoid.to_add_zero_class (@cyclotomic_field n ℚ rat.field)
               (@add_comm_monoid.to_add_monoid (@cyclotomic_field n ℚ rat.field)
                  (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
                     (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                        (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                           (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                              (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                                 (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                                    (@cyclotomic_field.field n ℚ rat.field))))))))))
         (@module.to_mul_action_with_zero ℤ (@cyclotomic_field n ℚ rat.field)
            (@comm_semiring.to_semiring ℤ
               (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain)))
            (@non_unital_non_assoc_semiring.to_add_comm_monoid (@cyclotomic_field n ℚ rat.field)
               (@non_assoc_semiring.to_non_unital_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                  (@semiring.to_non_assoc_semiring (@cyclotomic_field n ℚ rat.field)
                     (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                        (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                           (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                              (@cyclotomic_field.field n ℚ rat.field)))))))
            (@algebra.to_module ℤ (@cyclotomic_field n ℚ rat.field)
               (@comm_ring.to_comm_semiring ℤ (@euclidean_domain.to_comm_ring ℤ int.euclidean_domain))
               (@ring.to_semiring (@cyclotomic_field n ℚ rat.field)
                  (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                     (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                        (@cyclotomic_field.field n ℚ rat.field))))
               (@new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ int.comm_ring rat.field _
                  (@algebra_int ℚ (@ordered_ring.to_ring ℚ rat.ordered_ring))
                  rat.is_fraction_ring)))) =
    @sub_neg_monoid.has_scalar_int (@cyclotomic_field n ℚ rat.field)
      (@add_group.to_sub_neg_monoid (@cyclotomic_field n ℚ rat.field)
         (@add_comm_group.to_add_group (@cyclotomic_field n ℚ rat.field)
            (@ring.to_add_comm_group (@cyclotomic_field n ℚ rat.field)
               (@division_ring.to_ring (@cyclotomic_field n ℚ rat.field)
                  (@field.to_division_ring (@cyclotomic_field n ℚ rat.field)
                     (@cyclotomic_field.field n ℚ rat.field))))))

Very good

[Kevin Buzzard]

The bad instance is coming from algebra.to_has_scalar

[Riccardo Brasca]

Yes, I just arrived to the conclusion that the problem is the Z-algebra structure on the cyclotomic field.

[Riccardo Brasca]

Let me check where it comes from.

[Chris Birkbeck]

Does it come from cyclotomic_field_algebra?

[Kevin Buzzard]

Yes, the bad instance has new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ in it

[Riccardo Brasca]

It's

instance cyclotomic_field_algebra : algebra A (cyclotomic_field n K) :=
((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra

[Chris Birkbeck]

Maybe for it doesn't like that its a composition when defined for Z?

[Riccardo Brasca]

Can it be universe related:

example : (new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ) =
  algebra ℤ (cyclotomic_field n ℚ) := sorry

is not happy with

type mismatch at application
  new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ = algebra ℤ (cyclotomic_field n ℚ)
term
  algebra ℤ (cyclotomic_field n ℚ)
has type
  Type : Type 1
but is expected to have type
  algebra ℤ (cyclotomic_field n ℚ) : Type

[Kevin Buzzard]

that's some type error, you have (term) = (type of the term)

[Kevin Buzzard]

But this works :-/

noncomputable def foo : algebra ℤ (cyclotomic_field n ℚ) := infer_instance
example : new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ = foo n := rfl

[Kevin Buzzard]

oh but that's just because type class inference finds precisely this term

[Kevin Buzzard]

so here's the problem:

-- this is `new_cyclotomic_field.cyclotomic_field_algebra n ℤ ℚ`
noncomputable def foo : algebra ℤ (cyclotomic_field n ℚ) := by show_term {apply_instance}
-- remove the instance
local attribute [-instance] new_cyclotomic_field.cyclotomic_field_algebra
-- still works, now `algebra_int`
noncomputable def bar : algebra ℤ (cyclotomic_field n ℚ) := by show_term {apply_instance}
-- but they're not defeq
example : foo n = bar n := rfl -- fails

[Kevin Buzzard]

The new instance new_cyclotomic_field.cyclotomic_field_algebra is giving a non-defeq $\Z$-algebra structure

[Chris Birkbeck]

Yeah it must be because its defined as a composition

[Riccardo Brasca]

Oh gosh, thank you

[Chris Birkbeck]

or not, I dont know

[Riccardo Brasca]

In any case this is a problem that we have to solve

[Riccardo Brasca]

Let me see if I have enough time

[Kevin Buzzard]

example (A K L : Type) [comm_ring A] [field K] [field L] [algebra A K] [algebra K L] : algebra A L :=
infer_instance -- fails

Is this expected to fail? (i.e. do I need more imports?) I thought it would be worth looking at how analogues of cyclotomic_field_algebra are defined in mathlib.

[Johan Commelin]

@Kevin Buzzard Yes, that's supposed to fail. You need to use scalar towers.

[Johan Commelin]

Lean cannot guess which K it should be looking for.

[Adam Topaz]

I thought that was the whole point of scalar towers?

[Kevin Buzzard]

So the issue is that if A is the integers and if algebra A K is the instance discovered by type class inference (algebra_int) then we wantalgebra A L to end up also being defeq to this instance.

[Kevin Buzzard]

Right now this fails (of course):

example (K L : Type) [field K] [field L] [algebra K L] :
  (int.cast_ring_hom L : ℤ →+* L) = (algebra_map K L).comp (int.cast_ring_hom K) := rfl -- fails

because the RHS has got some random _inst_3 in it. So

instance cyclotomic_field_algebra : algebra A (cyclotomic_field n K) :=
((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra

will always cause trouble if A = ℤ

[Johan Commelin]

I'm actually surprised that we haven't hit this issue earlier...

[Johan Commelin]

There are tons of instance : algebra A blabla in mathlib. But blabla will always already have an algebra ℤ blabla instance coming from algebra_int.

[Adam Topaz]

maybe algebra_int shouldn't be an instance?

[Kevin Buzzard]

algebra_int has priority 99, perhaps this helps (by which I mean perhaps this is why we didn't run into it before)

[Johan Commelin]

Yeah, maybe. Having algebra_int not be an instance is quite disappointing though.

[Adam Topaz]

The alternative is to have all algebra A B instances extend is_scalar_tower \Z A B or something like that?

[Kevin Buzzard]

That feels very much like how we have solved previous problems of this nature

[Johan Commelin]

Does that even help? You would get an is_scalar_tower ℤ ℤ B, which shows that the two scalar actions are propeq. But they still wouldn't be defeq.

[Adam Topaz]

sigh

[Riccardo Brasca]

I have to stop, but I agree with Johan that it is strange we never encountered this before.

[Johan Commelin]

Maybe this is why:

src/ring_theory/subsemiring.lean
842-/-- The action by a subsemiring is the action by the underlying semiring. -/
843-instance [add_comm_monoid α] [module R' α] (S : subsemiring R') : module S α :=
844:{ smul := (•), .. module.comp_hom _ S.subtype }

src/algebra/module/basic.lean
107-@[reducible] def module.comp_hom [semiring S] (f : S →+* R) :
108-  module S M :=
109:{ smul := has_scalar.comp.smul f,

src/group_theory/group_action/defs.lean
169-  an additive action of `N` on `α` "-/]
170-def comp (g : N → M) : has_scalar N α :=
171:{ smul := has_scalar.comp.smul g }
--
309-@[reducible, to_additive] def comp_hom [monoid N] (g : N →* M) :
310-  mul_action N α :=
311:{ smul := has_scalar.comp.smul g,
--
396-@[reducible] def distrib_mul_action.comp_hom [monoid N] (f : N →* M) :
397-  distrib_mul_action N A :=
398:{ smul := has_scalar.comp.smul f,
--
476-@[reducible] def mul_distrib_mul_action.comp_hom [monoid N] (f : N →* M) :
477-  mul_distrib_mul_action N A :=
478:{ smul := has_scalar.comp.smul f,

[Johan Commelin]

All these examples use .comp for the definition of smul. But they are all defs.

[Kevin Buzzard]

i.e. none of them are instances

[Johan Commelin]

There is also

288-instance lift2_alg {F : intermediate_field K L} {E : intermediate_field F L} : algebra K E :=
289-{ to_fun := (algebra_map F E).comp (algebra_map K F),
290-  map_zero' := ((algebra_map F E).comp (algebra_map K F)).map_zero,
291-  map_one' := ((algebra_map F E).comp (algebra_map K F)).map_one,
292-  map_add' := ((algebra_map F E).comp (algebra_map K F)).map_add,
293-  map_mul' := ((algebra_map F E).comp (algebra_map K F)).map_mul,
294:  smul := λ a b, (((algebra_map F E).comp (algebra_map K F)) a) * b,

So maybe we can construct a problem there when K = ℚ.

[Kevin Buzzard]

rat.algebra_rat is indeed an instance (every char 0 division ring is a Q-algebra)

[Johan Commelin]

So

instance cyclotomic_field_algebra : algebra A (cyclotomic_field n K) :=
((algebra_map K (cyclotomic_field n K)).comp (algebra_map A K)).to_algebra

is evil. Right? What are the assumption on A and K here?

[Johan Commelin]

I should clone the repo.

[Chris Birkbeck]

We have [is_domain A] [algebra A K] [is_fraction_ring A K]

[Riccardo Brasca]

K is the fraction field

[Johan Commelin]

Aha. Then I guess we should just make this a def. And provide the relevant is_scalar_tower instances for it (after making it an instance locally).

[Johan Commelin]

Do you think you will need this as an instance a lot?

[Riccardo Brasca]

We are going to work with Z, so a def is perfectly fine

[Johan Commelin]

Certainly, when you specialize to ℤ and ℚ, you can give the "correct" instance, which doesn't cause a diamond.

[Riccardo Brasca]

The definition is much more general than what we need

[Johan Commelin]

Right, that's what I suspected.

[Eric Wieser]

Skimming this thread, I'd claim any algebra instance created with (x.comp y).to_algebra will turn out to be evil

[Kevin Buzzard]

However mathematicians want to say "B is an A-algebra and C is a B-algebra so C is obviously an A-algebra"

[Kevin Buzzard]

because if everything is a commutative ring then "B is an A-algebra" is just code for f : A ->+* B

[Riccardo Brasca]

There is no problem in changing the definition, but I don't see how to get rid of the diamond

[Eric Wieser]

Kevin Buzzard said:

However mathematicians want to say "B is an A-algebra and C is a B-algebra so C is obviously an A-algebra"

That's incompatible with the design currently used by mathlib, which is to say "B is an A-algebra, C is a B-algebra, C is an A-algebra in the obvious way", where the last part is is_scalar_tower A B C.

[Eric Wieser]

I'll try a PR to intermediate_field.lift2_alg to fix the smul-diamond.

[Kevin Buzzard]

But using is_scalar_tower isn't going to fix the diamond, right?

[Eric Wieser]

It fixes one of the two diamonds

[Eric Wieser]

(the one in smul but not the one in algebra_map)

[Eric Wieser]

Done: #10012. It's great when the fix is to delete code! replace actual proofs with "we already proved this"

[Eric Wieser]

At a glance I think this fixes the problem at the top of the thread, since it was a diamond in has_scalar not algebra_map

[Riccardo Brasca]

So, I made cyclotomic_field_algebra a lemma instead of an instance. We can just put

local attribute [instance] new_cyclotomic_field.cyclotomic_field_algebra

if we need it.

[Riccardo Brasca]

Now this is one is solved, the same thing happens with the other is_scalar_tower is docs#class_group.fintype_of_admissible_of_finite, but it is surely the same diamond.

[Riccardo Brasca]

number_theory/cyclotomic/class_group finally compiles without errors :grinning:

[Riccardo Brasca]

Thanks to everybody!

[Riccardo Brasca]

I will try this afternoon to make number_theory/cyclotomic/cyclotomic_units using the new definition.

[Eric Wieser]

I think #10019 might solve some more algebra issues, but I might need to change splitting_field too

[Riccardo Brasca]

Thanks! In any case we can work without the algebra instance (over Z), and have it later.

[Riccardo Brasca]

I don't think we need cyclotomic fields over anything than Q for this project.

[Eric Wieser]

Looking more closely at new_cyclotomic_field.cyclotomic_field_algebra, the diamond is caused by the nasty recursion stuff going on to define the field instance

[Eric Wieser]

The field.zsmul that appears in that recursion is not defeq to the algebra.smul that appears in the algebra recursion

[Eric Wieser]

Here's an example of how recursors can create diamonds:

variables {α β : Type*} (f0 : α) (fs : ℕ → α → α) (g0 : β) (gs : ℕ → β → β)

def rec1 : ℕ → α × β
| 0 := (f0, g0)
| (n + 1) := (fs n (rec1 n).1, gs n (rec1 n).2)

def rec2 : ℕ → α × β
| n := (nat.rec_on n f0 fs, nat.rec_on n g0 gs)

-- not definitionally equal
example (n : ℕ) : rec1 f0 fs g0 gs n = rec2 f0 fs g0 gs n := rfl

-- but equal nonetheless
lemma rec1_eq_rec2 : Π n, rec1 f0 fs g0 gs n = rec2 f0 fs g0 gs n
| 0 := rfl
| (n + 1) := begin
  have := rec1_eq_rec2 n,
  dsimp [rec1, rec2, ←nat.succ_eq_add_one],
  rw this,
  refl,
end

[Chris Birkbeck]

Sorry, I've been afk all day today (and will be on most Thursdays), but I'll try and catch-up on all this today/tomorrow :)

[Eric Wieser]

The replacement for lift_alg2 is merged, did it make any difference?

[Chris Birkbeck]

it's working now! edit: no its not. I hadn't read all the messages :(

[Chris Birkbeck]

Thank you!

[Riccardo Brasca]

You should make the two def an instance to check if it's really working. I can do this tomorrow

[Chris Birkbeck]

Oh no you're right. I made them instances and its complaining about is_scalar_tower ℤ ℚ (cyclotomic_field n ℚ)

[Eric Rodriguez]

i just pushed some old work that I did on cyclotomic things, maybe it can give some inspiration for figuring out the general proofs for is_cyclotomic_extension {n} A B

[Eric Rodriguez]

I was looking and thinking, and I think the best way to go about getting any primitive root (at which point the API is good enough for us to do pretty much whatever) is through finding that the cardinality of the roots of unity set is n. I think my specialized argument works, mostly, apart from it requires that X^n-1 splits, whilst we "only" have that there is a root of cyclotomic n F.

We definitely need to assume that our cyclotomic extension is normal, because otherwise we get to the weird Frobenius-y counterexamples, which leads to my final question: do we have a maths-proof that if cyclotomic n F splits, then so does X ^ n - 1? It seems perfectly reasonable to me, but every proof that I'd think of assumes we have a prim-root of unity.

[Riccardo Brasca]

In ready_for_mathlib/cyclotomic there is

lemma is_root_cyclotomic_iff {n : ℕ} {R : Type*} [comm_ring R] [is_domain R] {μ : R}
  : is_primitive_root μ n ↔ is_root (cyclotomic n R) μ := sorry

It shouldn't be difficult.

[Eric Rodriguez]

char_zero simplifies it (it's wrong for some charp; φ₄ ∈ F₂[x], for example) but I don't think it's as trivial as it seems mathematically

[Riccardo Brasca]

Ahahah, yes, that is obviously false, one needs to assume $n \neq 0$ in the base ring.

[Riccardo Brasca]

A simple proof is: let $a$ be a root, then $a^n = 1$ (since $\psi_n$ divides $X^n-1$) so $a$ is a $n$-th root of unity. If $a^m=1$ with $m < n$, then we obtain a repeated root of $X^n-1$, that is impossible.

[Riccardo Brasca]

I used a similar strategy to prove the irreducibility, so all of these is doable without too much effort even in Lean.

[Riccardo Brasca]

To obtain the repeated root we write $X^n-1 = \Psi_n \prod_{i | n, i < n}\Psi_i$, and $X^m-1$ appears in the second product.

[Riccardo Brasca]

Even better: we prove first of all that $a$ is a $n$-th root of unity iff it is the root of some $\Psi_i$ with $i|n$ (this is trivial since we have the product formula). Then it's clear that we obtain a double root.

[Eric Rodriguez]

Ooh, I was looking at the product formula for cyclotomic', which requires a primitive root to be there. Woop! That's good news :) ill try work on this soon

[Eric Rodriguez]

(also #9779 ever relevant...)

[Riccardo Brasca]

cyclotomic' is just implementation, it should never be used unless something is missing in the API for cyclotomic. But then one should add it :)

[Riccardo Brasca]

Ah yes, if we now squarefreeness over any ring even better! For fields it's already there

[Riccardo Brasca]

But docs#polynomial.separable.squarefree is over a field, so one has to generalize this too

[Riccardo Brasca]

I will not have time tomorrow, but I can write all the details on Friday.

[Riccardo Brasca]

@Eric Rodriguez Did you make any progress on the roots of cyclotomic polynomials?

[Riccardo Brasca]

I see you did :)

[Eric Rodriguez]

It's now done!! :) Proof could use with a bit of neatening up but I will do that when I'm not on a potato laptop ;b

[Riccardo Brasca]

Very nice! The only place you uses a field rather than a domain is docs#polynomial.separable.squarefree right?

[Eric Rodriguez]

Yes! And that's actually just too strong of a requirement, too:

import field_theory.separable

variables {F : Type*} [comm_ring F] [is_domain F]

open polynomial
open_locale classical

lemma multiplicity_le_one_of_separable {p q : polynomial F} (hq : ¬ is_unit q)
  (hsep : separable p) : multiplicity q p ≤ 1 :=
begin
  contrapose! hq,
  apply is_unit_of_self_mul_dvd_separable hsep,
  rw ← sq,
  apply multiplicity.pow_dvd_of_le_multiplicity,
  simpa only [nat.cast_one, nat.cast_bit0] using enat.add_one_le_of_lt hq
end

lemma separable.squarefree {p : polynomial F}  (hsep : separable p) : squarefree p :=
begin
  rw multiplicity.squarefree_iff_multiplicity_le_one p,
  intro f,
  by_cases hunit : is_unit f,
  { exact or.inr hunit },
  exact or.inl (multiplicity_le_one_of_separable hunit hsep)
end

[Eric Rodriguez]

oh, maybe it's a bit more dependent on it thinking about it, but I think it just takes replacing ↑n ≠ 0 to is_unit n, possibly

[Riccardo Brasca]

We don't want is_unit n (this is false in the ring of integers), ↑n ≠ 0 is perfect I think.

[Riccardo Brasca]

The main application for us will be the ring of integers in some cyclotomic field

[Riccardo Brasca]

Feel free to add your generalization of separable.squarefree to the project!

[Eric Rodriguez]

the state of the art so far is docs#polynomial.separable_X_pow_sub_C_unit, I've not given much thought to the separability/squarefreeness of X^n-1 in general rings; that's the main issue

[Eric Rodriguez]

it's just the same as the usual code with the typeclasses updated ^^ I will refactor mathlib soon instead

[Riccardo Brasca]

Ah, in docs#polynomial.separable_X_pow_sub_C_unit there is hn : is_unit ↑n...

[Riccardo Brasca]

So we really need fields

[Riccardo Brasca]

We can probably "cheat" using the field of fraction: a root of the cyclotomic polynomial over a domain is a primitive root when considered in in the field of fraction, so it is a primitive root even in the domain.

[Eric Rodriguez]

oh... so it turns out we reinvented the wheel! (EDIT:) docs#polynomial.order_of_root_cyclotomic_eq. The proof looks pretty identical to my proof, too

[Eric Rodriguez]

(yes, it's currently only for zmod, but I assume that's just what was needed)

[Riccardo Brasca]

Oh, and I even wrote that proof!

[Eric Rodriguez]

I'm having a jaunt at all this right now, and I'm just considering how to structure the basic.lean. I think for splitting_field_cyclotomic and most things after it it'll be nice to have the defn of zeta', which is currently in cyclotomic_units (we now get that it's a primitive root for "free"). however, this proof is limited (currently) to fields; is the correct approach to use the localization trick to generalize this result to comm_rings, and then use that there? or just sorry that proof for now, copy everything in, and try work on everything else? it does move it a lot earlier in the import hierarchy

[Riccardo Brasca]

I think it's false for a general ring, but we want it for a domain. The proof using the field of fraction should be easy, right?

[Riccardo Brasca]

But I agree that zeta' should be available as soon as possible

[Eric Rodriguez]

OK, my today has been taken up with the separable generalization, which is now finished: #10337. will be back to flt in a bit :)

[Riccardo Brasca]

I think the definition of is_cyclotomic_extension will not change anymore (at least not in the near future), so it's probably a good idea to finish the basic API and open a PR. I will start working on the sorry in number_theory/cyclotomic/basic, but if you think you have basic results/definition somewhere else (like for example the definition of zeta') don't hesitate to move them to basic.

[Chris Birkbeck]

Awesome. I'm super busy this week, but I should have lots more time for this next week, so I can help with these sorrys (if any remain!)

[Eric Rodriguez]

i've finally had some time to look at some things, but I think this is the sort of thing where I'd want people's inputs. Firstly, I think n : R ≠ 0 will be pretty important for the basic cyclotomic theory, so I propose carrying around in a fact. Everyone accept this as ok?

[Eric Rodriguez]

Secondly, there's a TC timeout in cyclotomic_units:182 - do we worry about it now? Or until we unsorry instances? I don't know how to debug such things

[Riccardo Brasca]

Using := by convert ... instead of := ... seems to fix the timeout for me. I didn't investigate why.

[Eric Rodriguez]

What do you think of the fact idea?

[Kevin Buzzard]

My student Ashvni has been working with p-adic stuff and told me yesterday that fact p.prime drove her nuts :-) In the definition of the p-adic numbers the decision was made to make p the parameter rather than hp : prime p, so what we write in lean corresponds to what we write in papers, but it also makes things quite inconvenient in practice apparently. On the other hand we used facts quite a bit in the perfectoid projectLTE. @Johan Commelin did facts drive you nuts? Don't forget the alternative, which is just to carry hn : n ≠ 0 around by hand

[Johan Commelin]

We didn't use fact in the perfectoid project. Do you mean LTE?

[Johan Commelin]

I found the facts quite convenient. Certainly fact p.prime has been quite pleasant to use for me.

[Johan Commelin]

What exactly are the problems that Ashvni is hitting?

[Riccardo Brasca]

@Eric Rodriguez I don't have any strong opinion about your fact idea, but it is surely true that n : R ≠ 0 is needed in a lot of places. In my opinion we should try to keep things as modular as possible, so we should have a subfolder of the (nonexistent) number_theory/cyclotomic folder called separable (or whatever) where we put all the results that need n : R ≠ 0. We should try to see if having the assumption as fact really reduces what we have to write.

[Johan Commelin]

Here is one reason why fact is sometimes a powerful tool: before we used fact we had two separate types zmod and zmodp. The latter was only defined for primes, and it carried a field instance. But with fact we could unify these, and now zmod n has a ring instance, but in the presence of fact p.prime then zmod p will also have a field instance.

[Alex J. Best]

Yes, this is a very important feature of fact, I think the annoyance comes when you have to mix things that are based on fact and things that just use a regular hypothesis. You have to start writing out everywhere, not so bad, but also take care that tactics can see the fact. For instance library_searhc

import data.nat.prime

lemma a {p : ℕ} [fact p.prime] : 2 ≤ p :=
begin
  library_search, --fails

end


lemma b {p : ℕ} (hp : p.prime) : 2 ≤ p :=
begin
  library_search, --works

end

[Alex J. Best]

I'm not sure if the intended use of fact is to make the hypotheses regular parameters and do haveI : fact p.prime := hp when you know you are going to need it, or to make the hypotheses facts and use have hp : p.prime := fact.out when you want the actual thing

[Johan Commelin]

My rule of thumb is: if you would start the LaTeX version of the file with "For the rest of this paper, we fix a prime number p", then you use fact. But if you are working with various prime numbers, or various types of prime numbers, then regular parameters is probably better.

[Alex J. Best]

Yeah for the library as it is right now you really do need both, so you have to convert between the two at some point

[Johan Commelin]

Note that you can also assume [hp : fact p.prime]. Then hp.1 is a term of type p.prime. Which works quite smoothly, I think.

[Alex J. Best]

But in my example you still have to either know the lemma library searched for, or ahead of time add the line have := hp.1 to your context for every fact

[Johan Commelin]

Or fix library_search :rofl:

[Alex J. Best]

You have to make a lot of other tactics fact aware too though!

[Alex J. Best]

Like assumption for instance

[Johan Commelin]

Ooh, sure, if you want interop with all tactics.

[Johan Commelin]

I was thinking of the discussion that extracts proof fields out of structures, before running a tactic such as library_search.

[Alex J. Best]

Well I would just love all the benefits of fact without having to modify my proofs and habits, at least thats what gets to me about it

[Alex J. Best]

Yeah it would be nice to have a "unfact" tactic, but its still unfortunate to run it at all

[Riccardo Brasca]

I will not have time to work on this during the weekend, but if someone wants to contribute I am stuck at (this is in number_theory/cyclotomic/basic)

lemma union_left [h : is_cyclotomic_extension T A B] (hS : S ⊆ T) :
  is_cyclotomic_extension S A (adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 }) :=
begin
  refine ⟨λ n hn, _, λ b, _⟩,
  { obtain ⟨b, hb⟩ := ((iff _ _ _).1 h).1 n (hS hn),
    refine ⟨⟨b, subset_adjoin ⟨n, hn, _⟩⟩, _⟩,
    { rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← is_root.def] at hb,
      suffices : (X ^ (n : ℕ) - 1).is_root b,
      { simpa [sub_eq_zero] using this },
      rw [← (eq_cyclotomic_iff n.pos _).1 rfl],
      exact root_mul_right_of_is_root _ hb },
      rwa [← subalgebra.coe_eq_zero, aeval_subalgebra_coe, subtype.coe_mk] },
  { sorry }
end

The goal is

...
b: ↥(adjoin A {b : B | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1})
⊢ b ∈ adjoin A {b : ↥(adjoin A {b : B | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1}) | ∃ (a : ℕ+), a ∈ S ∧ b ^ ↑a = 1}

I didn't tried hard, but working with subtypes is annoying! One this is done (or maybe a better reformulation?) the ending the proof of

lemma finite [h₁ : fintype S] [h₂ : is_cyclotomic_extension S A B] : finite A B

should be easy.

[Eric Rodriguez]

this is such a pesky goal...

[Riccardo Brasca]

I agree... But I don't see a better formulation of the result, that is meaningful

[Yakov Pechersky]

You should be able to say "cases b with b hb" to destruct the subtype

[Riccardo Brasca]

I have to sleep now, but that seems to help, thank you!

[Riccardo Brasca]

Is someone working on the last sorrys in number_theory/cyclotomic/basic? If not I will try to work on them tomorrow.
Once these sorrys are done I think we can PR the definition.

[Chris Birkbeck]

So I had said I was going to help with these, but I've had less time than I thought, so haven't been able to look at this :(

[Chris Birkbeck]

Sorry!

[Riccardo Brasca]

No problem!

[Eric Rodriguez]

Yes, I was going to work on them,but I got distracted by the cyclotomic positive proof and degree applications... Hopefully I'll give them a look tonight!

[Riccardo Brasca]

I've proved four sorrys. Now all the basic facts about is_cyclotomic_extension are sorry free. Any ideas on something basic missing? Otherwise would just go for a PR and see what people think about this.

[Chris Birkbeck]

Go for it :) I guess we'll find out later on what other things we need (if any).

[Eric Rodriguez]

I just uploaded a proof that cyclotomic_field n K is a cyclotomic extension (which is pretty much previous work refactored a bit). this approach currently doesn't scale to cyclotomic_ring, and I don't see an obvious workaround; I'm not too versed in no_smul_divisors and such like, but what we need is that the algebra_map K (cyclotomic_ring n K) is injective (which morally it is as it's morally the inclusion map), but I don't see an obvious way to prove that from what we have about algebras and such, e.g. by sidetracking through the fraction ring. If I don't come up with a better solution by tomorrow, I'm just going to sprinkle some char_zero and work on actual FLT instead of side-tracking myself about char-p cyclotomic extensions of domains...

[Riccardo Brasca]

Great work! I am still quite busy this week, but I will try to have a look. I am not completely sure we will need that cyclotomic_ring is a cyclotomic extension, maybe knowing that its field of fraction is cyclotomic_field will be enough.

[Eric Rodriguez]

I've just bumped again, if anyone has time please check I've not moved things wrongly.

[Alex J. Best]

I also tried to bump today, and made basically the same changes as you so mostly LGTM.
However one difference is I came to the conclusion that we should just assume

instance is_cyclotomic_extension [char_zero K] :

as IMO it is way too unwieldy to keep this fact about nested coes floating around, what do you think? For this project I don't think we will need this theory for positive characteristic (though it might be handy), but if we do need it I think we should worry about the extension to that case then rather than having this extra TC now.

[Alex J. Best]

I think the instance is still true if the characteristic divides n right? its just the proof is very annoying

[Eric Rodriguez]

I don't know the proof if the fact isn't true; it's definitely a completely different route to get there, though (I thought I found some counterexamples in Sage a couple days ago, but it was just a off-by-one error instead of anything real). But yea, I definitely think we should have that instance and forget about non-char zero. I added a fact that implies it, but maybe it's better to make my current instance a def and make a char_zero instance for now

[Riccardo Brasca]

Which result are you talking about?

[Riccardo Brasca]

In any case I am pretty sure that for this project char_zero is enough.

[Eric Rodriguez]

Whether cyclotomic_field is actually a cyclotomic extension in the case where is_root_cyclotomic_iff doesn't apply

[Riccardo Brasca]

I think this is true because if F is a field of characteristic p and n = m * p ^ s, with p that does not divide m, then cyclotomic n F = (cyclotomic m F) ^(p^s - p^(s-1)), but we don't have this result yet

[Riccardo Brasca]

Sorry for my long absence, I was super busy lately. I am preparing a PR with a definition of cyclotomic field, so this will be fixed once and for all.

[Riccardo Brasca]

#10849

[Eric Rodriguez]

sorry for always posting here when I make minimal progress; we're close to finishing off the proof of cyclotomic_ring being a cyclotomic extension; I'm once again stuck on proving things are non-zero... if people want to take a look, that's there, else hopefully I'll wake up with inspiration into how to turn algebra_map K (cyclotomic_ring n K) being injective into subalgebra.inclusion \bot (cyclotomic_ring n K) being injective (which is already in the library). Considering I always seem to work on the boring stuff lately, is there any other part of the proof people would like me to help out with instead? I'm happy to help anywhere^^

[Riccardo Brasca]

Having a look now

[Riccardo Brasca]

This is indeed quite annoying, but I will do it.

[Riccardo Brasca]

If you are looking for something slightly more interesting, there is zeta'.embeddings_equiv_primitive_roots in src/number_theory/cyclotomic/cyclotomic_units.lean.

[Riccardo Brasca]

This is false in general, but true over ℚ, that is enough for us

[Riccardo Brasca]

It probable makes sense to think a little bit to a more general version

[Riccardo Brasca]

Injectivity of algebra_map A (cyclotomic_ring n A K) is done.

[Riccardo Brasca]

Now the only sorry left in src/ready_for_mathlib/cyclotomic/basic.lean is

is_fraction_ring (cyclotomic_ring n A K) (cyclotomic_field n K)

I am not sure we need this now, so I made it a lemma, just to bu sure it's not used automatically somewhere

[Riccardo Brasca]

Ops, we already use it... so let me prove the instance

[Riccardo Brasca]

@Eric Rodriguez I see we are working on the same proof... no problem of course.
Have you any idea for surj?

[Riccardo Brasca]

It seems the only nontrivial statement for is_fraction_ring...

[Riccardo Brasca]

Ops, you finished eq_iff_exists, and your proof is better than mine :)

[Eric Rodriguez]

I'm currently thinking of getting the power basis for cyclotomic_field; hopefully that then just lets us use the existing fraction_ring instance to do everything else

[Eric Rodriguez]

I think it's in ring_theory.adjoin.basis or something

[Riccardo Brasca]

Using that cyclotomic_field n K is adjoin K ... I think we can do it with algebra.adjoin_induction without too much trouble

[Riccardo Brasca]

Currently we know this if (((n : ℕ) : A) ≠ 0, but sooner or later we will remove this

[Eric Rodriguez]

The proof of the cyclotomic power thing doesn't seem too bad, just mildly irritating, too. I think Alex's homogenization+factorization stuff will come in handy there

[Alex J. Best]

What's the cyclotomic power thing?

[Eric Rodriguez]

ɸ_{np^k}(x) = ɸₙ(x^p^k)/ɸₙ(x^p^(k-1)) modulo off by one errors

[Riccardo Brasca]

Nonsense

[Riccardo Brasca]

My math proof consists of going to C, where everything splits, and comparing the roots (with multiplicity)

[Alex J. Best]

That does seem annoying, well I hope it helps but it still seems tricky yes

[Riccardo Brasca]

In any case we don't need it

[Alex J. Best]

I thought it was helpful to get rid of some of the char_zero assumptions (or p \ne 0 in K)?

[Riccardo Brasca]

I don't see where we need it, but of course it would be nice to do everything in full generality.

Having this assumption seems to me a good compromise since I will be very easy to remove it when someone will prove the full result

[Riccardo Brasca]

src/ready_for_mathlib/cyclotomic/basic.lean is finally sorry free.

[Riccardo Brasca]

The proof of

is_fraction_ring (cyclotomic_ring n A K) (cyclotomic_field n K)

is not that nice, but at least it works

[Riccardo Brasca]

I've PRed more basic properties of cyclotomic extensions in #11264.

[Eric Rodriguez]

by the way, the algebra_rat diamond came up again when doing the galois proof. was fairly easy to get round when I realised it happened. I'm now going to re-fix ne_zero and then get some sleep