Discriminant

Stream: FLT-regular

[Riccardo Brasca]

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]

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]

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]

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]

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

[Chris Birkbeck]

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

[Riccardo Brasca]

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]

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

[Chris Birkbeck]

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]

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]

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]

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]

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

[Riccardo Brasca]

That's probably better

[Kevin Buzzard]

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]

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]

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]

You want leanproject get-mathlib-cache

[Kevin Buzzard]

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]

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]

Its working now, thanks :)

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

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]

We can also have the similar statement using the finset of roots of the minimal polynomial.

[Yaël Dillies]

(you'll be happy to hear that univ.product univ = univ :wink:)

[Riccardo Brasca]

Ah yes, and I am pretty sure that diagonal exists, so that is just the complement of the diagonal

[Yaël Dillies]

Yeah exactly. You can use univ.off_diag (docs#finset.off_diag) here.

[Riccardo Brasca]

Ah nice, I didn't spot it

[Yaël Dillies]

Damn, I really became that finset person.

[Kevin Buzzard]

diag_empty was only added to mathlib 17 hours ago!

[Riccardo Brasca]

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]

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]

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]

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

[Riccardo Brasca]

• $\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]

Great!

[Riccardo Brasca]

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]

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]

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]

But then if one wants the determinant of M matrix n n R will have to write the n and nhave 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]

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]

Well you could add a default argument / tactic I believe

[Alex J. Best]

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]

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]

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

[Yakov Pechersky]

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]

docs#linear_map.det

[Yakov Pechersky]

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

[Riccardo Brasca]

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]

Yes, using reindex is what I am proposing.

[Yakov Pechersky]

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]

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]

discriminant.eq_det_embeddings_matrix_reindex_pow_two is proved. Everything went really smoothly even with reindex :)

[Alex J. Best]

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]

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]

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]

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]

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]

Did you say refactor? :smirk:

[Riccardo Brasca]

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]

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]

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]

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

[Kevin Buzzard]

in that case the min poly is the char poly

[Kevin Buzzard]

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]

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]

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

[Alex J. Best]

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

[Chris Birkbeck]

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]

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

[Chris Birkbeck]

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]

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]

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]

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]

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

[Chris Birkbeck]

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]

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]

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]

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

Samuel seems indeed more elementary

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

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]

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]

Does Lean have matrices indexed by an arbitrary finite set ? In any case, aA: matrix I J could only have a determinant if I=J, otherwise it would be well defined up to a sign.

[Riccardo Brasca]

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]

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]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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]

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]

@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]

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]

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]

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

[Chris Birkbeck]

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

[Chris Birkbeck]

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]

I mean to prove the analogue result for the norm.

[Riccardo Brasca]

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

[Chris Birkbeck]

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]

Is norm even defined?

[Riccardo Brasca]

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]

docs#algebra.norm

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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

[Riccardo Brasca]

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]

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]

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]

norm_eq_prod_embeddings is done.

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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]

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]

neg_one_pow_eq_pow_mod_two is somewhat close

[Ruben Van de Velde]

Or neg_one_pow_eq_or with nat.neg_one_pow_eq_one_iff_even

[Riccardo Brasca]

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]

Nice work!

[Riccardo Brasca]

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]

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]

I am having a look

[Riccardo Brasca]

It's done

[Riccardo Brasca]

The main point is using docs#ring_hom.map_nat_cast

[Eric Rodriguez]

woop, thanks :D

[Riccardo Brasca]

@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]

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

[Riccardo Brasca]

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]

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

[Eric Rodriguez]

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]

Okay, Riccardo - should we just specialise the lemma to \Q? Otherwise, we need some conditions for cyclotomic n Kto be the minpoly of every primitive root. I'm going to go on a walk and think about this for a bit

[Eric Rodriguez]

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]

If you are taking about zeta'.embeddings_equiv_primitive_roots_applywe can prove it for Q.

[Riccardo Brasca]

And thanks for all your work!

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

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]

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

[Chris Birkbeck]

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

[Riccardo Brasca]

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]

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

[Chris Birkbeck]

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]

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]

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]

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]

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

[Riccardo Brasca]

That's probably better

[Kevin Buzzard]

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]

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]

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]

You want leanproject get-mathlib-cache

[Kevin Buzzard]

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]

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]

Its working now, thanks :)

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

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]

We can also have the similar statement using the finset of roots of the minimal polynomial.

[Yaël Dillies]

(you'll be happy to hear that univ.product univ = univ :wink:)

[Riccardo Brasca]

Ah yes, and I am pretty sure that diagonal exists, so that is just the complement of the diagonal

[Yaël Dillies]

Yeah exactly. You can use univ.off_diag (docs#finset.off_diag) here.

[Riccardo Brasca]

Ah nice, I didn't spot it

[Yaël Dillies]

Damn, I really became that finset person.

[Kevin Buzzard]

diag_empty was only added to mathlib 17 hours ago!

[Riccardo Brasca]

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]

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]

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]

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

[Riccardo Brasca]

• $\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]

Great!

[Riccardo Brasca]

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]

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]

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]

But then if one wants the determinant of M matrix n n R will have to write the n and nhave 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]

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]

Well you could add a default argument / tactic I believe

[Alex J. Best]

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]

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]

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

[Yakov Pechersky]

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]

docs#linear_map.det

[Yakov Pechersky]

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

[Riccardo Brasca]

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]

Yes, using reindex is what I am proposing.

[Yakov Pechersky]

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]

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]

discriminant.eq_det_embeddings_matrix_reindex_pow_two is proved. Everything went really smoothly even with reindex :)

[Alex J. Best]

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]

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]

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]

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]

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]

Did you say refactor? :smirk:

[Riccardo Brasca]

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]

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]

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]

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

[Kevin Buzzard]

in that case the min poly is the char poly

[Kevin Buzzard]

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]

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]

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

[Alex J. Best]

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

[Chris Birkbeck]

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]

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

[Chris Birkbeck]

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]

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]

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]

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]

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

[Chris Birkbeck]

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]

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]

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]

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

Samuel seems indeed more elementary

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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.

[Johan Commelin]

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]

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]

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]

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]

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]

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]

Does Lean have matrices indexed by an arbitrary finite set ? In any case, aA: matrix I J could only have a determinant if I=J, otherwise it would be well defined up to a sign.

[Riccardo Brasca]

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]

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]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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]

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]

@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]

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]

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]

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

[Chris Birkbeck]

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

[Chris Birkbeck]

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]

I mean to prove the analogue result for the norm.

[Riccardo Brasca]

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

[Chris Birkbeck]

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]

Is norm even defined?

[Riccardo Brasca]

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]

docs#algebra.norm

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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

[Riccardo Brasca]

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]

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]

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]

norm_eq_prod_embeddings is done.

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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]

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]

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]

neg_one_pow_eq_pow_mod_two is somewhat close

[Ruben Van de Velde]

Or neg_one_pow_eq_or with nat.neg_one_pow_eq_one_iff_even

[Riccardo Brasca]

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]

Nice work!

[Riccardo Brasca]

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]

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]

I am having a look

[Riccardo Brasca]

It's done

[Riccardo Brasca]

The main point is using docs#ring_hom.map_nat_cast

[Eric Rodriguez]

woop, thanks :D

[Riccardo Brasca]

@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]

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

[Riccardo Brasca]

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]

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

[Eric Rodriguez]

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]

Okay, Riccardo - should we just specialise the lemma to \Q? Otherwise, we need some conditions for cyclotomic n Kto be the minpoly of every primitive root. I'm going to go on a walk and think about this for a bit

[Eric Rodriguez]

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]

If you are taking about zeta'.embeddings_equiv_primitive_roots_applywe can prove it for Q.

[Riccardo Brasca]

And thanks for all your work!

[Riccardo Brasca]

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]

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]

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