# 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_field`

is a better option. I think the second option is better suited to Galois theory (as then the `.gal`

has 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 $\mathbb{Q}(\zeta_n)/\mathbb{Q}$ is $(\mathbb{Z}/n\mathbb{Z})^\times$" should be phrased in terms of `E ≃ₐ[F] E`

, rather than `(X ^ n - 1).gal`

.

#### Eric Rodriguez (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 $L|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 $K$ of characteristic $p$ is $K$ 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 `enat`

for 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(\mu_5)$, I can consider all powers of 5 to consider $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 $0$-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 $\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 $ℚ(ζ_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 $\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 $\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 $\widehat{\mathbb{Z}}^\times$. This would also give us the $\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 $\widehat{\mathbb{Z}}^\times$. This would also give us the $\mathbb{Z}_p$ from Iwasawa theory.

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

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

@Riccardo Brasca Right, so you will need an instance for $ℚ(ζ_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 $n$, should we prove a cyclotomic instance for $S = \{n\}$ or for $S$ the divisors of $n$?

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

Adam Topaz said:

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

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

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

#### Kevin Buzzard (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 $\mathbb{Z}\times G\to G$ and a proof that this map sends $(n,g)$ to $g^n$, and this random extra field is there for the same sort of reason.

#### Chris Birkbeck (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$-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 want`algebra 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 $n \neq 0$ in the base ring.

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

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

#### Riccardo Brasca (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 $X^n-1 = \Psi_n \prod_{i | n, i < n}\Psi_i$, and $X^m-1$ appears in the second product.

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

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

#### Eric Rodriguez (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_ring`

s, 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 `fact`

s 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):

#### 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_field`

is a better option. I think the second option is better suited to Galois theory (as then the `.gal`

has 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 $\mathbb{Q}(\zeta_n)/\mathbb{Q}$ is $(\mathbb{Z}/n\mathbb{Z})^\times$" should be phrased in terms of `E ≃ₐ[F] E`

, rather than `(X ^ n - 1).gal`

.

#### Eric Rodriguez (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 $L|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 $K$ of characteristic $p$ is $K$ 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 `enat`

for 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(\mu_5)$, I can consider all powers of 5 to consider $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 $0$-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:

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 $\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 $ℚ(ζ_p)$.

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

Riccardo Brasca said:

`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 $\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 $\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 $\widehat{\mathbb{Z}}^\times$. This would also give us the $\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:

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 $ℚ(ζ_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 $n$, should we prove a cyclotomic instance for $S = \{n\}$ or for $S$ the divisors of $n$?

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

Adam Topaz said:

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:

`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):

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

#### Kevin Buzzard (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 $\mathbb{Z}\times G\to G$ and a proof that this map sends $(n,g)$ to $g^n$, and this random extra field is there for the same sort of reason.

#### Chris Birkbeck (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:

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:

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):

#### 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 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:

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$-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 want`algebra 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:

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 $n \neq 0$ in the base ring.

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

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

#### Riccardo Brasca (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 $X^n-1 = \Psi_n \prod_{i | n, i < n}\Psi_i$, and $X^m-1$ appears in the second product.

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

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

#### Eric Rodriguez (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_ring`

s, 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~~LTE. @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 `fact`

s 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):

#### 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