Setting up ultrametric spaces

Stream: lean4

[Sophie Morel]

With some colleagues, we are trying to formalize the theory of ultrametric spaces in Lean4, where the ultrametric distance is allowed to take values in any linear order (with a Bot acting as 0). My first idea was to take Mathlib.Topology.MetricSpace.Basic and adapt it, and also to put a MetricSpace instance on an ultrametric space whose distance takes values in nonnegative reals. I quickly ran into problems when I tried to put a UniformSpace instance on a pseudo ultrametric space. Here is a (somewhat M)WE, where I ignore the bornology:

import Mathlib.Tactic
import Mathlib.Tactic.Positivity
import Mathlib.Topology.Algebra.Order.Compact
import Mathlib.Topology.MetricSpace.EMetricSpace
import Mathlib.Topology.Bornology.Constructions
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Order.Filter.Basic
import Mathlib.Topology.UniformSpace.Basic


open Set Filter TopologicalSpace
open scoped BigOperators Uniformity Topology

universe u v w

variable {α : Type u} {β : Type v} [LinearOrder β]


/-- Define a `UniformSpace` using a "ultradistance" function. The function can be, e.g., the
distance in an ultrametric space or a nonarchimedean norm. -/


def UniformSpace.ofUltrafun {α : Type u} {β : Type v} [LinearOrder β]
    (d : α → α → WithZero β) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
    (triangle : ∀ x y z, d x z ≤ max (d x y) (d y z)) :
    UniformSpace α :=
.ofCore
  { uniformity := ⨅ r > 0, 𝓟 { x | d x.1 x.2 < r }
    refl := by
      simp only [gt_iff_lt, not_lt, le_iInf_iff, le_principal_iff, mem_principal, idRel_subset, mem_setOf_eq]
      exact fun _ hpos a => by rw [refl a]; exact hpos
    symm := by simp only [gt_iff_lt, not_lt, tendsto_iInf, tendsto_principal, mem_setOf_eq, Prod.fst_swap, Prod.snd_swap]
               intro i hpos
               unfold Filter.Eventually
               simp only
               apply Filter.mem_iInf_of_mem i; apply Filter.mem_iInf_of_mem
               simp only [mem_principal, setOf_subset_setOf, Prod.forall]
               exact fun _ _ hab => by rw [symm]; exact hab
               exact hpos
    comp := by simp only [gt_iff_lt, not_lt, le_iInf_iff, le_principal_iff]
               intro i hpos
               unfold Filter.lift'
               unfold Filter.lift
               apply Filter.mem_iInf_of_mem ({ x | d x.1 x.2 < i})
               apply Filter.mem_iInf_of_mem
               simp only [Function.comp_apply, mem_principal]
               rw [Set.subset_def]
               simp only [mem_setOf_eq, Prod.forall, mem_compRel, forall_exists_index, and_imp]
               intro a b x hax hxb
               apply lt_of_le_of_lt (triangle a x b)
               simp only [ge_iff_le, max_lt_iff]
               exact ⟨hax, hxb⟩
               apply Filter.mem_iInf_of_mem i; apply Filter.mem_iInf_of_mem
               simp only [mem_principal, setOf_subset_setOf, imp_self, Prod.forall, implies_true]
               exact hpos
               }


/-- Construct a uniform structure from an ultradistance function and ultrametric space axioms -/
def UniformSpace.ofUltradist (udist : α → α → WithZero β) (udist_self : ∀ x : α, udist x x = 0)
    (udist_comm : ∀ x y : α, udist x y = udist y x)
    (udist_strong_triangle : ∀ x y z : α, udist x z ≤ max (udist x y) (udist y z)) : UniformSpace α :=
  .ofUltrafun udist udist_self udist_comm udist_strong_triangle



/-- The ultradistance function (given an ambient ultrametric space on `α`), which returns
  an element of WithZero β `udist x y` given `x y : α`. -/
@[ext]
class Ultradist (α : Type _) (β : Type _) [LinearOrder β] where
  udist : α → α → WithZero β

export Ultradist (udist)

/- Pseudo ultrametric spaces-/

class PseudoUltrametricSpace (α : Type u) (β : Type v) [LinearOrder β] extends Ultradist α β : Type (max u v) where
  udist_self : ∀ x : α, udist x x = 0
  udist_comm : ∀ x y : α, udist x y = udist y x
  udist_strong_triangle : ∀ x y z : α, udist x z ≤ max (udist x y) (udist y z)
  toUniformSpace : UniformSpace α := .ofUltradist udist udist_self udist_comm udist_strong_triangle
  uniformity_udist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | udist p.1 p.2 < ε } := by intros; rfl



variable [PseudoUltrametricSpace α β]

attribute [instance] PseudoUltrametricSpace.toUniformSpace --  cannot find synthesization order for instance @PseudoUltrametricSpace.toUniformSpace with type
  --{α : Type u} → (β : Type v) → [inst : LinearOrder β] → [self : PseudoUltrametricSpace α β] → UniformSpace α all remaining arguments have metavariables:
  -- LinearOrder ?β @PseudoUltrametricSpace α ?β ?inst✝

Is the problem that the pseudo ultrametric space depends on the parameters α and β, while only α explicitly appears in the the uniform space ?

[Sophie Morel]

Also, more generally, I wonder if this is the right way to proceed or if it will cause trouble in the future. For example:
(1) While it cause trouble for ultrametric spaces with real-valued distance function to a have a MetricSpace instance ? They would then get UniformSpace instances from the ultrametric space and the metric space structures.
(2) What about spaces with two "natural" ultrametric distances, for example a finite extension of $\mathbb{Q}_p$ with either its normalization valuation, or the unique extension of the normalized valuation of $\mathbb{Q}_p$ ? It would also get two UniformSpace instances from that. Is there a better way to proceed that would avoid this problem, or are we doomed to pain one way or another ?

[Johan Commelin]

In the latter example, I think we should define both ultrametrics, but we shouldn't mark them as instance globally. Then people can choose which one the want to use on a local level.

[Yaël Dillies]

Can't explain much more right now, but you're basically hitting the same problem that made us specialise metric_space to real in the first place. In the case of ultrametric spaces, have you tried making them a non-class structure? that is, work with the type of ultrametrics, rather than with a canonical ultrametric space?

[Olivier Taïbi]

yes, the alternative that we see is to mimic the Valuation/Valued design, do you recommend it?

[Yaël Dillies]

Yes, I believe it will spare you a lot of pain, at the cost of making some steps (eg translation from and to a metric space)

[Johan Commelin]

I don't know the details, but in the measure theory library there is a solution to have a "default measure" on a space, but still it is quite convenient to integrate against a different measure if needed. Maybe a similar thing can be done for ultrametrics?

[Patrick Massot]

Bienvenue Olivier !

[Patrick Massot]

Sophie, you immediate issue can be solved by marking β as outParam. For instance class Ultradist (α : Type _) (β : outParam $ Type _) [LinearOrder β]. This tells the type class resolution system to look for β later.

[Patrick Massot]

And then indeed you can probably take inspiration from docs4#Valued.

[Sophie Morel]

Yaël Dillies said:

Can't explain much more right now, but you're basically hitting the same problem that made us specialise metric_space to real in the first place. In the case of ultrametric spaces, have you tried making them a non-class structure? that is, work with the type of ultrametrics, rather than with a canonical ultrametric space?

I'm afraid I don't know enough to apply that suggestion, sorry. I don't know what exactly a class is except the name of certain types of structures in mathlib... I clearly need to spend some more time thinking about this.

[Eric Wieser]

I'm also not sure what Yael means there. I think that decision was before my time, but I suspect it was done that way just because no one needed the generalization

[Eric Wieser]

docs#inner_product_space is an example of a similar typeclass design that doesn't limit the output type to real

[Sophie Morel]

Patrick Massot said:

Sophie, you immediate issue can be solved by marking β as outParam. For instance class Ultradist (α : Type _) (β : outParam $ Type _) [LinearOrder β]. This tells the type class resolution system to look for β later.

Thanks Patrick ! Your suggestion worked, for now, and though we'll probably have to rewrite the file entirely I learned something useful. Now I just want universes problems to pop up too so that I can use the tricks I learned in the other thread. :grinning_face_with_smiling_eyes:

So it seems that it might be better to make UltrametricSpace a class that extends UniformSpace ? (And probably Bornology as well.)

[Eric Wieser]

Is there a reason you're using [LinearOrder β] and WithZero β instead of [OrderBot β] [LinearOrder β] and β?

[Sophie Morel]

Eric Wieser said:

docs#inner_product_space is an example of a similar typeclass design that doesn't limit the output type to real

Interesting, thank you for the reference !
We had the "real versus more general value groups" discussion, and decided that we didn't want to restrict to reals, as valuations of rank greater than 1 are becoming more and more important in p-adic geometry.

[Adam Topaz]

I think the target of your ultradist should be a LinearOrderedCommMonoidWithZero, similar to how it's done in docs4#Valuation

[Sophie Morel]

Eric Wieser said:

Is there a reason you're using [LinearOrder β] and WithZero β instead of [OrderBot β] [LinearOrder β] and β?

Well, it was because, except for $\mathbb{R}_{\geq 0}$, all the other value groups that I have met do arise as linearly ordered commutative groups with a smallest element added, so it seemed like a natural thing to do. But later I also thought about using [Zero β] [LinearOrder β] instead, and it certainly seems as if it would make the comparison with metric spaces easier. So it's up for debate.

If you have any wisdom on that subject (for example, if you can see that one of the solutions would lead to much more pain down the road), then I would be glad to listen to it.

[Sophie Morel]

Adam Topaz said:

I think the target of your ultradist should be a LinearOrderedCommMonoidWithZero, similar to how it's done in docs4#Valuation

Hi Adam, to make sense of the definition of an ultrametric we don't even need an addition, just an order with a smallest element and a notion of the max of two elements, i.e. a SemilatticeSup with a Bot. Even the LinearOrder is too much and I have been feeling a bit guilty about using it. For later I agree that we should not jump into ordered groups too quickly and stick with ordered monoids as long as possible.

[Adam Topaz]

Oh, I see okay. In that case, I do agree with Eric

[Adam Topaz]

Have you tried using SemilatticeSup?

[Sophie Morel]

Adam Topaz said:

Have you tried using SemilatticeSup?

In the next version I probably will try !

[Sophie Morel]

(Although I am not alone in this, so maybe I will be overruled by my more reasonable colleagues.)

[Eric Wieser]

[Zero β] [LinearOrder β] is not the same as [LinearOrder β] [OrderBot β], as the former does not require that 0 be the lowest element

[Sophie Morel]

Eric Wieser said:

[Zero β] [LinearOrder β] is not the same as [OrderBot β] [LinearOrder β], as the former does not require that 0 be the lowest element

Ah, thank ! Then I definitely want the second and not the first.

[Eric Wieser]

But as Adam says, you might only need [SemiLatticeSup β] [OrderBot β]

[Adam Topaz]

The annoying thing is that if and when you do want to relate this to some valuation, it may be annoying to go back and forth between \bot and 0.

[Eric Wieser]

Right, it's very believable that all this generality is useless and LinearOrderedCommMonoidWithZero is enough (as you said above)

[Sophie Morel]

Eric Wieser said:

Right, it's very believable that all this generality is useless and LinearOrderedCommMonoidWithZero is enough (as you said above)

I thought that one of the principles of Lean was that you don't put conditions on stuff before you actually need them.

[Adam Topaz]

Within reason :)

[Sophie Morel]

The addition is totally irrelevant to the definition of an ultrametric and only appears when you define a valuation on something that has a multiplication.

[Eric Wieser]

For a counterexample, see docs#module; that doesn't "need" add_comm_monoid, has_add and has_zero would suffice; but no one cares about that generality

[Eric Wieser]

docs#LinearOrderedCommMonoidWithZero has no addition though?

[Adam Topaz]

It's multiplication. Mathlib's valuations have multipicative value groups

[Sophie Morel]

Eric Wieser said:

docs#LinearOrderedCommMonoidWithZero has no addition though?

It has a commutative binary operation, which I was calling "addition".

[Sophie Morel]

To define an ultrametric, you only to know what the max of two elements is. This is a purely order-theoretic thing.

[Eric Wieser]

If you're going to call the binary operation "+", then you'll need to call the unit "0", and so now the zero you added is called "bot" after all

[Sophie Morel]

Though it is not my field, I know that there are people who study ultrametric spaces unconnected to any valued ring. If I can set up a theory that would be useful to them without making my life too complicated, then I think this is a valuable thing to do.

[Eric Wieser]

(I should probably mention that I know very little about ultrametric spaces, only about mathlib's order and algebra)

[Sophie Morel]

Eric Wieser said:

If you're going to call the binary operation "+", then you'll need to call the unit "0", and so now the zero you added is called "bot" after all

When I start using it in Lean, I'll call it whatever mathlib calls it. But in my non-Lean life, I call the operation +, the unit element 0 and the smallest element $-\infty$, so it bled over into this discussion. Sorry for the confusion.

[Adam Topaz]

But even that's backwards, isn't it? I'm used to valuations taking values in $\Gamma \cup \{\infty\}$ and taking $\exp(-v(-))$ for the absolute value in the rank 1 case.

[Adam Topaz]

We have docs4#AddValuation

[Sophie Morel]

Adam Topaz said:

But even that's backwards, isn't it? I'm used to valuations taking values in $\Gamma \cup \{\infty\}$ and taking $\exp(-v(-))$ for the absolute value in the rank 1 case.

From what I've seen, both definitions are used, with the same name ! It's all very confusing. And some people use "absolute value" sometimes, to add to the confusion.

[Sophie Morel]

Adam Topaz said:

But even that's backwards, isn't it? I'm used to valuations taking values in $\Gamma \cup \{\infty\}$ and taking $\exp(-v(-))$ for the absolute value in the rank 1 case.

Yeah, "additive valuations" and "multiplicative valuations"... I remember the day I realized they were the same up to reversing the order on the value group and changing the name of the binary operation, and that day I cursed the people who had invented the terminology.
Since mathlib made a choice in the definition of Valued, I'm quite willing to stick with it.

[Adam Topaz]

lean+mathlib has actually convinced me that the multiplicative variant is the "right" choice.

[Sophie Morel]

Adam Topaz said:

lean+mathlib has actually convinced me that the multiplicative variant is the "right" choice.

I'm not that far along, I don't think there's a right choice. You'll still get people who complain that with your definition the "p-adic valuation" is not a valuation (to which I'd reply, "just take minus the p-adic valuation and imagine that $\mathbb{Z}$ multiplicative". :stuck_out_tongue:)
But I think it's useful to make a choice and stop confusing people.

[Olivier Taïbi]

many thanks for the advices