with_top \Z

Stream: maths

[Ashvni Narayanan]

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!

[Sebastien Gouezel]

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.

[Adam Topaz]

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

[Johan Commelin]

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

[Ashvni Narayanan]

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.

[Johan Commelin]

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.

[Adam Topaz]

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).

[Ashvni Narayanan]

I see. Thank you!

[Ashvni Narayanan]

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!

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

How did you end up defining a DVR?

[Kevin Buzzard]

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

[Ashvni Narayanan]

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

[Adam Topaz]

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.

[Ashvni Narayanan]

Oh that sounds like a great idea!