Poincaré geodesics are Euclidean circles orthogonal to the unit circle

Conformal/Poincare/Geodesic.lean builds the unit-speed geodesic lines of the Poincaré disc, TauCeti.PoincareDisc.geodesicLine a u, as the radial geodesics t ↦ u * Real.tanh t carried off the origin by a Moebius isometry, and Conformal/Poincare/Betweenness.lean shows that these are all the geodesic lines. What neither says is what a geodesic looks like in the Euclidean plane away from the origin: through the origin it is a diameter, and off the origin it is the classical arc of a circle meeting the unit circle at right angles. This file proves that, and its converse: the diameters and those arcs are exactly the geodesics.

The route is to read "lies on the geodesic through a in direction u" as an equation. Applying the Moebius isometry that sends a to the origin turns it into "lies on a diameter", which is the reality of conj u * z; pulling that back through z ↦ (z - a) / (1 - conj a * z) and clearing the denominator gives the equation

Im (conj u * (z - a) * (1 - a * conj z)) = 0,

and TauCeti.im_conj_mul_sub_mul_one_sub_mul_conj rearranges it into the shape of a Euclidean circle equation, Im (B * z) = A * (‖z‖ ^ 2 + 1) with A = Im (conj u * a) and B = conj u - u * conj a ^ 2. The coefficient of ‖z‖ ^ 2 and the constant term are equal, and that is exactly orthogonality to the unit circle: completing the square in that equation gives the circle of centre c = TauCeti.orthogonalCircleCenter u a and radius R = TauCeti.orthogonalCircleRadius u a, which satisfy ‖c‖ ^ 2 = R ^ 2 + 1, the Pythagorean relation saying that the tangent length from c to the unit circle is R. That relation, and the positivity of the radius, come from the identity

‖B‖ ^ 2 - 4 * A ^ 2 = ‖u‖ ^ 2 * (1 - ‖a‖ ^ 2) ^ 2

(TauCeti.normSq_sub_mul_conj_sq_sub_four_mul_sq_im); reading it at ‖u‖ = 1, together with ‖a‖ < 1, is where those two hypotheses enter. The degenerate case A = 0 is exactly the case in which the geodesic passes through the origin, and then the equation collapses to the Euclidean diameter Im (conj u * z) = 0.

The converse

Reading the same computation backwards realises a prescribed circle. Every circle orthogonal to the unit circle meets the ray through its centre at a point k * w of the open disc — the near point, at distance k = ‖c‖ - R from the origin, which the orthogonality relation identifies with 1 / (‖c‖ + R) < 1 — and the hyperbolic line through that point perpendicular to the ray has centre ((1 + k ^ 2) / (2 * k)) * w and radius (1 - k ^ 2) / (2 * k) (TauCeti.orthogonalCircleCenter_I_mul_ofReal_mul, TauCeti.orthogonalCircleRadius_I_mul_ofReal_mul). The orthogonality relation is exactly what makes those two numbers ‖c‖ and R again, so the prescribed circle is the circle of that line (TauCeti.exists_orthogonalCircleCenter_eq_orthogonalCircleRadius_eq). Together with the diameters, which the radial geodesics already trace, this closes the description into an iff.

Main results

• TauCeti.PoincareDisc.mem_range_radialGeodesic_iff — a point of the Poincaré disc lies on the radial geodesic in direction u exactly when conj u * z is real.
• TauCeti.PoincareDisc.mem_range_geodesicLine_iff — the equation of the geodesic line through a in direction u, and TauCeti.PoincareDisc.toPoincare_zero_mem_range_geodesicLine_iff — that equation at the origin, which is what makes Im (conj u * a) the geometric discriminator of the case split below.
• TauCeti.orthogonalCircleCenter and TauCeti.orthogonalCircleRadius — the centre and radius parameters read off by completing the square, which for ‖u‖ = 1, ‖a‖ < 1 and Im (conj u * a) ≠ 0 are the centre and radius of the Euclidean circle traced by a hyperbolic line missing the origin, together with TauCeti.orthogonalCircleRadius_pos and the orthogonality relation TauCeti.norm_orthogonalCircleCenter_sq.
• TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere — a geodesic line missing the origin traces ball 0 1 ∩ sphere c R for that Euclidean circle, which is orthogonal to the unit circle, ‖c‖ ^ 2 = R ^ 2 + 1, and the complementary case TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_setOf_im — a geodesic line through the origin traces the Euclidean diameter in its direction, of which TauCeti.PoincareDisc.range_coe_toUnitDisc_radialGeodesic_eq is the reading at the base point 0.
• TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_or — the two cases together: every geodesic line of the Poincaré disc traces the intersection of the disc with a Euclidean line through the origin or with a Euclidean circle orthogonal to the unit circle.
• TauCeti.PoincareDisc.range_coe_toUnitDisc_eq_ball_inter_or_of_isometry — the same for an arbitrary isometric embedding of the real line, which is the parametrisation-free form of that description.
• TauCeti.orthogonalCircleCenter_I_mul_ofReal_mul and TauCeti.orthogonalCircleRadius_I_mul_ofReal_mul — the two parameters at the perpendicular pair u = I * w, a = k * w for a unit vector w, which for k in Ioo 0 1 are the centre and radius of the hyperbolic line through k * w perpendicular to the radius through w, and TauCeti.exists_orthogonalCircleCenter_eq_orthogonalCircleRadius_eq — every circle orthogonal to the unit circle is the circle of a hyperbolic line.
• TauCeti.PoincareDisc.exists_range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere — the converse direction in the circular case: every arc ball 0 1 ∩ sphere c R with 0 < R and ‖c‖ ^ 2 = R ^ 2 + 1 is traced by a geodesic. The converse for the diameters needs nothing new, TauCeti.PoincareDisc.range_coe_toUnitDisc_radialGeodesic_eq being already an equality of sets.
• TauCeti.PoincareDisc.exists_range_coe_toUnitDisc_geodesicLine_eq_iff and TauCeti.PoincareDisc.exists_isometry_range_coe_toUnitDisc_eq_iff — the classification: the traces of the geodesics of the Poincaré disc are exactly the Euclidean diameters and the arcs of Euclidean circles orthogonal to the unit circle, in the parametrised and parametrisation-free readings.

Generality

In accordance with the generality bar of ConformalMapping/README.md, which fixes scalar ℂ for layers L0--L6, everything is stated for the complex unit disc. The plane-geometry lemmas of the first section ask nothing of a beyond ‖a‖ < 1 and nothing of u beyond ‖u‖ = 1 — and several of them ask less: the discriminant identity is homogeneous in u and needs no hypothesis at all, and the degenerate case needs only ‖a‖ ≠ 1. They are stated for bare complex numbers so that they can be reused off the PoincareDisc synonym.

Coordination with upstream Mathlib

This is L2 material, "the hyperbolic / Poincaré metric on 𝔻" of TauCetiRoadmap/ConformalMapping/README.md, and as such falls under that roadmap's coordination clause for the in-progress human-curated Riemann-mapping effort mathlib4#33505: it should be refactored onto upstream API if that work lands a Poincaré-disc geometry. The pinned Mathlib has the hyperbolic metric on the upper half-plane (Analysis/Complex/UpperHalfPlane) but no Poincaré metric on the disc and no description of its geodesics; nothing is vendored here.

References

• L. V. Ahlfors, Conformal Invariants, Ch. 1 (the hyperbolic metric of the disc).
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. III (Moebius transformations and circles).

The equation of a hyperbolic line in the plane

theorem TauCeti.im_conj_mul_sub_mul_one_sub_mul_conj (u a z : ℂ) : ((starRingEnd ℂ) u * (z - a) * (1 - a * (starRingEnd ℂ) z)).im = (((starRingEnd ℂ) u - u * (starRingEnd ℂ) a ^ 2) * z).im - ((starRingEnd ℂ) u * a).im * (Complex.normSq z + 1)

The geodesic equation is a Euclidean circle equation. The quantity Im (conj u * (z - a) * (1 - a * conj z)), which cuts out the hyperbolic line through a in direction u, is Im (B * z) - A * (‖z‖ ^ 2 + 1) for A = Im (conj u * a) and B = conj u - u * conj a ^ 2.

The point of the rearrangement is that the coefficient of ‖z‖ ^ 2 and the constant term are the same number A. For A ≠ 0 an equation A * ‖z‖ ^ 2 - Im (B * z) + C = 0 describes a circle, and that circle is orthogonal to the unit circle exactly when A = C, so for A ≠ 0 the geodesic equation is the equation of such a circle (TauCeti.setOf_im_eq_ball_inter_sphere). For A = 0 it is not a circle equation at all: it is linear, and describes a Euclidean line through the origin (TauCeti.setOf_im_eq_ball_inter_setOf_im). No hypothesis is needed for the rearrangement itself: this is an identity of real numbers.

theorem TauCeti.normSq_sub_mul_conj_sq_sub_four_mul_sq_im (u a : ℂ) : Complex.normSq ((starRingEnd ℂ) u - u * (starRingEnd ℂ) a ^ 2) - 4 * ((starRingEnd ℂ) u * a).im ^ 2 = Complex.normSq u * (1 - Complex.normSq a) ^ 2

The discriminant identity behind the radius. The linear coefficient B and the quadratic coefficient A of the geodesic equation (TauCeti.im_conj_mul_sub_mul_one_sub_mul_conj) satisfy ‖B‖ ^ 2 - 4 * A ^ 2 = ‖u‖ ^ 2 * (1 - ‖a‖ ^ 2) ^ 2. Both sides are homogeneous of degree two in u, so no normalisation of u is needed; at ‖u‖ = 1 the right-hand side is (1 - ‖a‖ ^ 2) ^ 2.

Completing the square turns the geodesic equation into ‖z - c‖ ^ 2 = ‖c‖ ^ 2 - 1 with ‖c‖ ^ 2 = ‖B‖ ^ 2 / (4 * A ^ 2), so this identity is what makes the radius (1 - ‖a‖ ^ 2) / (2 * |A|) positive when ‖u‖ = 1 and ‖a‖ < 1: the circle is a genuine circle and not a point or the empty set.

The centre and radius of the orthogonal circle

noncomputable def TauCeti.orthogonalCircleCenter (u a : ℂ) : ℂ

The centre parameter c = I * conj B / (2 * A), with A = Im (conj u * a) and B = conj u - u * conj a ^ 2, read off by completing the square in the geodesic equation Im (B * z) = A * (‖z‖ ^ 2 + 1) of TauCeti.im_conj_mul_sub_mul_one_sub_mul_conj.

Nothing is asked of u or a here, so on its own this is an algebraic parameter: at A = 0 the division is by zero and the value is 0, and A ≠ 0 alone does not make it the centre of a genuine circle, since the companion radius TauCeti.orthogonalCircleRadius u a vanishes at ‖a‖ = 1 and is negative beyond. It is the centre of the Euclidean circle traced by the hyperbolic line through a in direction u under the hypotheses ‖u‖ = 1, ‖a‖ < 1 and A ≠ 0 of TauCeti.setOf_im_eq_ball_inter_sphere, the last of which says that that line misses the origin.

Equations

• TauCeti.orthogonalCircleCenter u a = Complex.I * (starRingEnd ℂ) ((starRingEnd ℂ) u - u * (starRingEnd ℂ) a ^ 2) / ↑(2 * ((starRingEnd ℂ) u * a).im)

noncomputable def TauCeti.orthogonalCircleRadius (u a : ℂ) : ℝ

The quantity R = (1 - ‖a‖ ^ 2) / (2 * |A|), with A = Im (conj u * a), read off by completing the square as in TauCeti.orthogonalCircleCenter.

Nothing is asked of u or a here, so this is a signed algebraic parameter: at A = 0 the division is by zero and the value is 0, and for A ≠ 0 it is negative for ‖a‖ > 1 (at u = 1 and a = 2 * I it is -3/4). Under ‖a‖ < 1 and A ≠ 0 it is positive (TauCeti.orthogonalCircleRadius_pos), but it is the radius of the Euclidean circle traced by the hyperbolic line through a in direction u only once ‖u‖ = 1 as well (TauCeti.setOf_im_eq_ball_inter_sphere): unlike the centre, R is not invariant under rescaling u, because A scales with u while the numerator does not.

Equations

• TauCeti.orthogonalCircleRadius u a = (1 - ‖a‖ ^ 2) / (2 * |((starRingEnd ℂ) u * a).im|)

theorem TauCeti.orthogonalCircleCenter_def (u a : ℂ) : orthogonalCircleCenter u a = Complex.I * (starRingEnd ℂ) ((starRingEnd ℂ) u - u * (starRingEnd ℂ) a ^ 2) / ↑(2 * ((starRingEnd ℂ) u * a).im)

The defining formula for TauCeti.orthogonalCircleCenter, so that the advertised expression is available without unfolding the definition.

theorem TauCeti.orthogonalCircleRadius_def (u a : ℂ) : orthogonalCircleRadius u a = (1 - ‖a‖ ^ 2) / (2 * |((starRingEnd ℂ) u * a).im|)

The defining formula for TauCeti.orthogonalCircleRadius, so that the advertised expression is available without unfolding the definition.

theorem TauCeti.orthogonalCircleRadius_pos {u a : ℂ} (ha : ‖a‖ < 1) (hA : ((starRingEnd ℂ) u * a).im ≠ 0) : 0 < orthogonalCircleRadius u a

The radius parameter is positive on the disc, away from the origin. ‖a‖ < 1 makes the numerator positive and Im (conj u * a) ≠ 0 makes the denominator positive; no unit direction is needed for that. At ‖u‖ = 1 the second hypothesis says that the hyperbolic line through a in direction u misses the origin, and positivity is then what makes the Euclidean set that line traces a genuine circle rather than a point or the empty set (TauCeti.setOf_im_eq_ball_inter_sphere).

theorem TauCeti.norm_orthogonalCircleCenter_sq {u a : ℂ} (hu : ‖u‖ = 1) (hA : ((starRingEnd ℂ) u * a).im ≠ 0) : ‖orthogonalCircleCenter u a‖ ^ 2 = orthogonalCircleRadius u a ^ 2 + 1

The circle of a hyperbolic line is orthogonal to the unit circle. The centre c = TauCeti.orthogonalCircleCenter u a and the parameter R = TauCeti.orthogonalCircleRadius u a satisfy ‖c‖ ^ 2 = R ^ 2 + 1. This is TauCeti.normSq_sub_mul_conj_sq_sub_four_mul_sq_im at ‖u‖ = 1, and as an identity it needs no bound on ‖a‖.

Once ‖a‖ < 1 makes R positive (TauCeti.orthogonalCircleRadius_pos), so that the circle of centre c and radius R is a genuine circle, the relation is Pythagoras for the right triangle whose legs are the radius 1 of the unit circle and the radius R, and it then says precisely that the two circles meet at right angles.

theorem TauCeti.setOf_im_eq_ball_inter_sphere {u a : ℂ} (hu : ‖u‖ = 1) (ha : ‖a‖ < 1) (hA : ((starRingEnd ℂ) u * a).im ≠ 0) : {z : ℂ | ‖z‖ < 1 ∧ ((starRingEnd ℂ) u * (z - a) * (1 - a * (starRingEnd ℂ) z)).im = 0} = Metric.ball 0 1 ∩ Metric.sphere (orthogonalCircleCenter u a) (orthogonalCircleRadius u a)

A hyperbolic line off the origin is an arc of a Euclidean circle orthogonal to the unit circle. If ‖u‖ = 1, ‖a‖ < 1 and the geodesic through a in direction u misses the origin — which is exactly Im (conj u * a) ≠ 0 — then its plane equation cuts out ball 0 1 ∩ sphere c R for the centre c = TauCeti.orthogonalCircleCenter u a and the radius R = TauCeti.orthogonalCircleRadius u a.

That this is a genuine circle, and that it meets the unit circle at right angles, are TauCeti.orthogonalCircleRadius_pos and TauCeti.norm_orthogonalCircleCenter_sq.

theorem TauCeti.setOf_im_eq_ball_inter_setOf_im {u a : ℂ} (ha : ‖a‖ ≠ 1) (hA : ((starRingEnd ℂ) u * a).im = 0) : {z : ℂ | ‖z‖ < 1 ∧ ((starRingEnd ℂ) u * (z - a) * (1 - a * (starRingEnd ℂ) z)).im = 0} = Metric.ball 0 1 ∩ {z : ℂ | ((starRingEnd ℂ) u * z).im = 0}

A hyperbolic line through the origin is a Euclidean diameter. As an equality of sets: if Im (conj u * a) = 0 — the case excluded in TauCeti.setOf_im_eq_ball_inter_sphere — then the equation cutting out the line through a in direction u collapses to the reality of conj u * z. The two equations differ by the scalar factor 1 - ‖a‖ ^ 2, so of a only ‖a‖ ≠ 1 is asked, and of u nothing at all.

The geometric reading needs u ≠ 0, which holds for the unit direction u of a geodesic: then the hypothesis says that a is a real multiple of u, so that the geodesic through a in direction u is the one through the origin, and the right-hand side is the Euclidean diameter in direction u.

Realising a prescribed orthogonal circle

The lemmas above read off the circle of a given hyperbolic line. This section runs the other way: it exhibits, for a prescribed circle orthogonal to the unit circle, a base point and a direction whose circle it is. The base point is the point of the circle nearest the origin and the direction is perpendicular to the radius through it, so the pair to compute with is a = k * w, u = I * w for a unit vector w and a real k; that is the normal form the lemmas below treat.

@[simp]

theorem TauCeti.orthogonalCircleCenter_I_mul_ofReal_mul {w : ℂ} (hw : ‖w‖ = 1) (k : ℝ) : orthogonalCircleCenter (Complex.I * w) (↑k * w) = ↑((1 + k ^ 2) / (2 * k)) * w

The centre parameter at the perpendicular pair. For a unit w and any real k, the centre parameter of u = I * w, a = k * w is ((1 + k ^ 2) / (2 * k)) * w, again on the radius through w.

As at TauCeti.orthogonalCircleCenter itself, nothing is asked of k, so on its own this is an algebraic computation: at k = 0 the two sides are the two divisions by zero, both 0. It is exactly for 0 < |k| < 1 that k * w lies in the open unit disc away from the origin, and for 0 < k < 1 the value is the centre of the Euclidean circle traced by the hyperbolic line through k * w in the direction I * w perpendicular to the radius through w. That reading, together with TauCeti.orthogonalCircleRadius_I_mul_ofReal_mul, is the computation that makes every circle orthogonal to the unit circle a hyperbolic line: as k ranges over Ioo 0 1 the centre sweeps out the whole ray beyond the unit circle.

@[simp]

theorem TauCeti.orthogonalCircleRadius_I_mul_ofReal_mul {w : ℂ} (hw : ‖w‖ = 1) (k : ℝ) : orthogonalCircleRadius (Complex.I * w) (↑k * w) = (1 - k ^ 2) / (2 * |k|)

The radius parameter at the perpendicular pair. The companion of TauCeti.orthogonalCircleCenter_I_mul_ofReal_mul: for a unit w and any real k, the radius parameter of u = I * w, a = k * w is (1 - k ^ 2) / (2 * |k|). Unlike the centre, which is a signed expression in Im (conj u * a), the radius divides by 2 * |Im (conj u * a)| = 2 * |k|, whence the absolute value; for 0 < k it reads (1 - k ^ 2) / (2 * k), and at k = 0 both sides are the division by zero, 0.

Positivity of the value is the further information 0 < |k| < 1, that is, that k * w lies in the open disc away from the origin; at k = 0 the value is 0 and for |k| > 1 it is negative, so neither describes a circle. It is under 0 < k < 1 that this is the radius of the Euclidean circle traced by the hyperbolic line through k * w in the direction I * w.

theorem TauCeti.exists_orthogonalCircleCenter_eq_orthogonalCircleRadius_eq {c : ℂ} {R : ℝ} (hR : 0 < R) (horth : ‖c‖ ^ 2 = R ^ 2 + 1) : ∃ (u : ℂ) (a : ℂ), ‖u‖ = 1 ∧ ‖a‖ < 1 ∧ ((starRingEnd ℂ) u * a).im ≠ 0 ∧ orthogonalCircleCenter u a = c ∧ orthogonalCircleRadius u a = R

Every circle orthogonal to the unit circle is the circle of a hyperbolic line. Given a Euclidean circle of centre c and positive radius R meeting the unit circle at right angles — the relation ‖c‖ ^ 2 = R ^ 2 + 1 of TauCeti.norm_orthogonalCircleCenter_sq — there are a base point a in the open unit disc and a unit direction u missing the origin whose hyperbolic line has exactly that centre and radius.

The witnesses are a = k * w and u = I * w, where w = c / ‖c‖ is the direction of the centre and k = ‖c‖ - R is the distance from the origin to the near point of the circle: the orthogonality relation makes k the reciprocal of ‖c‖ + R, hence a point of Ioo 0 1, and the two computations TauCeti.orthogonalCircleCenter_I_mul_ofReal_mul and TauCeti.orthogonalCircleRadius_I_mul_ofReal_mul then return c and R on the nose.

The geodesics of the Poincaré disc

theorem TauCeti.PoincareDisc.mem_range_radialGeodesic_iff (u : Circle) (z : PoincareDisc) : z ∈ Set.range (radialGeodesic u) ↔ ((starRingEnd ℂ) ↑u * ↑(toUnitDisc z)).im = 0

The equation of a geodesic through the origin. A point z of the Poincaré disc lies on the radial geodesic in direction u exactly when conj u * z is real, that is, when z lies on the Euclidean diameter in direction u.

theorem TauCeti.PoincareDisc.mem_range_geodesicLine_iff (a : PoincareDisc) (u : Circle) (z : PoincareDisc) : z ∈ Set.range (a.geodesicLine u) ↔ ((starRingEnd ℂ) ↑u * (↑(toUnitDisc z) - ↑(toUnitDisc a)) * (1 - ↑(toUnitDisc a) * (starRingEnd ℂ) ↑(toUnitDisc z))).im = 0

The equation of a geodesic line. A point z of the Poincaré disc lies on the geodesic line through a in direction u exactly when Im (conj u * (z - a) * (1 - a * conj z)) = 0.

The Moebius isometry sending a to the origin straightens the geodesic into the radial one (TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv_geodesicLine), where TauCeti.PoincareDisc.mem_range_radialGeodesic_iff applies; clearing the Moebius denominator, which is nonzero on the disc, gives the polynomial form.

theorem TauCeti.PoincareDisc.toPoincare_zero_mem_range_geodesicLine_iff (a : PoincareDisc) (u : Circle) : Complex.UnitDisc.toPoincare 0 ∈ Set.range (a.geodesicLine u) ↔ ((starRingEnd ℂ) ↑u * ↑(toUnitDisc a)).im = 0

The geodesic line through a in direction u passes through the origin exactly when Im (conj u * a) = 0. This is TauCeti.PoincareDisc.mem_range_geodesicLine_iff read at the origin, and it is what makes Im (conj u * a) the geometric discriminator of the case split below: the vanishing of that number is not an algebraic accident but says that the geodesic contains the origin, which is exactly when it traces a Euclidean diameter rather than an arc of a circle.

theorem TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq (a : PoincareDisc) (u : Circle) : (Set.range fun (t : ℝ) => ↑(toUnitDisc (a.geodesicLine u t))) = {z : ℂ | ‖z‖ < 1 ∧ ((starRingEnd ℂ) ↑u * (z - ↑(toUnitDisc a)) * (1 - ↑(toUnitDisc a) * (starRingEnd ℂ) z)).im = 0}

The plane description of the geodesic line through a in direction u: it traces the set of points of the open unit disc satisfying the geodesic equation.

theorem TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere (a : PoincareDisc) (u : Circle) (hA : ((starRingEnd ℂ) ↑u * ↑(toUnitDisc a)).im ≠ 0) : (Set.range fun (t : ℝ) => ↑(toUnitDisc (a.geodesicLine u t))) = Metric.ball 0 1 ∩ Metric.sphere (orthogonalCircleCenter ↑u ↑(toUnitDisc a)) (orthogonalCircleRadius ↑u ↑(toUnitDisc a))

A geodesic line missing the origin traces an arc of a Euclidean circle orthogonal to the unit circle. If Im (conj u * a) ≠ 0 — which by TauCeti.PoincareDisc.toPoincare_zero_mem_range_geodesicLine_iff says that the line misses the origin — the geodesic line of the Poincaré disc through a in direction u sweeps out ball 0 1 ∩ sphere c R for the Euclidean circle of centre TauCeti.orthogonalCircleCenter and radius TauCeti.orthogonalCircleRadius, whose radius is positive (TauCeti.orthogonalCircleRadius_pos) and which satisfies ‖c‖ ^ 2 = R ^ 2 + 1 (TauCeti.norm_orthogonalCircleCenter_sq), the Pythagorean relation expressing that it meets the unit circle at right angles.

This is the classical picture of the Poincaré disc, and it is TauCeti.setOf_im_eq_ball_inter_sphere read through TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq.

theorem TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_setOf_im (a : PoincareDisc) (u : Circle) (hA : ((starRingEnd ℂ) ↑u * ↑(toUnitDisc a)).im = 0) : (Set.range fun (t : ℝ) => ↑(toUnitDisc (a.geodesicLine u t))) = Metric.ball 0 1 ∩ {z : ℂ | ((starRingEnd ℂ) ↑u * z).im = 0}

A geodesic line through the origin traces a Euclidean diameter. The complementary case of TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere: when Im (conj u * a) = 0 — which by TauCeti.PoincareDisc.toPoincare_zero_mem_range_geodesicLine_iff says that the line passes through the origin — the base point a is a real multiple of the direction u, so the geodesic line through a is the radial one and traces the Euclidean diameter in direction u.

theorem TauCeti.PoincareDisc.range_coe_toUnitDisc_radialGeodesic_eq (u : Circle) : (Set.range fun (t : ℝ) => ↑(toUnitDisc (radialGeodesic u t))) = Metric.ball 0 1 ∩ {z : ℂ | ((starRingEnd ℂ) ↑u * z).im = 0}

A geodesic through the origin traces a Euclidean diameter. The radial geodesic in direction u sweeps out exactly the intersection of the open unit disc with the Euclidean line through the origin in direction u.

This is TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_setOf_im at the base point 0, where the geodesic line is the radial one (TauCeti.PoincareDisc.geodesicLine_toPoincare_zero).

theorem TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_or (a : PoincareDisc) (u : Circle) : (∃ (v : ℂ), ‖v‖ = 1 ∧ (Set.range fun (t : ℝ) => ↑(toUnitDisc (a.geodesicLine u t))) = Metric.ball 0 1 ∩ {z : ℂ | (v * z).im = 0}) ∨ ∃ (c : ℂ) (R : ℝ), 0 < R ∧ ‖c‖ ^ 2 = R ^ 2 + 1 ∧ (Set.range fun (t : ℝ) => ↑(toUnitDisc (a.geodesicLine u t))) = Metric.ball 0 1 ∩ Metric.sphere c R

The geodesics of the Poincaré disc, in Euclidean terms. Every geodesic line of the Poincaré disc traces either the intersection of the open unit disc with a Euclidean line through the origin, or its intersection with a Euclidean circle orthogonal to the unit circle (‖c‖ ^ 2 = R ^ 2 + 1). Which of the two happens is decided by whether the line passes through the origin, that being the content of TauCeti.PoincareDisc.toPoincare_zero_mem_range_geodesicLine_iff for the discriminator Im (conj u * a) of the case split.

This is the two cases TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_setOf_im and TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere put together; the individual statements say which case occurs and, in the circular case, what the centre and radius are. The implication runs from the geodesic to the Euclidean set it traces; the converse is TauCeti.PoincareDisc.exists_range_coe_toUnitDisc_geodesicLine_eq_iff, which packages the two directions into a description of the geodesics.

theorem TauCeti.PoincareDisc.range_coe_toUnitDisc_eq_ball_inter_or_of_isometry {γ : ℝ → PoincareDisc} (hγ : Isometry γ) : (∃ (v : ℂ), ‖v‖ = 1 ∧ (Set.range fun (t : ℝ) => ↑(toUnitDisc (γ t))) = Metric.ball 0 1 ∩ {z : ℂ | (v * z).im = 0}) ∨ ∃ (c : ℂ) (R : ℝ), 0 < R ∧ ‖c‖ ^ 2 = R ^ 2 + 1 ∧ (Set.range fun (t : ℝ) => ↑(toUnitDisc (γ t))) = Metric.ball 0 1 ∩ Metric.sphere c R

Every geodesic of the Poincaré disc is a Euclidean diameter or an arc of a Euclidean circle orthogonal to the unit circle. Any isometric embedding γ : ℝ → PoincareDisc — which by TauCeti.PoincareDisc.existsUnique_eq_geodesicLine is a TauCeti.PoincareDisc.geodesicLine, with no hypothesis on where it starts — traces either the intersection of the open unit disc with a Euclidean line through the origin, or its intersection with a Euclidean circle satisfying the orthogonality relation ‖c‖ ^ 2 = R ^ 2 + 1.

This is the classical picture of the Poincaré disc, and it is TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_or freed of the parametrisation: nothing here refers to geodesicLine, only to being a geodesic line. It runs in one direction only, from a geodesic to the Euclidean set it traces; that every such diameter or orthogonal circular arc is in turn traced by a geodesic is the converse half of TauCeti.PoincareDisc.exists_isometry_range_coe_toUnitDisc_eq_iff.

The converse: every such Euclidean set is a geodesic

theorem TauCeti.PoincareDisc.exists_range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere {c : ℂ} {R : ℝ} (hR : 0 < R) (horth : ‖c‖ ^ 2 = R ^ 2 + 1) : ∃ (a : PoincareDisc) (u : Circle), (Set.range fun (t : ℝ) => ↑(toUnitDisc (a.geodesicLine u t))) = Metric.ball 0 1 ∩ Metric.sphere c R

Every arc of a Euclidean circle orthogonal to the unit circle is traced by a geodesic. This is the converse of TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere: a Euclidean circle of positive radius R and centre c subject to the orthogonality relation ‖c‖ ^ 2 = R ^ 2 + 1 meets the open unit disc in the trace of a geodesic line of the Poincaré disc.

The base point and direction are supplied by TauCeti.exists_orthogonalCircleCenter_eq_orthogonalCircleRadius_eq: the base point is the point of the circle nearest the origin and the direction is perpendicular to the radius through it.

theorem TauCeti.PoincareDisc.exists_range_coe_toUnitDisc_geodesicLine_eq_iff {S : Set ℂ} : (∃ (a : PoincareDisc) (u : Circle), (Set.range fun (t : ℝ) => ↑(toUnitDisc (a.geodesicLine u t))) = S) ↔ (∃ (v : ℂ), ‖v‖ = 1 ∧ S = Metric.ball 0 1 ∩ {z : ℂ | (v * z).im = 0}) ∨ ∃ (c : ℂ) (R : ℝ), 0 < R ∧ ‖c‖ ^ 2 = R ^ 2 + 1 ∧ S = Metric.ball 0 1 ∩ Metric.sphere c R

The geodesics of the Poincaré disc are exactly the Euclidean diameters and the arcs of Euclidean circles orthogonal to the unit circle. A subset of the plane is the trace of a geodesic line of the Poincaré disc if and only if it is the intersection of the open unit disc with a Euclidean line through the origin or with a Euclidean circle of positive radius satisfying ‖c‖ ^ 2 = R ^ 2 + 1.

The forward implication is TauCeti.PoincareDisc.range_coe_toUnitDisc_geodesicLine_eq_ball_inter_or, which also says which of the two cases occurs and, in the circular case, computes the centre and radius. Backwards, the circular case is TauCeti.PoincareDisc.exists_range_coe_toUnitDisc_geodesicLine_eq_ball_inter_sphere, while the diameter case is TauCeti.PoincareDisc.range_coe_toUnitDisc_radialGeodesic_eq, which is already an equality of sets: all that the proof adds there is the direction realising a prescribed line, conj v rather than v, the conjugation coming from the conj u * z in which the equation of the radial geodesic is written.

theorem TauCeti.PoincareDisc.exists_isometry_range_coe_toUnitDisc_eq_iff {S : Set ℂ} : (∃ (γ : ℝ → PoincareDisc), Isometry γ ∧ (Set.range fun (t : ℝ) => ↑(toUnitDisc (γ t))) = S) ↔ (∃ (v : ℂ), ‖v‖ = 1 ∧ S = Metric.ball 0 1 ∩ {z : ℂ | (v * z).im = 0}) ∨ ∃ (c : ℂ) (R : ℝ), 0 < R ∧ ‖c‖ ^ 2 = R ^ 2 + 1 ∧ S = Metric.ball 0 1 ∩ Metric.sphere c R

The geodesics of the Poincaré disc, parametrisation-free. A subset of the plane is traced by some isometric embedding of the real line into the Poincaré disc — a geodesic, with no reference to TauCeti.PoincareDisc.geodesicLine — exactly when it is the intersection of the open unit disc with a Euclidean line through the origin or with a Euclidean circle orthogonal to the unit circle.

This is TauCeti.PoincareDisc.exists_range_coe_toUnitDisc_geodesicLine_eq_iff freed of the parametrisation, the two readings agreeing because every isometric embedding of the line is a geodesicLine (TauCeti.PoincareDisc.existsUnique_eq_geodesicLine) and every geodesicLine is an isometric embedding (TauCeti.PoincareDisc.isometry_geodesicLine).