Documentation

TauCeti.LowDimTopology.Handlebody.Basic

The standard handlebodies #

A handlebody of genus g is the orientable compact 3-manifold obtained from the 3-ball by attaching g one-handles; equivalently, it is the product F × [-1, 1] of the interval with a compact planar surface F of Euler characteristic 1 - g (Hempel, Chapter 2). This file fixes a concrete model of the second kind inside ℂ × ℝ.

The planar surface TauCeti.planarSurface g is the closed disc of radius g + 1 in ℂ with g open discs of radius 1 / 2 removed, centred at the real points 2k + 1 - g for k < g. These holes are pairwise disjoint and lie in the open disc of radius g, so the surface is a closed disc with g holes, of Euler characteristic 1 - g. The standard handlebody TauCeti.handlebody g is its product with the interval [-1, 1]. Its manifold boundary is the closed orientable surface of genus g formed by the two copies of the planar surface and the annuli over the g + 1 boundary circles.

Handlebodies are the pieces of a Heegaard splitting of a closed orientable 3-manifold, and a subset of a space is a genus-g handlebody when it is homeomorphic to TauCeti.handlebody g.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.planarSurface (g : ℕ) :
Set ℂ

The closed disc of radius g + 1 in ℂ with g open discs of radius 1 / 2 removed, centred at the real points 2k + 1 - g for k < g. It is a compact planar surface with g + 1 boundary circles.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_planarSurface {g : ℕ} {z : ℂ} :
    z ∈ planarSurface g ↔ ‖z‖ ≤ ↑g + 1 ∧ ∀ (k : Fin g), 2⁻¹ ≤ ‖z - ↑(2 * ↑↑k + 1 - ↑g)‖
    source
    theorem TauCeti.isCompact_planarSurface (g : ℕ) :
    IsCompact (planarSurface g)

    The closed disc with g holes is compact.

    source
    @[simp]
    theorem TauCeti.planarSurface_zero :
    planarSurface 0 = Metric.closedBall 0 1

    The closed disc with no holes is the closed unit disc.

    source
    noncomputable def TauCeti.handlebody (g : ℕ) :
    Set (ℂ × ℝ)

    The standard handlebody of genus g: the product of the closed disc with g holes, TauCeti.planarSurface g, with the interval [-1, 1].

    Instances For
      source
      @[simp]
      theorem TauCeti.mem_handlebody {g : ℕ} {x : ℂ × ℝ} :
      x ∈ handlebody g ↔ x.1 ∈ planarSurface g ∧ x.2 ∈ Set.Icc (-1) 1
      source
      theorem TauCeti.isCompact_handlebody (g : ℕ) :
      IsCompact (handlebody g)

      The standard handlebodies are compact.

      source
      theorem TauCeti.isClosed_handlebody (g : ℕ) :
      IsClosed (handlebody g)

      The standard handlebodies are closed.

      source
      theorem TauCeti.handlebody_zero :
      handlebody 0 = Metric.closedBall 0 1

      The genus-zero handlebody is the closed unit ball of ℂ × ℝ, for the sup norm.

      source
      theorem TauCeti.nonempty_homeomorph_handlebody_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (hF : Module.finrank ℝ F = 3) :
      Nonempty (↑(Metric.closedBall 0 1) ≃ₜ ↑(handlebody 0))

      The genus-zero handlebody is a ball. The closed unit ball of any real normed space of dimension three is homeomorphic to the genus-zero handlebody.

      The genus-one handlebody #

      source
      theorem TauCeti.planarSurface_one :
      planarSurface 1 = {z : ℂ | 2⁻¹ ≤ ‖z‖ ∧ ‖z‖ ≤ 2}

      The closed disc with one hole is the closed annulus 1 / 2 ≤ ‖z‖ ≤ 2.

      source
      theorem TauCeti.nonempty_homeomorph_handlebody_one :
      Nonempty (↑(handlebody 1) ≃ₜ SolidTorus)

      The genus-one handlebody is a solid torus. The standard handlebody of genus one is homeomorphic to the solid torus D² × S¹.