Zulip Chat Archive

Stream: Is there code for X?

Topic: Hyperbolic Geometry

Alyssa McPoyle (Jun 27 2022 at 16:10):

Have any topics in hyperbolic geometry been formalized in Lean yet? In mathlib, I see that there is Euclidean and manifold under geometry, but that is it.

Yaël Dillies (Jun 27 2022 at 16:10):

I've seen a lot in that direction by @Yury G. Kudryashov recently.

Kevin Buzzard (Jun 27 2022 at 16:11):

There's plenty of work on the upper half plane: does that count? Do you have specific theorems or definitions in mind?

Alyssa McPoyle (Jun 27 2022 at 16:13):

Yes, the upper half plane would definitely count. I was thinking more in terms of the Poincare disk initially.

Kevin Buzzard (Jun 27 2022 at 16:21):

I guess people have been doing analysis on the upper half plane (e.g. defining modular forms) rather than geometry. I'm not even sure we have the hyperbolic distance on the upper half plane. Maybe a nice project would be to define the open disc, define hyperbolic metrics on both that and the upper half plane, and then prove that they're isometric?

Alyssa McPoyle (Jun 27 2022 at 16:24):

Interesting, I'll definitely spend some time experimenting with that.

Ruben Van de Velde (Jun 27 2022 at 16:30):

Is #14703 relevant?

Kevin Buzzard (Jun 27 2022 at 16:37):

Oh nice! Note that this is an as yet unmerged PR (but you can build on it anyway ;-) )

Kevin Buzzard (Jun 27 2022 at 16:39):

/-!
# Metric on the upper half-plane
In this file we define a `metric_space` structure on the `upper_half_plane`. The distance is given
by `dist z w = 2 * arsinh (dist (z : ℂ) w / (2 * real.sqrt (z.im * w.im)))`.
-/

Alyssa McPoyle (Jun 27 2022 at 16:41):

Very relevant! Thanks

Junyan Xu (Jun 27 2022 at 16:54):

Maybe we can generalize it to the upper half-space model (any dimension) without exceeding effort?

Yury G. Kudryashov (Jun 28 2022 at 11:58):

I'm going to add the unit disc too. About upper half space: what will be the type?

Last updated: Dec 20 2023 at 11:08 UTC