Geodesic spaces

Stream: maths

[Horatiu Cheval]

I am trying to define geodesic spaces. The definition I want to implement is, on paper, the following: A geodesic space is a metric space $(X, d)$ such that for all $x, y \in X$, there exists an isometry $\gamma_{x, y} : [0, d(x, y)] \to X$, such that $\gamma_{x, y}(0) = x$ and $\gamma_{x, y}((d(x, y)) = y$. I am faced with a choice between the following two definitions below, one where geodesics take arguments in set.Icc, and one where they are defined on the whole ℝ with junk values outside of the interval of interest.

import topology.metric_space.basic
import topology.metric_space.isometry

class geodesic_space1 (X : Type*) extends metric_space X :=
(geodesic : Π (x y : X), set.Icc 0 (dist x y) → X)
(geodesic_iso : ∀ x y, isometry (geodesic x y))
(left_point : ∀ x y, geodesic x y ⟨0, by simp only [set.left_mem_Icc]; apply dist_nonneg⟩ = x)
(right_point : ∀ x y, geodesic x y ⟨dist x y, by simp only [set.right_mem_Icc]; apply dist_nonneg⟩ = y)

class geodesic_space2 (X : Type*) extends metric_space X :=
(geodesic : Π x y : X, ℝ → X)
(geodesic_iso : ∀ (x y : X) (s t ∈ set.Icc 0 (dist x y)), dist (geodesic x y s) (geodesic x y t) = abs (s - t))
(left_point : ∀ x y, geodesic x y 0 = x)
(right_point : ∀ x y, geodesic x y (dist x y) = y)

Which one do you think is best? With geodesic_space1 I worry that keeping working with coercions to set.Icc might turn out cumbersome in the long run, but at the same time this allows me to use docs#isometry in the definition, so that I may easily rely on the lemmas about it.

[Sebastien Gouezel]

There is a problem with both your definitions, that you are putting data into it. Which can lead to diamonds later on. Instead, you could (should?) define it as Prop-valued (and as a mixin on metric spaces, instead of extending metric spaces) -- and then the precise definition doesn't matter, because they are equivalent. What you can do then, under the assumptions [metric_space X] [geodesic_space X], is to choose some geodesic between x and y (and I'd probably choose it as a function on Icc, but providing also the extended value on the whole line, equal to x before 0 and to yafter d(x,y) to have a globally continuous object).

[Kevin Buzzard]

If it's a prop you could call it is_geodesic_space X, which makes it easier for people to guess that it's a Prop

[Horatiu Cheval]

Thank you for the suggestions. Let me see if I understood it correctly. Is something like this what you mean?

import topology.metric_space.basic
import topology.metric_space.isometry

structure is_geodesic {X : Type*} [metric_space X] (x y : X) (γ : set.Icc 0 (dist x y) → X) : Prop :=
(iso : isometry γ)
(left_point : γ ⟨0, by simp only [set.left_mem_Icc]; apply dist_nonneg⟩  = x)
(right_point : γ ⟨dist x y, by simp only [set.right_mem_Icc]; apply dist_nonneg⟩ = y)

class is_geodesic_space (X : Type*) [metric_space X] : Prop :=
(geodesic : ∀ x y : X, ∃ γ, is_geodesic x y γ)

[Horatiu Cheval]

Also, I am not sure what do you mean by defining it on Icc while also providing the extension to the whole line? Do you mean that I should then define something like this?

noncomputable def geodesic_to_whole_line
{X : Type*} [metric_space X] (x y : X) (γ : set.Icc 0 (dist x y) → X) : ℝ → X := λ t,
if ha : t < 0 then x
else if hb : dist x y < t then y
else γ ⟨t, sorry⟩

[Yury G. Kudryashov]

Note that we have docs#set.proj_Icc

[Yury G. Kudryashov]

Also, we have some theory about paths indexed by Icc 0 1 (e.g., homotopies), so you might want to use f : Icc 0 1 → X with dist (f a) (f b) = dist x y * dist a b.