Zulip Chat Archive

Stream: FLT-regular

Topic: Cyclotomic field defn


Eric Rodriguez (Oct 25 2021 at 17:09):

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 (Oct 25 2021 at 17:12):

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 (Oct 25 2021 at 17:13):

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

Alex J. Best (Oct 25 2021 at 17:19):

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 (Oct 25 2021 at 17:20):

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 (Oct 25 2021 at 17:31):

.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 (Oct 25 2021 at 17:32):

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 (Oct 25 2021 at 17:33):

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 (Oct 25 2021 at 17:37):

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 (Oct 25 2021 at 17:42):

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

Eric Rodriguez (Oct 25 2021 at 17:42):

What is the point of polynomial.gal then?

Thomas Browning (Oct 25 2021 at 17:45):

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 (Oct 25 2021 at 17:52):

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 (Oct 25 2021 at 17:54):

I am almost tempted to have is_cyclotomic_field

Johan Commelin (Oct 25 2021 at 17:56):

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

Riccardo Brasca (Oct 25 2021 at 18:01):

Yes, sure

Riccardo Brasca (Oct 25 2021 at 18:01):

Let me try

Riccardo Brasca (Oct 25 2021 at 18:37):

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

Chris Birkbeck (Oct 25 2021 at 18:41):

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

Johan Commelin (Oct 25 2021 at 18:44):

Do we already have some sort of is_ring_of_integers?

Johan Commelin (Oct 25 2021 at 18:45):

@Anne Baanen I forgot the status...

Riccardo Brasca (Oct 25 2021 at 18:47):

Chris Birkbeck said:

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

I am fixing it

Alex J. Best (Oct 25 2021 at 18:55):

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 (Oct 25 2021 at 18:58):

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

Riccardo Brasca (Oct 25 2021 at 19:03):

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 (Oct 25 2021 at 19:09):

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 (Oct 25 2021 at 19:10):

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 (Oct 25 2021 at 19:11):

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 (Oct 25 2021 at 19:22):

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 (Oct 25 2021 at 19:23):

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 (Oct 25 2021 at 19:25):

Ah, we have docs#is_integral_closure!

Riccardo Brasca (Oct 25 2021 at 19:26):

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 (Oct 25 2021 at 19:47):

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 (Oct 25 2021 at 19:47):

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

Eric Rodriguez (Oct 25 2021 at 19:57):

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

Eric Rodriguez (Oct 25 2021 at 19:57):

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

Riccardo Brasca (Oct 25 2021 at 20:25):

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 (Oct 25 2021 at 20:26):

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

Adam Topaz (Oct 25 2021 at 20:26):

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

Riccardo Brasca (Oct 25 2021 at 20:27):

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

Adam Topaz (Oct 25 2021 at 20:27):

What's the problem with char p?

Adam Topaz (Oct 25 2021 at 20:27):

The p-cyclotomic extension of a field KK of characteristic pp is KK itself.

Riccardo Brasca (Oct 25 2021 at 20:28):

I mean, if I want to use is_splitting_field

Riccardo Brasca (Oct 25 2021 at 20:28):

I need a base field

Eric Rodriguez (Oct 25 2021 at 20:29):

What about is_cyclotomic_extension F K n?

Riccardo Brasca (Oct 25 2021 at 20:30):

Defined using is_splitting_field?

Thomas Browning (Oct 25 2021 at 20:30):

meaning?

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

Riccardo Brasca (Oct 25 2021 at 20:30):

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

Adam Topaz (Oct 25 2021 at 20:31):

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 (Oct 25 2021 at 20:44):

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 (Oct 25 2021 at 20:46):

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 (Oct 25 2021 at 21:00):

Could I have permission to push? (username tb65536)

Eric Rodriguez (Oct 25 2021 at 22:19):

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

Scott Morrison (Oct 25 2021 at 22:25):

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

Adam Topaz (Oct 25 2021 at 23:00):

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 (Oct 25 2021 at 23:15):

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 (Oct 25 2021 at 23:24):

Why closed under multiplication?

Adam Topaz (Oct 25 2021 at 23:26):

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

Alex J. Best (Oct 25 2021 at 23:29):

@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 (Oct 25 2021 at 23:45):

Adam Topaz said:

Why closed under multiplication?

Sorry, I meant closed under lcm.

Thomas Browning (Oct 25 2021 at 23:45):

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 (Oct 26 2021 at 01:35):

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 (Oct 26 2021 at 04:55):

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 (Oct 26 2021 at 08:48):

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 (Oct 26 2021 at 08:49):

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

Chris Birkbeck (Oct 26 2021 at 08:56):

I agree infinite cyclotomic extensions would be great.

Riccardo Brasca (Oct 26 2021 at 09:01):

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

Riccardo Brasca (Oct 26 2021 at 09:01):

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

Riccardo Brasca (Oct 26 2021 at 12:17):

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 (Oct 26 2021 at 12:34):

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 (Oct 26 2021 at 12:44):

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

Adam Topaz (Oct 26 2021 at 12:45):

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

Johan Commelin (Oct 26 2021 at 12:46):

Hmm, that's a good point (-;

Adam Topaz (Oct 26 2021 at 12:46):

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 (Oct 26 2021 at 12:47):

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

Riccardo Brasca (Oct 26 2021 at 12:48):

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

Adam Topaz (Oct 26 2021 at 12:48):

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 (Oct 26 2021 at 12:49):

OK, let's try pnat.

Adam Topaz (Oct 26 2021 at 12:51):

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

Riccardo Brasca (Oct 26 2021 at 12:53):

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

Riccardo Brasca (Oct 26 2021 at 13:22):

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 (Oct 26 2021 at 13:24):

I'm happy with that.

Johan Commelin (Oct 26 2021 at 13:28):

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

Johan Commelin (Oct 26 2021 at 13:28):

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

Johan Commelin (Oct 26 2021 at 13:30):

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 (Oct 26 2021 at 13:30):

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

Adam Topaz (Oct 26 2021 at 13:31):

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

Riccardo Brasca (Oct 26 2021 at 13:35):

⋃ 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 (Oct 26 2021 at 13:35):

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 (Oct 26 2021 at 13:35):

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

Johan Commelin (Oct 26 2021 at 13:36):

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

Riccardo Brasca (Oct 26 2021 at 13:36):

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

Riccardo Brasca (Oct 26 2021 at 13:38):

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 (Oct 26 2021 at 13:38):

That looks good to me!

Adam Topaz (Oct 26 2021 at 13:39):

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 (Oct 26 2021 at 13:39):

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

Johan Commelin (Oct 26 2021 at 13:40):

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

Johan Commelin (Oct 26 2021 at 13:40):

Then proofs don't need to start with rw eq_top_iff

Riccardo Brasca (Oct 26 2021 at 13:47):

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 (Oct 26 2021 at 13:50):

I wouldn't worry about this for now.

Johan Commelin (Oct 26 2021 at 13:50):

Just assume commutativity.

Adam Topaz (Oct 26 2021 at 13:53):

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 (Oct 26 2021 at 13:53):

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

Riccardo Brasca (Oct 26 2021 at 13:59):

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

Adam Topaz (Oct 26 2021 at 14:01):

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 (Oct 26 2021 at 14:02):

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

Riccardo Brasca (Oct 26 2021 at 14:05):

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 (Oct 26 2021 at 14:21):

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

Riccardo Brasca (Oct 26 2021 at 14:29):

good point

Thomas Browning (Oct 26 2021 at 14:47):

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 (Oct 26 2021 at 14:49):

We get the extension generated by all roots of unity.

Thomas Browning (Oct 26 2021 at 14:49):

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

Riccardo Brasca (Oct 26 2021 at 14:50):

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

Riccardo Brasca (Oct 26 2021 at 15:03):

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 (Oct 26 2021 at 15:03):

But that doesn't matter right?

Johan Commelin (Oct 26 2021 at 15:04):

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

Thomas Browning (Oct 26 2021 at 15:04):

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 (Oct 26 2021 at 15:07):

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

Riccardo Brasca (Oct 26 2021 at 15:08):

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

Thomas Browning (Oct 26 2021 at 15:10):

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 Z^×\widehat{\mathbb{Z}}^\times. This would also give us the Zp\mathbb{Z}_p from Iwasawa theory.

Thomas Browning (Oct 26 2021 at 15:10):

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

Adam Topaz (Oct 26 2021 at 15:11):

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 Z^×\widehat{\mathbb{Z}}^\times. This would also give us the Zp\mathbb{Z}_p from Iwasawa theory.

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

Johan Commelin (Oct 26 2021 at 15:12):

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

Thomas Browning (Oct 26 2021 at 15:12):

Could you do both simultaneously with adjoin_root?

Adam Topaz (Oct 26 2021 at 15:12):

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

Thomas Browning (Oct 26 2021 at 15:13):

Adam Topaz said:

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

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 (Oct 26 2021 at 15:14):

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 (Oct 26 2021 at 15:14):

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

Riccardo Brasca (Oct 26 2021 at 15:15):

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 (Oct 26 2021 at 15:15):

No, we want all the roots

Thomas Browning (Oct 26 2021 at 15:16):

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

Thomas Browning (Oct 26 2021 at 15:16):

This might even generalize the splitting field construction

Johan Commelin (Oct 26 2021 at 15:19):

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

Riccardo Brasca (Oct 26 2021 at 15:19):

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 (Oct 26 2021 at 15:20):

Yes exactly, having the field we can work there

Riccardo Brasca (Oct 26 2021 at 15:20):

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

Riccardo Brasca (Oct 26 2021 at 16:09):

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 (Oct 26 2021 at 16:10):

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

Riccardo Brasca (Oct 26 2021 at 16:10):

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 (Oct 26 2021 at 16:14):

Awesome!

Chris Birkbeck (Oct 27 2021 at 08:34):

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 (Oct 27 2021 at 08:41):

It means there is a cycle of instances

Riccardo Brasca (Oct 27 2021 at 08:41):

Where is it?

Chris Birkbeck (Oct 27 2021 at 08:42):

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 (Oct 27 2021 at 08:43):

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

Riccardo Brasca (Oct 27 2021 at 08:43):

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 (Oct 27 2021 at 08:45):

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 (Oct 27 2021 at 08:45):

But no problem for your commit :)

Chris Birkbeck (Oct 27 2021 at 08:46):

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

Chris Birkbeck (Oct 27 2021 at 08:48):

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

Riccardo Brasca (Oct 27 2021 at 08:53):

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 (Oct 27 2021 at 08:57):

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 (Oct 27 2021 at 08:59):

There is no open here or am I blind?

Riccardo Brasca (Oct 27 2021 at 08:59):

But let me check the real error

Chris Birkbeck (Oct 27 2021 at 08:59):

Oh wait, maybe I pushed the wrong thing.

Chris Birkbeck (Oct 27 2021 at 09:01):

Yes I forgot to hit save before pushing, sorry!

Riccardo Brasca (Oct 27 2021 at 09:03):

I get an invalid namespace name 'new_cyclotomic_field' error.

Chris Birkbeck (Oct 27 2021 at 09:04):

Yeah, did you delete that namespace?

Riccardo Brasca (Oct 27 2021 at 09:05):

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

Chris Birkbeck (Oct 27 2021 at 09:06):

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

Chris Birkbeck (Oct 27 2021 at 09:07):

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

Riccardo Brasca (Oct 27 2021 at 09:08):

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 (Oct 27 2021 at 09:15):

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 (Oct 27 2021 at 09:26):

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 (Oct 27 2021 at 09:41):

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 (Oct 27 2021 at 09:44):

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 (Oct 27 2021 at 09:47):

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 (Oct 27 2021 at 09:48):

Oh, OK, I see

Riccardo Brasca (Oct 27 2021 at 09:48):

euclidean_domain does not need ring

Riccardo Brasca (Oct 27 2021 at 09:49):

Bu the other problem is still there

Alex J. Best (Oct 27 2021 at 09:49):

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

Chris Birkbeck (Oct 27 2021 at 10:31):

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 (Oct 27 2021 at 10:33):

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

Kevin Buzzard (Oct 27 2021 at 10:35):

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 (Oct 27 2021 at 10:36):

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 (Oct 27 2021 at 10:37):

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((x1,y1),(x2,y2)):=(d(x1,y1)2+d(x2,y2)2d((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 (Oct 27 2021 at 10:39):

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×VU\times V) whereas the topology coming from the metric has a basis which are "discs" (i.e. distance from a fixed point is <r<r).

Kevin Buzzard (Oct 27 2021 at 10:39):

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

Chris Birkbeck (Oct 27 2021 at 10:40):

Aha that makes perfect sense, thank you!

Kevin Buzzard (Oct 27 2021 at 10:40):

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 (Oct 27 2021 at 10:41):

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 (Oct 27 2021 at 10:41):

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 (Oct 27 2021 at 10:43):

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 (Oct 27 2021 at 10:44):

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

Chris Birkbeck (Oct 27 2021 at 10:48):

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

Johan Commelin (Oct 27 2021 at 10:52):

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 (Oct 27 2021 at 10:55):

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 (Oct 27 2021 at 10:57):

Credits to Julian Berman for writing it!

Kevin Buzzard (Oct 27 2021 at 11:10):

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 (Oct 27 2021 at 11:11):

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

Johan Commelin (Oct 27 2021 at 11:11):

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

Kevin Buzzard (Oct 27 2021 at 11:13):

Gotcha

Johan Commelin (Oct 27 2021 at 11:15):

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

Johan Commelin (Oct 27 2021 at 11:15):

Which contains your metric space example.

Riccardo Brasca (Oct 27 2021 at 11:25):

@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 (Oct 27 2021 at 11:37):

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 (Oct 27 2021 at 12:43):

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 (Oct 27 2021 at 12:46):

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

Riccardo Brasca (Oct 27 2021 at 12:57):

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 (Oct 27 2021 at 12:57):

I've unfolded the def by hand.

Riccardo Brasca (Oct 27 2021 at 12:59):

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 (Oct 27 2021 at 12:59):

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

Riccardo Brasca (Oct 27 2021 at 13:08):

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 (Oct 27 2021 at 13:20):

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 (Oct 27 2021 at 13:33):

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 (Oct 27 2021 at 13:34):

It has to be a lemma, not an instance.

Riccardo Brasca (Oct 27 2021 at 13:34):

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

Chris Birkbeck (Oct 27 2021 at 13:35):

Riccardo Brasca said:

It has to be a lemma, not an instance.

Ahh ok.

Chris Birkbeck (Oct 27 2021 at 13:35):

Riccardo Brasca said:

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

Oh no

Riccardo Brasca (Oct 27 2021 at 13:37):

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 (Oct 27 2021 at 13:37):

(deleted)

Riccardo Brasca (Oct 27 2021 at 13:38):

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

Riccardo Brasca (Oct 27 2021 at 13:39):

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 (Oct 27 2021 at 13:40):

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

Riccardo Brasca (Oct 27 2021 at 13:42):

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

Riccardo Brasca (Oct 27 2021 at 14:28):

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 (Oct 27 2021 at 14:29):

@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 (Oct 27 2021 at 14:30):

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

Marc Masdeu (Oct 27 2021 at 14:40):

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 (Oct 27 2021 at 15:28):

yeah I didn't click through :-)

Kevin Buzzard (Oct 27 2021 at 15:31):

The diamond error is that Lean is failing to solve

smul_with_zero.to_has_scalar = sub_neg_monoid.has_scalar_int

Riccardo Brasca (Oct 27 2021 at 15:36):

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

Kevin Buzzard (Oct 27 2021 at 15:37):

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 (Oct 27 2021 at 15:38):

I'm still thinking about it

Kevin Buzzard (Oct 27 2021 at 15:38):

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 (Oct 27 2021 at 15:39):

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

Kevin Buzzard (Oct 27 2021 at 15:41):

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

Kevin Buzzard (Oct 27 2021 at 15:42):

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 (Oct 27 2021 at 15:43):

The two goals are OK

Kevin Buzzard (Oct 27 2021 at 15:43):

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

Kevin Buzzard (Oct 27 2021 at 15:43):

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

Riccardo Brasca (Oct 27 2021 at 15:45):

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 (Oct 27 2021 at 15:46):

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 (Oct 27 2021 at 15:48):

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

Johan Commelin (Oct 27 2021 at 15:48):

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 (Oct 27 2021 at 15:49):

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 (Oct 27 2021 at 15:52):

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 (Oct 27 2021 at 15:53):

The definition of cyclotomic_field n K is

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

Kevin Buzzard (Oct 27 2021 at 15:54):

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 (Oct 27 2021 at 15:54):

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

Riccardo Brasca (Oct 27 2021 at 15:57):

@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 (Oct 27 2021 at 16:16):

The bad instance is coming from algebra.to_has_scalar

Riccardo Brasca (Oct 27 2021 at 16:22):

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

Riccardo Brasca (Oct 27 2021 at 16:22):

Let me check where it comes from.

Chris Birkbeck (Oct 27 2021 at 16:23):

Does it come from cyclotomic_field_algebra?

Kevin Buzzard (Oct 27 2021 at 16:24):

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

Riccardo Brasca (Oct 27 2021 at 16:25):

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 (Oct 27 2021 at 16:27):

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

Riccardo Brasca (Oct 27 2021 at 16:34):

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 (Oct 27 2021 at 16:35):

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

Kevin Buzzard (Oct 27 2021 at 16:36):

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 (Oct 27 2021 at 16:37):

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

Kevin Buzzard (Oct 27 2021 at 16:38):

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 (Oct 27 2021 at 16:39):

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

Chris Birkbeck (Oct 27 2021 at 16:39):

Yeah it must be because its defined as a composition

Riccardo Brasca (Oct 27 2021 at 16:39):

Oh gosh, thank you

Chris Birkbeck (Oct 27 2021 at 16:40):

or not, I dont know

Riccardo Brasca (Oct 27 2021 at 16:41):

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

Riccardo Brasca (Oct 27 2021 at 16:41):

Let me see if I have enough time

Kevin Buzzard (Oct 27 2021 at 16:45):

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 (Oct 27 2021 at 16:47):

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

Johan Commelin (Oct 27 2021 at 16:48):

Lean cannot guess which K it should be looking for.

Adam Topaz (Oct 27 2021 at 16:48):

I thought that was the whole point of scalar towers?

Kevin Buzzard (Oct 27 2021 at 16:48):

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 (Oct 27 2021 at 16:52):

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 (Oct 27 2021 at 16:52):

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

Johan Commelin (Oct 27 2021 at 16:53):

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 (Oct 27 2021 at 16:53):

maybe algebra_int shouldn't be an instance?

Kevin Buzzard (Oct 27 2021 at 16:53):

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 (Oct 27 2021 at 16:54):

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

Adam Topaz (Oct 27 2021 at 16:55):

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

Kevin Buzzard (Oct 27 2021 at 16:56):

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

Johan Commelin (Oct 27 2021 at 16:56):

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 (Oct 27 2021 at 16:57):

sigh

Riccardo Brasca (Oct 27 2021 at 17:06):

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

Johan Commelin (Oct 27 2021 at 17:09):

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 (Oct 27 2021 at 17:09):

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

Kevin Buzzard (Oct 27 2021 at 17:10):

i.e. none of them are instances

Johan Commelin (Oct 27 2021 at 17:10):

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 (Oct 27 2021 at 17:11):

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

Johan Commelin (Oct 27 2021 at 17:16):

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 (Oct 27 2021 at 17:16):

I should clone the repo.

Chris Birkbeck (Oct 27 2021 at 17:17):

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

Riccardo Brasca (Oct 27 2021 at 17:17):

K is the fraction field

Johan Commelin (Oct 27 2021 at 17:34):

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 (Oct 27 2021 at 17:34):

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

Riccardo Brasca (Oct 27 2021 at 17:35):

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

Johan Commelin (Oct 27 2021 at 17:35):

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

Riccardo Brasca (Oct 27 2021 at 17:36):

The definition is much more general than what we need

Johan Commelin (Oct 27 2021 at 17:37):

Right, that's what I suspected.

Eric Wieser (Oct 27 2021 at 21:15):

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

Kevin Buzzard (Oct 27 2021 at 21:16):

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 (Oct 27 2021 at 21:17):

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

Riccardo Brasca (Oct 27 2021 at 21:46):

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

Eric Wieser (Oct 27 2021 at 22:04):

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 (Oct 27 2021 at 22:07):

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

Kevin Buzzard (Oct 27 2021 at 22:09):

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

Eric Wieser (Oct 27 2021 at 22:21):

It fixes one of the two diamonds

Eric Wieser (Oct 27 2021 at 22:22):

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

Eric Wieser (Oct 27 2021 at 22:46):

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

Eric Wieser (Oct 27 2021 at 23:48):

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 (Oct 28 2021 at 08:07):

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 (Oct 28 2021 at 08:08):

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 (Oct 28 2021 at 08:26):

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

Riccardo Brasca (Oct 28 2021 at 08:26):

Thanks to everybody!

Riccardo Brasca (Oct 28 2021 at 08:53):

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

Eric Wieser (Oct 28 2021 at 11:10):

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

Riccardo Brasca (Oct 28 2021 at 11:31):

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

Riccardo Brasca (Oct 28 2021 at 11:32):

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

Eric Wieser (Oct 28 2021 at 12:09):

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 (Oct 28 2021 at 12:10):

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

Eric Wieser (Oct 28 2021 at 12:28):

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 (Oct 28 2021 at 18:46):

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 (Oct 28 2021 at 19:02):

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

Chris Birkbeck (Oct 28 2021 at 19:52):

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

Chris Birkbeck (Oct 28 2021 at 19:53):

Thank you!

Riccardo Brasca (Oct 28 2021 at 19:59):

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

Chris Birkbeck (Oct 28 2021 at 20:03):

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

Eric Rodriguez (Nov 10 2021 at 01:52):

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 (Nov 10 2021 at 20:15):

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 (Nov 10 2021 at 20:30):

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 (Nov 10 2021 at 20:48):

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 (Nov 10 2021 at 20:54):

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

Riccardo Brasca (Nov 10 2021 at 20:57):

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

Riccardo Brasca (Nov 10 2021 at 20:58):

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

Riccardo Brasca (Nov 10 2021 at 21:02):

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

Riccardo Brasca (Nov 10 2021 at 21:04):

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

Eric Rodriguez (Nov 10 2021 at 21:06):

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 (Nov 10 2021 at 21:07):

(also #9779 ever relevant...)

Riccardo Brasca (Nov 10 2021 at 21:08):

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 (Nov 10 2021 at 21:10):

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

Riccardo Brasca (Nov 10 2021 at 21:11):

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

Riccardo Brasca (Nov 10 2021 at 21:15):

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

Riccardo Brasca (Nov 12 2021 at 09:18):

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

Riccardo Brasca (Nov 12 2021 at 09:19):

I see you did :)

Eric Rodriguez (Nov 12 2021 at 11:18):

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 (Nov 12 2021 at 11:25):

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

Eric Rodriguez (Nov 12 2021 at 11:39):

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

Eric Rodriguez (Nov 12 2021 at 11:40):

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 (Nov 12 2021 at 11:44):

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

Riccardo Brasca (Nov 12 2021 at 11:44):

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

Riccardo Brasca (Nov 12 2021 at 11:50):

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

Eric Rodriguez (Nov 12 2021 at 11:51):

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 (Nov 12 2021 at 11:51):

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

Riccardo Brasca (Nov 12 2021 at 11:56):

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

Riccardo Brasca (Nov 12 2021 at 11:57):

So we really need fields

Riccardo Brasca (Nov 12 2021 at 11:59):

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 (Nov 14 2021 at 15:52):

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 (Nov 14 2021 at 15:53):

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

Riccardo Brasca (Nov 14 2021 at 19:05):

Oh, and I even wrote that proof!

Eric Rodriguez (Nov 15 2021 at 00:37):

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 (Nov 15 2021 at 09:14):

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 (Nov 15 2021 at 09:30):

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

Eric Rodriguez (Nov 15 2021 at 19:00):

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 (Nov 17 2021 at 14:46):

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 (Nov 17 2021 at 22:08):

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 (Nov 19 2021 at 00:33):

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 (Nov 19 2021 at 00:34):

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 (Nov 19 2021 at 08:23):

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

Eric Rodriguez (Nov 19 2021 at 09:51):

What do you think of the fact idea?

Kevin Buzzard (Nov 19 2021 at 09:59):

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 (Nov 19 2021 at 10:04):

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

Johan Commelin (Nov 19 2021 at 10:04):

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

Johan Commelin (Nov 19 2021 at 10:05):

What exactly are the problems that Ashvni is hitting?

Riccardo Brasca (Nov 19 2021 at 10:35):

@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 (Nov 19 2021 at 10:37):

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 (Nov 19 2021 at 13:17):

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 (Nov 19 2021 at 13:19):

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 (Nov 19 2021 at 13:26):

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 (Nov 19 2021 at 13:27):

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 (Nov 19 2021 at 13:28):

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 (Nov 19 2021 at 13:29):

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 (Nov 19 2021 at 13:29):

Or fix library_search :rofl:

Alex J. Best (Nov 19 2021 at 13:32):

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

Alex J. Best (Nov 19 2021 at 13:33):

Like assumption for instance

Johan Commelin (Nov 19 2021 at 13:36):

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

Johan Commelin (Nov 19 2021 at 13:36):

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

Alex J. Best (Nov 19 2021 at 13:37):

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 (Nov 19 2021 at 13:37):

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

Riccardo Brasca (Nov 20 2021 at 09:10):

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 (Nov 20 2021 at 18:00):

this is such a pesky goal...

Riccardo Brasca (Nov 20 2021 at 19:21):

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

Yakov Pechersky (Nov 20 2021 at 23:33):

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

Riccardo Brasca (Nov 21 2021 at 00:55):

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

Riccardo Brasca (Dec 01 2021 at 15:42):

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 (Dec 01 2021 at 15:43):

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 (Dec 01 2021 at 15:43):

Sorry!

Riccardo Brasca (Dec 01 2021 at 15:46):

No problem!

Eric Rodriguez (Dec 01 2021 at 15:49):

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 (Dec 02 2021 at 15:55):

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 (Dec 02 2021 at 19:24):

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

Eric Rodriguez (Dec 09 2021 at 02:22):

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 (Dec 09 2021 at 09:43):

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 (Dec 13 2021 at 00:11):

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

Alex J. Best (Dec 13 2021 at 00:25):

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 (Dec 13 2021 at 00:25):

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

Eric Rodriguez (Dec 13 2021 at 00:37):

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 (Dec 13 2021 at 07:54):

Which result are you talking about?

Riccardo Brasca (Dec 13 2021 at 07:55):

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

Eric Rodriguez (Dec 13 2021 at 10:13):

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

Riccardo Brasca (Dec 13 2021 at 11:07):

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 (Dec 16 2021 at 15:43):

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 (Dec 16 2021 at 19:19):

#10849

Eric Rodriguez (Dec 21 2021 at 05:48):

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 (Dec 21 2021 at 08:43):

Having a look now

Riccardo Brasca (Dec 21 2021 at 09:56):

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

Riccardo Brasca (Dec 21 2021 at 09:58):

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 (Dec 21 2021 at 09:58):

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

Riccardo Brasca (Dec 21 2021 at 09:58):

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

Riccardo Brasca (Dec 21 2021 at 12:52):

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

Riccardo Brasca (Dec 21 2021 at 13:37):

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 (Dec 21 2021 at 13:40):

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

Riccardo Brasca (Dec 21 2021 at 15:20):

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

Riccardo Brasca (Dec 21 2021 at 15:21):

It seems the only nontrivial statement for is_fraction_ring...

Riccardo Brasca (Dec 21 2021 at 15:21):

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

Eric Rodriguez (Dec 21 2021 at 15:24):

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 (Dec 21 2021 at 15:25):

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

Riccardo Brasca (Dec 21 2021 at 15:36):

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 (Dec 21 2021 at 15:37):

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

Eric Rodriguez (Dec 21 2021 at 15:45):

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 (Dec 21 2021 at 15:46):

What's the cyclotomic power thing?

Eric Rodriguez (Dec 21 2021 at 15:51):

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

Riccardo Brasca (Dec 21 2021 at 15:51):

Nonsense

Riccardo Brasca (Dec 21 2021 at 15:54):

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

Alex J. Best (Dec 21 2021 at 15:56):

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

Riccardo Brasca (Dec 21 2021 at 16:01):

In any case we don't need it

Alex J. Best (Dec 21 2021 at 16:03):

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

Riccardo Brasca (Dec 21 2021 at 16:08):

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 (Dec 21 2021 at 17:40):

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

Riccardo Brasca (Dec 21 2021 at 17:42):

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 (Jan 05 2022 at 16:32):

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

Eric Rodriguez (Feb 01 2022 at 00:56):

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 (Oct 25 2021 at 17:09):

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 (Oct 25 2021 at 17:12):

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 (Oct 25 2021 at 17:13):

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

Alex J. Best (Oct 25 2021 at 17:19):

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 (Oct 25 2021 at 17:20):

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 (Oct 25 2021 at 17:31):

.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 (Oct 25 2021 at 17:32):

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 (Oct 25 2021 at 17:33):

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 (Oct 25 2021 at 17:37):

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 (Oct 25 2021 at 17:42):

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

Eric Rodriguez (Oct 25 2021 at 17:42):

What is the point of polynomial.gal then?

Thomas Browning (Oct 25 2021 at 17:45):

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 (Oct 25 2021 at 17:52):

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 (Oct 25 2021 at 17:54):

I am almost tempted to have is_cyclotomic_field

Johan Commelin (Oct 25 2021 at 17:56):

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

Riccardo Brasca (Oct 25 2021 at 18:01):

Yes, sure

Riccardo Brasca (Oct 25 2021 at 18:01):

Let me try

Riccardo Brasca (Oct 25 2021 at 18:37):

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

Chris Birkbeck (Oct 25 2021 at 18:41):

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

Johan Commelin (Oct 25 2021 at 18:44):

Do we already have some sort of is_ring_of_integers?

Johan Commelin (Oct 25 2021 at 18:45):

@Anne Baanen I forgot the status...

Riccardo Brasca (Oct 25 2021 at 18:47):

Chris Birkbeck said:

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

I am fixing it

Alex J. Best (Oct 25 2021 at 18:55):

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 (Oct 25 2021 at 18:58):

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

Riccardo Brasca (Oct 25 2021 at 19:03):

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 (Oct 25 2021 at 19:09):

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 (Oct 25 2021 at 19:10):

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 (Oct 25 2021 at 19:11):

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 (Oct 25 2021 at 19:22):

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 (Oct 25 2021 at 19:23):

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 (Oct 25 2021 at 19:25):

Ah, we have docs#is_integral_closure!

Riccardo Brasca (Oct 25 2021 at 19:26):

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 (Oct 25 2021 at 19:47):

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 (Oct 25 2021 at 19:47):

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

Eric Rodriguez (Oct 25 2021 at 19:57):

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

Eric Rodriguez (Oct 25 2021 at 19:57):

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

Riccardo Brasca (Oct 25 2021 at 20:25):

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 (Oct 25 2021 at 20:26):

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

Adam Topaz (Oct 25 2021 at 20:26):

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

Riccardo Brasca (Oct 25 2021 at 20:27):

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

Adam Topaz (Oct 25 2021 at 20:27):

What's the problem with char p?

Adam Topaz (Oct 25 2021 at 20:27):

The p-cyclotomic extension of a field KK of characteristic pp is KK itself.

Riccardo Brasca (Oct 25 2021 at 20:28):

I mean, if I want to use is_splitting_field

Riccardo Brasca (Oct 25 2021 at 20:28):

I need a base field

Eric Rodriguez (Oct 25 2021 at 20:29):

What about is_cyclotomic_extension F K n?

Riccardo Brasca (Oct 25 2021 at 20:30):

Defined using is_splitting_field?

Thomas Browning (Oct 25 2021 at 20:30):

meaning?

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

Riccardo Brasca (Oct 25 2021 at 20:30):

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

Adam Topaz (Oct 25 2021 at 20:31):

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 (Oct 25 2021 at 20:44):

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 (Oct 25 2021 at 20:46):

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 (Oct 25 2021 at 21:00):

Could I have permission to push? (username tb65536)

Eric Rodriguez (Oct 25 2021 at 22:19):

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

Scott Morrison (Oct 25 2021 at 22:25):

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

Adam Topaz (Oct 25 2021 at 23:00):

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 (Oct 25 2021 at 23:15):

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 (Oct 25 2021 at 23:24):

Why closed under multiplication?

Adam Topaz (Oct 25 2021 at 23:26):

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

Alex J. Best (Oct 25 2021 at 23:29):

@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 (Oct 25 2021 at 23:45):

Adam Topaz said:

Why closed under multiplication?

Sorry, I meant closed under lcm.

Thomas Browning (Oct 25 2021 at 23:45):

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 (Oct 26 2021 at 01:35):

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 (Oct 26 2021 at 04:55):

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 (Oct 26 2021 at 08:48):

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 (Oct 26 2021 at 08:49):

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

Chris Birkbeck (Oct 26 2021 at 08:56):

I agree infinite cyclotomic extensions would be great.

Riccardo Brasca (Oct 26 2021 at 09:01):

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

Riccardo Brasca (Oct 26 2021 at 09:01):

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

Riccardo Brasca (Oct 26 2021 at 12:17):

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 (Oct 26 2021 at 12:34):

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 (Oct 26 2021 at 12:44):

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

Adam Topaz (Oct 26 2021 at 12:45):

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

Johan Commelin (Oct 26 2021 at 12:46):

Hmm, that's a good point (-;

Adam Topaz (Oct 26 2021 at 12:46):

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 (Oct 26 2021 at 12:47):

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

Riccardo Brasca (Oct 26 2021 at 12:48):

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

Adam Topaz (Oct 26 2021 at 12:48):

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 (Oct 26 2021 at 12:49):

OK, let's try pnat.

Adam Topaz (Oct 26 2021 at 12:51):

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

Riccardo Brasca (Oct 26 2021 at 12:53):

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

Riccardo Brasca (Oct 26 2021 at 13:22):

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 (Oct 26 2021 at 13:24):

I'm happy with that.

Johan Commelin (Oct 26 2021 at 13:28):

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

Johan Commelin (Oct 26 2021 at 13:28):

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

Johan Commelin (Oct 26 2021 at 13:30):

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 (Oct 26 2021 at 13:30):

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

Adam Topaz (Oct 26 2021 at 13:31):

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

Riccardo Brasca (Oct 26 2021 at 13:35):

⋃ 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 (Oct 26 2021 at 13:35):

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 (Oct 26 2021 at 13:35):

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

Johan Commelin (Oct 26 2021 at 13:36):

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

Riccardo Brasca (Oct 26 2021 at 13:36):

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

Riccardo Brasca (Oct 26 2021 at 13:38):

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 (Oct 26 2021 at 13:38):

That looks good to me!

Adam Topaz (Oct 26 2021 at 13:39):

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 (Oct 26 2021 at 13:39):

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

Johan Commelin (Oct 26 2021 at 13:40):

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

Johan Commelin (Oct 26 2021 at 13:40):

Then proofs don't need to start with rw eq_top_iff

Riccardo Brasca (Oct 26 2021 at 13:47):

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 (Oct 26 2021 at 13:50):

I wouldn't worry about this for now.

Johan Commelin (Oct 26 2021 at 13:50):

Just assume commutativity.

Adam Topaz (Oct 26 2021 at 13:53):

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 (Oct 26 2021 at 13:53):

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

Riccardo Brasca (Oct 26 2021 at 13:59):

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

Adam Topaz (Oct 26 2021 at 14:01):

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 (Oct 26 2021 at 14:02):

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

Riccardo Brasca (Oct 26 2021 at 14:05):

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 (Oct 26 2021 at 14:21):

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

Riccardo Brasca (Oct 26 2021 at 14:29):

good point

Thomas Browning (Oct 26 2021 at 14:47):

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 (Oct 26 2021 at 14:49):

We get the extension generated by all roots of unity.

Thomas Browning (Oct 26 2021 at 14:49):

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

Riccardo Brasca (Oct 26 2021 at 14:50):

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

Riccardo Brasca (Oct 26 2021 at 15:03):

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 (Oct 26 2021 at 15:03):

But that doesn't matter right?

Johan Commelin (Oct 26 2021 at 15:04):

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

Thomas Browning (Oct 26 2021 at 15:04):

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 (Oct 26 2021 at 15:07):

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

Riccardo Brasca (Oct 26 2021 at 15:08):

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

Thomas Browning (Oct 26 2021 at 15:10):

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 Z^×\widehat{\mathbb{Z}}^\times. This would also give us the Zp\mathbb{Z}_p from Iwasawa theory.

Thomas Browning (Oct 26 2021 at 15:10):

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

Adam Topaz (Oct 26 2021 at 15:11):

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 Z^×\widehat{\mathbb{Z}}^\times. This would also give us the Zp\mathbb{Z}_p from Iwasawa theory.

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

Johan Commelin (Oct 26 2021 at 15:12):

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

Thomas Browning (Oct 26 2021 at 15:12):

Could you do both simultaneously with adjoin_root?

Adam Topaz (Oct 26 2021 at 15:12):

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

Thomas Browning (Oct 26 2021 at 15:13):

Adam Topaz said:

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

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 (Oct 26 2021 at 15:14):

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 (Oct 26 2021 at 15:14):

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

Riccardo Brasca (Oct 26 2021 at 15:15):

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 (Oct 26 2021 at 15:15):

No, we want all the roots

Thomas Browning (Oct 26 2021 at 15:16):

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

Thomas Browning (Oct 26 2021 at 15:16):

This might even generalize the splitting field construction

Johan Commelin (Oct 26 2021 at 15:19):

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

Riccardo Brasca (Oct 26 2021 at 15:19):

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 (Oct 26 2021 at 15:20):

Yes exactly, having the field we can work there

Riccardo Brasca (Oct 26 2021 at 15:20):

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

Riccardo Brasca (Oct 26 2021 at 16:09):

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 (Oct 26 2021 at 16:10):

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

Riccardo Brasca (Oct 26 2021 at 16:10):

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 (Oct 26 2021 at 16:14):

Awesome!

Chris Birkbeck (Oct 27 2021 at 08:34):

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 (Oct 27 2021 at 08:41):

It means there is a cycle of instances

Riccardo Brasca (Oct 27 2021 at 08:41):

Where is it?

Chris Birkbeck (Oct 27 2021 at 08:42):

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 (Oct 27 2021 at 08:43):

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

Riccardo Brasca (Oct 27 2021 at 08:43):

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 (Oct 27 2021 at 08:45):

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 (Oct 27 2021 at 08:45):

But no problem for your commit :)

Chris Birkbeck (Oct 27 2021 at 08:46):

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

Chris Birkbeck (Oct 27 2021 at 08:48):

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

Riccardo Brasca (Oct 27 2021 at 08:53):

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 (Oct 27 2021 at 08:57):

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 (Oct 27 2021 at 08:59):

There is no open here or am I blind?

Riccardo Brasca (Oct 27 2021 at 08:59):

But let me check the real error

Chris Birkbeck (Oct 27 2021 at 08:59):

Oh wait, maybe I pushed the wrong thing.

Chris Birkbeck (Oct 27 2021 at 09:01):

Yes I forgot to hit save before pushing, sorry!

Riccardo Brasca (Oct 27 2021 at 09:03):

I get an invalid namespace name 'new_cyclotomic_field' error.

Chris Birkbeck (Oct 27 2021 at 09:04):

Yeah, did you delete that namespace?

Riccardo Brasca (Oct 27 2021 at 09:05):

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

Chris Birkbeck (Oct 27 2021 at 09:06):

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

Chris Birkbeck (Oct 27 2021 at 09:07):

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

Riccardo Brasca (Oct 27 2021 at 09:08):

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 (Oct 27 2021 at 09:15):

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 (Oct 27 2021 at 09:26):

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 (Oct 27 2021 at 09:41):

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 (Oct 27 2021 at 09:44):

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 (Oct 27 2021 at 09:47):

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 (Oct 27 2021 at 09:48):

Oh, OK, I see

Riccardo Brasca (Oct 27 2021 at 09:48):

euclidean_domain does not need ring

Riccardo Brasca (Oct 27 2021 at 09:49):

Bu the other problem is still there

Alex J. Best (Oct 27 2021 at 09:49):

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

Chris Birkbeck (Oct 27 2021 at 10:31):

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 (Oct 27 2021 at 10:33):

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

Kevin Buzzard (Oct 27 2021 at 10:35):

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 (Oct 27 2021 at 10:36):

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 (Oct 27 2021 at 10:37):

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((x1,y1),(x2,y2)):=(d(x1,y1)2+d(x2,y2)2d((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 (Oct 27 2021 at 10:39):

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×VU\times V) whereas the topology coming from the metric has a basis which are "discs" (i.e. distance from a fixed point is <r<r).

Kevin Buzzard (Oct 27 2021 at 10:39):

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

Chris Birkbeck (Oct 27 2021 at 10:40):

Aha that makes perfect sense, thank you!

Kevin Buzzard (Oct 27 2021 at 10:40):

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 (Oct 27 2021 at 10:41):

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 (Oct 27 2021 at 10:41):

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 (Oct 27 2021 at 10:43):

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 (Oct 27 2021 at 10:44):

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

Chris Birkbeck (Oct 27 2021 at 10:48):

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

Johan Commelin (Oct 27 2021 at 10:52):

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 (Oct 27 2021 at 10:55):

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 (Oct 27 2021 at 10:57):

Credits to Julian Berman for writing it!

Kevin Buzzard (Oct 27 2021 at 11:10):

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 (Oct 27 2021 at 11:11):

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

Johan Commelin (Oct 27 2021 at 11:11):

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

Kevin Buzzard (Oct 27 2021 at 11:13):

Gotcha

Johan Commelin (Oct 27 2021 at 11:15):

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

Johan Commelin (Oct 27 2021 at 11:15):

Which contains your metric space example.

Riccardo Brasca (Oct 27 2021 at 11:25):

@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 (Oct 27 2021 at 11:37):

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 (Oct 27 2021 at 12:43):

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 (Oct 27 2021 at 12:46):

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

Riccardo Brasca (Oct 27 2021 at 12:57):

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 (Oct 27 2021 at 12:57):

I've unfolded the def by hand.

Riccardo Brasca (Oct 27 2021 at 12:59):

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 (Oct 27 2021 at 12:59):

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

Riccardo Brasca (Oct 27 2021 at 13:08):

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 (Oct 27 2021 at 13:20):

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 (Oct 27 2021 at 13:33):

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 (Oct 27 2021 at 13:34):

It has to be a lemma, not an instance.

Riccardo Brasca (Oct 27 2021 at 13:34):

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

Chris Birkbeck (Oct 27 2021 at 13:35):

Riccardo Brasca said:

It has to be a lemma, not an instance.

Ahh ok.

Chris Birkbeck (Oct 27 2021 at 13:35):

Riccardo Brasca said:

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

Oh no

Riccardo Brasca (Oct 27 2021 at 13:37):

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 (Oct 27 2021 at 13:37):

(deleted)

Riccardo Brasca (Oct 27 2021 at 13:38):

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

Riccardo Brasca (Oct 27 2021 at 13:39):

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 (Oct 27 2021 at 13:40):

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

Riccardo Brasca (Oct 27 2021 at 13:42):

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

Riccardo Brasca (Oct 27 2021 at 14:28):

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 (Oct 27 2021 at 14:29):

@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 (Oct 27 2021 at 14:30):

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

Marc Masdeu (Oct 27 2021 at 14:40):

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 (Oct 27 2021 at 15:28):

yeah I didn't click through :-)

Kevin Buzzard (Oct 27 2021 at 15:31):

The diamond error is that Lean is failing to solve

smul_with_zero.to_has_scalar = sub_neg_monoid.has_scalar_int

Riccardo Brasca (Oct 27 2021 at 15:36):

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

Kevin Buzzard (Oct 27 2021 at 15:37):

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 (Oct 27 2021 at 15:38):

I'm still thinking about it

Kevin Buzzard (Oct 27 2021 at 15:38):

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 (Oct 27 2021 at 15:39):

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

Kevin Buzzard (Oct 27 2021 at 15:41):

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

Kevin Buzzard (Oct 27 2021 at 15:42):

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 (Oct 27 2021 at 15:43):

The two goals are OK

Kevin Buzzard (Oct 27 2021 at 15:43):

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

Kevin Buzzard (Oct 27 2021 at 15:43):

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

Riccardo Brasca (Oct 27 2021 at 15:45):

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 (Oct 27 2021 at 15:46):

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 (Oct 27 2021 at 15:48):

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

Johan Commelin (Oct 27 2021 at 15:48):

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 (Oct 27 2021 at 15:49):

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 (Oct 27 2021 at 15:52):

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 (Oct 27 2021 at 15:53):

The definition of cyclotomic_field n K is

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

Kevin Buzzard (Oct 27 2021 at 15:54):

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 (Oct 27 2021 at 15:54):

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

Riccardo Brasca (Oct 27 2021 at 15:57):

@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 (Oct 27 2021 at 16:16):

The bad instance is coming from algebra.to_has_scalar

Riccardo Brasca (Oct 27 2021 at 16:22):

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

Riccardo Brasca (Oct 27 2021 at 16:22):

Let me check where it comes from.

Chris Birkbeck (Oct 27 2021 at 16:23):

Does it come from cyclotomic_field_algebra?

Kevin Buzzard (Oct 27 2021 at 16:24):

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

Riccardo Brasca (Oct 27 2021 at 16:25):

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 (Oct 27 2021 at 16:27):

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

Riccardo Brasca (Oct 27 2021 at 16:34):

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 (Oct 27 2021 at 16:35):

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

Kevin Buzzard (Oct 27 2021 at 16:36):

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 (Oct 27 2021 at 16:37):

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

Kevin Buzzard (Oct 27 2021 at 16:38):

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 (Oct 27 2021 at 16:39):

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

Chris Birkbeck (Oct 27 2021 at 16:39):

Yeah it must be because its defined as a composition

Riccardo Brasca (Oct 27 2021 at 16:39):

Oh gosh, thank you

Chris Birkbeck (Oct 27 2021 at 16:40):

or not, I dont know

Riccardo Brasca (Oct 27 2021 at 16:41):

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

Riccardo Brasca (Oct 27 2021 at 16:41):

Let me see if I have enough time

Kevin Buzzard (Oct 27 2021 at 16:45):

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 (Oct 27 2021 at 16:47):

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

Johan Commelin (Oct 27 2021 at 16:48):

Lean cannot guess which K it should be looking for.

Adam Topaz (Oct 27 2021 at 16:48):

I thought that was the whole point of scalar towers?

Kevin Buzzard (Oct 27 2021 at 16:48):

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 (Oct 27 2021 at 16:52):

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 (Oct 27 2021 at 16:52):

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

Johan Commelin (Oct 27 2021 at 16:53):

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 (Oct 27 2021 at 16:53):

maybe algebra_int shouldn't be an instance?

Kevin Buzzard (Oct 27 2021 at 16:53):

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 (Oct 27 2021 at 16:54):

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

Adam Topaz (Oct 27 2021 at 16:55):

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

Kevin Buzzard (Oct 27 2021 at 16:56):

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

Johan Commelin (Oct 27 2021 at 16:56):

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 (Oct 27 2021 at 16:57):

sigh

Riccardo Brasca (Oct 27 2021 at 17:06):

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

Johan Commelin (Oct 27 2021 at 17:09):

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 (Oct 27 2021 at 17:09):

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

Kevin Buzzard (Oct 27 2021 at 17:10):

i.e. none of them are instances

Johan Commelin (Oct 27 2021 at 17:10):

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 (Oct 27 2021 at 17:11):

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

Johan Commelin (Oct 27 2021 at 17:16):

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 (Oct 27 2021 at 17:16):

I should clone the repo.

Chris Birkbeck (Oct 27 2021 at 17:17):

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

Riccardo Brasca (Oct 27 2021 at 17:17):

K is the fraction field

Johan Commelin (Oct 27 2021 at 17:34):

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 (Oct 27 2021 at 17:34):

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

Riccardo Brasca (Oct 27 2021 at 17:35):

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

Johan Commelin (Oct 27 2021 at 17:35):

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

Riccardo Brasca (Oct 27 2021 at 17:36):

The definition is much more general than what we need

Johan Commelin (Oct 27 2021 at 17:37):

Right, that's what I suspected.

Eric Wieser (Oct 27 2021 at 21:15):

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

Kevin Buzzard (Oct 27 2021 at 21:16):

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 (Oct 27 2021 at 21:17):

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

Riccardo Brasca (Oct 27 2021 at 21:46):

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

Eric Wieser (Oct 27 2021 at 22:04):

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 (Oct 27 2021 at 22:07):

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

Kevin Buzzard (Oct 27 2021 at 22:09):

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

Eric Wieser (Oct 27 2021 at 22:21):

It fixes one of the two diamonds

Eric Wieser (Oct 27 2021 at 22:22):

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

Eric Wieser (Oct 27 2021 at 22:46):

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

Eric Wieser (Oct 27 2021 at 23:48):

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 (Oct 28 2021 at 08:07):

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 (Oct 28 2021 at 08:08):

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 (Oct 28 2021 at 08:26):

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

Riccardo Brasca (Oct 28 2021 at 08:26):

Thanks to everybody!

Riccardo Brasca (Oct 28 2021 at 08:53):

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

Eric Wieser (Oct 28 2021 at 11:10):

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

Riccardo Brasca (Oct 28 2021 at 11:31):

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

Riccardo Brasca (Oct 28 2021 at 11:32):

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

Eric Wieser (Oct 28 2021 at 12:09):

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 (Oct 28 2021 at 12:10):

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

Eric Wieser (Oct 28 2021 at 12:28):

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 (Oct 28 2021 at 18:46):

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 (Oct 28 2021 at 19:02):

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

Chris Birkbeck (Oct 28 2021 at 19:52):

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

Chris Birkbeck (Oct 28 2021 at 19:53):

Thank you!

Riccardo Brasca (Oct 28 2021 at 19:59):

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

Chris Birkbeck (Oct 28 2021 at 20:03):

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

Eric Rodriguez (Nov 10 2021 at 01:52):

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 (Nov 10 2021 at 20:15):

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 (Nov 10 2021 at 20:30):

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 (Nov 10 2021 at 20:48):

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 (Nov 10 2021 at 20:54):

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

Riccardo Brasca (Nov 10 2021 at 20:57):

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

Riccardo Brasca (Nov 10 2021 at 20:58):

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

Riccardo Brasca (Nov 10 2021 at 21:02):

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

Riccardo Brasca (Nov 10 2021 at 21:04):

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

Eric Rodriguez (Nov 10 2021 at 21:06):

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 (Nov 10 2021 at 21:07):

(also #9779 ever relevant...)

Riccardo Brasca (Nov 10 2021 at 21:08):

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 (Nov 10 2021 at 21:10):

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

Riccardo Brasca (Nov 10 2021 at 21:11):

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

Riccardo Brasca (Nov 10 2021 at 21:15):

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

Riccardo Brasca (Nov 12 2021 at 09:18):

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

Riccardo Brasca (Nov 12 2021 at 09:19):

I see you did :)

Eric Rodriguez (Nov 12 2021 at 11:18):

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 (Nov 12 2021 at 11:25):

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

Eric Rodriguez (Nov 12 2021 at 11:39):

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

Eric Rodriguez (Nov 12 2021 at 11:40):

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 (Nov 12 2021 at 11:44):

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

Riccardo Brasca (Nov 12 2021 at 11:44):

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

Riccardo Brasca (Nov 12 2021 at 11:50):

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

Eric Rodriguez (Nov 12 2021 at 11:51):

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 (Nov 12 2021 at 11:51):

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

Riccardo Brasca (Nov 12 2021 at 11:56):

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

Riccardo Brasca (Nov 12 2021 at 11:57):

So we really need fields

Riccardo Brasca (Nov 12 2021 at 11:59):

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 (Nov 14 2021 at 15:52):

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 (Nov 14 2021 at 15:53):

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

Riccardo Brasca (Nov 14 2021 at 19:05):

Oh, and I even wrote that proof!

Eric Rodriguez (Nov 15 2021 at 00:37):

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 (Nov 15 2021 at 09:14):

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 (Nov 15 2021 at 09:30):

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

Eric Rodriguez (Nov 15 2021 at 19:00):

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 (Nov 17 2021 at 14:46):

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 (Nov 17 2021 at 22:08):

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 (Nov 19 2021 at 00:33):

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 (Nov 19 2021 at 00:34):

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 (Nov 19 2021 at 08:23):

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

Eric Rodriguez (Nov 19 2021 at 09:51):

What do you think of the fact idea?

Kevin Buzzard (Nov 19 2021 at 09:59):

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 (Nov 19 2021 at 10:04):

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

Johan Commelin (Nov 19 2021 at 10:04):

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

Johan Commelin (Nov 19 2021 at 10:05):

What exactly are the problems that Ashvni is hitting?

Riccardo Brasca (Nov 19 2021 at 10:35):

@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 (Nov 19 2021 at 10:37):

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 (Nov 19 2021 at 13:17):

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 (Nov 19 2021 at 13:19):

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 (Nov 19 2021 at 13:26):

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 (Nov 19 2021 at 13:27):

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 (Nov 19 2021 at 13:28):

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 (Nov 19 2021 at 13:29):

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 (Nov 19 2021 at 13:29):

Or fix library_search :rofl:

Alex J. Best (Nov 19 2021 at 13:32):

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

Alex J. Best (Nov 19 2021 at 13:33):

Like assumption for instance

Johan Commelin (Nov 19 2021 at 13:36):

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

Johan Commelin (Nov 19 2021 at 13:36):

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

Alex J. Best (Nov 19 2021 at 13:37):

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 (Nov 19 2021 at 13:37):

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

Riccardo Brasca (Nov 20 2021 at 09:10):

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 (Nov 20 2021 at 18:00):

this is such a pesky goal...

Riccardo Brasca (Nov 20 2021 at 19:21):

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

Yakov Pechersky (Nov 20 2021 at 23:33):

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

Riccardo Brasca (Nov 21 2021 at 00:55):

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

Riccardo Brasca (Dec 01 2021 at 15:42):

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 (Dec 01 2021 at 15:43):

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 (Dec 01 2021 at 15:43):

Sorry!

Riccardo Brasca (Dec 01 2021 at 15:46):

No problem!

Eric Rodriguez (Dec 01 2021 at 15:49):

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 (Dec 02 2021 at 15:55):

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 (Dec 02 2021 at 19:24):

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

Eric Rodriguez (Dec 09 2021 at 02:22):

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 (Dec 09 2021 at 09:43):

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 (Dec 13 2021 at 00:11):

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

Alex J. Best (Dec 13 2021 at 00:25):

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 (Dec 13 2021 at 00:25):

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

Eric Rodriguez (Dec 13 2021 at 00:37):

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 (Dec 13 2021 at 07:54):

Which result are you talking about?

Riccardo Brasca (Dec 13 2021 at 07:55):

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

Eric Rodriguez (Dec 13 2021 at 10:13):

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

Riccardo Brasca (Dec 13 2021 at 11:07):

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 (Dec 16 2021 at 15:43):

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 (Dec 16 2021 at 19:19):

#10849

Eric Rodriguez (Dec 21 2021 at 05:48):

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 (Dec 21 2021 at 08:43):

Having a look now

Riccardo Brasca (Dec 21 2021 at 09:56):

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

Riccardo Brasca (Dec 21 2021 at 09:58):

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 (Dec 21 2021 at 09:58):

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

Riccardo Brasca (Dec 21 2021 at 09:58):

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

Riccardo Brasca (Dec 21 2021 at 12:52):

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

Riccardo Brasca (Dec 21 2021 at 13:37):

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 (Dec 21 2021 at 13:40):

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

Riccardo Brasca (Dec 21 2021 at 15:20):

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

Riccardo Brasca (Dec 21 2021 at 15:21):

It seems the only nontrivial statement for is_fraction_ring...

Riccardo Brasca (Dec 21 2021 at 15:21):

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

Eric Rodriguez (Dec 21 2021 at 15:24):

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 (Dec 21 2021 at 15:25):

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

Riccardo Brasca (Dec 21 2021 at 15:36):

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 (Dec 21 2021 at 15:37):

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

Eric Rodriguez (Dec 21 2021 at 15:45):

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 (Dec 21 2021 at 15:46):

What's the cyclotomic power thing?

Eric Rodriguez (Dec 21 2021 at 15:51):

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

Riccardo Brasca (Dec 21 2021 at 15:51):

Nonsense

Riccardo Brasca (Dec 21 2021 at 15:54):

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

Alex J. Best (Dec 21 2021 at 15:56):

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

Riccardo Brasca (Dec 21 2021 at 16:01):

In any case we don't need it

Alex J. Best (Dec 21 2021 at 16:03):

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

Riccardo Brasca (Dec 21 2021 at 16:08):

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 (Dec 21 2021 at 17:40):

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

Riccardo Brasca (Dec 21 2021 at 17:42):

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 (Jan 05 2022 at 16:32):

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

Eric Rodriguez (Feb 01 2022 at 00:56):

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


Last updated: Dec 20 2023 at 11:08 UTC