## Stream: maths

### Topic: with_top \Z

#### 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!

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

#### 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}?

#### Johan Commelin (Jul 06 2020 at 14:19):

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

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

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

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

#### Ashvni Narayanan (Jul 06 2020 at 14:30):

I see. Thank you!

#### 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!

#### 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?

#### 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?

#### 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

#### Adam Topaz (Jul 06 2020 at 15:06):

How did you end up defining a DVR?

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

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

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

#### Ashvni Narayanan (Jul 06 2020 at 15:17):

Oh that sounds like a great idea!

Last updated: May 10 2021 at 07:15 UTC