Zulip Chat Archive

Stream: Is there code for X?

Topic: I-adic valuation on R


view this post on Zulip Kevin Buzzard (Aug 06 2020 at 13:00):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 11:59):


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 12:15):

@Ashvni Narayanan @Frederick Eidsnes Thøgersen

view this post on Zulip Kenny Lau (Sep 02 2020 at 12:46):

docs#multiplicity

view this post on Zulip Kenny Lau (Sep 02 2020 at 12:47):

@Kevin Buzzard

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 12:47):

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

view this post on Zulip Kenny Lau (Sep 02 2020 at 12:47):

just use ideal.span

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 12:47):

It's the wrong way

view this post on Zulip Kenny Lau (Sep 02 2020 at 12:48):

ideals form a semiring

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 12:50):

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

view this post on Zulip Kevin Buzzard (Sep 02 2020 at 12:51):

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

view this post on Zulip Adam Topaz (Sep 02 2020 at 13:07):

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

view this post on Zulip 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:

view this post on Zulip 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