The special orthogonal group of the hyperbolic plane

The hyperbolic plane hyperbolicPlane R, the form x₀² - x₁² on Fin 2 → R, factors as (x₀ + x₁) (x₀ - x₁), so ![1, 1] and ![1, -1] span two distinguished isotropic rank-one submodules (over a field, these are its only two isotropic lines). For a unit t, the linear automorphism scaling ![1, 1] by t and ![1, -1] by t⁻¹ is a proper isometry: it is the diagonal torus diag(t, t⁻¹) of the xy-model written in the diagonal coordinates, and we construct it as the torus TauCeti.QuadraticMap.hyperbolicPairTorus of the hyperbolic pair ![1, 1], ⅟4 • ![1, -1].

These are all the proper isometries, so the torus is an isomorphism Rˣ ≃* SO(H) over any commutative ring in which two is invertible: an isometry sends ![1, 1] and ![1, -1] to isotropic vectors with polar pairing 4, and determinant 1 then forces it to preserve both of these distinguished submodules.

Main definitions

• TauCeti.hyperbolicTorus: the homomorphism Rˣ →* SO(H), t ↦ diag(t, t⁻¹) in the isotropic basis ![1, 1], ![1, -1].
• TauCeti.hyperbolicTorusEquiv: the isomorphism Rˣ ≃* SO(H) it induces.

Main results

• TauCeti.hyperbolicTorus_apply_one_one, TauCeti.hyperbolicTorus_apply_one_neg_one: the torus acts on the isotropic vectors by t and t⁻¹.
• TauCeti.hyperbolicTorus_injective, TauCeti.hyperbolicTorus_surjective: the torus is injective, and every proper isometry of the hyperbolic plane lies on it.

noncomputable def TauCeti.hyperbolicTorus (R : Type u_1) [CommRing R] [Invertible 2] : Rˣ →* ↥(QuadraticMap.specialOrthogonalGroup (hyperbolicPlane R))

The diagonal torus of the hyperbolic plane: the proper isometry diag(t, t⁻¹) in the isotropic basis ![1, 1], ![1, -1], which scales ![1, 1] by t and ![1, -1] by t⁻¹ (hyperbolicTorus_apply_one_one, hyperbolicTorus_apply_one_neg_one). It is the torus hyperbolicPairTorus of the hyperbolic pair ![1, 1], ⅟4 • ![1, -1].

theorem TauCeti.hyperbolicTorus_apply {R : Type u_1} [CommRing R] [Invertible 2] (t : Rˣ) (x : Fin 2 → R) : ↑((hyperbolicTorus R) t) x = ![⅟2 * ((↑t + ↑t⁻¹) * x 0 + (↑t - ↑t⁻¹) * x 1), ⅟2 * ((↑t - ↑t⁻¹) * x 0 + (↑t + ↑t⁻¹) * x 1)]

The diagonal torus in the coordinates of the hyperbolic plane.

@[simp]

theorem TauCeti.hyperbolicTorus_apply_one_one {R : Type u_1} [CommRing R] [Invertible 2] (t : Rˣ) : ↑((hyperbolicTorus R) t) ![1, 1] = ↑t • ![1, 1]

The diagonal torus scales the isotropic vector ![1, 1] by t.

@[simp]

theorem TauCeti.hyperbolicTorus_apply_one_neg_one {R : Type u_1} [CommRing R] [Invertible 2] (t : Rˣ) : ↑((hyperbolicTorus R) t) ![1, -1] = ↑t⁻¹ • ![1, -1]

The diagonal torus scales the isotropic vector ![1, -1] by t⁻¹.

theorem TauCeti.hyperbolicTorus_injective {R : Type u_1} [CommRing R] [Invertible 2] : Function.Injective ⇑(hyperbolicTorus R)

The diagonal torus of the hyperbolic plane is injective.

theorem TauCeti.hyperbolicTorus_surjective {R : Type u_1} [CommRing R] [Invertible 2] : Function.Surjective ⇑(hyperbolicTorus R)

Every proper isometry of the hyperbolic plane lies on the diagonal torus. An isometry sends the isotropic vectors ![1, 1] and ![1, -1] to isotropic vectors with polar pairing 4; together with determinant 1 this forces it to scale ![1, 1] by a unit t and ![1, -1] by t⁻¹.

noncomputable def TauCeti.hyperbolicTorusEquiv (R : Type u_1) [CommRing R] [Invertible 2] : Rˣ ≃* ↥(QuadraticMap.specialOrthogonalGroup (hyperbolicPlane R))

The diagonal torus identifies the units with the special orthogonal group of the hyperbolic plane.

@[simp]

theorem TauCeti.hyperbolicTorusEquiv_apply {R : Type u_1} [CommRing R] [Invertible 2] (t : Rˣ) : (hyperbolicTorusEquiv R) t = (hyperbolicTorus R) t

The isomorphism hyperbolicTorusEquiv R is the diagonal torus.

theorem TauCeti.coe_hyperbolicTorusEquiv_symm_apply {R : Type u_1} [CommRing R] [Invertible 2] (g : ↥(QuadraticMap.specialOrthogonalGroup (hyperbolicPlane R))) : ↑((hyperbolicTorusEquiv R).symm g) = ↑g ![1, 1] 0

The parameter of a proper isometry of the hyperbolic plane is the first coordinate of the image of the isotropic vector ![1, 1].