## Stream: FLT-regular

### Topic: Further properties of the discriminant

#### Riccardo Brasca (Jan 05 2022 at 17:47):

I am going to start to prove that the discriminant of $L/K$ kills $\mathcal{O}_L/A[x]$, where $L$ is a finite extension of $K=\operatorname{Frac}(A)$ and $x$ is integral over $A$. This is the second step in the proof that $\mathcal{O}_{\mathbb{Q}(\zeta_p)}=\mathbb{Z}[\zeta_p]$.

My current pen and paper proof is the following: first of all $A[x] \subseteq \mathcal{O}_L$ (this should be trivial) and the discriminant $d$ lies in $A$ (I hope not too difficult). Now, if $z \in \mathcal{O}_L$ then we can write $z = \sum a_i x^i$, where $a_i \in K$. Multiplying this equation by $x^j$, for $j=0,\ldots, n-1$, where $n = \deg(x)$ and taking the trace, we get a $n \times n$ linear system (the $a_i$ are the unknowns) whose associated matrix has determinant $d$ by definition, so, by Cramer's rule, the $a_i$ are in $\frac{1}{d}A$ and $d$ kills $\mathcal{O}_K/A[x]$ as wanted.

If you have a better (ie more Leanable) proof, all suggestions are welcome!

#### Kevin Buzzard (Jan 05 2022 at 17:59):

Is A some integral thing? How are you writing z as sum_i a_i x^i ? Aah -- the a_i are in K, right? Wait -- what is the difference between A and O_K? Oh, you mean O_{K(x)}?

#### Riccardo Brasca (Jan 05 2022 at 18:02):

Yes, they are in $K$. Think $A=\mathbb{Z}$ and $K=\mathbb{Q}$, I am ignoring the precise assumptions here.

#### Kevin Buzzard (Jan 05 2022 at 18:02):

Then O_K=Z so A[x] \sub O_K isn't true if x isn't in Z.

#### Riccardo Brasca (Jan 05 2022 at 18:06):

Sorry $K$ is a finite extension of $\mathbb{Q}$.

#### Chris Birkbeck (Jan 05 2022 at 18:06):

Yeah I guess the a_i are in O_{K(x)}

#### Riccardo Brasca (Jan 05 2022 at 18:09):

I've corrected the proof, now $K=\operatorname{Frac}(A)$ and $x \in L$, a finite extension of $K$, is integral over $A$.

#### Kevin Buzzard (Jan 05 2022 at 18:10):

You probably also need that A is the full ring of integers of K

#### Riccardo Brasca (Jan 05 2022 at 18:10):

Kevin Buzzard said:

You probably also need that A is the full ring of integers of K

Yes, there are surely assumptions I am missing in general

#### Riccardo Brasca (Jan 05 2022 at 18:12):

I am just a little bit worried about the part "...whose associated matrix has determinant $d$ by definition, so, by Cramer's rule, the $a_i$ are in $\frac{1}{d}A$ " since I don't know if this is easy to state in Lean (but we have Cramer's rule). I will see

#### Chris Birkbeck (Jan 05 2022 at 18:16):

Riccardo Brasca said:

I am just a little bit worried about the part "...whose associated matrix has determinant $d$ by definition, so, by Cramer's rule, the $a_i$ are in $\frac{1}{d}A$ " since I don't know if this is easy to state in Lean (but we have Cramer's rule). I will see

Yes this is what I was just looking up. Crame's rule is there, I just wonder if it will be a pain to say something about the associated matrix.

#### Chris Birkbeck (Jan 05 2022 at 18:16):

I've never turned a linear map into a matrix in lean (or at least cant remember doing so), how good is this part of the API?

#### Chris Birkbeck (Jan 05 2022 at 18:19):

that said, I think this is probably the best proof to go for. This is pretty much whats in the blueprint, and thats the only proof I know of this.

#### Riccardo Brasca (Jan 05 2022 at 18:19):

I don't know, but we can even avoid talking about linear maps, the matrix associated to the linear system is literally the matrix used to define the discriminant (well, probably up to some coercion).

#### Chris Birkbeck (Jan 05 2022 at 18:19):

Aha yes I see. Nice

#### Riccardo Brasca (Jan 10 2022 at 22:07):

discr_mul_is_integral_mem_adjoin here is an almost finished proof of the following

lemma discr_mul_is_integral_mem_adjoin {R K L : Type*} [comm_ring R] [field K] [field L]
[algebra R K] [algebra K L] [algebra R L][is_scalar_tower R K L]
[is_domain R] [is_integrally_closed R] [is_separable K L]
{α : L} (hx : _root_.is_integral R α) {z : K⟮α⟯}
(hy : z ∈ integral_closure R K⟮α⟯) :
(is_integral_of_is_scalar_tower α hx : _root_.is_integral K α)).basis) • z : L) ∈
adjoin R ({α} : set L)


#### Riccardo Brasca (Jan 10 2022 at 22:08):

I will finish the proof tomorrow, but the two remaining sorry should be easy. (Then of course the proof should be golfed).

#### Kevin Buzzard (Jan 11 2022 at 06:54):

What's with all the _root_s?

#### Riccardo Brasca (Jan 11 2022 at 06:59):

Since we are in the algebra namespace we need them to avoid docs#algebra.is_integral

#### Johan Commelin (Jan 11 2022 at 07:05):

Should algebra.is_integral be made protected?

#### Johan Commelin (Jan 11 2022 at 07:05):

Or you could make a local notation for _root_.is_integral, if you want to...

#### Riccardo Brasca (Jan 11 2022 at 07:06):

I don't know about protected, but I think _root_.is_integral is more commonly used, but maybe not in the algebra namespace.

#### Riccardo Brasca (Jan 11 2022 at 09:07):

discr_mul_is_integral_mem_adjoin is sorry free. I was a little bit worried about it, but the pen and paper proof turned out to be quite leanable.

#### Riccardo Brasca (Jan 05 2022 at 17:47):

I am going to start to prove that the discriminant of $L/K$ kills $\mathcal{O}_L/A[x]$, where $L$ is a finite extension of $K=\operatorname{Frac}(A)$ and $x$ is integral over $A$. This is the second step in the proof that $\mathcal{O}_{\mathbb{Q}(\zeta_p)}=\mathbb{Z}[\zeta_p]$.

My current pen and paper proof is the following: first of all $A[x] \subseteq \mathcal{O}_L$ (this should be trivial) and the discriminant $d$ lies in $A$ (I hope not too difficult). Now, if $z \in \mathcal{O}_L$ then we can write $z = \sum a_i x^i$, where $a_i \in K$. Multiplying this equation by $x^j$, for $j=0,\ldots, n-1$, where $n = \deg(x)$ and taking the trace, we get a $n \times n$ linear system (the $a_i$ are the unknowns) whose associated matrix has determinant $d$ by definition, so, by Cramer's rule, the $a_i$ are in $\frac{1}{d}A$ and $d$ kills $\mathcal{O}_K/A[x]$ as wanted.

If you have a better (ie more Leanable) proof, all suggestions are welcome!

#### Kevin Buzzard (Jan 05 2022 at 17:59):

Is A some integral thing? How are you writing z as sum_i a_i x^i ? Aah -- the a_i are in K, right? Wait -- what is the difference between A and O_K? Oh, you mean O_{K(x)}?

#### Riccardo Brasca (Jan 05 2022 at 18:02):

Yes, they are in $K$. Think $A=\mathbb{Z}$ and $K=\mathbb{Q}$, I am ignoring the precise assumptions here.

#### Kevin Buzzard (Jan 05 2022 at 18:02):

Then O_K=Z so A[x] \sub O_K isn't true if x isn't in Z.

#### Riccardo Brasca (Jan 05 2022 at 18:06):

Sorry $K$ is a finite extension of $\mathbb{Q}$.

#### Chris Birkbeck (Jan 05 2022 at 18:06):

Yeah I guess the a_i are in O_{K(x)}

#### Riccardo Brasca (Jan 05 2022 at 18:09):

I've corrected the proof, now $K=\operatorname{Frac}(A)$ and $x \in L$, a finite extension of $K$, is integral over $A$.

#### Kevin Buzzard (Jan 05 2022 at 18:10):

You probably also need that A is the full ring of integers of K

#### Riccardo Brasca (Jan 05 2022 at 18:10):

Kevin Buzzard said:

You probably also need that A is the full ring of integers of K

Yes, there are surely assumptions I am missing in general

#### Riccardo Brasca (Jan 05 2022 at 18:12):

I am just a little bit worried about the part "...whose associated matrix has determinant $d$ by definition, so, by Cramer's rule, the $a_i$ are in $\frac{1}{d}A$ " since I don't know if this is easy to state in Lean (but we have Cramer's rule). I will see

#### Chris Birkbeck (Jan 05 2022 at 18:16):

Riccardo Brasca said:

I am just a little bit worried about the part "...whose associated matrix has determinant $d$ by definition, so, by Cramer's rule, the $a_i$ are in $\frac{1}{d}A$ " since I don't know if this is easy to state in Lean (but we have Cramer's rule). I will see

Yes this is what I was just looking up. Crame's rule is there, I just wonder if it will be a pain to say something about the associated matrix.

#### Chris Birkbeck (Jan 05 2022 at 18:16):

I've never turned a linear map into a matrix in lean (or at least cant remember doing so), how good is this part of the API?

#### Chris Birkbeck (Jan 05 2022 at 18:19):

that said, I think this is probably the best proof to go for. This is pretty much whats in the blueprint, and thats the only proof I know of this.

#### Riccardo Brasca (Jan 05 2022 at 18:19):

I don't know, but we can even avoid talking about linear maps, the matrix associated to the linear system is literally the matrix used to define the discriminant (well, probably up to some coercion).

#### Chris Birkbeck (Jan 05 2022 at 18:19):

Aha yes I see. Nice

#### Riccardo Brasca (Jan 10 2022 at 22:07):

discr_mul_is_integral_mem_adjoin here is an almost finished proof of the following

lemma discr_mul_is_integral_mem_adjoin {R K L : Type*} [comm_ring R] [field K] [field L]
[algebra R K] [algebra K L] [algebra R L][is_scalar_tower R K L]
[is_domain R] [is_integrally_closed R] [is_fraction_ring R K] [is_separable K L]
{α : L} (hx : _root_.is_integral R α) {z : K⟮α⟯}
(hz : _root_.is_integral R z) :
(is_integral_of_is_scalar_tower α hx : _root_.is_integral K α)).basis) • z : L) ∈
adjoin R ({α} : set L)


#### Riccardo Brasca (Jan 10 2022 at 22:08):

I will finish the proof tomorrow, but the two remaining sorry should be easy. (Then of course the proof should be golfed).

#### Kevin Buzzard (Jan 11 2022 at 06:54):

What's with all the _root_s?

#### Riccardo Brasca (Jan 11 2022 at 06:59):

Since we are in the algebra namespace we need them to avoid docs#algebra.is_integral

#### Johan Commelin (Jan 11 2022 at 07:05):

Should algebra.is_integral be made protected?

#### Johan Commelin (Jan 11 2022 at 07:05):

Or you could make a local notation for _root_.is_integral, if you want to...

#### Riccardo Brasca (Jan 11 2022 at 07:06):

I don't know about protected, but I think _root_.is_integral is more commonly used, but maybe not in the algebra namespace.

#### Riccardo Brasca (Jan 11 2022 at 09:07):

discr_mul_is_integral_mem_adjoin is sorry free. I was a little bit worried about it, but the pen and paper proof turned out to be quite leanable.

Last updated: Dec 20 2023 at 11:08 UTC