Zulip Chat Archive

Stream: new members

Topic: Strange behavior of `mul_eq_zero`


view this post on Zulip 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) :=
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!

view this post on Zulip Alex J. Best (Nov 15 2020 at 00:06):

I get an error at not_is_unit.

view this post on Zulip Alex J. Best (Nov 15 2020 at 00:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Nov 15 2020 at 00:14):

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

view this post on Zulip 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.

view this post on Zulip 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]?

view this post on Zulip 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

view this post on Zulip Riccardo Brasca (Nov 15 2020 at 00:17):

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

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Nov 15 2020 at 00:55):

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

view this post on Zulip 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.

view this post on Zulip Aaron Anderson (Nov 15 2020 at 04:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: May 15 2021 at 22:14 UTC