Absolute values & multiplicative ring norms

Stream: maths

[Yaël Dillies]

What is the difference supposed to be between multiplicative ring norms and absolute values? The following proves that they are the same under [ring R] [linear_ordered_comm_ring S] [nontrivial R] [is_domain S]:

import algebra.order.absolute_value

instance ohuh {R S : Type*} [ring R] [ordered_comm_ring S] [nontrivial R] [is_domain S] :
  mul_ring_norm_class (absolute_value R S) R S :=
{ map_neg_eq_map := λ f, f.map_neg,
  eq_zero_of_map_eq_zero := λ f a, f.eq_zero.1,
  ..absolute_value.subadditive_hom_class, ..absolute_value.monoid_with_zero_hom_class }

def uhoh {R S F : Type*} [ring R] [linear_ordered_semiring S] [mul_ring_norm_class F R S] (f : F) :
  absolute_value R S :=
{ to_fun := f,
  map_mul' := map_mul f,
  nonneg' := map_nonneg f,
  eq_zero' := λ _, map_eq_zero_iff_eq_zero f,
  add_le' := map_add_le_add f }

[Yaël Dillies]

cc @María Inés de Frutos Fernández

[Antoine Chambert-Loir]

Do you mean, besides the fact that norms take their values in real numbers, while for absolute values arbitrary ordered monoids are allowed? — nothing.

[Eric Wieser]

docs#mul_ring_norm_class doesn't require the norm to be a real number either, @Antoine Chambert-Loir

[Antoine Chambert-Loir]

Actually, people like Roland Huber call norms docs#absolute_value, more precisely, he studies seminorms, hence the variant of docs#absolute_value where the stuff can be zero on nonzero elements. (They must be in mathlib , otherwise I can't understand how @Kevin Buzzard managed to study perfectoids…)

[Antoine Chambert-Loir]

Eric Wieser said:

docs#mul_ring_norm_class doesn't require the norm to be a real number either, Antoine Chambert-Loir

What is docs#mul_ring_norm as compared with docs#mul_ring_norm_class ?

[Eric Wieser]

I think I see what you're getting at; it is a bit odd how docs#mul_ring_norm is restricted to reals but docs#mul_ring_norm_class isn't. Usually the class version is essentially identical to the structure.

[Antoine Chambert-Loir]

Shouldn't there a coherent way to define structures/typeclasses hand in hand, with just a kind of @[to_class] label?

[Eric Wieser]

I think that was dismissed as "something to try in Lean 4", which now means "something to try after the port"

[Adam Topaz]

The target of docs#valuation don't need a semiring structure

[Adam Topaz]

That's the main difference

[Yaël Dillies]

because it involves max instead of + in the codomain, right

[Yaël Dillies]

But here I am concretely talking about mul_ring_norm_class and absolute_value. The discussion seems to conclude that there really shouldn't be any difference.

[Yaël Dillies]

Does that mean I have approval from both the algebra and analysis worlds to merge them into one hom structure + one hom class? If so, should I keep absolute_value or mul_ring_norm as a name?

[María Inés de Frutos Fernández]

I have been away and I just saw the discussion. Yes, absolute_value and mul_ring_norm are equivalent. I am not sure about which name I would prefer to keep - maybe absolute_value is more common, but mul_ring_norm is consistent with the ring_seminorm, etc. nomenclature in mathlib.

[Yaël Dillies]

@Antoine Chambert-Loir, @María Inés de Frutos Fernández, what typeclass assumptions would satisfy both uses? Currently we have

• [non_assoc_ring α] [ordered_semiring β] for docs#mul_ring_norm_class
• [semiring α] [ordered_semiring β] for docs#absolute_value

[Antoine Chambert-Loir]

Why does one require [non_assoc_ring α] and the other one [semiring α]?
Is there something such as [non_assoc_semiring α]?
Moreover, non archimedean valuations are usually defined on a ring, and take their values into an ordered abelian group extended with a 0 element, a structure that becomes an ordered semiring using (min, +) algebra. (All conventions exist in respectable math texts, with respect to the group law should be additive or multiplicative, and the ordering of the triangular inequality…).

[Yaël Dillies]

The problem here is that we want f (-a) = f a for (multiplicative) ring norms, but it's true for absolute values only under stronger conditions ([ring R] [ordered_comm_ring S] [no_zero_divisors S], see docs#absolute_value.map_neg).

[Yaël Dillies]

docs#non_assoc_semiring exists, FWIW

[Yaël Dillies]

Is it reasonable to add f (-a) = f a as an axiom to absolute_value? That will have the cost of requiring α to be a ring, as opposed to just a semiring.

[Yaël Dillies]

To be quite fair, f (-a) = f a holds for absolute values according to Wikipedia's definition, because they define absolute values on integral domains only.

[Yaël Dillies]

And to clarify, the non_assoc isn't the main difference. Most of algebra.order.absolute_value generalises to non associative (semi)rings (I just tried), but likely it isn't very interesting mathematically.

[Yaël Dillies]

See branch#unify_absolute_value_mul_ring_norm for thoughts.

[Eric Wieser]

I think being able to state that id is an absolute value function on the naturals is sensible to support

[Yaël Dillies]

Is it, though? Applications here are field theoretic and analytic.