Show that no polynomial ring with more than one indeterminat

Stream: new members

[Nick_adfor]

My goal is to show that no polynomial ring with more than one indeterminate is a PID.
Now I have written this:

import Mathlib

open MvPolynomial Ideal

variable (R : Type*) [Field R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ]

theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by
  -- Select two distinct variables i and j from σ
  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h

  let x : MvPolynomial σ R := X i
  let y : MvPolynomial σ R := X j

  -- Consider the ideal I = (x, y)
  let I := span ({x, y} : Set (MvPolynomial σ R))

  -- First part: I ≠ ⊤
  have proper : I ≠ ⊤ := by
    intro hI
    have one_mem : (1 : MvPolynomial σ R) ∈ I := by rw [hI]; trivial

    obtain ⟨a, b, eq1⟩ := mem_span_pair.mp one_mem

    have const_eq : coeff (0 : σ →₀ ℕ) 1 = coeff (0 : σ →₀ ℕ) (a * x + b * y) := by
      rw [eq1]

    have coeff_x_zero : coeff (0 : σ →₀ ℕ) x = 0 := by
      rw [@coeff_zero_X]

    have coeff_y_zero : coeff (0 : σ →₀ ℕ) y = 0 := by
      rw [@coeff_zero_X]

    have rhs_const : coeff (0 : σ →₀ ℕ) (a * x + b * y) = 0 := by
      rw [coeff_add, coeff_mul, coeff_mul]
      simp
      rw [coeff_x_zero, coeff_y_zero]
      simp

    rw [coeff_one, rhs_const] at const_eq
    exact one_ne_zero const_eq

  -- Second part: Assume PID and derive a contradiction
  intro hPID
  -- Correct way to get the principal ideal generator
  haveI := hPID
  obtain ⟨f, hf⟩ := (IsPrincipalIdealRing.principal I).principal

  -- x and y are both in I
  have x_mem : x ∈ I := subset_span (by simp)
  have y_mem : y ∈ I := subset_span (by simp)
  rw [hf] at x_mem y_mem

  -- Therefore, there exist a, b such that x = a*f and y = b*f
  obtain ⟨a, ha⟩ := mem_span_singleton.mp x_mem
  obtain ⟨b, hb⟩ := mem_span_singleton.mp y_mem

  -- Key step: Prove that f must be a unit
  have : IsUnit f := by
    have : coeff (0 : σ →₀ ℕ) x = coeff (0 : σ →₀ ℕ) (f * a) := by rw [ha]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true, ite_false, coeff_mul, zero_mul, add_zero] at this
    -- Now this : (coeff 0 f) * (coeff 0 a) = 0
    have coeff_f_zero_of_a : coeff (0 : σ →₀ ℕ) a ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by sorry

    have : coeff (0 : σ →₀ ℕ) y = coeff (0 : σ →₀ ℕ) (f * b) := by rw [hb]
    simp only [coeff_X, ne_eq, hij.symm, not_false_eq_true, ite_false, coeff_mul, zero_mul, add_zero] at this
    have coeff_f_zero_of_b : coeff (0 : σ →₀ ℕ) b ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by sorry

--(to be continued)

But I have no idea about the two sorry. Can anyone give a hand?

[Nick_adfor]

(deleted)

[Ruben Van de Velde]

simp [coeff_f_zero_of_a ha_ne_zero] solves it

[Nick_adfor]

Ruben Van de Velde said:

simp [coeff_f_zero_of_a ha_ne_zero] solves it

Sorry, but it cannot work. In what part do you use this simp? I was trying to prove coeff_f_zero_of_a. How can I use it in simp?

[Ruben Van de Velde]

      have : coeff 0 f * coeff 0 a = 0 := by
        simp [coeff_f_zero_of_a ha_ne_zero]

[Nick_adfor]

Ruben Van de Velde said:

      have : coeff 0 f * coeff 0 a = 0 := by
        simp [coeff_f_zero_of_a ha_ne_zero]

I have to say that it cannot work

Lean 4 Web with my code

[Ruben Van de Velde]

Oh, that's because your split code confused me

[Ruben Van de Velde]

What's your pen-and-paper argument?

[Nick_adfor]

Ruben Van de Velde said:

What's your pen-and-paper argument?

Theorem:

No polynomial ring with more than one indeterminate is a PID.

Proof:

Assume card(σ) ≥ 2. Since the set of variables has at least two elements, we can choose two distinct variables i and j from σ.

Let x = X i and y = X j be the corresponding variables in the multivariable polynomial ring.

Now define the ideal

I := span {x, y} ⊂ MvPolynomial σ R.

Step 1: Show that I is a proper ideal (i.e., I ≠ ⊤)

Suppose for contradiction that I = ⊤. Then 1 ∈ I, so there exist polynomials a and b such that:

1 = a * x + b * y

Taking the constant term (i.e., the coefficient of 0 ∈ σ →₀ ℕ) on both sides:

coeff₀(1) = coeff₀(a * x + b * y)

But since both x and y have no constant term, any product with them also has zero constant term. So the right-hand side is 0, while the left-hand side is 1, contradiction.

Therefore, I is a proper ideal.

Step 2: Suppose for contradiction that MvPolynomial σ R is a principal ideal ring

If so, then the ideal I = (f) for some polynomial f. That means:

x ∈ (f), so x = a * f for some a

y ∈ (f), so y = b * f for some b

Let’s analyze the structure of f.

Case 1: coeff₀(f) = 0

We know:

degreeOf i (a * f) ≥ 1

degreeOf j (b * f) ≥ 1

Also, since degrees are nonnegative:

degreeOf i f ≥ 1 - degreeOf i a ≥ 1 - 0 = 1

degreeOf j f ≥ 1 - degreeOf j b ≥ 1 - 0 = 1

Thus, f must involve both variables i and j, meaning i ∈ support(f) and j ∈ support(f).

But x = a * f, and so support(f) ⊆ support(x). Since x = X i, we know support(x) = {i}, so j ∉ support(f). Contradiction.

Case 2: coeff₀(f) ≠ 0

Then f has a nonzero constant term, which means f is a unit in MvPolynomial σ R (units are constant polynomials with nonzero coefficients).

So I = (f) = ⊤, again contradicting the earlier result that I ≠ ⊤.

Conclusion:

In both cases, assuming I is principal leads to a contradiction. Therefore, MvPolynomial σ R is not a principal ideal ring when card(σ) ≥ 2.

∎

[Luigi Massacci]

Here you go:

    have h_mul_zero : coeff (0 : σ →₀ ℕ) x = coeff (0 : σ →₀ ℕ) (f * a) := by rw [ha]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero
    have coeff_f_zero_of_a : coeff (0 : σ →₀ ℕ) a ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 a = 0 := by
        rw [← h_mul_zero, ← coeff_zero_X i]

[Luigi Massacci]

The lemma you needed was that the zeroth term is the product of zeroth terms (so Finset.antidiagonal_zero) thought I wouldn't be surprised if there's already a lemma about it expresed directly for polynomials

[Nick_adfor]

Ruben Van de Velde said:

What's your pen-and-paper argument?

Now following my pen-and-paper argument and Luigi Massacci's help, I try to accomplish my code this way:

import Mathlib

open MvPolynomial Ideal

variable (R : Type*) [Field R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ]

theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by

  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h

  let x : MvPolynomial σ R := X i
  let y : MvPolynomial σ R := X j


  let I := span ({x, y} : Set (MvPolynomial σ R))

  have proper : I ≠ ⊤ := by
    intro hI
    have one_mem : (1 : MvPolynomial σ R) ∈ I := by rw [hI]; trivial

    obtain ⟨a, b, eq1⟩ := mem_span_pair.mp one_mem

    have const_eq : coeff (0 : σ →₀ ℕ) 1 = coeff (0 : σ →₀ ℕ) (a * x + b * y) := by
      rw [eq1]

    have coeff_x_zero : coeff (0 : σ →₀ ℕ) x = 0 := by
      rw [@coeff_zero_X]

    have coeff_y_zero : coeff (0 : σ →₀ ℕ) y = 0 := by
      rw [@coeff_zero_X]

    have rhs_const : coeff (0 : σ →₀ ℕ) (a * x + b * y) = 0 := by
      rw [coeff_add, coeff_mul, coeff_mul]
      simp
      rw [coeff_x_zero, coeff_y_zero]
      simp

    rw [coeff_one, rhs_const] at const_eq
    exact one_ne_zero const_eq


  intro hPID

  haveI := hPID
  obtain ⟨f, hf⟩ := (IsPrincipalIdealRing.principal I).principal


  have x_mem : x ∈ I := subset_span (by simp)
  have y_mem : y ∈ I := subset_span (by simp)
  rw [hf] at x_mem y_mem

  obtain ⟨a, ha⟩ := mem_span_singleton.mp x_mem
  obtain ⟨b, hb⟩ := mem_span_singleton.mp y_mem


  have : IsUnit f := by
    have h_mul_zero_x : coeff (0 : σ →₀ ℕ) x = coeff (0 : σ →₀ ℕ) (f * a) := by rw [ha]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_x
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_x
    have coeff_f_zero_of_a : coeff (0 : σ →₀ ℕ) a ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 a = 0 := by
        rw [← h_mul_zero_x, ← coeff_zero_X i]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    have h_mul_zero_y : coeff (0 : σ →₀ ℕ) y = coeff (0 : σ →₀ ℕ) (f * b) := by rw [hb]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_y
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_y
    have coeff_f_zero_of_b : coeff (0 : σ →₀ ℕ) b ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 b = 0 := by
        rw [← h_mul_zero_y, ← coeff_zero_X j]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    by_cases ha0 : coeff (0 : σ →₀ ℕ) a ≠ 0
    · have hf0 := coeff_f_zero_of_a ha0
      have hfx : coeff 0 (f * a) = coeff 0 f * coeff 0 a := by
        simp only [coeff_mul, Finset.antidiagonal_zero, Finset.sum_singleton]
      rw [hf0, zero_mul] at hfx
      rw [← h_mul_zero_x, coeff_zero_X i] at hfx
      exact ha0 hfx
    by_cases hb0 : coeff (0 : σ →₀ ℕ) b ≠ 0
    · have hf0 := coeff_f_zero_of_b hb0
      have hfy : coeff 0 (f * b) = coeff 0 f * coeff 0 b := by
        simp only [coeff_mul, Finset.antidiagonal_zero, Finset.sum_singleton]
      rw [hf0, zero_mul] at hfy
      rw [← h_mul_zero_y, coeff_zero_X j] at hfy
      exact hb0 hfy
    -- If both a and b have zero constant term, then f must be a unit
    push_neg at ha0 hb0
    rw [← mem_span_singleton] at hf
    refine isUnit_of_dvd_one ?_
    have : 1 ∈ span {f} := by
      rw [← hf]
      exact Ideal.eq_top_iff_one.mp rfl
    exact mem_span_singleton.mp this

  -- Now we know f is a unit, which implies I = (1), contradicting properness
  have I_top : I = ⊤ := by
    rw [hf]
    exact Ideal.span_singleton_eq_top.mp (IsUnit.span_singleton_eq_top this)
  exact proper I_top

Absolutely there is still something wrong: rw [← h_mul_zero_x, coeff_zero_X i] at hfx,  rw [← mem_span_singleton] at hf, exact Ideal.span_singleton_eq_top.mp (IsUnit.span_singleton_eq_top this).

Lean 4 Web with my new code

[Nick_adfor]

(deleted)

[Nick_adfor]

The pen-and-paper writing is as follows:

Case 1: coeff₀(a) ≠ 0

Then:

coeff₀(x) = coeff₀(f * a) = coeff₀(f) * coeff₀(a)

But coeff₀(x) = 0, and coeff₀(a) ≠ 0, so:

coeff₀(f) = 0

Case 2: coeff₀(b) ≠ 0

Same reasoning:

coeff₀(y) = coeff₀(f * b) = coeff₀(f) * coeff₀(b)

But coeff₀(y) = 0, and coeff₀(b) ≠ 0, so:

coeff₀(f) = 0

Case 3: coeff₀(a) = 0 and coeff₀(b) = 0

Then both a and b have no constant term — they lie in the augmentation ideal 𝔪 := { g | coeff₀(g) = 0 }.

Hence:

f * a ∈ 𝔪, so x ∈ 𝔪

f * b ∈ 𝔪, so y ∈ 𝔪

So the ideal ⟨x, y⟩ ⊆ 𝔪, but then f cannot generate the unit ideal unless f is a unit (because 𝔪 is a proper ideal, not the whole ring).

So in this case, f must be a unit.

The code above still have something wrong, and I cannot find an appropriate one in rw[]... : (

[Kenny Lau]

@Nick_adfor you've posted many snippets of code, sometimes with a full link, and sometimes without; which link are we meant to follow now?

[Nick_adfor]

Kenny Lau said:

Nick_adfor you've posted many snippets of code, sometimes with a full link, and sometimes without; which link are we meant to follow now?

OK, I've deleted all the code snippets, leaving only the complete code.

[Kenny Lau]

it seems like you need this theorem which is unfortunately not in mathlib(?):

theorem MvPolynomial.coeff_zero_mul {α : Type*} {R : Type*} [CommSemiring R] (p q : MvPolynomial α R) :
    coeff 0 (p * q) = coeff 0 p * coeff 0 q := by
  classical
  simp [coeff_mul]

[Kenny Lau]

you can add this theorem to the top

[Nick_adfor]

Kenny Lau said:

it seems like you need this theorem which is unfortunately not in mathlib(?):

theorem MvPolynomial.coeff_zero_mul {α : Type*} {R : Type*} [CommSemiring R] (p q : MvPolynomial α R) :
    coeff 0 (p * q) = coeff 0 p * coeff 0 q := by
  classical
  simp [coeff_mul]

Oh, it is already in mathlib

@[simp]
theorem Polynomial.mul_coeff_zero{R : Type u} [Semiring R] (p q : Polynomial R) :
(p * q).coeff 0 = p.coeff 0 * q.coeff 0

[Kenny Lau]

@Nick_adfor no, Polynomial and MvPolynomial are different

[Nick_adfor]

I just checked my code, seeming that I do not use this theorem, but write

      have hfx : coeff 0 (f * a) = coeff 0 f * coeff 0 a := by
        simp only [coeff_mul, Finset.antidiagonal_zero, Finset.sum_singleton]

[Kenny Lau]

yes, but in the general philosophy it's better to extract lemmas whenever possible

[Nick_adfor]

Kenny Lau said:

Nick_adfor no, Polynomial and MvPolynomial are different

It's my misunderstanding : ( Sorry!

[Nick_adfor]

Kenny Lau said:

yes, but in the general philosophy it's better to extract lemmas whenever possible

Thanks for the advice! Now I just get the whole proof into one theorem, but absolutely I can extract some lemmas to make the main proof precise.

[Nick_adfor]

Now I'm stuck in three tactic rw failed: rw [← h_mul_zero_x, coeff_zero_X i] at hfx,  w [← h_mul_zero_y, coeff_zero_X j] at hfy, rw [← mem_span_singleton] at hf, 

and one invalid field notation: exact Ideal.span_singleton_eq_top.mp (IsUnit.span_singleton_eq_top this).

[Kenny Lau]

updated link?

[Nick_adfor]

The updated link is here

[Jz Pan]

Kenny Lau said:

it seems like you need this theorem which is unfortunately not in mathlib(?):

theorem MvPolynomial.coeff_zero_mul {α : Type*} {R : Type*} [CommSemiring R] (p q : MvPolynomial α R) :
    coeff 0 (p * q) = coeff 0 p * coeff 0 q := by
  classical
  simp [coeff_mul]

You can use MvPolynomial.constantCoeff which is a RingHom hence it preserves multiplication.

[Kenny Lau]

hmm that doesn't seem like a good name :slight_smile:

[Kenny Lau]

Nick_adfor said:

The updated link is here

well, yeah you're getting the same error because the thing you're trying to rewrite still looks like coeff 0 (f * a)

[Kenny Lau]

the fact that you've proved coeff 0 (f * a) = coeff 0 f * coeff 0 a separately doesn't mean that Lean now automatically assumes that they're equal everywhere

[Jz Pan]

BTW, if it's me, I will prove that (X) in a multi-variable polynomial ring over a field is a non-zero prime ideal but not a maximal ideal, hence such ring has Krull dimension >=2 and cannot be PID. This is overkill, unfortunately.

[Kenny Lau]

Jz Pan said:

BTW, if it's me, I will prove that (X) in a multi-variable polynomial ring over a field is a non-zero prime ideal but not a maximal ideal, hence such ring has Krull dimension >=2 and cannot be PID. This is overkill, unfortunately.

I claim that if you unfold the proofs (I know Lean doesn't like that) you would end up with the same proof

[Jz Pan]

Oh, we even don't need to prove this, as we can use docs#ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial and do a one-liner.

[Kenny Lau]

lol

[Kenny Lau]

the joy of higher theory

[Jz Pan]

But... do we have IsPrincipalIdealRing -> ringKrullDim <= 1? Especially, is it true without domain assumption?

[Kenny Lau]

presumably you get a PID after quotienting by any prime ideal...

[Kenny Lau]

suppose P1 < P2 < P3 are primes, then R/P1 is PID, and P1/P1 < P2/P1 < P3/P1 (wait... is this true?)

[Kenny Lau]

(this is true because quotienting is the same as in Z-Mod, and Z-Mods behave nicely :rofl: )

[Nick_adfor]

Jz Pan said:

Oh, we even don't need to prove this, as we can use docs#ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial and do a one-liner.

This is completely a beauty of higher theory (theorem ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial)! But unfortunately I was using v4.16.0. Mathlib.RingTheory.KrullDimension.NonZeroDivisors only exists upper than v4.19.0 : (

[Kenny Lau]

ok who wants to submit a one-line PR to generalise docs#IsPrincipalIdealRing.krullDimLE_one to non-domains?

[Kenny Lau]

@Nick_adfor don't let us derail you lol, it's still good practise to do lower theory

[Nick_adfor]

Now I'm still stuck in three tactic rw failed: rw [← h_mul_zero_x, coeff_zero_X i] at hfx,  w [← h_mul_zero_y, coeff_zero_X j] at hfy, rw [← mem_span_singleton] at hf, 

and one invalid field notation: exact Ideal.span_singleton_eq_top.mp (IsUnit.span_singleton_eq_top this).

The updated Lean 4 Web link is here

[Kenny Lau]

@Nick_adfor not sure if you have read my comments:

Kenny Lau: Nick_adfor said:

The updated link is here

well, yeah you're getting the same error because the thing you're trying to rewrite still looks like coeff 0 (f * a)

Kenny Lau: the fact that you've proved coeff 0 (f * a) = coeff 0 f * coeff 0 a separately doesn't mean that Lean now automatically assumes that they're equal everywhere

[Jz Pan]

Kenny Lau said:

ok who wants to submit a one-line PR to generalise docs#IsPrincipalIdealRing.krullDimLE_one to non-domains?

I'm still thinking the proof... Is ringKrullDim R = ⨆ I : Ideal R, ringKrullDim (R ⧸ I) true? (Or PrimeSpectrum if you like.) I want to use docs#Order.krullDim_eq_iSup_coheight Order.krullDim α = ⨆ a, ↑(Order.coheight a) and the latter should be ringKrullDim (R ⧸ P) but seems that there is no Ideal.coheight nor its relation to the Krull dimension of quotient ring...

[Nick_adfor]

Kenny Lau said:

Nick_adfor not sure if you have read my comments:

Kenny Lau: Nick_adfor said:

The updated link is here

well, yeah you're getting the same error because the thing you're trying to rewrite still looks like coeff 0 (f * a)

Kenny Lau: the fact that you've proved coeff 0 (f * a) = coeff 0 f * coeff 0 a separately doesn't mean that Lean now automatically assumes that they're equal everywhere

I've noticed that. But now I don't know that where I should add hfx : coeff 0 (f * a) = coeff 0 f * coeff 0 a

[Kenny Lau]

well, preferably as a lemma above your main theorem :slight_smile:

[Kenny Lau]

but you can basically add it anywhere

[Andrew Yang]

Note that docs#ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial is not a deep result. It is basically the consequence of the fact that X is not a zero divisor and that minimal primes are contained in zero divisors, both of which comes from basic manipulation of the definitions.

The nontrivial part is the upperbound of dimension of polynomial ring.

[Nick_adfor]

Nick_adfor said:

Now I'm still stuck in three tactic rw failed: rw [← h_mul_zero_x, coeff_zero_X i] at hfx,  w [← h_mul_zero_y, coeff_zero_X j] at hfy, rw [← mem_span_singleton] at hf, 

and one invalid field notation: exact Ideal.span_singleton_eq_top.mp (IsUnit.span_singleton_eq_top this).

The updated Lean 4 Web link is here

How can I just fix the four error without import higher theory?

[Kenny Lau]

I told you already; is there something you don't understand?

[Junyan Xu]

ringKrullDim R = ⨆ I : Ideal R, ringKrullDim (R ⧸ I) is definitely true since you can take I = \bot. If I ranges in the prime spectrum, you are just missing
ringKrullDim_quotient and Order.coheight_eq_krullDim_Ici (noting that zeroLocus is defeq to Ici).

[Jz Pan]

Kenny Lau said:

ok who wants to submit a one-line PR to generalise docs#IsPrincipalIdealRing.krullDimLE_one to non-domains?

I'm doing it; while I found a TODO in https://github.com/leanprover-community/mathlib4/blob/7deb334c5f5104f4edad1a6396dd02a8cddefb86/Mathlib/RingTheory/PrincipalIdealDomain.lean#L232-L247

BTW the theorem name IsPrime.to_maximal_ideal is weird, IMHO it should called Ideal.IsPrime.isMaximal(_of_XXX).

[Jz Pan]

PR created as 25702 #25728.

[Nick_adfor]

Kenny Lau said:

I told you already; is there something you don't understand?

I mean that I have problem with error in three rwand one exact. The original goal of this post is to fix the code with little change of the code. Of course some new idea about KrullDim is OK, but that does not help for fixing (I mean to fix, not to destroy and rebuild the code). Now hfx : coeff 0 (f * a) = coeff 0 f * coeff 0 a seems to be a possible error, but is it that all the four error come from hfx?

[Kenny Lau]

@Nick_adfor if you select the text containing the error, you will be able to see what the error is

[Kenny Lau]

image.png

[Kenny Lau]

see how on the left I selected the text with red underline

[Kenny Lau]

the whole line reads:

rw [← h_mul_zero_x, coeff_zero_X i] at hfx

[Kenny Lau]

and from the infoview on the right, you can see that hfx is:

hfx : coeff 0 (f * a) = 0

[Kenny Lau]

and the thing you're trying to rewrite with, which is h_mul_zero_x, is:

h_mul_zero_x : coeff 0 x = coeff 0 f * coeff 0 a

[Kenny Lau]

so the rewrite fails, because you're trying to replace the string coeff 0 (f * a), and Lean cannot match it with the provided coeff 0 f * coeff 0 a

[Kenny Lau]

@Nick_adfor is this clearer now?

[Nick_adfor]

Kenny Lau said:

Nick_adfor is this clearer now?

Yes. For this part I want to show coeff (0 : σ →₀ ℕ) a = 0 and then get a contradiction with coeff (0 : σ →₀ ℕ) a ≠ 0. But for a lot of trials, I just get 0=0 (cannot give a contradiction)

[Nick_adfor]

For the following one to check the code, I'll give a precise one here:

import Mathlib

open MvPolynomial Ideal

variable (R : Type*) [Field R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ]

theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by

  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h

  let x : MvPolynomial σ R := X i
  let y : MvPolynomial σ R := X j


  let I := span ({x, y} : Set (MvPolynomial σ R))

  have proper : I ≠ ⊤ := by
    sorry
    --The sorry has been proved. I just deleted to make the code precise

  intro hPID

  haveI := hPID
  obtain ⟨f, hf⟩ := (IsPrincipalIdealRing.principal I).principal


  have x_mem : x ∈ I := subset_span (by simp)
  have y_mem : y ∈ I := subset_span (by simp)
  rw [hf] at x_mem y_mem

  obtain ⟨a, ha⟩ := mem_span_singleton.mp x_mem
  obtain ⟨b, hb⟩ := mem_span_singleton.mp y_mem


  have : IsUnit f := by
    have h_mul_zero_x : coeff (0 : σ →₀ ℕ) x = coeff (0 : σ →₀ ℕ) (f * a) := by rw [ha]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_x
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_x
    have coeff_f_zero_of_a : coeff (0 : σ →₀ ℕ) a ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      sorry
    --The sorry has been proved. I just deleted to make the code precise

    have h_mul_zero_y : coeff (0 : σ →₀ ℕ) y = coeff (0 : σ →₀ ℕ) (f * b) := by rw [hb]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_y
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_y
    have coeff_f_zero_of_b : coeff (0 : σ →₀ ℕ) b ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      sorry
    --The sorry has been proved. I just deleted to make the code precise

    by_cases ha0 : coeff (0 : σ →₀ ℕ) a ≠ 0
    · have hf0 := coeff_f_zero_of_a ha0
      have hfx : coeff 0 (f * a) = coeff 0 f * coeff 0 a := by
        simp only [coeff_mul, Finset.antidiagonal_zero, Finset.sum_singleton]
      rw [hf0, zero_mul] at hfx
      rw [← h_mul_zero_x, coeff_zero_X i] at hfx
--↑Here is an error
      exact ha0 hfx
    by_cases hb0 : coeff (0 : σ →₀ ℕ) b ≠ 0
    · have hf0 := coeff_f_zero_of_b hb0
      have hfy : coeff 0 (f * b) = coeff 0 f * coeff 0 b := by
        simp only [coeff_mul, Finset.antidiagonal_zero, Finset.sum_singleton]
      rw [hf0, zero_mul] at hfy
      rw [← h_mul_zero_y, coeff_zero_X j] at hfy
--↑Here is the same error
      exact hb0 hfy
    -- If both a and b have zero constant term, then f must be a unit
    push_neg at ha0 hb0
    rw [← mem_span_singleton] at hf
--↑Here is another error
    refine isUnit_of_dvd_one ?_
    have : 1 ∈ span {f} := by
      rw [← hf]
      exact Ideal.eq_top_iff_one.mp rfl
    exact mem_span_singleton.mp this

  -- Now we know f is a unit, which implies I = (1), contradicting properness
  have I_top : I = ⊤ := by
    rw [hf]
    exact Ideal.span_singleton_eq_top.mp (IsUnit.span_singleton_eq_top this)
--↑Here is the end error
  exact proper I_top

[Nick_adfor]

The whole Lean 4 Web link is here

[Kenny Lau]

@Nick_adfor you keep getting the same error for the same reason; i'm not sure if you actually read what i said

[Nick_adfor]

Kenny Lau said:

Nick_adfor you keep getting the same error for the same reason; i'm not sure if you actually read what i said

Sorry to hear that. Actually reading really not means actually understanding and actually fixing : (

[Nick_adfor]

My lean version is v4.16.0. And now my idea is to fix the code with these four error, but not use KrullDim to rebuild all my code. Seems that hfx : coeff 0 (f * a) = coeff 0 f * coeff 0 a causes the first two errors, but I do not know how to fix them. And for the last two errors, I have not known the reason. So I ask for a kind help. Thanks!

[Luigi Massacci]

Out of curiosity, how did you write the code you already have?

[Nick_adfor]

Luigi Massacci said:

Out of curiosity, how did you write the code you already have?

Construct a proof by first sketching a rough outline on paper. Then, start translating this outline into Lean code, initially filling in the gaps with many sorry. As I replace these sorry statements, I'll also refine and adjust the overall structure of the proof as needed. I've noticed that sometimes code suggestions from Copilot in VSCode aren't very helpful for my specific tasks, although Copilot often automatically popping up in VsCode. It may give some pseudo theorem not in Mathlib. While the rw? tactic is occasionally useful for rewriting using Mathlib theorems, it's frustrating that it can't leverage my own custom definitions and theorems. I feel like I'm getting stuck in the weeds of the code and losing the ability to think clearly about the underlying mathematical ideas. I suspect I might just be experiencing 'code fatigue'.

[Nick_adfor]

Now the code is written this way.

import Mathlib

open MvPolynomial Ideal

variable (R : Type*) [Field R]
variable (σ : Type*) [Fintype σ] [DecidableEq σ]


theorem mvPolynomial_not_pid_of_card_ge_two (h : 2 ≤ Fintype.card σ) :
    ¬ IsPrincipalIdealRing (MvPolynomial σ R) := by

  obtain ⟨i, j, hij⟩ := Fintype.exists_pair_of_one_lt_card h

  let x : MvPolynomial σ R := X i
  let y : MvPolynomial σ R := X j


  let I := span ({x, y} : Set (MvPolynomial σ R))

  have proper : I ≠ ⊤ := by
    intro hI
    have one_mem : (1 : MvPolynomial σ R) ∈ I := by rw [hI]; trivial

    obtain ⟨a, b, eq1⟩ := mem_span_pair.mp one_mem

    have const_eq : coeff (0 : σ →₀ ℕ) 1 = coeff (0 : σ →₀ ℕ) (a * x + b * y) := by
      rw [eq1]

    have coeff_x_zero : coeff (0 : σ →₀ ℕ) x = 0 := by
      rw [@coeff_zero_X]

    have coeff_y_zero : coeff (0 : σ →₀ ℕ) y = 0 := by
      rw [@coeff_zero_X]

    have rhs_const : coeff (0 : σ →₀ ℕ) (a * x + b * y) = 0 := by
      rw [coeff_add, coeff_mul, coeff_mul]
      simp
      rw [coeff_x_zero, coeff_y_zero]
      simp

    rw [coeff_one, rhs_const] at const_eq
    exact one_ne_zero const_eq


  intro hPID

  haveI := hPID
  obtain ⟨f, hf⟩ := (IsPrincipalIdealRing.principal I).principal


  have x_mem : x ∈ I := subset_span (by simp)
  have y_mem : y ∈ I := subset_span (by simp)
  rw [hf] at x_mem y_mem

  obtain ⟨a, ha⟩ := mem_span_singleton.mp x_mem
  obtain ⟨b, hb⟩ := mem_span_singleton.mp y_mem


  have : IsUnit f := by
    have h_mul_zero_x : coeff (0 : σ →₀ ℕ) x = coeff (0 : σ →₀ ℕ) (f * a) := by rw [ha]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_x
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_x
    have coeff_f_zero_of_a : coeff (0 : σ →₀ ℕ) a ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 a = 0 := by
        rw [← h_mul_zero_x, ← coeff_zero_X i]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    have h_mul_zero_y : coeff (0 : σ →₀ ℕ) y = coeff (0 : σ →₀ ℕ) (f * b) := by rw [hb]
    simp only [coeff_X, ne_eq, hij, not_false_eq_true,
      ite_false, coeff_mul, zero_mul, add_zero] at h_mul_zero_y
    simp only [Finset.antidiagonal_zero, Finset.sum_singleton] at h_mul_zero_y
    have coeff_f_zero_of_b : coeff (0 : σ →₀ ℕ) b ≠ 0 → coeff (0 : σ →₀ ℕ) f = 0 := by
      intro ha_ne_zero
      have : coeff 0 f * coeff 0 b = 0 := by
        rw [← h_mul_zero_y, ← coeff_zero_X j]
      apply Or.elim (mul_eq_zero.mp this)
      · intro hf_zero
        exact hf_zero
      · intro ha_zero
        contradiction

    by_cases ha0 : coeff (0 : σ →₀ ℕ) a ≠ 0
    · have f0 := coeff_f_zero_of_a ha0
      have f_dvd_Xi : f ∣ x := by
        use a
      obtain ⟨g, rfl⟩ : ∃ g, f = x * g := by
        have a_decomp: a = C (a.coeff 0) + (a - C (a.coeff 0)) := by simp
        have key_eq : f * C (a.coeff 0) = x - f * (a - C (a.coeff 0)) := by
          rw [ha]
          ring
        refine ⟨a * (C (a.coeff 0)⁻¹), ?_⟩
        have const_zero : coeff 0 f = 0 := coeff_f_zero_of_a ha0
        have zero_term : f * (a - C (a.coeff 0)) = 0 := by sorry
        rw [zero_term, sub_zero] at key_eq
        have : f = x * (a * C (a.coeff 0)⁻¹) := by
          sorry
        exact this
      have : x * g ∣ y := by rw [hb]; exact dvd_mul_right (x * g) b
      have dvd_x_y: x ∣ y := by
        apply dvd_trans (dvd_mul_right x g) this
      have eq_ij : i = j := by
        sorry
      contradiction

--to be continued

[Nick_adfor]

Without caring if this construction of by_cases ha0 may cause long-proof lemma, I finish this part with three sorry. And I realize ∃ g, f = x * g by obtain. I do not know if this obtain can be realized automatically by lean.