Develop basic theory of integrally closed domain

[riccardobrasca]

To develop algebraic number theory we need basic results about integrally closed domains.

For example, Gauss' lemma is true in such generality (at least for monic polynomials): this would allow to generalize certains results about the minimal polyomial, that are now stated for GCD domains.

[riccardobrasca]

Here is a quick math proof of what I mean.

Let R be an integrally closed domain with fraction field K and let f : polynomial R be monic. If f = g * h over K, then g and h have coefficients in R. Indeed, we can assume that g and h are monic (by factoring out the leading coefficients). If L is a splitting field of f, then writing f as a product of linear factors over L we see that both g and h are product of factors of the form X - a, where a ranges over a subset of the roos of f, that are algebraic over R by assumption. By Vieta, the coefficients of g and h are also algebraic over R, but lie K and so they are in R.

[alreadydone]

I have been able to prove (full proof):

theorem eq_map_of_dvd {R} [comm_ring R] [is_domain R] [is_integrally_closed R]
  {f : R[X]} (hf : f.monic) (g : (fraction_ring R)[X]) (hg : g.monic)
  (hd : g ∣ f.map (algebra_map R _)) : ∃ g' : R[X], g'.map (algebra_map R _) = g :=

I think the next step is to generalize most results about minpoly from fields to integrally closed domains. To apply these results to GCD domains, we'd need to show that GCD domains are integrally closed. (cc'ing @erdOne as he's working on some commutative algebra recently.)

[riccardobrasca]

I have been able to prove (full proof):

theorem eq_map_of_dvd {R} [comm_ring R] [is_domain R] [is_integrally_closed R]
  {f : R[X]} (hf : f.monic) (g : (fraction_ring R)[X]) (hg : g.monic)
  (hd : g ∣ f.map (algebra_map R _)) : ∃ g' : R[X], g'.map (algebra_map R _) = g :=

I think the next step is to generalize most results about minpoly from fields to integrally closed domains. To apply these results to GCD domains, we'd need to show that GCD domains are integrally closed. (cc'ing @erdOne as he's working on some commutative algebra recently.)

This is great!! What we want is to generalize in https://leanprover-community.github.io/mathlib_docs/ring_theory/polynomial/gauss_lemma.html. Once this is done generalizing the results about minimal polynomial should be trivial.

[erdOne]

@alreadydone I could do that if you are not planning to. In fact this result will be useful for me as well, since I am two PR's away from showing that valuation rings are GCD domains.

[alreadydone]

@erdOne You mean showing that GCD domains are integrally closed right? I have only found a reference for a proof, but have not started working on it, and you're welcome to take it up!

@riccardobrasca I looked at the Gauss lemma file and I think it's easy to generalize the irreducible_iff and dvd_iff results to monic polynomials over integrally closed domains. In fact, when p is monic the dvd_iff result is an easy consequence of polynomial.map_dvd_map and doesn't require integral-closedness, and q doesn't need to be primitive (this condition seems redundant in the original statement as well). I think the strongest result to generalize is probably minpoly.dvd; the generalization would say that the annihilator ideal in R[X] of an integral element in an R-algebra is generated by its minpoly for integrally closed R, and it seems to require direct application of this eq_map_of_dvd result I just showed.

A bit of Google/literature search reveals that at least the primitive version of the irreducible_iff result cannot be generalized to all integrally closed domains: we at least need that R is integrally closed with trivial Picard group, according to the paper Factorization of certain sets of polynomials an integral domain. Reasoning: the irreducible_iff result is obviously equivalent to the "property (P)" for primitive polynomials: if the polynomial factors into a product of positive degree polynomials over the field of fractions, it also does over the ring R itself. Primitivity is weaker than content (ideal generated by the coefficients) being the unit ideal. The paper shows property (P) for all polynomials with content=(1) is equivalent to integrally closed + Pic(R)=0. Moreover property (P) for all polynomials is equivalent to R Schreier. So the strength of the irreducible_iff result lies somewhere between IC+Pic(R)=0 and Schreier. In fact it's between the stronger condition of IC+Cl_t(R)=0 and Schreier, where the former condition corresponds to superprimitive polynomials.

Since the primitive version doesn't hold in general, I'll focus on the monic case for now.

[riccardobrasca]

Sorry, I was also thinking about the monic case, that is the most important one in my opinion.

[riccardobrasca]

I have been able to prove (full proof):

theorem eq_map_of_dvd {R} [comm_ring R] [is_domain R] [is_integrally_closed R]
  {f : R[X]} (hf : f.monic) (g : (fraction_ring R)[X]) (hg : g.monic)
  (hd : g ∣ f.map (algebra_map R _)) : ∃ g' : R[X], g'.map (algebra_map R _) = g :=

I think the next step is to generalize most results about minpoly from fields to integrally closed domains. To apply these results to GCD domains, we'd need to show that GCD domains are integrally closed. (cc'ing @erdOne as he's working on some commutative algebra recently.)

@alreadydone Are you going to PR this?

[alreadydone]

@riccardobrasca I haven't got around to generalize the Gauss lemmas and minpoly, and I'm not currently working on them; whether you want to do the generalization yourself or simply PR my proof as is, please feel free! I'd also suggest that you add a TODO saying that we would like redefine polynomial.splits and generalize splitting_field to be able to generalize the proof to non-domains as in https://mathoverflow.net/a/123526/3332.

[Paul-Lez]

cc @riccardobrasca

I'm PRing @alreadydone's result eq_map_of_dvd in #18021, along with the generalization of minpoly.dvd. I'm hoping to deal with Gauss' lemma in a subsequent PR.