## Stream: Is there code for X?

### Topic: I-adic valuation on R

#### Kevin Buzzard (Aug 06 2020 at 13:00):

If $R$ is a ring and $J$ is an ideal then I am pretty sure that Chris or Kenny showed me a function last week from $R$ to with_top \N taking $r$ to the largest $n$ with $r\in J^n$. What's the name of this function? I want to make a valuation on a valuation ring

#### Kevin Buzzard (Sep 02 2020 at 11:59):

I would be happy with enat. I still cannot find this function in mathlib. Kenny did you show me some unfinished PR or something?

#### Kevin Buzzard (Sep 02 2020 at 11:59):




#### Kevin Buzzard (Sep 02 2020 at 11:59):

import all

example (R : Type) [comm_ring R] (I : ideal R) (x : R) : enat :=
by suggest -- fails


#### Kevin Buzzard (Sep 02 2020 at 12:05):

@Johan Commelin roption also fails -- were you talking about some roption-valued function? Is this on a branch of yours?

#### Kevin Buzzard (Sep 02 2020 at 12:15):

I want this function because it's now the unique thing holding up DVRs, and I don't want to duplicate work. I'll happily write an API if I'm deluded and it's not there.

#### Kevin Buzzard (Sep 02 2020 at 12:15):

@Ashvni Narayanan @Frederick Eidsnes Thøgersen

#### Kenny Lau (Sep 02 2020 at 12:46):

docs#multiplicity

@Kevin Buzzard

#### Kevin Buzzard (Sep 02 2020 at 12:47):

but this is for an element. I want an ideal.

#### Kenny Lau (Sep 02 2020 at 12:47):

just use ideal.span

#### Kevin Buzzard (Sep 02 2020 at 12:47):

It's the wrong way

#### Kenny Lau (Sep 02 2020 at 12:48):

ideals form a semiring

#### Kevin Buzzard (Sep 02 2020 at 12:50):

@Frederick Eidsnes Thøgersen I know how to do it

#### Kevin Buzzard (Sep 02 2020 at 12:51):

Kenny, that was the comment you made a few weeks ago which I had forgotten

#### Adam Topaz (Sep 02 2020 at 13:07):

Cool! (The valuation associated to a blowup arises like this, right?)

#### Johan Commelin (Sep 02 2020 at 13:13):

But we don't have the relative Proj construction yet... so we can't define blowups :sad:

#### Adam Topaz (Sep 02 2020 at 13:17):

But you just got the valuation of their exceptional divisor! :wink:

Last updated: May 07 2021 at 17:36 UTC