The thick part of a group action on a metric space

For a group G acting on a metric space X and a real number ε, the ε-thick part TauCeti.thickPart G ε is the set of points moved a distance at least ε by every nonidentity element of G. Its complement, the thin part, consists of the points moved less than ε by some nonidentity element. For a discrete group of isometries of a hyperbolic manifold this is the thick-thin decomposition, whose thick part has compact image in the quotient when the quotient has finite volume.

Main declarations

• TauCeti.thickPart G ε: the points moved at least ε by every nonidentity element.
• TauCeti.isClosed_thickPart: the thick part of an action by continuous maps is closed.
• TauCeti.smul_mem_thickPart_iff: the thick part of an isometric action is invariant.

References

• Riccardo Benedetti and Carlo Petronio, Lectures on Hyperbolic Geometry, Universitext, Springer, 1992, Chapter D (the thick-thin decomposition).

def TauCeti.thickPart (G : Type u_1) {X : Type u_2} [Group G] [PseudoMetricSpace X] [MulAction G X] (ε : ℝ) : Set X

The ε-thick part of an action on a metric space: the points moved a distance at least ε by every nonidentity element. For 0 < ε it excludes every point with nontrivial stabilizer.

@[simp]

theorem TauCeti.mem_thickPart {G : Type u_1} {X : Type u_2} [Group G] [PseudoMetricSpace X] [MulAction G X] {ε : ℝ} {x : X} : x ∈ thickPart G ε ↔ ∀ (g : G), g ≠ 1 → ε ≤ dist (g • x) x

Membership in the thick part, unfolded.

theorem TauCeti.isClosed_thickPart (G : Type u_1) {X : Type u_2} [Group G] [PseudoMetricSpace X] [MulAction G X] [ContinuousConstSMul G X] (ε : ℝ) : IsClosed (thickPart G ε)

The thick part of an action by continuous maps is closed.

theorem TauCeti.smul_mem_thickPart_iff {G : Type u_1} {X : Type u_2} [Group G] [PseudoMetricSpace X] [MulAction G X] [IsIsometricSMul G X] {ε : ℝ} (g : G) {x : X} : g • x ∈ thickPart G ε ↔ x ∈ thickPart G ε

The thick part of an isometric action is invariant.