Zulip Chat Archive

Stream: maths

Topic: with_top \Z


view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 14:07):

I want to show something like this:

lemma with_top.has_inf : has_Inf (with_top )(0 : with_top ) :=

No matter how I rephrase it, I get a

failed to synthesize type class instance for

error.
Any help is appreciated, thank you!

view this post on Zulip Sebastien Gouezel (Jul 06 2020 at 14:12):

has_Inf (with_top ℤ) is a proposition asserting that an operator Inf is defined on the subsets of with_top ℤ. So, Lean gets that you want to compare a proposition with the number 0, and it doesn't understand what you mean.

view this post on Zulip Adam Topaz (Jul 06 2020 at 14:18):

Are you are trying to define a has_Inf instance on { x : with_top \Z // x \ge 0}?

view this post on Zulip Johan Commelin (Jul 06 2020 at 14:19):

Note that { x : with_top \Z // x \ge 0} is isomorphic to enat.

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 14:23):

I am actually looking at a subset of has_top \Z \geq 0 :

S : ideal (val_ring K),
P : set (with_top ) := {a : with_top  |  (x : (val_ring K)) (H : x  S), a = v x}

and I want to show

K : Type u_1,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K,
S : ideal (val_ring K),
P : set (with_top ) := {a : with_top  |  (x : (val_ring K)) (H : x  S), a = v x},
f : bdd_below P
 has_Inf P

using f, but I keep getting an error which asks for Inf to be defined on with_top \Z, hence my question above.

view this post on Zulip Johan Commelin (Jul 06 2020 at 14:27):

Aha... Lean is not going to figure out that ↥P is a type for which infima exist. It has never heard of this P before, so it know almost nothing about it.

view this post on Zulip Adam Topaz (Jul 06 2020 at 14:27):

Note that arbitrary subsets of with_top \Z do not have an Inf. So you might run into some complications since the type of P is set (with_top \Z).

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 14:30):

I see. Thank you!

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 14:34):

This seems to be an equivalent definition that does not throw up any error(yet) :

K : Type u_1,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K,
S : ideal (val_ring K),
P : Prop :=  (x : (val_ring K)) (H : x  S), 0  v x

I hope it works!

view this post on Zulip Kevin Buzzard (Jul 06 2020 at 14:57):

So there is already enat and with_top nat. I wonder if it would just be easier to use them?

view this post on Zulip Adam Topaz (Jul 06 2020 at 15:00):

What's the actual goal here? Are you trying to prove that a DVR is a PID?

view this post on Zulip Kevin Buzzard (Jul 06 2020 at 15:05):

I think the goal is that if we start with a discrete valuation field, then the stuff with valuation >= 0 is a discrete valuation ring

view this post on Zulip Adam Topaz (Jul 06 2020 at 15:06):

How did you end up defining a DVR?

view this post on Zulip Kevin Buzzard (Jul 06 2020 at 15:09):

I think Ashvni went with Serre's definition: a PID with precisely one non-zero prime ideal.

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 15:11):

Yes, the local goal is to show that the ring obtained from a DVF is a PIR.

view this post on Zulip Adam Topaz (Jul 06 2020 at 15:12):

I see. I guess what I'm wondering is whether the easiest way to approach this is to prove that the set of elements with nonnegative valuation is a Euclidean domain, since you already have the valuation function as part of the definition! This should follow easily from the ultrametric inequality. I think mathlib knows that Euclidean domain implies PID.

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 15:17):

Oh that sounds like a great idea!


Last updated: May 10 2021 at 07:15 UTC