Power basis of `adjoin R x`

Stream: Is there code for X?

[Paul Lezeau]

Do we have something of the form

variables {R S : Type*} [comm_ring R] [comm_ring S] [is_domain R] [is_domain S]
variables [is_dedekind_domain S] [algebra R S] {x: S}

example (h : function.injective (algebra_map R S)) (hx : is_integral R x) :
  power_basis R (algebra.adjoin R ({x} : set S)) := sorry

eventually with some extra hypotheses on R and S ? The closest I've found is algebra.adjoin.power_basis', but this requires R to be a normalized_gcd_monoid, which is something I'm trying to avoid.

[Junyan Xu]

Yeah Dedekind domains are integrally closed so this should be valid. I did something towards generalizing the theory of docs#minpoly to integrally closed domains but it's not yet PR'd.

[Paul Lezeau]

Ah that's great! I'll be need something along those lines for the general case of the Dedekind-Kummer theorem, so I'm happy to help with the PR process:)

[Riccardo Brasca]

I am almost sure we don't have it, unless S is a gcd thing. But please please generalize gauss lemma to integrally closed domain (and I mean, open the PR :stuck_out_tongue_wink: )

[Riccardo Brasca]

The main result is docs#adjoin_root.minpoly.equiv_adjoin, whose proof needs docs#minpoly.gcd_domain_dvd, that should be generalized to integrally closed domains.

[Paul Lezeau]

Just to be sure @Junyan Xu is this something you're planning on PRing, or should I do it? :smile:

[Junyan Xu]

@Paul Lezeau Thanks for the ping. As Riccardo said, the next step is to generalize the Gauss lemmas, and then generalize results about minpoly. Unfortunately I currently have two PRs that are blocking other PRs/works, so I guess I'll only return to this after one week or so. Please feel free to if you want to work on this!

[Paul Lezeau]

Okay fair enough! I'll probably be quite busy too in the next week or so, but I could start having a look after that!

[Paul Lezeau]

Have you already done anything/written code in that direction?

[Junyan Xu]

The main result mentioned in the issue #11523 is that if R is integrally closed with K its field of fractions, then any monic factor in K[X] of a monic polynomial in R[X] actually lies in R[X]. I think you can show relatively easily that the R-minpoly of an integral element in S is the same as the K-minpoly: both are monic, and the latter always divides the former (docs#minpoly.dvd).

To get the power basis, you need that the kernel of the map R[X]->S sending X to x is generated by the R-minpoly. For any element in the kernel, if you take the remainder modulo the R-minpoly, you get something of lower degree which is still in the kernel, so the K-minpoly divides it, so it's either zero or has degree at least the degree of the K-minpoly, which is the same as the degree of the R-minpoly, so it can only be zero.

[Paul Lezeau]

Ok cool! I'll start working on that as soon as I find some time

[Paul Lezeau]

@Junyan Xu In the end I haven't really found time to work on this and probably won't for the next two weeks, so feel free to do it!

[Riccardo Brasca]

Feel free to ping me if you open a PR.

[Paul Lezeau]

@Junyan Xu Have you been able to make any progress on this ? :grinning_face_with_smiling_eyes:

[Junyan Xu]

@Paul Lezeau No sorry, my Lean time was mostly spent on associativity of the elliptic curve group law lately :face_palm:

[Paul Lezeau]

Ah that's alright no worries ;)

[Paul Lezeau]

Hey @Junyan Xu, have you been able to work on this in the end ? :grinning_face_with_smiling_eyes:

[Paul Lezeau]

Otherwise I might start working on it again

[Junyan Xu]

@Paul Lezeau No updates from my side, and I'm not currently working on it.

[Paul Lezeau]

Ok cool, I'll get back to working on it :)

[Paul Lezeau]

@Riccardo Brasca I've made some good progress on this, and I'm hoping to open some PRs soon, including some work towards the generalization of the Gauss lemma to integrally closed rings. Would you be alright with reviewing the PRs?

[Eric Rodriguez]

I'll review them too so that it can be a quick maintainer merge :)

[Paul Lezeau]

Eric Rodriguez said:

I'll review them too so that it can be a quick maintainer merge :)

Thanks a lot, I'll make the first PR soonish :)

[Paul Lezeau]

@Eric Rodriguez here's a first PR : #18021. It still needs a little cleaning up, but it should be ready tomorrow hopefully