[Merged by Bors] - chore(field_theory/minimal_polynomial): generalize irreducible

[riccardobrasca]

I have removed the assumption that the base ring is a field for a minimal polynomial to be irreducible.

The proof is simple but long, it should be possible to use wlog to shorten it, but I do not understand how to do it...

[awainverse]

I think this can be golfed down with rcases and other tricks, but I think it's worth considering whether the approach currently taken with fields. Is it actually possible (over an integral domain at least) to have an integral element whose minimal (monic) polynomial is not the minimal-degree polynomial with that element as a root?

[riccardobrasca]

If R is not integrally closed, take any a ∈ K (K is the fraction field) that is integral over R and not in R. Then it satisfies some monic polynomial with coefficients in R, by definition, and it is a root of X - a : polynomial K.

More concretely, if you take R = ℤ[√5] = {a + b√5 s.t a b ∈ ℤ}, then a = (1 + √5)/2 is a root of X ^ 2 - X - 1, so is integral over R, but of course its minimal polynomial over K is just X - a.

I do not know the minimal assumption to have that minimal polynomials are primes (UFD? integrally closed?), but some results in the file definitely do not work over any domain.

[Vierkantor]

Thanks, this is very useful and the code looks clean! I would like to help with de-duplicating the proof when I have some time, so I have self-requested a review to remind me (you are welcome to go ahead without me of course!).

[riccardobrasca]

The proof is very linear, it is just what I would write on paper, except that I wouldn't do it for both factors. The annoying part is that by definition the minimal polynomial has minimal degree among the monic polynomials that have x has root, and the two factors are not necessarily monic. Maybe a preliminary lemma saying that the minimal polynomial has minimal degree among the polynomials with invertible leading coefficients could short the proof a bit, but not that much I believe.

[Vierkantor]

These would be my suggestions to generalize and deduplicate the code.

[riccardobrasca]

I can also add that for GCD domains the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. It should be just a few lines.

[Vierkantor]

If it's not too much work for you, I would appreciate it. Otherwise I'm happy with merging it after someone else has looked at my additions. Thanks for your work!

[riccardobrasca]

I have added gcd_domain_eq_field_fractions.

The statement is almost as long as the proof, but if I do not put @is_integral_of_is_scalar_tower α f.codomain γ _ _ _ _ _ _ _ x hx Lean is not happy, I think he tries to use β instead of f.codomain somehow (of course β = f.codomain, but there is no algebra structure of β). Also, I am not completely sure this is the best way of saying γ is a β-algebra, where β is the fraction field of α and in particular γ is a α-algebra.

[riccardobrasca]

I have no idea why CI fails on a file that I didn't touch... I modified irreducible, but in the minimal_polynomial namespace, so it shouldn't have any impact on the irreducible where CI failed.

[riccardobrasca]

It seems that in src/number_theory/sum_two_squares.lean Lean is trying to use irreducible_iff_prime instead of principal_ideal_ring.irreducible_iff_prime (if I open the file in my branch with VS and I click to go to definition it open nat.irreducible_iff_prime, if I do the same in a fresh mathlib folder it opens principal_ideal_ring.irreducible_iff_prime).

[Vierkantor]

Two small changes and it looks good to me. Thanks 🎉

bors d+

[Vierkantor]

Suggested change

	(ne_of_lt (minimal_polynomial.degree_pos H5)).symm,
	(ne_of_lt (minimal_polynomial.degree_pos H5)).symm,

[bors]

✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[riccardobrasca]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint style
• Run tests
• Lint mathlib