Heegaard splittings and Heegaard genus

A Heegaard splitting of genus g of a closed orientable 3-manifold M writes M as the union of two handlebodies of genus g meeting in their common boundary, a closed surface of genus g. The Heegaard genus of M is the least genus of a Heegaard splitting.

Here a splitting is recorded inside M, without gluing: TauCeti.HeegaardSplitting M consists of two subsets left and right of M covering it, each homeomorphic to the standard handlebody TauCeti.handlebody genus, whose intersection is the frontier of each. The definition makes sense for any topological space. When M is a 3-manifold without boundary, invariance of domain identifies the frontier of each piece with the image of the manifold boundary of the handlebody, so the two pieces meet exactly in their common boundary surface (TauCeti.HeegaardSplitting.coe_mem_right_iff). The standard handlebodies are orientable, so these are the splittings of orientable manifolds.

The Heegaard genus TauCeti.heegaardGenus M is defined only under [Nonempty (HeegaardSplitting M)], as the least genus of a splitting, so it never silently takes a junk value. The unit sphere of a four-dimensional real inner product space, split into two closed hemispheres along the equator, has a splitting of genus zero, so its Heegaard genus is zero.

Main definitions

• TauCeti.HeegaardSplitting M: a Heegaard splitting of a space M.
• TauCeti.HeegaardSplitting.ofIsClosed: two closed handlebodies covering a space, whose intersection lies in the closure of the complement of each.
• TauCeti.HeegaardSplitting.symm: the splitting with its two sides exchanged.
• TauCeti.HeegaardSplitting.transHomeomorph: transport of a splitting along a homeomorphism.
• TauCeti.HeegaardSplitting.ofIsOpenQuotientMap: the image of a splitting with saturated pieces under an open quotient map, when the images of the pieces are handlebodies.
• TauCeti.heegaardGenus M: the least genus of a Heegaard splitting of M.
• TauCeti.hemisphereHeegaardSplitting p: the splitting of the 3-sphere into the closed hemispheres around p and -p.

Main results

• TauCeti.heegaardGenus_le and TauCeti.exists_genus_eq_heegaardGenus: the Heegaard genus is the least genus of a splitting.
• TauCeti.heegaardGenus_congr: homeomorphic spaces have the same Heegaard genus.
• TauCeti.heegaardGenus_sphere: the 3-sphere has Heegaard genus zero.

References

• M. Scharlemann, Heegaard splittings of compact 3-manifolds, in Handbook of Geometric Topology, North-Holland (2002), Section 2.
• J. Hempel, 3-Manifolds, Annals of Mathematics Studies 86, Princeton University Press (1976), Chapter 2.

structure TauCeti.HeegaardSplitting (M : Type u_1) [TopologicalSpace M] : Type u_1

A Heegaard splitting of genus genus of a space M: two subsets left and right covering M, each homeomorphic to the standard handlebody of genus genus, whose intersection is the frontier of each of them. In a 3-manifold without boundary this intersection is the common boundary surface of the two handlebodies.

• genus : ℕ

  The genus of the splitting.

• left : Set M

  The first handlebody.

• right : Set M

  The second handlebody.

• union_eq_univ : self.left ∪ self.right = Set.univ

  The two handlebodies cover the space.

• inter_eq_frontier_left : self.left ∩ self.right = frontier self.left

  The two handlebodies meet in the frontier of the first.

• inter_eq_frontier_right : self.left ∩ self.right = frontier self.right

  The two handlebodies meet in the frontier of the second.

• nonempty_homeomorph_left : Nonempty (↑self.left ≃ₜ ↑(handlebody self.genus))

  The first piece is a handlebody of genus genus.

• nonempty_homeomorph_right : Nonempty (↑self.right ≃ₜ ↑(handlebody self.genus))

  The second piece is a handlebody of genus genus.

theorem TauCeti.HeegaardSplitting.ext {M : Type u_1} {inst✝ : TopologicalSpace M} {x y : HeegaardSplitting M} (genus : x.genus = y.genus) (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem TauCeti.HeegaardSplitting.ext_iff {M : Type u_1} {inst✝ : TopologicalSpace M} {x y : HeegaardSplitting M} : x = y ↔ x.genus = y.genus ∧ x.left = y.left ∧ x.right = y.right

theorem TauCeti.HeegaardSplitting.isClosed_left {M : Type u_1} [TopologicalSpace M] (s : HeegaardSplitting M) : IsClosed s.left

The first handlebody of a Heegaard splitting is closed.

theorem TauCeti.HeegaardSplitting.isClosed_right {M : Type u_1} [TopologicalSpace M] (s : HeegaardSplitting M) : IsClosed s.right

The second handlebody of a Heegaard splitting is closed.

def TauCeti.HeegaardSplitting.symm {M : Type u_1} [TopologicalSpace M] (s : HeegaardSplitting M) : HeegaardSplitting M

The Heegaard splitting with its two handlebodies exchanged.

@[simp]

theorem TauCeti.HeegaardSplitting.symm_genus {M : Type u_1} [TopologicalSpace M] (s : HeegaardSplitting M) : s.symm.genus = s.genus

@[simp]

theorem TauCeti.HeegaardSplitting.symm_left {M : Type u_1} [TopologicalSpace M] (s : HeegaardSplitting M) : s.symm.left = s.right

@[simp]

theorem TauCeti.HeegaardSplitting.symm_right {M : Type u_1} [TopologicalSpace M] (s : HeegaardSplitting M) : s.symm.right = s.left

@[simp]

theorem TauCeti.HeegaardSplitting.symm_symm {M : Type u_1} [TopologicalSpace M] (s : HeegaardSplitting M) : s.symm.symm = s

def TauCeti.HeegaardSplitting.transHomeomorph {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) (e : M ≃ₜ N) : HeegaardSplitting N

The image of a Heegaard splitting under a homeomorphism.

def TauCeti.HeegaardSplitting.ofIsClosed {M : Type u_1} [TopologicalSpace M] {L R : Set M} (g : ℕ) (hL : IsClosed L) (hR : IsClosed R) (hLR : L ∪ R = Set.univ) (hLc : L ∩ R ⊆ closure Lᶜ) (hRc : L ∩ R ⊆ closure Rᶜ) (eL : Nonempty (↑L ≃ₜ ↑(handlebody g))) (eR : Nonempty (↑R ≃ₜ ↑(handlebody g))) : HeegaardSplitting M

Two closed handlebodies meeting along their common frontier. Two closed subsets L and R covering M, each homeomorphic to the standard handlebody of genus g, form a Heegaard splitting as soon as every point of L ∩ R is a limit of points outside L and of points outside R; then L ∩ R is the frontier of each of them.

@[simp]

theorem TauCeti.HeegaardSplitting.ofIsClosed_genus {M : Type u_1} [TopologicalSpace M] {L R : Set M} (g : ℕ) (hL : IsClosed L) (hR : IsClosed R) (hLR : L ∪ R = Set.univ) (hLc : L ∩ R ⊆ closure Lᶜ) (hRc : L ∩ R ⊆ closure Rᶜ) (eL : Nonempty (↑L ≃ₜ ↑(handlebody g))) (eR : Nonempty (↑R ≃ₜ ↑(handlebody g))) : (ofIsClosed g hL hR hLR hLc hRc eL eR).genus = g

@[simp]

theorem TauCeti.HeegaardSplitting.ofIsClosed_left {M : Type u_1} [TopologicalSpace M] {L R : Set M} (g : ℕ) (hL : IsClosed L) (hR : IsClosed R) (hLR : L ∪ R = Set.univ) (hLc : L ∩ R ⊆ closure Lᶜ) (hRc : L ∩ R ⊆ closure Rᶜ) (eL : Nonempty (↑L ≃ₜ ↑(handlebody g))) (eR : Nonempty (↑R ≃ₜ ↑(handlebody g))) : (ofIsClosed g hL hR hLR hLc hRc eL eR).left = L

@[simp]

theorem TauCeti.HeegaardSplitting.ofIsClosed_right {M : Type u_1} [TopologicalSpace M] {L R : Set M} (g : ℕ) (hL : IsClosed L) (hR : IsClosed R) (hLR : L ∪ R = Set.univ) (hLc : L ∩ R ⊆ closure Lᶜ) (hRc : L ∩ R ⊆ closure Rᶜ) (eL : Nonempty (↑L ≃ₜ ↑(handlebody g))) (eR : Nonempty (↑R ≃ₜ ↑(handlebody g))) : (ofIsClosed g hL hR hLR hLc hRc eL eR).right = R

@[simp]

theorem TauCeti.HeegaardSplitting.transHomeomorph_genus {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) (e : M ≃ₜ N) : (s.transHomeomorph e).genus = s.genus

@[simp]

theorem TauCeti.HeegaardSplitting.transHomeomorph_left {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) (e : M ≃ₜ N) : (s.transHomeomorph e).left = ⇑e '' s.left

@[simp]

theorem TauCeti.HeegaardSplitting.transHomeomorph_right {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) (e : M ≃ₜ N) : (s.transHomeomorph e).right = ⇑e '' s.right

def TauCeti.HeegaardSplitting.ofIsOpenQuotientMap {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) {π : M → N} (hπ : IsOpenQuotientMap π) (hl : π ⁻¹' π '' s.left = s.left) (hr : π ⁻¹' π '' s.right = s.right) (g : ℕ) (el : Nonempty (↑(π '' s.left) ≃ₜ ↑(handlebody g))) (er : Nonempty (↑(π '' s.right) ≃ₜ ↑(handlebody g))) : HeegaardSplitting N

Heegaard splittings descend along open quotient maps. If both pieces of a Heegaard splitting of M are saturated for an open quotient map π : M → N, and their images are handlebodies of genus g, then the images form a Heegaard splitting of N of genus g.

@[simp]

theorem TauCeti.HeegaardSplitting.ofIsOpenQuotientMap_genus {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) {π : M → N} (hπ : IsOpenQuotientMap π) (hl : π ⁻¹' π '' s.left = s.left) (hr : π ⁻¹' π '' s.right = s.right) (g : ℕ) (el : Nonempty (↑(π '' s.left) ≃ₜ ↑(handlebody g))) (er : Nonempty (↑(π '' s.right) ≃ₜ ↑(handlebody g))) : (s.ofIsOpenQuotientMap hπ hl hr g el er).genus = g

@[simp]

theorem TauCeti.HeegaardSplitting.ofIsOpenQuotientMap_left {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) {π : M → N} (hπ : IsOpenQuotientMap π) (hl : π ⁻¹' π '' s.left = s.left) (hr : π ⁻¹' π '' s.right = s.right) (g : ℕ) (el : Nonempty (↑(π '' s.left) ≃ₜ ↑(handlebody g))) (er : Nonempty (↑(π '' s.right) ≃ₜ ↑(handlebody g))) : (s.ofIsOpenQuotientMap hπ hl hr g el er).left = π '' s.left

@[simp]

theorem TauCeti.HeegaardSplitting.ofIsOpenQuotientMap_right {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (s : HeegaardSplitting M) {π : M → N} (hπ : IsOpenQuotientMap π) (hl : π ⁻¹' π '' s.left = s.left) (hr : π ⁻¹' π '' s.right = s.right) (g : ℕ) (el : Nonempty (↑(π '' s.left) ≃ₜ ↑(handlebody g))) (er : Nonempty (↑(π '' s.right) ≃ₜ ↑(handlebody g))) : (s.ofIsOpenQuotientMap hπ hl hr g el er).right = π '' s.right

Heegaard genus

noncomputable def TauCeti.heegaardGenus (M : Type u_1) [TopologicalSpace M] [h : Nonempty (HeegaardSplitting M)] : ℕ

The Heegaard genus of a space admitting a Heegaard splitting: the least genus of its Heegaard splittings.

theorem TauCeti.exists_genus_eq_heegaardGenus (M : Type u_1) [TopologicalSpace M] [h : Nonempty (HeegaardSplitting M)] : ∃ (s : HeegaardSplitting M), s.genus = heegaardGenus M

Some Heegaard splitting realizes the Heegaard genus.

theorem TauCeti.heegaardGenus_le {M : Type u_1} [TopologicalSpace M] [h : Nonempty (HeegaardSplitting M)] (s : HeegaardSplitting M) : heegaardGenus M ≤ s.genus

The Heegaard genus is at most the genus of any Heegaard splitting.

theorem TauCeti.le_heegaardGenus_iff {M : Type u_1} [TopologicalSpace M] [h : Nonempty (HeegaardSplitting M)] {n : ℕ} : n ≤ heegaardGenus M ↔ ∀ (s : HeegaardSplitting M), n ≤ s.genus

A lower bound for the Heegaard genus is a lower bound for the genus of every splitting.

theorem TauCeti.heegaardGenus_eq_zero_iff {M : Type u_1} [TopologicalSpace M] [h : Nonempty (HeegaardSplitting M)] : heegaardGenus M = 0 ↔ ∃ (s : HeegaardSplitting M), s.genus = 0

The Heegaard genus vanishes exactly when there is a splitting of genus zero.

theorem TauCeti.heegaardGenus_congr {M : Type u_1} [TopologicalSpace M] [h : Nonempty (HeegaardSplitting M)] {N : Type u_2} [TopologicalSpace N] [Nonempty (HeegaardSplitting N)] (e : M ≃ₜ N) : heegaardGenus M = heegaardGenus N

The Heegaard genus is a topological invariant.

The genus-zero splitting of the 3-sphere

def TauCeti.hemisphereHeegaardSplitting {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 4)] (p : ↑(Metric.sphere 0 1)) : HeegaardSplitting ↑(Metric.sphere 0 1)

The genus-zero Heegaard splitting of the unit sphere of a four-dimensional real inner product space into the closed hemispheres around p and -p, meeting along the equator.

@[simp]

theorem TauCeti.hemisphereHeegaardSplitting_genus {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 4)] (p : ↑(Metric.sphere 0 1)) : (hemisphereHeegaardSplitting p).genus = 0

@[simp]

theorem TauCeti.hemisphereHeegaardSplitting_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 4)] (p : ↑(Metric.sphere 0 1)) : (hemisphereHeegaardSplitting p).left = {x : ↑(Metric.sphere 0 1) | 0 ≤ inner ℝ ↑x ↑p}

@[simp]

theorem TauCeti.hemisphereHeegaardSplitting_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 4)] (p : ↑(Metric.sphere 0 1)) : (hemisphereHeegaardSplitting p).right = {x : ↑(Metric.sphere 0 1) | inner ℝ ↑x ↑p ≤ 0}

instance TauCeti.instNonemptyHeegaardSplittingElemSphereOfNatReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 4)] : Nonempty (HeegaardSplitting ↑(Metric.sphere 0 1))

theorem TauCeti.heegaardGenus_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 4)] : heegaardGenus ↑(Metric.sphere 0 1) = 0

The 3-sphere has Heegaard genus zero.