# Zulip Chat Archive

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