Zulip Chat Archive

Stream: new members

Topic: Strange behavior of `mul_eq_zero`

Riccardo Brasca (Nov 14 2020 at 23:58):

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) :=
  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

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 (Nov 15 2020 at 00:06):

I get an error at not_is_unit.

Alex J. Best (Nov 15 2020 at 00:06):

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

Aaron Anderson (Nov 15 2020 at 00:10):

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 (Nov 15 2020 at 00:11):

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 (Nov 15 2020 at 00:12):

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

Riccardo Brasca (Nov 15 2020 at 00:14):

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

Alex J. Best (Nov 15 2020 at 00:15):

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 (Nov 15 2020 at 00:17):

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 (Nov 15 2020 at 00:17):

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 (Nov 15 2020 at 00:17):

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

Aaron Anderson (Nov 15 2020 at 00:18):

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 (Nov 15 2020 at 00:55):

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

Aaron Anderson (Nov 15 2020 at 04:41):

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

Aaron Anderson (Nov 15 2020 at 04:41):

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

Aaron Anderson (Nov 15 2020 at 04:42):

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 (Nov 15 2020 at 06:33):

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 (Nov 15 2020 at 10:17):

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 PR[X]P \in R[X] is primitive and P=Q1Q2P = Q_1 \cdot Q_2 is a non trivial factorization in K[X]K[X] then essentially Q1Q_1 and Q2Q_2 are already in R[X]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 KK considering only multiplication by elements of RR and he proves Gauss's lemma in this context.)

Last updated: Dec 20 2023 at 11:08 UTC