NormedGroup convention in Mathlib

Stream: mathlib4

[Sébastien Gouëzel]

The current definition we have of NormedGroup has the field dist_eq : ∀ x y, dist x y = ‖x / y‖. This means that the right action is an isometry, but not the left action in general. The other choice would be dist x y = ‖x ⁻¹ * y‖, ensuring that the left action is an isometry. One could argue that both choices are reasonable, and indeed in the early litterature both were common. However, in the last 50 years, in geometric theory the convention has settled that left actions should be isometric. This is to be seen for instance in the definition of the Cayley graph where one puts an edge between x and xs when s is in the generating set. So, Mathlib is at odds with a standard well-established convention here.

There is already a comment about that in Mathlib, saying

The current convention `dist x y = ‖x - y‖` means that the distance is invariant under right
addition, but actions in mathlib are usually from the left. This means we might want to change it to
`dist x y = ‖-x + y‖`.

I would be willing to do the refactor (although I expect it to be quite painful), but before I embark on it I wanted to check if everyone thinks it is a good idea. (I mean, there could be another area of mathematics I don't know as well where one always uses isometric right actions, and then the case would not be so clear)

[Patrick Massot]

I don’t have an opinion on this question, but I think a better title for this thread would be “NormedGroup convention in Mathlib” since there is nothing “wrong” here.

[Sébastien Gouëzel]

Renamed.

[Yaël Dillies]

I tend to agree with you.

[Edward van de Meent]

let me point out that mathlib's definition for the cayley graph (docs#SimpleGraph.circulantGraph, horrible name imo) has the right rather than left action preserving the graph:

import Mathlib.Combinatorics.SimpleGraph.Circulant

variable (G : Type*) {V : Type*}

class IsRelVAdd (r : V → V → Prop) [VAdd G V] where
  vadd_rel (g : G) : ∀ ⦃x y : V⦄, r x y → r (g +ᵥ x) (g +ᵥ y)

@[to_additive]
class IsRelSMul (r : V → V → Prop) [SMul G V] where
  smul_rel (g : G) : ∀ ⦃x y : V⦄, r x y → r (g • x) (g • y)

@[to_additive]
abbrev IsGraphSMul (U : SimpleGraph V) [SMul G V] :=
  IsRelSMul G (U.Adj)

instance [AddGroup G] (S : Set G) : IsGraphVAdd Gᵃᵒᵖ (.circulantGraph S) where
  vadd_rel g := by
    intro x y
    simp only [SimpleGraph.circulantGraph_adj, AddOpposite.vadd_eq_add_unop, add_left_inj,
      add_sub_add_right_eq_sub, imp_self]

[Edward van de Meent]

so ideally that should be fixed too

[Sébastien Gouëzel]

Yes, that's definitely among the things that the refactor would improve.

[Jireh Loreaux]

I might suggest keep the docs#dist_eq_norm lemma (not the structure field) as dist a b = ‖a - b‖, even though it would require Comm. Then add a fresh lemma for dist a b = ‖-a + b‖. This might help minimize the fallout from / effort for the PR, both in Mathlib and downstream. This is also what I would expect from a usability standpoint. The docstring for dist_eq_norm can be expanded to explain why Comm is necessary and the justification for it.