# Zulip Chat Archive

## Stream: new members

### Topic: finite sequence of elements of a ring

#### Jack J Garzella (Jul 19 2023 at 01:30):

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 (Jul 19 2023 at 02:20):

Using `seq.getD i 0`

instead of `seq[a]`

fixes the error.

For an `Inhabited`

type `R`

, you can extract the `i`

th 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 (Jul 19 2023 at 03:48):

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 (Jul 19 2023 at 03:49):

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 (Jul 19 2023 at 04:49):

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 (Jul 19 2023 at 04:59):

Can you write `∀ m : ℕ, m ≤ height I → ...`

and then `.take m`

?

#### Jack J Garzella (Jul 19 2023 at 18:37):

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 (Jul 19 2023 at 18:39):

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 (Jul 19 2023 at 18:42):

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 (Jul 21 2023 at 22:11):

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 (Jul 21 2023 at 22:57):

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 (Aug 04 2023 at 01:56):

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 (Aug 04 2023 at 02:03):

```
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 (Aug 04 2023 at 02:03):

BTW Currently `(R : Type _)`

is also a footgun: I'd recommend `universe uR`

and `R : Type uR`

.

#### Kevin Buzzard (Aug 04 2023 at 02:13):

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 (Aug 04 2023 at 02:13):

```
-- 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 (Aug 04 2023 at 02:15):

In Lean 3 the explicit `(_ : set R)`

saves us

Last updated: Dec 20 2023 at 11:08 UTC