Lines in upper half-space

Solution 1:

You can rediscover the geometry if you assume that the isometries of the geometry are given by some homographies.

The group of orientation-preserving homographies who leave $\Bbb P^1(\Bbb R)$ invariant is $G = PGL_2^+(\Bbb R) = GL_2^+(\Bbb R) / \Bbb R^*I_2$ (the $+$ indicates we only keep matrices with a positive determinant).
Its Lie algebra is $A = (M_2(\Bbb R), +) / \langle I_2 \rangle$ coming with the natural map $\exp : A \to G$

Given a point $z \in \Bbb C$ and an element $a \in A$, we get an orbit $\{\exp(ta).z \mid t \in \Bbb R\}$. Those orbits can be a line (or a segment), a circle (or an arc), or a kind of spiral.

Lines and circles can be symmetric with respect to complex conjugation, but spirals can't, so we can only look for lines and circles.

First, stand at a point $z$ in the upper half plane, and rotate around yourself. What you should be seeing should be given by a homography with a simple fixpoint at $z$ (and at its conjugate). The map $f \mapsto f'(z)$ is an isomorphism between the group of complex homographies fixing $z,\bar z$ and $\Bbb C^*$ ; the subgroup of real homographies then corresponds to the unit circle, and they are going to be our group of rotations around $z,\bar z$. So we decide they will be isometries of our geometry.

Looking at the orbits of the points around you through that circle group, you should see the upper half plane partitioned into lots of circles.
The circles can be characterized by the property that the image of $z$ by the inversion through them gives $\bar z$. (looking at the equations of those circles, they form a projective line, and all those circles are concurrent in a pair of conjugate points of the complexified real plane, which can be interpreted to be the conjugate pair $\{z,\bar z\}$)

Also, any circle in the upper half plane is such a circle (just ... look at the complex intersection points of the circle with the real line to get its "hyperbolic center")

What should an infinite line look like ?

Among complex homographies with a fixed point at a conjugate pair $\{z, \bar z\}$ there is another natural subgroup to consider, those with a derivative in $\Bbb R_{>0}$ (caution : those homographies are NOT real ! however, they satisy $f \circ \bar f = id$ ; so their orbits are still invariant by conjugation, so it is not that bad)

Those orbits will naturally make right angles with all our circles, so this gives another definition of a line as an object that makes right angles with all the circles centered around a point.

In particular they will make right angles with $\Bbb P^1(\Bbb R)$, so they are the vertical lines and circles with a center on the real axis.

Another way to define a line is as the bissecting line between two points $z_1,z_2$. Since we can judge when two points are at equal distance with another point, we can talk about such a bissector : $z$ is on the line bissecting $z_1$ and $z_2$ if there is a circle of "center" $z$ going through both $z_1$ and $z_2$. With this you obtain the circle (or vertical line) normal to the real line which inverts $z_1$ to $z_2$.

Finally, to get the distance between $2$ points, we look at the line joining them. It has two intersection points $r_1,r_2$ with the horizon (the real axis), so let us look at real homographies fixing $r_1,r_2 \in \Bbb P^1(\Bbb R)$. Again, looking at their (real) derivative at $r_1$ (the one at $r_2$ will be its multiplicative inverse) gives an isomorphism between this group and $(\Bbb R_{>0}, \times)$. Among this group, there is a particular homography sending $z_1$ to $z_2$. Taking the absolute value of the natural logarithm of that derivative is the only possible choice to define distance travelled by that homography, and so the distance between $z_1$ and $z_2$.

The simplest numerical example is when the line joins $0$ and $i\infty$. Then the group is simply $\Bbb R_{>0}$ acting by homothety. Given $iy_1$ and $iy_2$ on the line, their distance is therefore $|\log(y_2/y_1)| = |\log y_2 - \log y-1| = \int_\gamma \frac 1 y |dl|$.

Since rotations are supposed to be isometries, the length of a segment near $z$ doesn't depend on its direction : the length of an infinitesimal segment of euclidiean length $dl$ at $x+iy$ has to be $\frac 1y dl$, from which we recover the $ds^2 = (dx^2 + dy^2)/y^2$.