I-adic valuation on R

Stream: Is there code for X?

[Kevin Buzzard]

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]

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]

[Kevin Buzzard]

import all

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@Ashvni Narayanan @Frederick Eidsnes Thøgersen

[Kenny Lau]

docs#multiplicity

[Kenny Lau]

@Kevin Buzzard

[Kevin Buzzard]

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

[Kenny Lau]

just use ideal.span

[Kevin Buzzard]

It's the wrong way

[Kenny Lau]

ideals form a semiring

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

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