Hyperbolic space

Stream: mathlib4

[Oliver Nash]

In an experiment to see if I could use the lovely work of @Patrick Massot @Michael Rothgang @Sébastien Gouëzel and others to say something about hyperbolic space, I came up with the following (for the two-dimensional case):

import Mathlib.Analysis.Complex.UpperhalfPlane.Metric
import Mathlib.Geometry.Manifold.Riemannian.Basic
-- import Mathlib.Geometry.Manifold.Riemannian.PathELength
-- import Mathlib.Geometry.Manifold.VectorBundle.Tangent

noncomputable section

namespace UpperHalfPlane

open Bundle
open scoped ContDiff ENNReal UpperHalfPlane

local notation "𝓘ℍ" => modelWithCornersSelf ℝ ℂ
local notation "Tℍ" => fun x : ℍ ↦ TangentSpace 𝓘ℍ x

instance : ChartedSpace ℂ ℍ := isOpenEmbedding_coe.toPartialHomeomorph.singletonChartedSpace rfl
instance : IsManifold 𝓘ℍ ∞ ℍ := isOpenEmbedding_coe.toPartialHomeomorph.isManifold_singleton rfl

def riemannianMetric : RiemannianMetric Tℍ where
  inner x := (1 / x.im ^ 2) • innerSL ℝ (E := ℂ) -- TODO Do this without defeq abuse
  symm := sorry
  pos := sorry
  continuousAt := sorry
  isVonNBounded := sorry

instance : RiemannianBundle Tℍ := ⟨riemannianMetric⟩

instance : IsRiemannianManifold 𝓘ℍ ℍ := by
  refine ⟨fun x y ↦ ?_⟩
  rw [edist_dist, dist_eq]
  -- Argue that length-minimising arcs are subsets of lines / circles perpendicular to real line.
  -- Should be possible by arguing these are preserved by `SL(2, ℝ)` action which we know is
  -- isometric thanks to `UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal`
  sorry

-- After a long wait (~105 seconds on my fast MacBook) this says `(kernel) deterministic timeout`
-- instance : IsContMDiffRiemannianBundle 𝓘ℍ ∞ ℂ Tℍ := sorry

end UpperHalfPlane

[Oliver Nash]

I have three questions:

1. What is the right way to avoid the defeq abuse in riemannianMetric. I was quite surprised that I could not find (the general version of) example (x : ℍ) : Tℍ x ≃L[ℝ] ℂ := sorry in the library.
2. If I uncomment the last statement instance : IsContMDiffRiemannianBundle 𝓘ℍ ∞ ℂ Tℍ := sorry then as I remark in the comment, Lean pegs a CPU at 100% for nearly two minutes and then just says (kernel) deterministic timeout. Am I doing something wrong?
3. Does anyone want to try to prove the non-trivial sorry?

[Michael Rothgang]

I may be interested in some of (3) --- but let me finish proving the existence of Riemannian metrics first. :-)

[Michael Rothgang]

For (1), I suspect the proper generality is proving

• ℍ is an open subset of ℂ, hence Tℍ≃L[ℝ] Tℂ
• there's an isomorphism T𝕜 ≃L[𝕜] 𝕜 for any nontrivially normed field 𝕜

and then composing these isomorphisms.
Patrick and I have the second one on our big branch; I could PR that soon. I'm really surprised that the first one is missing.

[Michael Rothgang]

For (2): what happens when you upgrade your sorry about to a ContMDiffRiemannianMetric?

[Michael Rothgang]

Update: that helps; here's my version

import Mathlib.Analysis.Complex.UpperHalfPlane.Metric
import Mathlib.Geometry.Manifold.Riemannian.Basic
import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
-- import Mathlib.Geometry.Manifold.Riemannian.PathELength
-- import Mathlib.Geometry.Manifold.VectorBundle.Tangent

noncomputable section

namespace UpperHalfPlane

open Bundle
open scoped ContDiff ENNReal UpperHalfPlane

local notation "𝓘ℍ" => modelWithCornersSelf ℝ ℂ
local notation "Tℍ" => fun x : ℍ ↦ TangentSpace 𝓘ℍ x

instance : ChartedSpace ℂ ℍ := isOpenEmbedding_coe.toPartialHomeomorph.singletonChartedSpace rfl
instance : IsManifold 𝓘ℍ ∞ ℍ := isOpenEmbedding_coe.toPartialHomeomorph.isManifold_singleton rfl

def riemannianMetric : ContMDiffRiemannianMetric 𝓘ℍ ∞ ℂ Tℍ where
  inner x := (1 / x.im ^ 2) • innerSL ℝ (E := ℂ) -- TODO Do this without defeq abuse
  symm := sorry
  pos := sorry
  isVonNBounded := sorry
  contMDiff := sorry

instance : RiemannianBundle Tℍ := ⟨riemannianMetric.toRiemannianMetric⟩

instance : IsRiemannianManifold 𝓘ℍ ℍ := by
  refine ⟨fun x y ↦ ?_⟩
  rw [edist_dist, dist_eq]
  -- Argue that length-minimising arcs are subsets of lines / circles perpendicular to real line.
  -- Should be possible by arguing these are preserved by `SL(2, ℝ)` action which we know is
  -- isometric thanks to `UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal`
  sorry

#synth IsContMDiffRiemannianBundle 𝓘ℍ ∞ ℂ Tℍ -- is really fast

instance : IsContMDiffRiemannianBundle 𝓘ℍ ∞ ℂ Tℍ := by infer_instance -- is slow
-- After a long wait (~105 seconds on my fast MacBook) this says `(kernel) deterministic timeout`
--instance : IsContMDiffRiemannianBundle 𝓘ℍ ∞ ℂ Tℍ := sorry

end UpperHalfPlane

[Michael Rothgang]

So, Lean can infer the instance just fine --- but putting a new instance is really slow. I have no idea why, but would be very interested in explanations!

[Sébastien Gouëzel]

For 1, I'd say the defeq abuse is here to be abused -- in paper maths, you would write things exactly as you did here.

For 2, you are doing things perfectly right, and there is something fishy going on. I tried to investigate a little bit, but I couldn't understand what is wrong for now.

[Michael Rothgang]

About (2): since you're never stating continuity/smoothness of your metric, there's no way #synth IsContMDiffRiemannianBundle 𝓘ℍ ∞ ℂ Tℍ can succeed. So, strengthening the statement still feels right to me.

[Michael Rothgang]

I don't think Lean should take so long to fail, though: that is definitely not good.

[Sébastien Gouëzel]

Yes, for (2) I was talking about @Michael Rothgang's version, where the metric is defined as a ContMDiffRiemannianMetric.

[Sébastien Gouëzel]

Somewhat minimized, still not there:

import Mathlib

noncomputable section

namespace UpperHalfPlane

open Bundle
open scoped ContDiff ENNReal UpperHalfPlane

local notation "𝓘ℍ" => modelWithCornersSelf ℝ ℂ
local notation "Tℍ" => fun x : ℍ ↦ TangentSpace 𝓘ℍ x

instance : IsManifold 𝓘ℍ ∞ ℍ := isOpenEmbedding_coe.toPartialHomeomorph.isManifold_singleton rfl

irreducible_def riemannianMetric : ContMDiffRiemannianMetric 𝓘ℍ ∞ ℂ Tℍ := sorry

lemma works : VectorBundle ℝ ℂ fun (x : ℍ) ↦ TangentSpace 𝓘ℍ x := by infer_instance

instance : RiemannianBundle Tℍ := ⟨riemannianMetric.toRiemannianMetric⟩

def doesntwork : VectorBundle ℝ ℂ fun (x : ℍ) ↦ TangentSpace 𝓘ℍ x := by
  sorry

[Michael Rothgang]

Interesting, thanks for minimising! Is the upper half plane important for this example (or would e.g. working with C itself also work)?

[Oliver Nash]

Thank you both for corrections and investigations!

[Sébastien Gouëzel]

ok, I found it.

import Mathlib

noncomputable section

namespace UpperHalfPlane

open Bundle
open scoped ContDiff ENNReal UpperHalfPlane

local notation "𝓘ℍ" => modelWithCornersSelf ℝ ℂ

def foo (x : ℍ) : AddCommMonoid (TangentSpace 𝓘ℍ x) := by infer_instance

#print foo
/- NormedAddCommGroup.toENormedAddCommMonoid.toAddCommMonoid : AddCommMonoid (TangentSpace 𝓘ℍ x) -/

Before any Riemannian stuff, the AddCommMonoid instance on the tangent space to ℍ is inferred from a normed space structure. So when one registers another normed space structure on the tangent space through the Riemannian bundle business, we have two conflicting instances, and boom. The thing is that, initially, there shouldn't be any normed space structure on the tangent space. And in fact there isn't: if you ask for NormedAddCommGroup (TangentSpace 𝓘ℍ x), it fails as it should. But still this non-existing instance is summoned out of nowhere to construct the AddCommMonoid instance. This is a bug in Lean4, lean4#9077 striking again.

I could try to work around it by tweaking instances and so on, but I am afraid we will see it again and again, so I'm not sure it's worth it. Better fix it upstream, but @Sebastian Ullrich said on the issue that the bug won't be fixed. So I don't really know what to do, because I feel this bug should be really high-priority from the point of view of mathlib. Also, I don't know how much this is related to recent PRs by @Jovan Gerbscheid to fix some issue in typeclass inference (where the implementation doesn't really match the specs). @Kim Morrison, do you have an idea of how we could move forward on this?

[Sébastien Gouëzel]

Another example of boom, more minimal than the one reported in the issue, but still depending on mathlib:

import Mathlib

def myFoo : Type := ℂ

noncomputable instance : TopologicalSpace myFoo := inferInstanceAs (TopologicalSpace ℂ)
noncomputable instance : ENormedAddCommMonoid myFoo := by infer_instance

myFoo is only endowed with a topological space instance, but it inherits the enormed structure from ℂ.

Note that things are a little bit subtle here (and therefore hard to minimize) because, with ℝ instead of ℂ, the issue disappears.

[Matthew Ballard]

Has this been observed?

import Mathlib

def myFoo : Type := ℂ

noncomputable instance : TopologicalSpace myFoo := inferInstanceAs (TopologicalSpace ℂ)
set_option trace.Meta.synthInstance true in
-- uncomment below to get a failing #synth
-- noncomputable instance : NormedAddCommGroup myFoo := by infer_instance
#synth ENormedAddCommMonoid myFoo -- NormedAddCommGroup.toENormedAddCommMonoid

I can guess why but this is not ideal behavior.

[Edward van de Meent]

is this lean4#9077 ?

[Matthew Ballard]

Another incarnation, yes

[Matthew Ballard]

I think a reasonable invariant of typeclass synthesis is that if it succeeds returning X.toY to get Y then it should also succeed for X.

[Sebastian Ullrich]

We want to take another look at this issue but until that has concluded, I can't speculate on the outcome