Jørgensen's sequence

For elements A and B of a group, Jørgensen's sequence is the iteration B₀ = B, Bₙ₊₁ = Bₙ A Bₙ⁻¹ of conjugates of A. It stays in any subgroup containing A and B (TauCeti.jorgensenSeq_mem). In PSL(2, ℝ) it drives the discreteness arguments behind Shimizu's lemma, for a parabolic A, and Jørgensen's inequality, for a hyperbolic A: when the starting point is close enough to normalising ⟨A⟩ the sequence (or, for a hyperbolic A, suitable conjugates of it by powers of A) converges, and discreteness forces a term to reach the limit.

Main declarations

• TauCeti.jorgensenSeq: the sequence B₀ = B, Bₙ₊₁ = Bₙ A Bₙ⁻¹.
• TauCeti.jorgensenSeq_mem: it lies in every subgroup containing A and B.
• TauCeti.map_jorgensenSeq: group homomorphisms map it to the sequence of the images.

References

• Troels Jørgensen, On discrete groups of Möbius transformations, American Journal of Mathematics 98 (1976), 739–749.

def TauCeti.jorgensenSeq {G : Type u_1} [Group G] (A B : G) : ℕ → G

Jørgensen's sequence B₀ = B, Bₙ₊₁ = Bₙ A Bₙ⁻¹ of conjugates of A.

@[simp]

theorem TauCeti.jorgensenSeq_zero {G : Type u_1} [Group G] (A B : G) : jorgensenSeq A B 0 = B

Jørgensen's sequence starts at B.

theorem TauCeti.jorgensenSeq_succ {G : Type u_1} [Group G] (A B : G) (n : ℕ) : jorgensenSeq A B (n + 1) = jorgensenSeq A B n * A * (jorgensenSeq A B n)⁻¹

Each term of Jørgensen's sequence conjugates A by the previous term.

theorem TauCeti.jorgensenSeq_mem {G : Type u_1} [Group G] {H : Subgroup G} {A B : G} (hA : A ∈ H) (hB : B ∈ H) (n : ℕ) : jorgensenSeq A B n ∈ H

Jørgensen's sequence stays in every subgroup containing A and B.

@[simp]

theorem TauCeti.map_jorgensenSeq {G : Type u_1} [Group G] {H : Type u_2} {F : Type u_3} [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F) (A B : G) (n : ℕ) : f (jorgensenSeq A B n) = jorgensenSeq (f A) (f B) n

A group homomorphism maps Jørgensen's sequence of A and B to that of their images.