# Zulip Chat Archive

## Stream: FLT-regular

### Topic: Discriminant

#### Riccardo Brasca (Oct 30 2021 at 21:01):

I was having a look at `ring_theory.trace`

, where docs#algebra.trace_form is defined. We already have *a lot* of results, even about the relation with embeddings and so on. I am confident we can set up a good API for the discriminant quite quickly.

I think we only need the following results: let $L/K$ be a separable extension of fields with $\dim_K(L) = n$ and let $b = (b_1,\ldots, b_n)$ a family of elements of $L$. Let $\Delta = \mathrm{disc}_{L/K}(b)$.

- $\Delta \neq 0$ if and only if $b$ is a basis of $L$ over $K$.
- If $P$ is matrix with coefficients in $K$, then $\mathrm{disc}_{L/K}(P \cdot b) = \det(P)^2 \Delta$.
- $\Delta = \det(\sigma_i(b_j))$, where the $\sigma_i$ are the $K$-embeddings of $L$ in an algebraic closure of $L$.

*If $L = K(x)$ and $x_i$ are the conjugates of $x$ in an algebraic closure, then $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2 = (-1)^{\frac{n(n-1)}{2}} \mathrm{Norm}_{L/K}(\mathrm{\chi_x(x)}')$, where $\chi_x$ is the minimal polynomial of $x$.

I don't see any real problem in getting these results. The last one is probably the longest, but it seems very doable.

#### Kevin Buzzard (Oct 30 2021 at 22:39):

Instead of an algebraic closure of L you could use any field which contains a normal closure of L over K. I mention this because the complexes are not an algebraic closure of L, they're too big

#### Riccardo Brasca (Oct 30 2021 at 22:54):

Yes sure, mathlib results are for any algebraically closed field that contains `L`

. I don't know if we already have the normal closure

#### Chris Birkbeck (Oct 31 2021 at 12:09):

Oh I didn't know we had so much already about trace and their link to embeddings. I'll try and breakup the blueprint tomorrow to map out the results we'll need. Hopefully it'll be easy to create a bunch of sorried lemmas for this.

#### Riccardo Brasca (Nov 01 2021 at 11:14):

I will work on this today, hopefully writing all the relevant lemmas (sorried).

#### Chris Birkbeck (Nov 01 2021 at 11:20):

Ok cool. I'm just updating the blueprint with some of the missing lemmas.

#### Riccardo Brasca (Nov 01 2021 at 13:47):

I've written all the properties except $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2$, that requires a little work to be stated (since the embeddings are not naturally ordered), but I am not even sure we need it.

#### Riccardo Brasca (Nov 01 2021 at 13:47):

I have to stop now, but I will start proving things this evening.

#### Chris Birkbeck (Nov 01 2021 at 13:52):

I used this lemma to prove the link between discriminant and norm of the min. pol. But maybe there are ways to get around this?

#### Kevin Buzzard (Nov 01 2021 at 13:54):

That product is a little subtle I guess! IIRC one can use that result to prove that the integers of Q(zeta_p) are Z(zeta_p) because the discriminant of the powers of p is +-p^(p-2) by a valuation argument and this isn't divisible by the p-1st power of any prime. But maybe there's also a way of arguing directly from the definition

#### Kevin Buzzard (Nov 01 2021 at 13:55):

There's a `sym2`

which you could use but I'm wondering whether it would be more trouble than it's worth and one should just order the embeddings

#### Alex J. Best (Nov 01 2021 at 13:58):

Riccardo Brasca said:

I've written all the properties except $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2$, that requires a little work to be stated (since the embeddings are not naturally ordered), but I am not even sure we need it.

we could state

$\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2 = (-1)^{[L:K]([L:K] - 1)/2}\prod_{i \ne j} (x_i - x_j)$

(up to a sign or something) instead right? Where now the right hand side doesn't need an order?

#### Alex J. Best (Nov 01 2021 at 14:00):

I guess this is the sym2 suggestion of Kevin's too?

#### Riccardo Brasca (Nov 01 2021 at 14:03):

That's probably better

#### Kevin Buzzard (Nov 01 2021 at 14:07):

sym2 is unordered pairs so then one would have to somehow insert the proof that $(x-y)^2=(y-x)^2$ -- I think Alex's suggestion is better because it avoids this issue.

#### Kevin Buzzard (Nov 01 2021 at 14:07):

The product over $i\not=j$ is just a finprod or docs#finset.prod depending on what mood you're in (the set/finset is much easier to make)

#### Chris Birkbeck (Nov 01 2021 at 14:43):

Riccardo Brasca said:

I've written all the properties except $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2$, that requires a little work to be stated (since the embeddings are not naturally ordered), but I am not even sure we need it.

So I pulled these changes and now I'm stuck in orange bar hell and `leanproject get-cache`

isn't working. Any ideas on how to fix this?

#### Kevin Buzzard (Nov 01 2021 at 14:43):

You want `leanproject get-mathlib-cache`

#### Kevin Buzzard (Nov 01 2021 at 14:45):

If you're working on a project with mathlib as a dependency then the workflow is slightly different. Working on a branch of mathlib it's `get-cache`

. For a project which depends on mathlib you use `get-mathlib-cache`

and then compile your project yourself with `leanproject build`

unless you've set up your own continuous integration, in which case `get-cache`

might work.

#### Chris Birkbeck (Nov 01 2021 at 14:47):

Ah `leanproject build`

! I had tried `leanproject get-mathlib-cache`

and it hadn't worked, but it was because I hadn't built it I guess.

#### Chris Birkbeck (Nov 01 2021 at 14:48):

Its working now, thanks :)

#### Kevin Buzzard (Nov 01 2021 at 14:48):

Basically I know a bunch of these commands and I fiddle around on the command line until `lean --make src/<path_to_file_I'm_working_on>`

works, then I restart VS Code

#### Kevin Buzzard (Nov 01 2021 at 14:49):

if it doesn't work then on linux it starts printing out the name of the file it's compiling, and if it's something else in my project then I know that mathlib is OK but my project isn't compiled, and if it's `_target/deps/mathlib/src/tactic/rcases.lean`

or whatever then I know I've screwed up my mathlib oleans

#### Chris Birkbeck (Nov 01 2021 at 14:53):

Kevin Buzzard said:

Basically I know a bunch of these commands and I fiddle around on the command line until

`lean --make src/<path_to_file_I'm_working_on>`

works, then I restart VS Code

That's a good strategy, I'll try that next time :) (also I found out that in windows, you can also see the printout of the files its working on if you use the terminal inside VScode, but not if you use the `Git Bash`

terminal)

#### Kevin Buzzard (Nov 01 2021 at 14:55):

The trap you can fall into with throwing random `leanproject`

commands around, when working on a project with mathlib as a dependency, is that `leanproject build`

builds the current versions of the project lean files, but `leanproject up`

will IIRC first update mathlib to current `master`

and then build, and of course bumping mathlib might break the project in interesting ways, so should be done on some branch of your project other than `master`

.

#### Yaël Dillies (Nov 01 2021 at 15:45):

Bhavik and I wanted to have a sum running over `sym2`

of something and it turns out to be a pain, because

- Every time you want to move terms, you need to show that this move respects symmetry.
- Your terms have to be intrinsically symmetric. So here you can't refer to $(x_1 - x_j)^2$. You instead have to resort to an intermediary definition
`term (xy : sym2 something) : something_else := sym2.lift ⟨(xy.out.1 - xy.out.2)^2, a_proof⟩`

. - The
`sym2`

API is weak.

#### Yaël Dillies (Nov 01 2021 at 15:46):

I strongly advise you to square your sum and forget about `sym2`

. And that's what Bhavik and I did: double the sum and go on with our lives.

#### Yaël Dillies (Nov 01 2021 at 15:47):

Although here I understand that squaring might be undesirable. In our case, doubling was injective.

#### Riccardo Brasca (Nov 01 2021 at 15:48):

Something like

```
lemma of_power_basis_eq_prod : algebra_map K E (discriminant K pb.basis) ^ 2 =
((univ.product univ).filter (λ (σ : (L →ₐ[K] E) × (L →ₐ[K] E)), σ.1 ≠ σ.2)).prod
(λ σ, (σ.1 pb.gen - σ.2 pb.gen) ^ 2) := sorry
```

works. Here `E`

is algebraically closed (it is enough that splits the minimal polynomial of `pb.gen`

, the first element of a power basis `pb`

).

#### Riccardo Brasca (Nov 01 2021 at 15:49):

We can also have the similar statement using the `finset`

of roots of the minimal polynomial.

#### Yaël Dillies (Nov 01 2021 at 15:50):

(you'll be happy to hear that `univ.product univ = univ`

:wink:)

#### Riccardo Brasca (Nov 01 2021 at 15:51):

Ah yes, and I am pretty sure that `diagonal`

exists, so that is just the complement of the diagonal

#### Yaël Dillies (Nov 01 2021 at 15:51):

Yeah exactly. You can use `univ.off_diag`

(docs#finset.off_diag) here.

#### Riccardo Brasca (Nov 01 2021 at 15:52):

Ah nice, I didn't spot it

#### Yaël Dillies (Nov 01 2021 at 15:52):

Damn, I really became that finset person.

#### Kevin Buzzard (Nov 01 2021 at 15:53):

`diag_empty`

was only added to mathlib 17 hours ago!

#### Riccardo Brasca (Nov 01 2021 at 15:56):

A little golf

```
lemma of_power_basis_eq_prod : algebra_map K E (discriminant K pb.basis) ^ 2 =
(univ : finset ((L →ₐ[K] E) × (L →ₐ[K] E))).off_diag.prod
(λ σ, (σ.1.1 pb.gen - σ.1.2 pb.gen) ^ 2) := sorry
```

I don't like `σ.1.1`

, but that's OK

#### Riccardo Brasca (Nov 01 2021 at 21:45):

I proved that a linear dependent family has zero discriminant. It's an easy result, but the fact that the Lean proof is short is a good indication we are able to work with the trace.

#### Riccardo Brasca (Nov 01 2021 at 22:10):

And we have docs#matrix.det_vandermonde! So it's maybe a good idea to order the embeddings (keeping the more intrinsic statement).

#### Chris Birkbeck (Nov 02 2021 at 10:03):

That's good news! If picking an order makes things easier then I have no problem with that.

#### Riccardo Brasca (Nov 02 2021 at 17:51):

- $\Delta \neq 0$ if and only if $b$ is a basis of $L$ over $K$.
- If $P$ is matrix with coefficients in $K$, then $\mathrm{disc}_{L/K}(P \cdot b) = \det(P)^2 \Delta$.

Are proved.

#### Chris Birkbeck (Nov 02 2021 at 17:52):

Great!

#### Riccardo Brasca (Nov 03 2021 at 11:30):

I've started writing down the proof that $\Delta = \det(\sigma_i(b_j))^2$. I don't see any real problem, and that's good. But I think we can't avoid some sort of order on the embeddings: if `b : ι → L`

is a family of elements of `L`

, then `λ (i : ι) (σ : L →ₐ[K] E), σ ( b i)`

gives a matrix `M : matrix ι (L →ₐ[K] E) E`

. There is no way to make `M`

a square matrix: even if `E`

is algebraically closed and `fintype.card ι = finrank K L`

, we only get an equiv `ι ≃ L →ₐ[K] E`

, so we need to apply some `reindex`

. The only possibility is to literally take `ι = L →ₐ[K] E`

, but this is too restrictive.

The most flexible way of stating the results is, I think, to have it taking an equiv `ι ≃ L →ₐ[K] E`

as input. Any better idea?

#### Eric Rodriguez (Nov 03 2021 at 11:37):

Maybe the 'correct' thing to do is generalise det to `matrix m n R`

and return junk if they are not the same cardinality, but that seems like a huuuge refactor

#### Alex J. Best (Nov 03 2021 at 11:45):

I like the sound of that, would it really be such a big refactor? If all the results about det are about `det`

of a `matrix n n`

then apart from the very basic API it might not need that much work

#### Riccardo Brasca (Nov 03 2021 at 11:51):

But then if one wants the determinant of `M matrix n n R`

will have to write the `n`

and `n`

have the same cardinality (trivial, but you'll write it everywhere). And having the same cardinality breaks computability I think, since the construction of the bijection is not computable. `det`

can take the equiv as input, but essentially this means using `reindex`

, and that is already there.

#### Riccardo Brasca (Nov 03 2021 at 11:54):

I mean, unless we really change the definition, having the determinant of a matrix indexed by types with the same cardinality boils down to take the determinant of the reindexed matrix, that is really square.

#### Alex J. Best (Nov 03 2021 at 12:05):

Well you could add a default argument / tactic I believe

#### Alex J. Best (Nov 03 2021 at 12:09):

The reason this sounded nice to me was the other way of defining discriminants is to take the determinant of the Sylvester matrix, this matrix is most naturally the result of stacking two rectangular matrices on top of each other, so you can define it on fin n x fin n with an if, but the most aesthetically pleasing way you would need a definition of det that works if the indexing types have the same card but doesn't require the types to be syntactically equal

#### Riccardo Brasca (Nov 03 2021 at 12:21):

I am not experienced enough to have a strong opinion, but my impression is that the determinant is defined for square-in-mathlib-sense matrices. Even in real world mathematics. What we usually do is that we only consider matrices of type `matrix (fin n) (fin m) R`

and we constantly choose bijections of some set of indexes with `fin n`

, reindex the matrix, and take the determinant.

I think that, working in Lean, we really do what we have to do, but usually we don't say it and of course we don't write it. Having the determinant of `M : matrix n m R`

will make things more similar to what we do on paper, but here we are really cheating when doing unformal mathematics, and usually Lean punishes us if we try to do similar stuff.

#### Riccardo Brasca (Nov 03 2021 at 12:23):

I can be very wrong of course, but I am sure that one should ask the community before starting such a refactor.

#### Yakov Pechersky (Nov 03 2021 at 12:25):

Sorry, I don't have the full context here, but a couple of questions. Is it that you truly have a square matrix, but the types are different yet with same cardinality? Or is it that you have a rectangular matrix?

#### Yakov Pechersky (Nov 03 2021 at 12:25):

#### Yakov Pechersky (Nov 03 2021 at 12:28):

Could you use that, after composing some "reindexing" maps?

#### Riccardo Brasca (Nov 03 2021 at 12:28):

It's a square matrix in the sense that the two types have the same cardinality. docs#linear_map.det has the same problem, the associated linear map is between two vector spaces of the same dimension.

#### Riccardo Brasca (Nov 03 2021 at 12:28):

Yes, using `reindex`

is what I am proposing.

#### Yakov Pechersky (Nov 03 2021 at 12:31):

For a refactor, I'd first make a new det definition for matrices or linear maps, one that is over a single arbitrary fintype, that takes an order_iso to a fin n. If that one works, two ways of extending it. First, prove that the choice of order_iso doesn't matter, which let's you use the trunc.out one. Then, extend to two fintypes with the order_iso to the same fin n.

#### Yakov Pechersky (Nov 03 2021 at 12:33):

The "take a reindexing function as part of the definition" is similar to how we define sums, prods, infs, and sups over finsets.

#### Riccardo Brasca (Nov 03 2021 at 13:57):

`discriminant.eq_det_embeddings_matrix_reindex_pow_two`

is proved. Everything went really smoothly even with `reindex`

:)

#### Alex J. Best (Nov 03 2021 at 14:00):

Well for this specific det^2 function the indexing order choice shouldn't matter right? Even if you use a different order on each side the det only changes sign, so this function is somehow even more canonical than the usual det

#### Riccardo Brasca (Nov 03 2021 at 14:14):

This is already stated taking an arbitrary equiv as input, but yes, changing the equiv permutes the rows (or the columns, no idea) of the matrix of the embeddings. The proof uses that the matrix of the traces is the matrix of the embeddings multiplied by its transpose, so if one determinant changes sign also the other does.

#### Riccardo Brasca (Nov 03 2021 at 14:50):

And this gives me the impression that refactoring the determinant is not possible: the new determinant would be defined only up to a sign, right?

#### Kevin Buzzard (Nov 03 2021 at 21:24):

Alex is observing that if `M : matrix i j R`

and we choose a bijection i -> j then the sign of det(M) depends on the bijection (up to a sign) but det(M)^2 is independent of the choice of bijection.

#### Riccardo Brasca (Nov 03 2021 at 21:51):

Yes, this is what I am also saying, the determinant wouldn't be well defined. In our case we are only interested in the square, so no problem, but I don't think a general refactor of `det`

is doable. And moreover in another thread people started proposing *a different* refactor of `det`

motivated by a completely unrelated problem :rolling_on_the_floor_laughing:

These guys like refactoring

#### Yaël Dillies (Nov 03 2021 at 21:52):

Did you say refactor? :smirk:

#### Riccardo Brasca (Nov 03 2021 at 21:53):

In any case $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2$ is proved. The statement is

```
lemma of_power_basis_eq_prod (pb : power_basis K L) (e : fin pb.dim ≃ (L →ₐ[K] E)) :
algebra_map K E (discriminant K pb.basis) =
∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j), (e j pb.gen- (e i pb.gen)) ^ 2 :=
```

#### Riccardo Brasca (Nov 03 2021 at 22:05):

Now the only basic fact that is missing a proof is $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = (-1)^{\frac{n(n-1)}{2}} \mathrm{Norm}_{L/K}(\chi_x'(x))$, where $\chi_x$ is the minimal polynomial of $x$. I have to think a little bit for this one.

#### Kevin Buzzard (Nov 03 2021 at 22:24):

this doesn't quite look right -- the degree of the min poly will depend on x. Do you mean the char poly or something? Example: x=1. The disc is 0 if L != K, but the norm is 1.

#### Riccardo Brasca (Nov 03 2021 at 22:26):

I mean with the assumption that $L = K(x)$.

#### Kevin Buzzard (Nov 03 2021 at 22:26):

in that case the min poly is the char poly

#### Kevin Buzzard (Nov 03 2021 at 22:27):

If that assumption is false then the char poly has repeated roots and the powers won't span so both sides will be 0

#### Riccardo Brasca (Nov 03 2021 at 22:29):

Currently I am working with that assumption, if it helps. For cyclotomic fields in practice it is always satisfied (for the elements we want to consider). We will see if we need anything more general.

#### Riccardo Brasca (Nov 03 2021 at 22:30):

Looking at the blueprint, in the section about the discriminant, I think lemma 2.12 is going to be a pain.

#### Alex J. Best (Nov 03 2021 at 22:48):

Is it used other than for showing the ring of integers of Q(zeta) is Z[zeta]?

#### Chris Birkbeck (Nov 03 2021 at 22:49):

~~yes, its used in the proof I wrote down, but there could be other proofs that dont use it. Or maybe ways around it, but I've not thought about it.~~

#### Chris Birkbeck (Nov 03 2021 at 22:53):

Oh sorry, I misread your message. Not for what we need (I don't think)

#### Chris Birkbeck (Nov 03 2021 at 22:54):

But its handy for finding integral bases in general and for example tells you in the disc of a set of alg. ints. is square-free then you have an integral basis.

#### Riccardo Brasca (Nov 03 2021 at 22:55):

It's the key point in the proof, so we will have to get our hands dirty at some point, but it deserves some thought if we want to suffer as less as possible

#### Alex J. Best (Nov 03 2021 at 23:20):

I was looking at the proof in Neukirch (lemma I 10.2) the other day with Sander and it doesn't seem to use exactly the same lemma, though certainly it uses some related results in Chapter I 2.9. It might be better to prove some things using that route instead?

#### Chris Birkbeck (Nov 03 2021 at 23:30):

Oh maybe. I don't have my copy of Neukirch at home, but Ill have a look tomorrow. But if it's easier then we should do that :)

#### Alex J. Best (Nov 03 2021 at 23:47):

I can't tell if its easier yet to be honest! Just an alternative seeming approach

#### Chris Birkbeck (Nov 04 2021 at 09:23):

So I just had a look at Pierre Samuels "algebraic theory of numbers", in it (in chapter 2.9) there is a proof of what the ring of integers is in the cyclotomic cases, which just uses properties or the trace function. It wouldn't work more generally, but I would be a way to avoid this annoying lemma if wanted to. Unfortunately I busy the rest of the day, so I won't be able to have look at how easy this alternative version really is (at least not until this evening).

#### Chris Birkbeck (Nov 04 2021 at 09:25):

Also it might not need some of the other results about discriminants (for example, we might not need to know the discriminant in the cyclotomic cases (if I've understood the proof correctly))

#### Riccardo Brasca (Nov 04 2021 at 09:31):

Ah, this seems like a genuinely different proof! I am having a look.

What I have in mind uses, in some way, that $\mathbb{Z}$ is of finite index in $\mathcal{O}_K$ and shows that no prime $p$ divides the index (I think it is essentially what you wrote in the blueprint).

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

Neukirch uses ramification, that is probably too complicated for us.

Samuel seems indeed more elementary

#### Riccardo Brasca (Nov 04 2021 at 11:37):

For those who do not have Samuel's book, the proof is also here, page 25.

#### Riccardo Brasca (Nov 04 2021 at 11:42):

It surely requires less machinery, but one has to consider $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{Z}[\zeta_p]$, $\mathcal{O}_{\mathbb{Q}(\zeta_p)}$ and $\mathbb{Q}(\zeta_p)$ and move elements between all these rings. This means that in Lean one has to work with *a lot* of maps and various compatibility conditions.

#### Riccardo Brasca (Nov 04 2021 at 12:01):

I propose the following strategy.

- Compute the discriminant of $\mathbb{Q}(\zeta_p)/\mathbb{Q}$. This will follow more or less easily by $\mathrm{disc}_{K(x)/K}(1, x, \ldots, x^{n-1}) = (-1)^{\frac{n(n-1)}{2}} \mathrm{Norm}_{L/K}(\chi_x'(x))$.
- Prove that if $\alpha \in \mathbb{Z}[x]$ and $d = \mathrm{disc}_{\mathbb{Q}(x)/\mathbb{Q}}$ then $d\alpha \in \mathbb{Z}$. This will be not so fun, but we have Cramer's rule, so it should be doable (even for general $A$ instead of $\mathbb{Z}$).
- Prove that if $\alpha$ is integral with minimanl polynomial that is Eisenstein at $p$, then for all $x \in \mathcal{O}_{\mathbb{Q}(\alpha)}$, we have $px \in \mathbb{Z}[\alpha]$. This is essentially a reformulation of what is written in the blueprint, and it's maybe a little easier.

#### Johan Commelin (Nov 04 2021 at 12:09):

Why do you need "*a lot* of maps"? Just make sure you have all the algebra instances and all the `is_scalar_tower`

instances that you need. And after that, it should be reasonably easy to write and work with these gadgets as you are used to.

#### Riccardo Brasca (Nov 04 2021 at 12:17):

Yes, all the maps are `algebra_map _ _`

, but the proofs involve a lot of small computation like $p\cdot x \in \mathbb{Z}$ for some $x \in \mathbb{Q}$, and every time we have this we need to say that there is $y \in \mathbb{Z}$ such that... So maybe the maps are not that many, but still the proof will not be very fun to write.

#### Kevin Buzzard (Nov 04 2021 at 12:17):

Right -- this "four rings and lots of maps between them and I don't know how to set it all up" was precisely what I was going bananas about a couple of years ago with the "algebra is not scaling for me" and what Kenny solved with `algebra_tower`

, then refined by Eric to `is_scalar_tower`

.

#### Riccardo Brasca (Nov 04 2021 at 12:22):

I am not at all complaining about the status of the algebra library. But I think that often computational proofs are more difficult to formalize than conceptual proofs

#### Eric Rodriguez (Nov 04 2021 at 13:36):

Riccardo Brasca said:

I propose the following strategy.

- Compute the discriminant of $\mathbb{Q}(\zeta_p)/\mathbb{Q}$. This will follow more or less easily by $\mathrm{disc}_{K(x)/K}(1, x, \ldots, x^{n-1}) = (-1)^{\frac{n(n-1)}{2}} \mathrm{Norm}_{L/K}(\chi_x'(x))$.
- Prove that if $\alpha \in \mathbb{Z}[x]$ and $d = \mathrm{disc}_{\mathbb{Q}(x)/\mathbb{Q}}$ then $d\alpha \in \mathbb{Z}$. This will be not so fun, but we have Cramer's rule, so it should be doable (even for general $A$ instead of $\mathbb{Z}$).
- Prove that if $\alpha$ is integral with minimanl polynomial that is Eisenstein at $p$, then for all $x \in \mathcal{O}_{\mathbb{Q}(\alpha)}$, we have $px \in \mathbb{Z}[\alpha]$. This is essentially a reformulation of what is written in the blueprint, and it's maybe a little easier.

I'm confused about your second step; do you mean if $\alpha \in \mathbb{Q}(x), d\alpha \in \mathcal{O}_{\mathbb{Q}(x)}$?

#### Riccardo Brasca (Nov 04 2021 at 13:46):

Ops! I mean the following: let $K = \mathbb{Q}(x)$, with $x$ integral over $\mathbb{Z}$ and let $d = \mathrm{disc}_{K/\mathbb{Q}}(1, x, x^2,\ldots)$. Then $d \cdot (\mathcal{O}_{\mathbb{Q}(x)}/\mathbb{Z}[x]) = 0$, so $\mathbb{Z}[x]$ can be smaller than $\mathcal{O}_{\mathbb{Q}(x)}$, but we always have $\mathbb{Z}[x] \subseteq \mathcal{O}_{\mathbb{Q}(x)} \subset \frac{1}{d}\mathbb{Z}[x]$.

#### Antoine Chambert-Loir (Nov 04 2021 at 13:50):

Does Lean have matrices indexed by an arbitrary finite set ? In any case, a`A: matrix I J`

could only have a determinant if `I=J`

, otherwise it would be well defined up to a sign.

#### Riccardo Brasca (Nov 04 2021 at 13:52):

Matrices are indexed by types, not by sets, but yes, this is what I was saying. In any case for the discriminant everything worked very well.

#### Antoine Chambert-Loir (Nov 04 2021 at 13:54):

Riccardo, you can probably use the fact that $\mathrm{Tr}(\alpha x^m) $ is an integer for all $m$.

Moreover, when $\alpha$ has a minimal polynomial which is Eisenstein at $p$, doesn't it generate the ring of integers (at $p$)?

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

This is more or less my strategy: the discriminant being a power $p$ implies that the index of $\mathbb{Z}[x]$ in the ring of integers is a power of $p$, but since the minimal polynomial is Eisenstein the index must be $1$.

#### Kevin Buzzard (Nov 04 2021 at 15:29):

you can just argue that p^{p-1} doesn't divide the disc of $\mathbb{Z}[\zeta_p]$ for that last part

#### Riccardo Brasca (Nov 04 2021 at 17:08):

Can you elaborate a little bit? I don't see where the $p^{p-1}$ comes from.

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

To start the work on the last "basic" property of the discriminant I've proved

```
local notation `n` := finrank K L
lemma of_power_basis_eq_prod'' (e : fin pb.dim ≃ (L →ₐ[K] E)) :
algebra_map K E (discriminant K pb.basis) =
(-1) ^ (n * (n - 1) / 2) * ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen)))
```

Given that we already have

```
lemma of_power_basis_eq_prod' (e : fin pb.dim ≃ (L →ₐ[K] E)) :
algebra_map K E (discriminant K pb.basis) =
∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
-((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen)))
```

the proof is mathematically trivial, but I messed up a lot to compute the correct exponent. If someone is good in doing stupid computations in Lean feel free to golf. I am tempted to write down the four cases modulo 4...

#### Chris Birkbeck (Nov 04 2021 at 22:07):

Riccardo Brasca said:

I propose the following strategy.

- Compute the discriminant of $\mathbb{Q}(\zeta_p)/\mathbb{Q}$. This will follow more or less easily by $\mathrm{disc}_{K(x)/K}(1, x, \ldots, x^{n-1}) = (-1)^{\frac{n(n-1)}{2}} \mathrm{Norm}_{L/K}(\chi_x'(x))$.
- [corrected] Prove that if $\alpha \in \mathcal{O}_{\mathbb{Q}(x)}$, where $x$ is integral, and $d = \mathrm{disc}_{\mathbb{Q}(x)/\mathbb{Q}}$ then $d\alpha \in \mathbb{Z}[x]$. This will be not so fun, but we have Cramer's rule, so it should be doable (even for general $A$ instead of $\mathbb{Z}$).
- Prove that if $\alpha$ is integral with minimanl polynomial that is Eisenstein at $p$, then for all $x \in \mathcal{O}_{\mathbb{Q}(\alpha)}$, we have $px \in \mathbb{Z}[\alpha]$. This is essentially a reformulation of what is written in the blueprint, and it's maybe a little easier.

I think this is best way to do it. The proof in Samuel's book is nice, but this works a lot more generally

#### Kevin Buzzard (Nov 04 2021 at 22:42):

Riccardo Brasca said:

Can you elaborate a little bit? I don't see where the $p^{p-1}$ comes from.

hrmph I am talking nonsense! I was going to argue that if you made the ring of integers bigger by a factor of p then the the discriminant would go up by p^{degree} but it only goes up by p.

#### Riccardo Brasca (Nov 04 2021 at 23:32):

Strangely enough mathlib knows that the trace is the sum of the embeddings, but not that the norm is the product of the embeddings. I will see tomorrow if we can quickly prove this.

#### Riccardo Brasca (Nov 04 2021 at 23:46):

@Anne Baanen I see that you PR basically all the stuff concerning the trace and the norm. Do you already have somewhere that the norm is the product of the embeddings? Otherwise I will do it.

#### Anne Baanen (Nov 05 2021 at 01:25):

We have one form of that statement available already in `ring theory/norm.lean`

, I believe. For a nicer version, you should be able to copy the approach in `trace.lean`

without too many issues I expect. I can take a better look when I am back next Monday if needed.

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

Transitivity of the norm seems more cumbersome than transitivity of the trace (the determinant is more complicated!). What we have seems to be enough if the basic extension is normal, that is the case for cyclotomic extensions, so I will only consider this particular case for the moment.

#### Riccardo Brasca (Nov 05 2021 at 10:07):

If someone wants to play with it, the relevant result is docs#algebra.trace_trace_of_basis.

#### Chris Birkbeck (Nov 05 2021 at 10:10):

Sorry, when you say, what we have, are you referring to trace or norm?

#### Chris Birkbeck (Nov 05 2021 at 10:10):

Riccardo Brasca said:

If someone wants to play with it, the relevant result is docs#algebra.trace_trace_of_basis.

oh I guess you mean trace

#### Riccardo Brasca (Nov 05 2021 at 10:11):

I mean to prove the analogue result for the norm.

#### Riccardo Brasca (Nov 05 2021 at 10:11):

We have transitivity of the trace, we want transitivity of the norm

#### Chris Birkbeck (Nov 05 2021 at 10:12):

Ah ok sorry, I see what you mean. I thought the link you sent was somehow related to proving this for norm (other than being the analogous result).

#### Chris Birkbeck (Nov 05 2021 at 10:13):

Is norm even defined?

#### Riccardo Brasca (Nov 05 2021 at 10:13):

It seems I am too old and I forgot when I proved this being a student: it is really more difficult, it's not only a Lean problem. For example here Keith Conrad gives a quite complicated proof, to avoid too much computations.

#### Riccardo Brasca (Nov 05 2021 at 10:13):

#### Riccardo Brasca (Nov 05 2021 at 10:14):

I think docs#algebra.norm_gen_eq_prod_roots is enough if the minimal polynomial splits, so I will impose this assumption.

#### Riccardo Brasca (Nov 05 2021 at 10:23):

Wait a second, we probably don't need full transitivity, but only when the element is in the intermediate field, and this is easy

#### Chris Birkbeck (Nov 05 2021 at 10:23):

I guess if you have the result that says the norm is the product of the embeddings then its no too bad (?) It comes down to showing some embeddings are distinct (but maybe this is the hard bit).

#### Chris Birkbeck (Nov 05 2021 at 10:24):

yeah actually do you need it at all? what result do you think uses it?

#### Riccardo Brasca (Nov 05 2021 at 10:30):

I want to prove that the norm is the product of the embedding. We know some relation with the product of the roots of the minimal polynomial (but not for a general element). Let me see what I can do.

#### Chris Birkbeck (Nov 05 2021 at 10:34):

Ah well you can prove it without that but maybe its still annoying. It might not help, but here are the full notes from which I extracted parts of the blueprint https://cbirkbeck.github.io/test2/ It has a proof that doesn't use transitivity of the norm, but it uses other things which are maybe similarly annoying.

#### Riccardo Brasca (Nov 05 2021 at 11:35):

I've proved

```
lemma norm_eq_norm_adjoin [finite_dimensional K L] [is_separable K L] (x : L) :
norm K x = (norm K (adjoin_simple.gen K x)) ^ (finrank K⟮x⟯ L)
```

So I am confident we don't need full transitivity.

#### Riccardo Brasca (Nov 05 2021 at 12:21):

`norm_eq_prod_embeddings`

is done.

#### Riccardo Brasca (Nov 05 2021 at 16:37):

I spent basically all the afternoon to prove the horrible `prod_filter_lt_mul_neg_eq_prod_off_diag`

in `ready_for_mathlib/fin`

, so I didn't finish the link between the discriminant and the norm of the derivative of the minimal polynomial, but now everything is there. I'm done for today and I think also for the weekend, but I next week I think I can compute the discriminant of the cyclotomic field.

#### Chris Birkbeck (Nov 05 2021 at 16:38):

Yeah that lemma sounded annoying, I'm glad its done now :)

#### Riccardo Brasca (Nov 08 2021 at 14:55):

```
lemma of_power_basis_eq_norm : discriminant K pb.basis =
(-1) ^ (n * (n - 1) / 2) * (norm K (aeval pb.gen (minpoly K pb.gen).derivative))
```

Is proved (the proof is quite horrible, but it is still a proof... playing with index sets is not very nice!). I think we now have all the basic properties of the discriminant.

#### Chris Birkbeck (Nov 08 2021 at 14:56):

awesome! yes I think that was the last thing. I'll update the links to the blueprint later :)

#### Riccardo Brasca (Nov 08 2021 at 14:56):

Next goal is the computation of the disciminant of the cyclotomic extension.

#### Riccardo Brasca (Nov 15 2021 at 15:31):

I've proved that $N_{\mathbb{Q}(\zeta_p)/\mathbb{Q}}(\zeta_p - 1) = p$, so the computation of the discriminant of the cyclotomic field is almost done.

#### Riccardo Brasca (Nov 16 2021 at 10:56):

Does anyone has a suggestion to minimize the pain of dealing with powers of $-1$? For example the statement about the discriminant of the cyclotomic field currently is

```
lemma discriminant_prime {p : ℕ+} [hp : fact (p : ℕ).prime] (hodd : p ≠ 2) :
discriminant ℚ (zeta'.power_basis p ℚ K).basis =
(-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2) :=
```

I've basically proved it, the goal is

```
(-1) ^ ((↑p - 1) * (↑p - 1 - 1) / 2) * ↑p ^ (↑p - 1).pred = (-1) ^ ((↑p - 1) / 2) * ↑p ^ (↑p - 2)
```

This is not too complicated but maybe there is a smarter way of stating the result.

#### Alex J. Best (Nov 16 2021 at 11:10):

You can start with -1 in units of the integers, then you can go to a statement about zpow when there are no other terms left, move everything to one side and hope some tactic will simplify the exponent

#### Eric Rodriguez (Nov 16 2021 at 11:23):

```
example : (-1 : ℤ) ^ (((p : ℕ) - 1) * ((p : ℕ) - 1 - 1) / 2) * (p : ℕ) ^ ((p : ℕ) - 1).pred = (-1) ^ (((p : ℕ) - 1) / 2) * (p : ℕ) ^ ((p : ℕ) - 2) :=
begin
congr' 1,
rw [pow_eq_mod_order_of, show order_of (-1 : ℤ) = 2, by sorry],
conv_rhs { rw [pow_eq_mod_order_of, show order_of (-1 : ℤ) = 2, by sorry] },
congr' 1,
--palatable goal modulo 2
end
```

maybe this is a way? can't seem to find the lemma that `(-1)^n = ite (even n) 1 -1`

#### Ruben Van de Velde (Nov 16 2021 at 13:30):

`neg_one_pow_eq_pow_mod_two`

is somewhat close

#### Ruben Van de Velde (Nov 16 2021 at 13:31):

Or `neg_one_pow_eq_or`

with `nat.neg_one_pow_eq_one_iff_even`

#### Riccardo Brasca (Nov 16 2021 at 15:00):

The computation of the discriminant of the cyclotomic field is done (it depends on some sorrys about the general theory of cyclotomic fields, but nothing serious).

#### Johan Commelin (Nov 16 2021 at 15:02):

Nice work!

#### Riccardo Brasca (Nov 16 2021 at 15:03):

The next step is the proof that if $L$ has an integral power basis $1, \alpha, \ldots$, then the discriminant of the power basis kills $\mathcal{O}_L/A[\alpha]$, where $K=\mathrm{Frac}(A)$ is the base field.

#### Eric Rodriguez (Nov 16 2021 at 15:42):

Riccardo, I just finished the generalization of the primitive root result to domains; it was indeed very easy with fraction rings, apart from one thing - I can't seem to get `(n:R) ≠ 0 → (n:fraction_ring R) ≠ 0`

to work. Maybe you or anyone else on this chat can knock out this easy `sorry`

? (last thing pushed).

#### Riccardo Brasca (Nov 16 2021 at 15:46):

I am having a look

#### Riccardo Brasca (Nov 16 2021 at 15:53):

It's done

#### Riccardo Brasca (Nov 16 2021 at 15:53):

The main point is using docs#ring_hom.map_nat_cast

#### Eric Rodriguez (Nov 16 2021 at 15:55):

woop, thanks :D

#### Riccardo Brasca (Dec 22 2021 at 09:45):

@Eric Rodriguez Are you working on the power basis thing? I thought about it a little bit and I think that having it over a field is enough.

#### Riccardo Brasca (Dec 22 2021 at 09:45):

At least, it is what we need to compute the discriminant

#### Riccardo Brasca (Dec 22 2021 at 09:46):

`zeta'.embeddings_equiv_primitive_roots_apply`

is not true in general, but we can safely move it to `src/number_theory/cyclotomic/rat.lean`

and prove it over `Q`

.

#### Eric Rodriguez (Dec 22 2021 at 10:23):

I was - over a field being enough should make everything work!

#### Eric Rodriguez (Dec 22 2021 at 13:25):

I've got the power basis - I still need to rewrite that, though, as I'm currently using evil type equality. The rest should follow pretty straight-forwardly with the `power_basis.something_lift`

.

#### Eric Rodriguez (Dec 22 2021 at 21:53):

Okay, Riccardo - should we just specialise the lemma to \Q? Otherwise, we need some conditions for `cyclotomic n K`

to be the minpoly of every primitive root. I'm going to go on a walk and think about this for a bit

#### Eric Rodriguez (Dec 22 2021 at 21:54):

Also, I think we can get some uniqueness results on cyclotomic extensions from `is_splitting_field`

and such; may be nice to help us not dupe the API. The proof is essentially sorry free modulo these two things

#### Riccardo Brasca (Dec 22 2021 at 21:58):

If you are taking about `zeta'.embeddings_equiv_primitive_roots_apply`

we can prove it for `Q`

.

#### Riccardo Brasca (Dec 22 2021 at 21:58):

And thanks for all your work!

#### Riccardo Brasca (Dec 22 2021 at 22:01):

I think we will soon ready to PR the computation of the discriminant... so mathlib will know the discriminant of a cyclotomic field before the discriminant of a quadratic field :joy:

#### Eric Rodriguez (Dec 23 2021 at 00:07):

I just realised the right condition is normality! Let's see if the lemmas to support that are around, else I'll just specialize it to \Q :)

#### Riccardo Brasca (Dec 23 2021 at 09:37):

I've fixed the problem in `exists_unit_mul_primitive_root_one_sub_zeta`

. The error came from `zeta_primitive_root`

that had a wrong assumption

#### Riccardo Brasca (Oct 30 2021 at 21:01):

I was having a look at `ring_theory.trace`

, where docs#algebra.trace_form is defined. We already have *a lot* of results, even about the relation with embeddings and so on. I am confident we can set up a good API for the discriminant quite quickly.

I think we only need the following results: let $L/K$ be a separable extension of fields with $\dim_K(L) = n$ and let $b = (b_1,\ldots, b_n)$ a family of elements of $L$. Let $\Delta = \mathrm{disc}_{L/K}(b)$.

- $\Delta \neq 0$ if and only if $b$ is a basis of $L$ over $K$.
- If $P$ is matrix with coefficients in $K$, then $\mathrm{disc}_{L/K}(P \cdot b) = \det(P)^2 \Delta$.
- $\Delta = \det(\sigma_i(b_j))$, where the $\sigma_i$ are the $K$-embeddings of $L$ in an algebraic closure of $L$.
- If $L = K(x)$ and $x_i$ are the conjugates of $x$ in an algebraic closure, then $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2 = (-1)^{\frac{n(n-1)}{2}} \mathrm{Norm}_{L/K}(\chi_x'(x))$, where $\chi_x$ is the minimal polynomial of $x$.

I don't see any real problem in getting these results. The last one is probably the longest, but it seems very doable.

#### Kevin Buzzard (Oct 30 2021 at 22:39):

Instead of an algebraic closure of L you could use any field which contains a normal closure of L over K. I mention this because the complexes are not an algebraic closure of L, they're too big

#### Riccardo Brasca (Oct 30 2021 at 22:54):

Yes sure, mathlib results are for any algebraically closed field that contains `L`

. I don't know if we already have the normal closure

#### Chris Birkbeck (Oct 31 2021 at 12:09):

Oh I didn't know we had so much already about trace and their link to embeddings. I'll try and breakup the blueprint tomorrow to map out the results we'll need. Hopefully it'll be easy to create a bunch of sorried lemmas for this.

#### Riccardo Brasca (Nov 01 2021 at 11:14):

I will work on this today, hopefully writing all the relevant lemmas (sorried).

#### Chris Birkbeck (Nov 01 2021 at 11:20):

Ok cool. I'm just updating the blueprint with some of the missing lemmas.

#### Riccardo Brasca (Nov 01 2021 at 13:47):

#### Riccardo Brasca (Nov 01 2021 at 13:47):

I have to stop now, but I will start proving things this evening.

#### Chris Birkbeck (Nov 01 2021 at 13:52):

I used this lemma to prove the link between discriminant and norm of the min. pol. But maybe there are ways to get around this?

#### Kevin Buzzard (Nov 01 2021 at 13:54):

That product is a little subtle I guess! IIRC one can use that result to prove that the integers of Q(zeta_p) are Z(zeta_p) because the discriminant of the powers of p is +-p^(p-2) by a valuation argument and this isn't divisible by the p-1st power of any prime. But maybe there's also a way of arguing directly from the definition

#### Kevin Buzzard (Nov 01 2021 at 13:55):

There's a `sym2`

which you could use but I'm wondering whether it would be more trouble than it's worth and one should just order the embeddings

#### Alex J. Best (Nov 01 2021 at 13:58):

Riccardo Brasca said:

we could state

$\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2 = (-1)^{[L:K]([L:K] - 1)/2}\prod_{i \ne j} (x_i - x_j)$

(up to a sign or something) instead right? Where now the right hand side doesn't need an order?

#### Alex J. Best (Nov 01 2021 at 14:00):

I guess this is the sym2 suggestion of Kevin's too?

#### Riccardo Brasca (Nov 01 2021 at 14:03):

That's probably better

#### Kevin Buzzard (Nov 01 2021 at 14:07):

sym2 is unordered pairs so then one would have to somehow insert the proof that $(x-y)^2=(y-x)^2$ -- I think Alex's suggestion is better because it avoids this issue.

#### Kevin Buzzard (Nov 01 2021 at 14:07):

The product over $i\not=j$ is just a finprod or docs#finset.prod depending on what mood you're in (the set/finset is much easier to make)

#### Chris Birkbeck (Nov 01 2021 at 14:43):

Riccardo Brasca said:

So I pulled these changes and now I'm stuck in orange bar hell and `leanproject get-cache`

isn't working. Any ideas on how to fix this?

#### Kevin Buzzard (Nov 01 2021 at 14:43):

You want `leanproject get-mathlib-cache`

#### Kevin Buzzard (Nov 01 2021 at 14:45):

If you're working on a project with mathlib as a dependency then the workflow is slightly different. Working on a branch of mathlib it's `get-cache`

. For a project which depends on mathlib you use `get-mathlib-cache`

and then compile your project yourself with `leanproject build`

unless you've set up your own continuous integration, in which case `get-cache`

might work.

#### Chris Birkbeck (Nov 01 2021 at 14:47):

Ah `leanproject build`

! I had tried `leanproject get-mathlib-cache`

and it hadn't worked, but it was because I hadn't built it I guess.

#### Chris Birkbeck (Nov 01 2021 at 14:48):

Its working now, thanks :)

#### Kevin Buzzard (Nov 01 2021 at 14:48):

Basically I know a bunch of these commands and I fiddle around on the command line until `lean --make src/<path_to_file_I'm_working_on>`

works, then I restart VS Code

#### Kevin Buzzard (Nov 01 2021 at 14:49):

if it doesn't work then on linux it starts printing out the name of the file it's compiling, and if it's something else in my project then I know that mathlib is OK but my project isn't compiled, and if it's `_target/deps/mathlib/src/tactic/rcases.lean`

or whatever then I know I've screwed up my mathlib oleans

#### Chris Birkbeck (Nov 01 2021 at 14:53):

Kevin Buzzard said:

`lean --make src/<path_to_file_I'm_working_on>`

works, then I restart VS Code

That's a good strategy, I'll try that next time :) (also I found out that in windows, you can also see the printout of the files its working on if you use the terminal inside VScode, but not if you use the `Git Bash`

terminal)

#### Kevin Buzzard (Nov 01 2021 at 14:55):

The trap you can fall into with throwing random `leanproject`

commands around, when working on a project with mathlib as a dependency, is that `leanproject build`

builds the current versions of the project lean files, but `leanproject up`

will IIRC first update mathlib to current `master`

and then build, and of course bumping mathlib might break the project in interesting ways, so should be done on some branch of your project other than `master`

.

#### Yaël Dillies (Nov 01 2021 at 15:45):

Bhavik and I wanted to have a sum running over `sym2`

of something and it turns out to be a pain, because

- Every time you want to move terms, you need to show that this move respects symmetry.
- Your terms have to be intrinsically symmetric. So here you can't refer to $(x_1 - x_j)^2$. You instead have to resort to an intermediary definition
`term (xy : sym2 something) : something_else := sym2.lift ⟨(xy.out.1 - xy.out.2)^2, a_proof⟩`

. - The
`sym2`

API is weak.

#### Yaël Dillies (Nov 01 2021 at 15:46):

I strongly advise you to square your sum and forget about `sym2`

. And that's what Bhavik and I did: double the sum and go on with our lives.

#### Yaël Dillies (Nov 01 2021 at 15:47):

Although here I understand that squaring might be undesirable. In our case, doubling was injective.

#### Riccardo Brasca (Nov 01 2021 at 15:48):

Something like

```
lemma of_power_basis_eq_prod : algebra_map K E (discriminant K pb.basis) ^ 2 =
((univ.product univ).filter (λ (σ : (L →ₐ[K] E) × (L →ₐ[K] E)), σ.1 ≠ σ.2)).prod
(λ σ, (σ.1 pb.gen - σ.2 pb.gen) ^ 2) := sorry
```

works. Here `E`

is algebraically closed (it is enough that splits the minimal polynomial of `pb.gen`

, the first element of a power basis `pb`

).

#### Riccardo Brasca (Nov 01 2021 at 15:49):

We can also have the similar statement using the `finset`

of roots of the minimal polynomial.

#### Yaël Dillies (Nov 01 2021 at 15:50):

(you'll be happy to hear that `univ.product univ = univ`

:wink:)

#### Riccardo Brasca (Nov 01 2021 at 15:51):

Ah yes, and I am pretty sure that `diagonal`

exists, so that is just the complement of the diagonal

#### Yaël Dillies (Nov 01 2021 at 15:51):

Yeah exactly. You can use `univ.off_diag`

(docs#finset.off_diag) here.

#### Riccardo Brasca (Nov 01 2021 at 15:52):

Ah nice, I didn't spot it

#### Yaël Dillies (Nov 01 2021 at 15:52):

Damn, I really became that finset person.

#### Kevin Buzzard (Nov 01 2021 at 15:53):

`diag_empty`

was only added to mathlib 17 hours ago!

#### Riccardo Brasca (Nov 01 2021 at 15:56):

A little golf

```
lemma of_power_basis_eq_prod : algebra_map K E (discriminant K pb.basis) ^ 2 =
(univ : finset ((L →ₐ[K] E) × (L →ₐ[K] E))).off_diag.prod
(λ σ, (σ.1.1 pb.gen - σ.1.2 pb.gen) ^ 2) := sorry
```

I don't like `σ.1.1`

, but that's OK

#### Riccardo Brasca (Nov 01 2021 at 21:45):

I proved that a linear dependent family has zero discriminant. It's an easy result, but the fact that the Lean proof is short is a good indication we are able to work with the trace.

#### Riccardo Brasca (Nov 01 2021 at 22:10):

And we have docs#matrix.det_vandermonde! So it's maybe a good idea to order the embeddings (keeping the more intrinsic statement).

#### Chris Birkbeck (Nov 02 2021 at 10:03):

That's good news! If picking an order makes things easier then I have no problem with that.

#### Riccardo Brasca (Nov 02 2021 at 17:51):

- $\Delta \neq 0$ if and only if $b$ is a basis of $L$ over $K$.
- If $P$ is matrix with coefficients in $K$, then $\mathrm{disc}_{L/K}(P \cdot b) = \det(P)^2 \Delta$.

Are proved.

#### Chris Birkbeck (Nov 02 2021 at 17:52):

Great!

#### Riccardo Brasca (Nov 03 2021 at 11:30):

I've started writing down the proof that $\Delta = \det(\sigma_i(b_j))^2$. I don't see any real problem, and that's good. But I think we can't avoid some sort of order on the embeddings: if `b : ι → L`

is a family of elements of `L`

, then `λ (i : ι) (σ : L →ₐ[K] E), σ ( b i)`

gives a matrix `M : matrix ι (L →ₐ[K] E) E`

. There is no way to make `M`

a square matrix: even if `E`

is algebraically closed and `fintype.card ι = finrank K L`

, we only get an equiv `ι ≃ L →ₐ[K] E`

, so we need to apply some `reindex`

. The only possibility is to literally take `ι = L →ₐ[K] E`

, but this is too restrictive.

The most flexible way of stating the results is, I think, to have it taking an equiv `ι ≃ L →ₐ[K] E`

as input. Any better idea?

#### Eric Rodriguez (Nov 03 2021 at 11:37):

Maybe the 'correct' thing to do is generalise det to `matrix m n R`

and return junk if they are not the same cardinality, but that seems like a huuuge refactor

#### Alex J. Best (Nov 03 2021 at 11:45):

I like the sound of that, would it really be such a big refactor? If all the results about det are about `det`

of a `matrix n n`

then apart from the very basic API it might not need that much work

#### Riccardo Brasca (Nov 03 2021 at 11:51):

But then if one wants the determinant of `M matrix n n R`

will have to write the `n`

and `n`

have the same cardinality (trivial, but you'll write it everywhere). And having the same cardinality breaks computability I think, since the construction of the bijection is not computable. `det`

can take the equiv as input, but essentially this means using `reindex`

, and that is already there.

#### Riccardo Brasca (Nov 03 2021 at 11:54):

I mean, unless we really change the definition, having the determinant of a matrix indexed by types with the same cardinality boils down to take the determinant of the reindexed matrix, that is really square.

#### Alex J. Best (Nov 03 2021 at 12:05):

Well you could add a default argument / tactic I believe

#### Alex J. Best (Nov 03 2021 at 12:09):

The reason this sounded nice to me was the other way of defining discriminants is to take the determinant of the Sylvester matrix, this matrix is most naturally the result of stacking two rectangular matrices on top of each other, so you can define it on fin n x fin n with an if, but the most aesthetically pleasing way you would need a definition of det that works if the indexing types have the same card but doesn't require the types to be syntactically equal

#### Riccardo Brasca (Nov 03 2021 at 12:21):

I am not experienced enough to have a strong opinion, but my impression is that the determinant is defined for square-in-mathlib-sense matrices. Even in real world mathematics. What we usually do is that we only consider matrices of type `matrix (fin n) (fin m) R`

and we constantly choose bijections of some set of indexes with `fin n`

, reindex the matrix, and take the determinant.

I think that, working in Lean, we really do what we have to do, but usually we don't say it and of course we don't write it. Having the determinant of `M : matrix n m R`

will make things more similar to what we do on paper, but here we are really cheating when doing unformal mathematics, and usually Lean punishes us if we try to do similar stuff.

#### Riccardo Brasca (Nov 03 2021 at 12:23):

I can be very wrong of course, but I am sure that one should ask the community before starting such a refactor.

#### Yakov Pechersky (Nov 03 2021 at 12:25):

Sorry, I don't have the full context here, but a couple of questions. Is it that you truly have a square matrix, but the types are different yet with same cardinality? Or is it that you have a rectangular matrix?

#### Yakov Pechersky (Nov 03 2021 at 12:25):

#### Yakov Pechersky (Nov 03 2021 at 12:28):

Could you use that, after composing some "reindexing" maps?

#### Riccardo Brasca (Nov 03 2021 at 12:28):

It's a square matrix in the sense that the two types have the same cardinality. docs#linear_map.det has the same problem, the associated linear map is between two vector spaces of the same dimension.

#### Riccardo Brasca (Nov 03 2021 at 12:28):

Yes, using `reindex`

is what I am proposing.

#### Yakov Pechersky (Nov 03 2021 at 12:31):

For a refactor, I'd first make a new det definition for matrices or linear maps, one that is over a single arbitrary fintype, that takes an order_iso to a fin n. If that one works, two ways of extending it. First, prove that the choice of order_iso doesn't matter, which let's you use the trunc.out one. Then, extend to two fintypes with the order_iso to the same fin n.

#### Yakov Pechersky (Nov 03 2021 at 12:33):

The "take a reindexing function as part of the definition" is similar to how we define sums, prods, infs, and sups over finsets.

#### Riccardo Brasca (Nov 03 2021 at 13:57):

`discriminant.eq_det_embeddings_matrix_reindex_pow_two`

is proved. Everything went really smoothly even with `reindex`

:)

#### Alex J. Best (Nov 03 2021 at 14:00):

Well for this specific det^2 function the indexing order choice shouldn't matter right? Even if you use a different order on each side the det only changes sign, so this function is somehow even more canonical than the usual det

#### Riccardo Brasca (Nov 03 2021 at 14:14):

This is already stated taking an arbitrary equiv as input, but yes, changing the equiv permutes the rows (or the columns, no idea) of the matrix of the embeddings. The proof uses that the matrix of the traces is the matrix of the embeddings multiplied by its transpose, so if one determinant changes sign also the other does.

#### Riccardo Brasca (Nov 03 2021 at 14:50):

And this gives me the impression that refactoring the determinant is not possible: the new determinant would be defined only up to a sign, right?

#### Kevin Buzzard (Nov 03 2021 at 21:24):

Alex is observing that if `M : matrix i j R`

and we choose a bijection i -> j then the sign of det(M) depends on the bijection (up to a sign) but det(M)^2 is independent of the choice of bijection.

#### Riccardo Brasca (Nov 03 2021 at 21:51):

Yes, this is what I am also saying, the determinant wouldn't be well defined. In our case we are only interested in the square, so no problem, but I don't think a general refactor of `det`

is doable. And moreover in another thread people started proposing *a different* refactor of `det`

motivated by a completely unrelated problem :rolling_on_the_floor_laughing:

These guys like refactoring

#### Yaël Dillies (Nov 03 2021 at 21:52):

Did you say refactor? :smirk:

#### Riccardo Brasca (Nov 03 2021 at 21:53):

In any case $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = \prod_{i < j} (x_i - x_j)^2$ is proved. The statement is

```
lemma of_power_basis_eq_prod (pb : power_basis K L) (e : fin pb.dim ≃ (L →ₐ[K] E)) :
algebra_map K E (discriminant K pb.basis) =
∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j), (e j pb.gen- (e i pb.gen)) ^ 2 :=
```

#### Riccardo Brasca (Nov 03 2021 at 22:05):

Now the only basic fact that is missing a proof is $\mathrm{disc}_{L/K}(1, x, \ldots, x^{n-1}) = (-1)^{\frac{n(n-1)}{2}} \mathrm{Norm}_{L/K}(\chi_x'(x))$, where $\chi_x$ is the minimal polynomial of $x$. I have to think a little bit for this one.

#### Kevin Buzzard (Nov 03 2021 at 22:24):

this doesn't quite look right -- the degree of the min poly will depend on x. Do you mean the char poly or something? Example: x=1. The disc is 0 if L != K, but the norm is 1.

#### Riccardo Brasca (Nov 03 2021 at 22:26):

I mean with the assumption that $L = K(x)$.

#### Kevin Buzzard (Nov 03 2021 at 22:26):

in that case the min poly is the char poly

#### Kevin Buzzard (Nov 03 2021 at 22:27):

If that assumption is false then the char poly has repeated roots and the powers won't span so both sides will be 0

#### Riccardo Brasca (Nov 03 2021 at 22:29):

Currently I am working with that assumption, if it helps. For cyclotomic fields in practice it is always satisfied (for the elements we want to consider). We will see if we need anything more general.

#### Riccardo Brasca (Nov 03 2021 at 22:30):

Looking at the blueprint, in the section about the discriminant, I think lemma 2.12 is going to be a pain.

#### Alex J. Best (Nov 03 2021 at 22:48):

Is it used other than for showing the ring of integers of Q(zeta) is Z[zeta]?

#### Chris Birkbeck (Nov 03 2021 at 22:49):

~~yes, its used in the proof I wrote down, but there could be other proofs that dont use it. Or maybe ways around it, but I've not thought about it.~~

#### Chris Birkbeck (Nov 03 2021 at 22:53):

Oh sorry, I misread your message. Not for what we need (I don't think)

#### Chris Birkbeck (Nov 03 2021 at 22:54):

But its handy for finding integral bases in general and for example tells you in the disc of a set of alg. ints. is square-free then you have an integral basis.

#### Riccardo Brasca (Nov 03 2021 at 22:55):

It's the key point in the proof, so we will have to get our hands dirty at some point, but it deserves some thought if we want to suffer as less as possible

#### Alex J. Best (Nov 03 2021 at 23:20):

I was looking at the proof in Neukirch (lemma I 10.2) the other day with Sander and it doesn't seem to use exactly the same lemma, though certainly it uses some related results in Chapter I 2.9. It might be better to prove some things using that route instead?

#### Chris Birkbeck (Nov 03 2021 at 23:30):

Oh maybe. I don't have my copy of Neukirch at home, but Ill have a look tomorrow. But if it's easier then we should do that :)

#### Alex J. Best (Nov 03 2021 at 23:47):

I can't tell if its easier yet to be honest! Just an alternative seeming approach

#### Chris Birkbeck (Nov 04 2021 at 09:23):

So I just had a look at Pierre Samuels "algebraic theory of numbers", in it (in chapter 2.9) there is a proof of what the ring of integers is in the cyclotomic cases, which just uses properties or the trace function. It wouldn't work more generally, but I would be a way to avoid this annoying lemma if wanted to. Unfortunately I busy the rest of the day, so I won't be able to have look at how easy this alternative version really is (at least not until this evening).

#### Chris Birkbeck (Nov 04 2021 at 09:25):

Also it might not need some of the other results about discriminants (for example, we might not need to know the discriminant in the cyclotomic cases (if I've understood the proof correctly))

#### Riccardo Brasca (Nov 04 2021 at 09:31):

Ah, this seems like a genuinely different proof! I am having a look.

What I have in mind uses, in some way, that $\mathbb{Z}$ is of finite index in $\mathcal{O}_K$ and shows that no prime $p$ divides the index (I think it is essentially what you wrote in the blueprint).

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

Neukirch uses ramification, that is probably too complicated for us.

Samuel seems indeed more elementary

#### Riccardo Brasca (Nov 04 2021 at 11:37):

For those who do not have Samuel's book, the proof is also here, page 25.

#### Riccardo Brasca (Nov 04 2021 at 11:42):

It surely requires less machinery, but one has to consider $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{Z}[\zeta_p]$, $\mathcal{O}_{\mathbb{Q}(\zeta_p)}$ and $\mathbb{Q}(\zeta_p)$ and move elements between all these rings. This means that in Lean one has to work with *a lot* of maps and various compatibility conditions.

#### Riccardo Brasca (Nov 04 2021 at 12:01):

I propose the following strategy.

- [corrected] Prove that if $\alpha \in \mathcal{O}_{\mathbb{Q}(x)}$, where $x$ is integral, and $d = \mathrm{disc}_{\mathbb{Q}(x)/\mathbb{Q}}$ then $d\alpha \in \mathbb{Z}[x]$. This will be not so fun, but we have Cramer's rule, so it should be doable (even for general $A$ instead of $\mathbb{Z}$).

#### Johan Commelin (Nov 04 2021 at 12:09):

Why do you need "*a lot* of maps"? Just make sure you have all the algebra instances and all the `is_scalar_tower`

instances that you need. And after that, it should be reasonably easy to write and work with these gadgets as you are used to.

#### Riccardo Brasca (Nov 04 2021 at 12:17):

Yes, all the maps are `algebra_map _ _`

, but the proofs involve a lot of small computation like $p\cdot x \in \mathbb{Z}$ for some $x \in \mathbb{Q}$, and every time we have this we need to say that there is $y \in \mathbb{Z}$ such that... So maybe the maps are not that many, but still the proof will not be very fun to write.

#### Kevin Buzzard (Nov 04 2021 at 12:17):

Right -- this "four rings and lots of maps between them and I don't know how to set it all up" was precisely what I was going bananas about a couple of years ago with the "algebra is not scaling for me" and what Kenny solved with `algebra_tower`

, then refined by Eric to `is_scalar_tower`

.

#### Riccardo Brasca (Nov 04 2021 at 12:22):

I am not at all complaining about the status of the algebra library. But I think that often computational proofs are more difficult to formalize than conceptual proofs

#### Eric Rodriguez (Nov 04 2021 at 13:36):

Riccardo Brasca said:

I propose the following strategy.

- Prove that if $\alpha \in \mathbb{Z}[x]$ and $d = \mathrm{disc}_{\mathbb{Q}(x)/\mathbb{Q}}$ then $d\alpha \in \mathbb{Z}$. This will be not so fun, but we have Cramer's rule, so it should be doable (even for general $A$ instead of $\mathbb{Z}$).

I'm confused about your second step; do you mean if $\alpha \in \mathbb{Q}(x), d\alpha \in \mathcal{O}_{\mathbb{Q}(x)}$?

#### Riccardo Brasca (Nov 04 2021 at 13:46):

Ops! I mean the following: let $K = \mathbb{Q}(x)$, with $x$ integral over $\mathbb{Z}$ and let $d = \mathrm{disc}_{K/\mathbb{Q}}(1, x, x^2,\ldots)$. Then $d \cdot (\mathcal{O}_{\mathbb{Q}(x)}/\mathbb{Z}[x]) = 0$, so $\mathbb{Z}[x]$ can be smaller than $\mathcal{O}_{\mathbb{Q}(x)}$, but we always have $\mathbb{Z}[x] \subseteq \mathcal{O}_{\mathbb{Q}(x)} \subset \frac{1}{d}\mathbb{Z}[x]$.

#### Antoine Chambert-Loir (Nov 04 2021 at 13:50):

Does Lean have matrices indexed by an arbitrary finite set ? In any case, a`A: matrix I J`

could only have a determinant if `I=J`

, otherwise it would be well defined up to a sign.

#### Riccardo Brasca (Nov 04 2021 at 13:52):

Matrices are indexed by types, not by sets, but yes, this is what I was saying. In any case for the discriminant everything worked very well.

#### Antoine Chambert-Loir (Nov 04 2021 at 13:54):

Riccardo, you can probably use the fact that $\mathrm{Tr}(\alpha x^m) $ is an integer for all $m$.

Moreover, when $\alpha$ has a minimal polynomial which is Eisenstein at $p$, doesn't it generate the ring of integers (at $p$)?

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

This is more or less my strategy: the discriminant being a power $p$ implies that the index of $\mathbb{Z}[x]$ in the ring of integers is a power of $p$, but since the minimal polynomial is Eisenstein the index must be $1$.

#### Kevin Buzzard (Nov 04 2021 at 15:29):

you can just argue that p^{p-1} doesn't divide the disc of $\mathbb{Z}[\zeta_p]$ for that last part

#### Riccardo Brasca (Nov 04 2021 at 17:08):

Can you elaborate a little bit? I don't see where the $p^{p-1}$ comes from.

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

To start the work on the last "basic" property of the discriminant I've proved

```
local notation `n` := finrank K L
lemma of_power_basis_eq_prod'' (e : fin pb.dim ≃ (L →ₐ[K] E)) :
algebra_map K E (discriminant K pb.basis) =
(-1) ^ (n * (n - 1) / 2) * ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen)))
```

Given that we already have

```
lemma of_power_basis_eq_prod' (e : fin pb.dim ≃ (L →ₐ[K] E)) :
algebra_map K E (discriminant K pb.basis) =
∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
-((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen)))
```

the proof is mathematically trivial, but I messed up a lot to compute the correct exponent. If someone is good in doing stupid computations in Lean feel free to golf. I am tempted to write down the four cases modulo 4...

#### Chris Birkbeck (Nov 04 2021 at 22:07):

Riccardo Brasca said:

I propose the following strategy.

- [corrected] Prove that if $\alpha \in \mathcal{O}_{\mathbb{Q}(x)}$, where $x$ is integral, and $d = \mathrm{disc}_{\mathbb{Q}(x)/\mathbb{Q}}$ then $d\alpha \in \mathbb{Z}[x]$. This will be not so fun, but we have Cramer's rule, so it should be doable (even for general $A$ instead of $\mathbb{Z}$).

I think this is best way to do it. The proof in Samuel's book is nice, but this works a lot more generally

#### Kevin Buzzard (Nov 04 2021 at 22:42):

Riccardo Brasca said:

Can you elaborate a little bit? I don't see where the $p^{p-1}$ comes from.

hrmph I am talking nonsense! I was going to argue that if you made the ring of integers bigger by a factor of p then the the discriminant would go up by p^{degree} but it only goes up by p.

#### Riccardo Brasca (Nov 04 2021 at 23:32):

Strangely enough mathlib knows that the trace is the sum of the embeddings, but not that the norm is the product of the embeddings. I will see tomorrow if we can quickly prove this.

#### Riccardo Brasca (Nov 04 2021 at 23:46):

@Anne Baanen I see that you PR basically all the stuff concerning the trace and the norm. Do you already have somewhere that the norm is the product of the embeddings? Otherwise I will do it.

#### Anne Baanen (Nov 05 2021 at 01:25):

We have one form of that statement available already in `ring theory/norm.lean`

, I believe. For a nicer version, you should be able to copy the approach in `trace.lean`

without too many issues I expect. I can take a better look when I am back next Monday if needed.

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

Transitivity of the norm seems more cumbersome than transitivity of the trace (the determinant is more complicated!). What we have seems to be enough if the basic extension is normal, that is the case for cyclotomic extensions, so I will only consider this particular case for the moment.

#### Riccardo Brasca (Nov 05 2021 at 10:07):

If someone wants to play with it, the relevant result is docs#algebra.trace_trace_of_basis.

#### Chris Birkbeck (Nov 05 2021 at 10:10):

Sorry, when you say, what we have, are you referring to trace or norm?

#### Chris Birkbeck (Nov 05 2021 at 10:10):

Riccardo Brasca said:

If someone wants to play with it, the relevant result is docs#algebra.trace_trace_of_basis.

oh I guess you mean trace

#### Riccardo Brasca (Nov 05 2021 at 10:11):

I mean to prove the analogue result for the norm.

#### Riccardo Brasca (Nov 05 2021 at 10:11):

We have transitivity of the trace, we want transitivity of the norm

#### Chris Birkbeck (Nov 05 2021 at 10:12):

Ah ok sorry, I see what you mean. I thought the link you sent was somehow related to proving this for norm (other than being the analogous result).

#### Chris Birkbeck (Nov 05 2021 at 10:13):

Is norm even defined?

#### Riccardo Brasca (Nov 05 2021 at 10:13):

It seems I am too old and I forgot when I proved this being a student: it is really more difficult, it's not only a Lean problem. For example here Keith Conrad gives a quite complicated proof, to avoid too much computations.

#### Riccardo Brasca (Nov 05 2021 at 10:13):

#### Riccardo Brasca (Nov 05 2021 at 10:14):

I think docs#algebra.norm_gen_eq_prod_roots is enough if the minimal polynomial splits, so I will impose this assumption.

#### Riccardo Brasca (Nov 05 2021 at 10:23):

Wait a second, we probably don't need full transitivity, but only when the element is in the intermediate field, and this is easy

#### Chris Birkbeck (Nov 05 2021 at 10:23):

I guess if you have the result that says the norm is the product of the embeddings then its no too bad (?) It comes down to showing some embeddings are distinct (but maybe this is the hard bit).

#### Chris Birkbeck (Nov 05 2021 at 10:24):

yeah actually do you need it at all? what result do you think uses it?

#### Riccardo Brasca (Nov 05 2021 at 10:30):

I want to prove that the norm is the product of the embedding. We know some relation with the product of the roots of the minimal polynomial (but not for a general element). Let me see what I can do.

#### Chris Birkbeck (Nov 05 2021 at 10:34):

Ah well you can prove it without that but maybe its still annoying. It might not help, but here are the full notes from which I extracted parts of the blueprint https://cbirkbeck.github.io/test2/ It has a proof that doesn't use transitivity of the norm, but it uses other things which are maybe similarly annoying.

#### Riccardo Brasca (Nov 05 2021 at 11:35):

I've proved

```
lemma norm_eq_norm_adjoin [finite_dimensional K L] [is_separable K L] (x : L) :
norm K x = (norm K (adjoin_simple.gen K x)) ^ (finrank K⟮x⟯ L)
```

So I am confident we don't need full transitivity.

#### Riccardo Brasca (Nov 05 2021 at 12:21):

`norm_eq_prod_embeddings`

is done.

#### Riccardo Brasca (Nov 05 2021 at 16:37):

I spent basically all the afternoon to prove the horrible `prod_filter_lt_mul_neg_eq_prod_off_diag`

in `ready_for_mathlib/fin`

, so I didn't finish the link between the discriminant and the norm of the derivative of the minimal polynomial, but now everything is there. I'm done for today and I think also for the weekend, but I next week I think I can compute the discriminant of the cyclotomic field.

#### Chris Birkbeck (Nov 05 2021 at 16:38):

Yeah that lemma sounded annoying, I'm glad its done now :)

#### Riccardo Brasca (Nov 08 2021 at 14:55):

```
lemma of_power_basis_eq_norm : discriminant K pb.basis =
(-1) ^ (n * (n - 1) / 2) * (norm K (aeval pb.gen (minpoly K pb.gen).derivative))
```

Is proved (the proof is quite horrible, but it is still a proof... playing with index sets is not very nice!). I think we now have all the basic properties of the discriminant.

#### Chris Birkbeck (Nov 08 2021 at 14:56):

awesome! yes I think that was the last thing. I'll update the links to the blueprint later :)

#### Riccardo Brasca (Nov 08 2021 at 14:56):

Next goal is the computation of the disciminant of the cyclotomic extension.

#### Riccardo Brasca (Nov 15 2021 at 15:31):

I've proved that $N_{\mathbb{Q}(\zeta_p)/\mathbb{Q}}(\zeta_p - 1) = p$, so the computation of the discriminant of the cyclotomic field is almost done.

#### Riccardo Brasca (Nov 16 2021 at 10:56):

Does anyone has a suggestion to minimize the pain of dealing with powers of $-1$? For example the statement about the discriminant of the cyclotomic field currently is

```
lemma discriminant_prime {p : ℕ+} [hp : fact (p : ℕ).prime] (hodd : p ≠ 2) :
discriminant ℚ (zeta'.power_basis p ℚ K).basis =
(-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2) :=
```

I've basically proved it, the goal is

```
(-1) ^ ((↑p - 1) * (↑p - 1 - 1) / 2) * ↑p ^ (↑p - 1).pred = (-1) ^ ((↑p - 1) / 2) * ↑p ^ (↑p - 2)
```

This is not too complicated but maybe there is a smarter way of stating the result.

#### Alex J. Best (Nov 16 2021 at 11:10):

You can start with -1 in units of the integers, then you can go to a statement about zpow when there are no other terms left, move everything to one side and hope some tactic will simplify the exponent

#### Eric Rodriguez (Nov 16 2021 at 11:23):

```
example : (-1 : ℤ) ^ (((p : ℕ) - 1) * ((p : ℕ) - 1 - 1) / 2) * (p : ℕ) ^ ((p : ℕ) - 1).pred = (-1) ^ (((p : ℕ) - 1) / 2) * (p : ℕ) ^ ((p : ℕ) - 2) :=
begin
congr' 1,
rw [pow_eq_mod_order_of, show order_of (-1 : ℤ) = 2, by sorry],
conv_rhs { rw [pow_eq_mod_order_of, show order_of (-1 : ℤ) = 2, by sorry] },
congr' 1,
--palatable goal modulo 2
end
```

maybe this is a way? can't seem to find the lemma that `(-1)^n = ite (even n) 1 -1`

#### Ruben Van de Velde (Nov 16 2021 at 13:30):

`neg_one_pow_eq_pow_mod_two`

is somewhat close

#### Ruben Van de Velde (Nov 16 2021 at 13:31):

Or `neg_one_pow_eq_or`

with `nat.neg_one_pow_eq_one_iff_even`

#### Riccardo Brasca (Nov 16 2021 at 15:00):

The computation of the discriminant of the cyclotomic field is done (it depends on some sorrys about the general theory of cyclotomic fields, but nothing serious).

#### Johan Commelin (Nov 16 2021 at 15:02):

Nice work!

#### Riccardo Brasca (Nov 16 2021 at 15:03):

The next step is the proof that if $L$ has an integral power basis $1, \alpha, \ldots$, then the discriminant of the power basis kills $\mathcal{O}_L/A[\alpha]$, where $K=\mathrm{Frac}(A)$ is the base field.

#### Eric Rodriguez (Nov 16 2021 at 15:42):

Riccardo, I just finished the generalization of the primitive root result to domains; it was indeed very easy with fraction rings, apart from one thing - I can't seem to get `(n:R) ≠ 0 → (n:fraction_ring R) ≠ 0`

to work. Maybe you or anyone else on this chat can knock out this easy `sorry`

? (last thing pushed).

#### Riccardo Brasca (Nov 16 2021 at 15:46):

I am having a look

#### Riccardo Brasca (Nov 16 2021 at 15:53):

It's done

#### Riccardo Brasca (Nov 16 2021 at 15:53):

The main point is using docs#ring_hom.map_nat_cast

#### Eric Rodriguez (Nov 16 2021 at 15:55):

woop, thanks :D

#### Riccardo Brasca (Dec 22 2021 at 09:45):

@Eric Rodriguez Are you working on the power basis thing? I thought about it a little bit and I think that having it over a field is enough.

#### Riccardo Brasca (Dec 22 2021 at 09:45):

At least, it is what we need to compute the discriminant

#### Riccardo Brasca (Dec 22 2021 at 09:46):

`zeta'.embeddings_equiv_primitive_roots_apply`

is not true in general, but we can safely move it to `src/number_theory/cyclotomic/rat.lean`

and prove it over `Q`

.

#### Eric Rodriguez (Dec 22 2021 at 10:23):

I was - over a field being enough should make everything work!

#### Eric Rodriguez (Dec 22 2021 at 13:25):

I've got the power basis - I still need to rewrite that, though, as I'm currently using evil type equality. The rest should follow pretty straight-forwardly with the `power_basis.something_lift`

.

#### Eric Rodriguez (Dec 22 2021 at 21:53):

Okay, Riccardo - should we just specialise the lemma to \Q? Otherwise, we need some conditions for `cyclotomic n K`

to be the minpoly of every primitive root. I'm going to go on a walk and think about this for a bit

#### Eric Rodriguez (Dec 22 2021 at 21:54):

Also, I think we can get some uniqueness results on cyclotomic extensions from `is_splitting_field`

and such; may be nice to help us not dupe the API. The proof is essentially sorry free modulo these two things

#### Riccardo Brasca (Dec 22 2021 at 21:58):

If you are taking about `zeta'.embeddings_equiv_primitive_roots_apply`

we can prove it for `Q`

.

#### Riccardo Brasca (Dec 22 2021 at 21:58):

And thanks for all your work!

#### Riccardo Brasca (Dec 22 2021 at 22:01):

I think we will soon ready to PR the computation of the discriminant... so mathlib will know the discriminant of a cyclotomic field before the discriminant of a quadratic field :joy:

#### Eric Rodriguez (Dec 23 2021 at 00:07):

~~I just realised the right condition is normality! Let's see if the lemmas to support that are around, else I'll just specialize it to \Q :)~~ Maybe I'm talking nonsense and got \dvd the wrong way round...

#### Riccardo Brasca (Dec 23 2021 at 09:37):

I've fixed the problem in `exists_unit_mul_primitive_root_one_sub_zeta`

. The error came from `zeta_primitive_root`

that had a wrong assumption

Last updated: Dec 20 2023 at 11:08 UTC