finite sequence of elements of a ring

Stream: new members

[Jack J Garzella]

I'm trying to formalize the (statement of the) following lemma:

import Mathlib.RingTheory.Ideal.Operations
import Mathlib.RingTheory.Ideal.LocalRing
import Mathlib.RingTheory.Ideal.MinimalPrime
import Mathlib.RingTheory.Noetherian

variable {R : Type _} [CommRing R] [IsNoetherian R R]

noncomputable def height (I : Ideal R) : WithBot (WithTop ℕ) := sorry


lemma exist_subideals_of_all_heights_of_height_n (I : Ideal R) :
∃ seq : List R, seq.length = height I ∧ ∀ i ∈ {m : ℕ | m ≤ height I},
(height (Ideal.span {seq[a] | a ≤ i})) = i := sorry

For a reference, this is theorem A.2 in Bruns-Herzog's Cohen-Macaulay Rings

However, I get an error that Lean is unable to prove the index is correct. I think I don't have an off by one error, but I'm afraid my attempt is just too complicated for Lean to figure it out. Is there an easier way to do this?

Related question, should I be using List or Array for things like this?

[Damiano Testa]

Using seq.getD i 0 instead of seq[a] fixes the error.

For an Inhabited type R, you can extract the ith element of a list L by L[i]!, with the exclamation point. Inhabited is used in case you give an out-of-bounds index.

However, Monoid-like types are not inhabited globally, since they would induce default elements 0 or 1 in Semiring-like types, creating diamonds.

If you find yourself wanting the panic-notation !, you can add

local instance : Inhabited R := ⟨0⟩

though this might cause other kinds of issues.

[Scott Morrison]

Is it possible to write something more like Ideal.span (seq.take i) (maybe some function moving from List to Set is required there). That would be more colloquial than using indexing into the list.

[Scott Morrison]

Also, usually we would write ∀ i ∈ {m : ℕ | m ≤ height I}, ... as ∀ m, m ≤ height I → .... This then avoids the coercions you have of i back to ℕ, which are both hard on the reader, and will probably cause pain later.

[Jack J Garzella]

Scott Morrison said:

Is it possible to write something more like Ideal.span (seq.take i) (maybe some function moving from List to Set is required there). That would be more colloquial than using indexing into the list.

When I try to use seq.take i it complains that i has type WithBot (WithTop ℕ) and not ℕ. For the purposes of this theorem, I am willing to assume that 1 ≤ i so i is in fact a natural number, but how would I convince the type checker of this?

[Scott Morrison]

Can you write ∀ m : ℕ, m ≤ height I → ... and then .take m?

[Jack J Garzella]

That worked, thanks!

Now, my statement looks like this:

lemma exist_subideals_of_all_heights_of_height_n (I : Ideal R) :
∃ seq : List R, seq.length = height I ∧ ∀ i : ℕ, 1 ≤ i ∧ i ≤ height I →
(height (Ideal.span (List.toFinset (seq.take i)))) = i := sorry

and Lean is complaining that R has no instance of DecidableEq. But I think that rings don't necessarily have decidable equality in general, so how might I proceed?

[Kevin Buzzard]

The rule with this decidable stuff is: if the statement of the lemma doesn't compile, add [DecidableEq R] to the statement. If the statement compiles but your proof doesn't work, use the classical tactic.

[Kevin Buzzard]

PS when Jujian and I discussed dimension theory, I suggested that a Nat-valued function would be easier to work with, but eventually he went for with WithBot WithTop thing. For degrees of polynomials we have "mathematically correct degree" taking values in WithBot Nat with deg(0)=bot, and we have "degree which is often easier to use in practice" where deg(0) is just defined to be a junk value but the target of the map is the naturals. If you have too much more trouble with WithBot WithTop Nat you might want to consider PRing a natDimension function sending the zero ring and infinite-dimensional rings to 0.

[Jack J Garzella]

Kevin Buzzard said:

PS when Jujian and I discussed dimension theory, I suggested that a Nat-valued function would be easier to work with, but eventually he went for with WithBot WithTop thing. For degrees of polynomials we have "mathematically correct degree" taking values in WithBot Nat with deg(0)=bot, and we have "degree which is often easier to use in practice" where deg(0) is just defined to be a junk value but the target of the map is the naturals. If you have too much more trouble with WithBot WithTop Nat you might want to consider PRing a natDimension function sending the zero ring and infinite-dimensional rings to 0.

I think there's some subtlety here because the "WithBot" (i.e. the zero ring) is "mathematically trivial" but the "WithTop" (infinite dimensional rings) is not. Many theorems hold without change for infinite dimensional rings, for example my statement in #new members > ✔ HSub on WithBot/WithTop? works as long as $\infty + 1 = \infty$. So I could at least imagine the use of something which ignores the zero ring but not infinite-dimensional ones.

On the other hand, if you're thinking about infinite-dimensional rings you might want to distinguish between countable and uncountable krull dimension (this is for example the difference between Lang-Ludwig and Du).

All this is pretty obscure though. As someone who has thought a little bit about infinite dimensional rings, I'd say the ideal "mathematically correct" thing would be a cardinal, and then we can use a natDimension and natHeight like you mentioned for everyday things.

[Kevin Buzzard]

I'm aware of the Lang-Ludwig work (Judith was my PhD student!); Jujian and I also discussed a definition taking values in WithBot Cardinal but this seemed even more exotic and hard to work with. Your comments on $\infty+1=\infty$ are interesting though. I should think that this is true for WithBot (WithTop Nat) though so you're OK.

[Jack J Garzella]

Kevin Buzzard said:

The rule with this decidable stuff is: if the statement of the lemma doesn't compile, add [DecidableEq R] to the statement. If the statement compiles but your proof doesn't work, use the classical tactic.

Ok, so I want to revive this after a short haitus... it turns out even with [DecidableEq R] Lean is still complaining about

typeclass instance problem is stuck, it is often due to metavariables
  CommRing (?m.52781 seq i)

I had abanodned trying to use lists/arrays for functions fin n → R instead, but I'm not sure this is a good option anymore and want to try both approaches. Here's my current #mwe:

import Mathlib.RingTheory.Ideal.Operations
import Mathlib.RingTheory.Ideal.LocalRing
import Mathlib.RingTheory.Ideal.MinimalPrime
import Mathlib.RingTheory.Noetherian


variable {R : Type _} [CommRing R] [IsNoetherian R R] [DecidableEq R]

noncomputable def height (I : Ideal R) : WithBot (WithTop ℕ) := sorry

--set_option trace.Meta.synthInstance true in

lemma exist_subideals_of_all_heights_of_height_n (I : Ideal R) :
∃ seq : List R, seq.length = height I ∧ ∀ i : ℕ, 1 ≤ i ∧ i ≤ height I →
(height (Ideal.span (List.toFinset (List.take i seq)))) = i := sorry

Can anyone explain why this error is popping up and how to fix it?

[Kevin Buzzard]

lemma exist_subideals_of_all_heights_of_height_n (I : Ideal R) :
∃ seq : List R, seq.length = height I ∧ ∀ i : ℕ, 1 ≤ i ∧ i ≤ height I →
(height (R := R) (Ideal.span (List.toFinset (List.take i seq)))) = i := sorry

Lean 4 is currently worse at unification than Lean 3.I take that back, they both fail here.

[Kevin Buzzard]

BTW Currently (R : Type _) is also a footgun: I'd recommend universe uR and R : Type uR.

[Kevin Buzzard]

Actually Lean 3 fails in a different place: it won't coerce the finset to a set. I think this is actually the same underlying problem. When coercing a finset to a set, 99.9% of the time you're going from finset X to set X as opposed to anything more exotic, but it always seems that Lean is reluctant to assume this. Perhaps this is the common cause?

[Kevin Buzzard]

-- Lean 3
import ring_theory.ideal.cotangent

variables (R : Type*) [comm_ring R]

def height {A : Type*} [comm_ring A] : ideal A → ℕ := sorry

lemma exist_subideals_of_all_heights_of_height_n (I : ideal R) [decidable_eq R]:
∃ seq : list R, seq.length = height I ∧ ∀ i : ℕ, 1 ≤ i ∧ i ≤ height I →
(height (ideal.span (list.to_finset (list.take i seq) : set R))) = i := sorry

[Kevin Buzzard]

In Lean 3 the explicit (_ : set R) saves us