Zulip Chat Archive

Stream: maths

Topic: Error when applying supr_le


view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 21:39):

Is nat a complete_lattice?

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 21:40):

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

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 21:40):

What would be the supr for an arbitrary set nat?

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:42):

a-ha

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:43):

so possibly I want to look at with_top ℕ instead?

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 21:44):

also known as enat I think

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 21:44):

But, lists are finite btw.

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:44):

Yes.

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:45):

That's intended in the context.

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:45):

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

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:46):

Actually I kinda want it to have a bot also

view this post on Zulip 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)

view this post on Zulip 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.)

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:49):

Is there a one-line way of doing:

  {
    intro h,
    exact supr_le h,
  },

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 21:51):

{ exact supr_le },

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:57):

Thank you :)

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:57):

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

view this post on Zulip Wrenna Robson (Dec 07 2020 at 21:58):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:00):

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

view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:01):

Right.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Dec 07 2020 at 22:02):

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

view this post on Zulip 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.)

view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:03):

Happy to take suggestions!

view this post on Zulip Reid Barton (Dec 07 2020 at 22:08):

I guess I would probably go for prime_ideal_chain myself

view this post on Zulip 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