Documentation

TauCeti.LinearAlgebra.QuadraticForm.OrthogonalGroup.HyperbolicPair

The split torus of a hyperbolic pair #

Let Q be a quadratic form with un-halved polar form B = polar Q, and let u, v be a hyperbolic pair: Q u = Q v = 0 and B u v = 1. For a unit t, the linear map

x ↦ x + ((t - 1) * B x v) • u + ((t⁻¹ - 1) * B x u) • v

scales u by t, scales v by t⁻¹, and fixes every vector orthogonal to both. It is an isometry of Q, and t ↦ (this map) is an injective homomorphism from Rˣ into the orthogonal group: the diagonal torus diag(t, t⁻¹) of the hyperbolic plane spanned by u and v, extended by the identity on its orthogonal complement, but written without choosing that complement. It is the product of the reflections in u + v and in u + t • v, so on a finite free module it has determinant one.

Over a normed field the vectors t • u are unbounded, so this torus is the standard witness that the orthogonal group of an isotropic nondegenerate form is not compact.

Main definitions #

Main results #

source
noncomputable def TauCeti.QuadraticMap.hyperbolicPairTorus {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {u v : M} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) :
Rˣ →* ↥(orthogonalGroup Q)

The split torus of a hyperbolic pair. For isotropic vectors u, v with polar Q u v = 1, the unit t acts by x ↦ x + ((t - 1) * polar Q x v) • u + ((t⁻¹ - 1) * polar Q x u) • v: it scales u by t, v by t⁻¹, and fixes every vector orthogonal to both. This is an injective homomorphism from Rˣ into the orthogonal group of Q.

Instances For
    source
    theorem TauCeti.QuadraticMap.hyperbolicPairTorus_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) (t : Rˣ) (x : M) :
    ↑((hyperbolicPairTorus Q hu hv huv) t) x = x + ((↑t - 1) * QuadraticMap.polar (⇑Q) x v) • u + ((↑t⁻¹ - 1) * QuadraticMap.polar (⇑Q) x u) • v

    The torus of a hyperbolic pair acts by x ↦ x + ((t - 1) * polar Q x v) • u + ((t⁻¹ - 1) * polar Q x u) • v.

    source
    @[simp]
    theorem TauCeti.QuadraticMap.hyperbolicPairTorus_apply_left {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) (t : Rˣ) :
    ↑((hyperbolicPairTorus Q hu hv huv) t) u = ↑t • u

    The torus of a hyperbolic pair scales the first vector by t.

    source
    @[simp]
    theorem TauCeti.QuadraticMap.hyperbolicPairTorus_apply_right {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) (t : Rˣ) :
    ↑((hyperbolicPairTorus Q hu hv huv) t) v = ↑t⁻¹ • v

    The torus of a hyperbolic pair scales the second vector by t⁻¹.

    source
    @[simp]
    theorem TauCeti.QuadraticMap.hyperbolicPairTorus_apply_of_polar_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) (t : Rˣ) {x : M} (hxu : QuadraticMap.polar (⇑Q) x u = 0) (hxv : QuadraticMap.polar (⇑Q) x v = 0) :
    ↑((hyperbolicPairTorus Q hu hv huv) t) x = x

    The torus of a hyperbolic pair fixes every vector orthogonal to both vectors of the pair.

    source
    theorem TauCeti.QuadraticMap.hyperbolicPairTorus_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) :
    Function.Injective ⇑(hyperbolicPairTorus Q hu hv huv)

    The torus of a hyperbolic pair is injective: t is recovered as polar Q (g u) v.

    source
    theorem TauCeti.QuadraticMap.hyperbolicPairTorus_eq_reflection_mul_reflection {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) (t : Rˣ) [Invertible (Q (u + v))] [Invertible (Q (u + ↑t • v))] :
    ↑((hyperbolicPairTorus Q hu hv huv) t) = reflection Q (u + v) * reflection Q (u + ↑t • v)

    The torus element t of a hyperbolic pair is the product of the reflections in u + v and in u + t • v, whose norms are 1 and t.

    source
    theorem TauCeti.QuadraticMap.hyperbolicPairTorus_mem_specialOrthogonalGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {u v : M} [Module.Free R M] [Module.Finite R M] (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) (t : Rˣ) :
    ↑((hyperbolicPairTorus Q hu hv huv) t) ∈ specialOrthogonalGroup Q

    On a finite free module, the torus of a hyperbolic pair lies in the special orthogonal group.