## Stream: maths

### Topic: Error when applying supr_le

#### Wrenna Robson (Dec 07 2020 at 21:37):

Here's an MWE:

import tactic ring_theory.localization

universe u

def is_pic {R : Type u} [comm_ring R]
( c : list (prime_spectrum R) ) : Prop :=
c ≠ list.nil ∧ c.chain' (λ x y, x.as_ideal < y.as_ideal)

def pic (R : Type u) [comm_ring R] :=
{C : list (prime_spectrum R) // is_pic C}

def pic_len (R : Type u) [comm_ring R] : pic R → ℕ :=
begin
rintros ⟨C, ⟨hCne, hCc⟩⟩,
exact C.length - 1,
end

noncomputable def krull_dim (R : Type u) [comm_ring R] : ℕ :=
supr (pic_len R)

def KD_le_n' (R : Type u) [comm_ring R] (n : ℕ) : Prop :=
krull_dim R ≤ n

def KD_le_n (R : Type u) [comm_ring R] (n : ℕ) : Prop :=
∀ x : pic R, pic_len R x ≤ n

theorem le_equiv {R : Type u} [comm_ring R] {n : ℕ} :
KD_le_n R n ↔ KD_le_n' R n :=
begin
rw KD_le_n,
rw KD_le_n',
split,
{
intro h,
rw krull_dim,
--apply supr_le h,
sorry,
},
{
sorry,
}
end


It seems to me that this is exactly a situation where supr_le applies, but if I uncomment the commented line, I get an error which suggest Lean is struggling to match the types. Can anyone see what I'm doing wrong? Do I need to adjust any definitions?

#### Yakov Pechersky (Dec 07 2020 at 21:39):

Is nat a complete_lattice?

#### Yakov Pechersky (Dec 07 2020 at 21:40):

None available, at least by #check (show complete_lattice ℕ, by apply_instance)

#### Yakov Pechersky (Dec 07 2020 at 21:40):

What would be the supr for an arbitrary set nat?

a-ha

#### Wrenna Robson (Dec 07 2020 at 21:43):

so possibly I want to look at with_top ℕ instead?

#### Yakov Pechersky (Dec 07 2020 at 21:44):

also known as enat I think

#### Yakov Pechersky (Dec 07 2020 at 21:44):

But, lists are finite btw.

Yes.

#### Wrenna Robson (Dec 07 2020 at 21:45):

That's intended in the context.

#### Wrenna Robson (Dec 07 2020 at 21:45):

A pic is a finite list of prime ideals of R, properly contained in one another.

#### Wrenna Robson (Dec 07 2020 at 21:46):

Actually I kinda want it to have a bot also

#### Yakov Pechersky (Dec 07 2020 at 21:46):

def pic_len (R : Type u) [comm_ring R] (C : pic R) : enat :=
enat.coe_hom (C.val.length - 1)

noncomputable def krull_dim (R : Type u) [comm_ring R] : enat :=
supr (pic_len R)


#### Wrenna Robson (Dec 07 2020 at 21:48):

(As in, a bot lower than 0: when R is trivial it should be, well, -1 or -infinity by convention.)

#### Wrenna Robson (Dec 07 2020 at 21:49):

Is there a one-line way of doing:

  {
intro h,
exact supr_le h,
},


#### Yakov Pechersky (Dec 07 2020 at 21:51):

{ exact supr_le },


#### Yakov Pechersky (Dec 07 2020 at 21:53):

import tactic ring_theory.localization

universe u

def is_pic {R : Type u} [comm_ring R]
( c : list (prime_spectrum R) ) : Prop :=
c ≠ list.nil ∧ c.chain' (λ x y, x.as_ideal < y.as_ideal)

def pic (R : Type u) [comm_ring R] :=
{C : list (prime_spectrum R) // is_pic C}

def pic_len (R : Type u) [comm_ring R] (C : pic R) : enat :=
enat.coe_hom (C.val.length - 1)

noncomputable def krull_dim (R : Type u) [comm_ring R] : enat :=
supr (pic_len R)

def KD_le_n' (R : Type u) [comm_ring R] (n : ℕ) : Prop :=
krull_dim R ≤ n

def KD_le_n (R : Type u) [comm_ring R] (n : ℕ) : Prop :=
∀ x : pic R, pic_len R x ≤ n

theorem le_equiv {R : Type u} [comm_ring R] {n : ℕ} :
KD_le_n R n ↔ KD_le_n' R n :=
by rw [KD_le_n, KD_le_n', krull_dim, supr_le_iff]


#### Wrenna Robson (Dec 07 2020 at 21:55):

We don't even need the rws, I realised (just makes it easier). Just found supr_le_iff and that's exactly what I wanted.

Thank you :)

#### Wrenna Robson (Dec 07 2020 at 21:57):

If prime_spectrum R is an empty type, what will happen?

#### Wrenna Robson (Dec 07 2020 at 21:58):

(This happens I believe exactly when R is trivial.)

#### Kevin Buzzard (Dec 07 2020 at 21:59):

The dimension of the 0 ring is one of those things where people disagree, maybe some people say it's -1, some say it's -infinity, but the truth is that nobody asks this question in practice.

#### Wrenna Robson (Dec 07 2020 at 22:00):

Aye. For the context, I think I am going to have to have it as -1 or at least, hmm, there's a good chance I will be plugging in the 0 ring into krull_dim.

#### Wrenna Robson (Dec 07 2020 at 22:00):

(I am trying to formalise a characterisation of the Krull dimension - though Kevin knows this, it's just for context.)

#### Yakov Pechersky (Dec 07 2020 at 22:00):

The way it is now is it evaluates to 0, because, of course, 0 - 1 = 0.

Right.

#### Wrenna Robson (Dec 07 2020 at 22:01):

I sort of want "the natural numbers, but also -1 is there for some reason". I don't know what the most natural way to do that is.

#### Reid Barton (Dec 07 2020 at 22:02):

by the way, I read pic as $\mathrm{Pic}$ and got pretty confused

#### Wrenna Robson (Dec 07 2020 at 22:02):

that's a good point (I need to think about naming, though this is going nowhere near mathlib, at least for now.)

#### Wrenna Robson (Dec 07 2020 at 22:03):

Happy to take suggestions!

#### Reid Barton (Dec 07 2020 at 22:08):

I guess I would probably go for prime_ideal_chain myself

#### Wrenna Robson (Dec 07 2020 at 22:15):

Yes, I did have that, it just felt unwieldy. But clearer.

Last updated: May 18 2021 at 07:19 UTC