MulRingNorm vs. AbsoluteValue

Stream: mathlib4

[Michael Stoll]

Is there a good reason to have MulRingNorm R in addition to AbsoluteValue R ℝ? Both are essentially equivalent:

import Mathlib.Analysis.Normed.Ring.Seminorm

variable {R : Type*} [Ring R] [Nontrivial R]

def mulRingNormEquivAbsoluteValue : MulRingNorm R ≃ AbsoluteValue R ℝ where
  toFun N := {
    toFun := N.toFun
    map_mul' := N.map_mul'
    nonneg' := apply_nonneg N
    eq_zero' x := ⟨N.eq_zero_of_map_eq_zero' x, fun h ↦ h ▸ N.map_zero'⟩
    add_le' := N.add_le'
  }
  invFun v := {
    toFun := v.toFun
    map_zero' := (v.eq_zero' 0).mpr rfl
    add_le' := v.add_le'
    neg' := v.map_neg
    map_one' := v.map_one
    map_mul' := v.map_mul'
    eq_zero_of_map_eq_zero' x := (v.eq_zero' x).mp
  }
  left_inv N := by ext1 x; simp only [MulRingSeminorm.toFun_eq_coe] -- `simp` does not work
  right_inv v := by ext1 x; simp

lemma mulRingNormEquivAbsoluteValue_apply (N : MulRingNorm R) (x : R) :
    mulRingNormEquivAbsoluteValue N x = N x := rfl

lemma mulRingNormEquivAbsoluteValue_symm_apply (v : AbsoluteValue R ℝ) (x : R) :
    mulRingNormEquivAbsoluteValue.symm v x = v x := rfl

(docs#MulRingNorm eats a docs#NonAssocRing and docs#AbsoluteValue eats a docs#Semiring, but I assume that one could weaken this to docs#NonAssocSemiring if desired. docs#AbsoluteValue is more general; the target does not have to be the real numbers.)

I came across this when looking up Ostrowski's Theorem in Mathlib (Rat.MulRingNorm.mulRingNorm_equiv_standard_or_padic; I was surprised that it is stated in terms of MulRingNorm and not AbsoluteValue.

Would it be OK to get rid of MulRingNorm R in favor of AbsoluteValue R Real?

[Yaël Dillies]

I was the one adding docs3#mul_ring_norm before immediately noticing that there was docs3#absolute_value. The issue is that docs#AbsoluteValue is mathematically correct only when the domain is a ring, and at the time I didn't know how to generalise it to semirings. If you know how to do that, then docs#MulRingNorm can go, yes!

[Michael Stoll]

I guess one could just add the neg' and map_one' fields to the definition of AbsoluteValue?

[Michael Stoll]

Maybe I'll have time to look into that. It would be good to have one standard spelling in view of developing the theory of heights...

[Yaël Dillies]

Michael Stoll said:

I guess one could just add the neg' and map_one' fields to the definition of AbsoluteValue?

But then it wouldn't apply to semirings?

[Kevin Buzzard]

I am a bit confused by the latter part of this discussion. The proposal is to ditch the declaration which asks for a ring and to keep the semiring version, right? So what needs generalizing?

[Michael Stoll]

Are there use cases for docs#MulRingNorm when the "ring" is not associative?

[Kevin Buzzard]

@Jireh Loreaux maybe is the person to ask?

[Jireh Loreaux]

I don't know of any, although I wouldn't say I'm an expert on non-associative material.

[Michael Stoll]

So maybe a minimally invasive approach would be to

• add some text to the docstring of docs#MulRingNorm that says that one should prefer docs#AbsoluteValue where possible, and
• follow this advice throughout Mathlib, adding API for docs#AbsoluteValue where necessary.

[Michael Stoll]

@David Ang @Fabrizio Barroero @Laura Capuano @Nirvana Coppola @María Inés de Frutos Fernández @Sam van G @Silvain Rideau-Kikuchi @Amos Turchet @Francesco Veneziano (I hope I got the authors of file#Mathlib/NumberTheory/Ostrowski correct)

It looks like file#Mathlib/NumberTheory/Ostrowski is basically the only customer of #MulRingNorm . Can you explain why you settled on using that instead of docs#AbsoluteValue ? And would you be opposed to switching over to docs#AbsoluteValue for the results in that file?

[Fabrizio Barroero]

We started the project that lead to  file#Mathlib/NumberTheory/Ostrowski during the #LFTCM 2024 workshop in March 2024 under the guidance of @María Inés de Frutos Fernández. If I remember correctly we had an old incomplete Lean 3 project and we took some definitions and statements from there. I do not know why the authors of that project used docs#MulRingNorm instead of docs#AbsoluteValue. Maybe @María Inés de Frutos Fernández, who was leading that project too, knows the reason for that choice.
In any case I am happy to help translating the content of file#Mathlib/NumberTheory/Ostrowski using  docs#AbsoluteValue

[Kevin Buzzard]

It would not surprise me if the very long journey towards Ostrowski (which I'd been pushing for years, I would often suggest it to undergrads) started before MulRingNormAbsoluteValue existed.

[Michael Stoll]

@Kevin Buzzard Did you mean AbsoluteValue instead of MulRingNorm?

[Michael Stoll]

#20362 refactors Ostrowski. Labeled awaiting-zulip for the time being.

The API material on docs#AbsoluteValue should be moved before merging.

[Fabrizio Barroero]

Michael Stoll said:

#20362 refactors Ostrowski. Labeled awaiting-zulip for the time being.

The API material on docs#AbsoluteValue should be moved before merging.

Very nice!

[Johan Commelin]

@Michael Stoll Thanks! If you want to move the API material to the right place, then I think we should merge this.

[Michael Stoll]

Will do.

[Michael Stoll]

I'm going to move Algebra.Order.AbsoluteValue to Algebra.Order.AbsoluteValue.Basic (creating a new folder) and will add a file Algebra.Order.AbsoluteValue.Equivalence for material about equivalent real-valued absolute values (this needs powers with real exponents, and Real is not visible in the current Algebra.Order.AbsoluteValue).
I've noticed that there is Algebra.Order.EuclideanAbsolutevalue. I think it makes sense to move that to Algebra.Order.AbsoluteValue.Euclidean at the same time. Are there objections to that?

[Johan Commelin]

Sounds good

[Michael Stoll]

#20362 should now be ready.

[Michael Stoll]

#20557 does the after-the-fact housekeeping:

• deprecate the docs#MulRingNorm related declarations that were copied to docs#AbsoluteValue for Ostrowski
• add the recommendation to use docs#AbsoluteValue instead of docs#MulRingNorm at the appropriate places
• add the equivalence between MulRingNorm R and AbsoluteValue R ℝ
• add NormedField.toAbsoluteValue for completeness

It also renames docs#AbsoluteValue.Equiv to IsEquiv, which I think is better as it is a Prop.