Shifts (translations?) of the hyperbolic plane

Stream: maths

[Yury G. Kudryashov]

In #33368, I define Complex.UnitDisc.shift to be the automorphism of the complex unit disc given by z.shift w = (z + w) / (1 + conj z * w).

• What would be a better name for this map?
• Should we use this map or some other variation with different signs as a named Mobius automorphism of the disc?
• Should we have a special name for this kind of map at all, or should we define UnitDisc.mobius that takes c : Circle and z : UnitDisc as arguments? This way, we can encode all the automorphisms.

CC: @Sébastien Gouëzel @Geoffrey Irving

[Geoffrey Irving]

Does it obey any algebra axioms? Enough that an operator makes sense?

[Yury G. Kudryashov]

It's a way to encode the $\operatorname{SL}_2(\mathbb R)$-action.

[Yury G. Kudryashov]

(if we add a c : Circle argument)

[Yury G. Kudryashov]

Of course, yet another way is to define the action + a map from (c : Circle) (z : UnitDisc) to SL2R.

[Yury G. Kudryashov]

Yet another question is whether we want to have a version of this map as a map $\mathbb C \to \mathbb C$, or just $\mathbb D \to \mathbb D$.

[Sébastien Gouëzel]

Would it make sense to first define the PSL(2,R) action, and then define various elements of PSL(2,R) in terms of the dynamical properties we want (like a translation for your shift, or the loxodromic element given by two different points on the circle and a translation length, or elliptic elements, and so on)? I think we already have the PSL(2) action on the upper half plane, so it's just a matter of conjugating by the usual iso between the disk and the upper half plane.

[Yury G. Kudryashov]

I'll look into this later today or tomorrow.

[David Loeffler]

We do indeed already have the PSL(2, R) action on the upper half-plane – indeed a huge amount of work has gone into this because it's fundamental to the whole theory of modular forms. Elliptic, hyperbolic, parabolic elements etc were recently added, and I have some in-progress work on classifying fixed points in terms of this classification. So let's not reinvent the wheel (or the disc?) here.

[Yury G. Kudryashov]

I'm rather busy at my day job now, but I'll add an equivalence to the upper half plane and the PSL(2, R) & PSL(2, Z) actions this weekend.

[Joseph Myers]

Note that we have a very old, probably abandoned PR #7861 that apparently does something with the PSL(2, ℝ) action - could someone familiar with this part of mathlib figure out what to do with that PR?

[Yury G. Kudryashov]

Note that we have this instance for SL(2, R).