Further properties of the discriminant

Stream: FLT-regular

[Riccardo Brasca]

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]

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]

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

[Kevin Buzzard]

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

[Riccardo Brasca]

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

[Chris Birkbeck]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

Aha yes I see. Nice

[Riccardo Brasca]

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⟮α⟯) :
  ((discr K (adjoin.power_basis
  (is_integral_of_is_scalar_tower α hx : _root_.is_integral K α)).basis) • z : L) ∈
  adjoin R ({α} : set L)

[Riccardo Brasca]

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

[Kevin Buzzard]

What's with all the _root_s?

[Riccardo Brasca]

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

[Johan Commelin]

Should algebra.is_integral be made protected?

[Johan Commelin]

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

[Riccardo Brasca]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Riccardo Brasca]

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

[Chris Birkbeck]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

Aha yes I see. Nice

[Riccardo Brasca]

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) :
  ((discr K (adjoin.power_basis
  (is_integral_of_is_scalar_tower α hx : _root_.is_integral K α)).basis) • z : L) ∈
  adjoin R ({α} : set L)

[Riccardo Brasca]

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

[Kevin Buzzard]

What's with all the _root_s?

[Riccardo Brasca]

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

[Johan Commelin]

Should algebra.is_integral be made protected?

[Johan Commelin]

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

[Riccardo Brasca]

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]

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.