[Merged by Bors] - feat(ring_theory/discrete_valuation_ring): add additive valuation #5094
Conversation
kbuzzard
added
the
awaiting-review
| -/ | ||
|
|
||
| /-- The `ℕ`-valued additive valuation on a DVR (returns junk at `0` rather than `+∞`) -/ | ||
| noncomputable def add_val (R : Type u) [integral_domain R] [discrete_valuation_ring R] : R → ℕ := |
There was a problem hiding this comment.
There's not much point, but you could declare this a zero_hom R ℕ to get a tiny bit of bundling
There was a problem hiding this comment.
I almost sent 0 to 37. This definition is really an auxiliary one; I will only be using it when defining the correct object, which is either the map to with_top nat sending 0 to top, or (more likely) the map to with_zero (multiplicative nat) or with_zero (multiplicative int), because the latter is the valuation right now (and the former isn't, but will be once I get round to generalising the definition of valuation).
Should I rename this function add_val_aux and define a new function add_val to with_top nat? This would have more functorial properties.
There was a problem hiding this comment.
I think adding _aux to the name is a useful flag that this is meant as implementation detail. You could also explicitly state that in the docstring.
Otoh, if we think we'll be using this later on, then I'd prefer to keep the name the way it is.
| λ r, if hr : r = 0 then 0 else | ||
| classical.some (associated_pow_irreducible hr (classical.some_spec $ exists_irreducible R)) | ||
|
|
||
| theorem add_val_spec {r : R} (hr : r ≠ 0) : |
There was a problem hiding this comment.
add_val_def is the more friendly version intended for general use, right?
| theorem add_val_spec {r : R} (hr : r ≠ 0) : | |
| /-- `add_val_spec` is a specific instantiation of `add_val_def` used to prove the latter. -/ | |
| theorem add_val_spec {r : R} (hr : r ≠ 0) : |
There was a problem hiding this comment.
Yes, add_val_def is the useful version. Even though it's not the actual definition, it's the "mathematician's definition" of the additive valuation. I'm not sure if add_val_spec is a specific instantiation of add_val_def -- I'm not really sure I understand what that means.
|
✌️ kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with |
robertylewis
added
awaiting-author
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
|
bors merge |
github-actions
bot
added
ready-to-merge
) Following the approach used for p-adic numbers, we define an additive valuation on a DVR R as a bare function v: R -> nat, with the convention that v(0)=0 instead of +infinity for convenience. Note that we have no `hom` structure (like `monoid_hom` or `add_monoid_hom`) for v(a*b)=v(a)+v(b) and anyway this doesn't even hold if ab=0. We prove all the usual axioms.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Following the approach used for p-adic numbers, we define an additive valuation on a DVR R as a bare function v: R -> nat, with the convention that v(0)=0 instead of +infinity for convenience. Note that we have no
homstructure (likemonoid_homoradd_monoid_hom) for v(a*b)=v(a)+v(b) and anyway this doesn't even hold if ab=0. We prove all the usual axioms.The "correct" thing to define is a multiplicative map but the ideal target would be with_zero (multiplicative nat), and we can't use valuations for this right now, because this isn't a group with zero. In future I propose to change the target of a valuation from a group_with_zero to a monoid_with_zero (still totally ordered), but I have to make two more ordered monoid classes before I can do this the way I want to do it.