Strange behavior of `mul_eq_zero`

Stream: new members

[Riccardo Brasca]

I am trying to prove that the minimal polynomial of an element x is irreducible, without the assumption that the base ring is a field, but only an integral domain. It's rather annoying (if someone see a quick way to do it all suggestions are welcome...). At some point I need to use that if the minimal polynomial is the product a * b then x is a root of a or of b: this should be easy, and I wanted to use mul_eq_zero as in the following code

import field_theory.minimal_polynomial

universes u v

open_locale classical

variables {α : Type u} {β : Type v}

namespace minimal_polynomial

variables [integral_domain α] [ring β] [algebra α β] {x : β} (hx : is_integral α x)

lemma test [integral_domain β] :  _root_.irreducible (minimal_polynomial hx) :=
begin
  have not_unit : ¬ is_unit (minimal_polynomial hx),
  { sorry },
  cases irreducible_or_factor (minimal_polynomial hx) not_unit with hirr hred,
  { exact hirr },
  obtain ⟨a, hred⟩ := hred,
  obtain ⟨b, hred⟩ := hred,
  have hzero : polynomial.aeval x a = 0 ∨ polynomial.aeval x b = 0,
  { apply mul_eq_zero.1,
    { sorry },
    have h₁ := integral_domain.to_domain β,
    have h₂ := @domain.to_no_zero_divisors β h₁,
    --exact h₂ does not work
    sorry
  },
  sorry
end

end minimal_polynomial

Ignore the sorry, my problem is where the comment is. As you can see mul_eq_zero asks to prove no_zero_divisors β, that is already strange since there is [integral_domain β] in the assumptions, but even if I try to do it it complains with some errors that I do not understand. Indeed h₂ seems to be exactly what it wants, but exact h₂ doesn't work.

What's going on? Thank you!

[Alex J. Best]

I get an error at not_is_unit.

[Alex J. Best]

Could it be becasue you have ring beta and integral domain beta?

[Aaron Anderson]

Alex J. Best said:

Could it be becasue you have ring beta and integral domain beta?

I tried replacing the original [ring beta] with [integral_domain beta] and deleting the second [integral_domain beta], it fixed this.

[Aaron Anderson]

It might not fix not_is_unit, because not_is_unit currently requires a field, but @Riccardo Brasca probably has modified not_is_unit locally.

[Riccardo Brasca]

@Alex J. Best Ah yes sorry! That's because I have modified not_is_unit in minimal_polynomial, now it should work.

[Riccardo Brasca]

Ah ok, I still do not understand clearly what to do to add assumptions like this...

[Alex J. Best]

integral domain includes a ring structure, so when you have ring X and integral_domain X you have introduced two (independent) ring structures on the same type which confuses lean.

[Riccardo Brasca]

But what is the general strategy if I am working with variable [ring R] defined somewhere and in a lemma I need [integral_domain R]?

[Aaron Anderson]

The best way to deal with this is to use the section command to have a section of your file where you start by defining variables [ring beta] and whatever other instances you want, for your general ring theorems, and then a new section starting with variables [integral_domain beta] for your integral domain theorems

[Riccardo Brasca]

@Aaron Anderson You almost answered my question before I asked it!

[Aaron Anderson]

Another potential strategy is to use [ring R] and then later [is_integral_domain R], but you won't always have that flexibility, and I'd still recommend going with the multiple sections.

[Riccardo Brasca]

I've put the (ugly) proof in quote #5006.

[Aaron Anderson]

I could help golf this down, but the way this currently works for fields is a sequence of lemmas.

[Aaron Anderson]

Do we know if some of them might work for a wider class of domains?

[Aaron Anderson]

Well, I guess we know that the second-to-last lemma, minimal_polynomial.prime, definitely works for gcd or unique factorization domains, because that's equivalent to irreducible there

[Aaron Anderson]

I think that the whole slew of results for fields should also hold for integrally closed domains - I think I read that minimal polynomials over integrally closed domains equal the minimal polynomial over the fraction field, which is really the key result here

[Riccardo Brasca]

I think that at the end everything boils down to en even stronger version of Gauss's lemma than the one I asked yesterday: If $P \in R[X]$ is primitive and $P = Q_1 \cdot Q_2$ is a non trivial factorization in $K[X]$ then essentially $Q_1$ and $Q_2$ are already in $R[X]$ (I mean, up to multiplication and division by a scalar). For PID I have a simple proof, I do not know a proof for integrally closed domain (if it is true...) and here http://www-users.math.umn.edu/~garrett/m/algebra/notes/12.pdf there is a proof for UFD that seems to be a proof for GCD domains. (Essentially he consider divisibility in $K$ considering only multiplication by elements of $R$ and he proves Gauss's lemma in this context.)