Error when applying supr_le

Stream: maths

[Wrenna Robson]

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]

Is nat a complete_lattice?

[Yakov Pechersky]

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

[Yakov Pechersky]

What would be the supr for an arbitrary set nat?

[Wrenna Robson]

a-ha

[Wrenna Robson]

so possibly I want to look at with_top ℕ instead?

[Yakov Pechersky]

also known as enat I think

[Yakov Pechersky]

But, lists are finite btw.

[Wrenna Robson]

Yes.

[Wrenna Robson]

That's intended in the context.

[Wrenna Robson]

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

[Wrenna Robson]

Actually I kinda want it to have a bot also

[Yakov Pechersky]

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]

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

[Wrenna Robson]

Is there a one-line way of doing:

  {
    intro h,
    exact supr_le h,
  },

[Yakov Pechersky]

{ exact supr_le },

[Yakov Pechersky]

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]

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.

[Wrenna Robson]

Thank you :)

[Wrenna Robson]

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

[Wrenna Robson]

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

[Kevin Buzzard]

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]

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]

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

[Yakov Pechersky]

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

[Wrenna Robson]

Right.

[Wrenna Robson]

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]

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

[Wrenna Robson]

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

[Wrenna Robson]

Happy to take suggestions!

[Reid Barton]

I guess I would probably go for prime_ideal_chain myself

[Wrenna Robson]

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