The genus of a surface from its rational first homology

A compact, connected, orientable surface of genus g has H₁(S; ℚ) ≅ ℚ²ᵍ when it is closed and H₁(S; ℚ) ≅ ℚ²ᵍ⁺ᵇ⁻¹ when it has b ≥ 1 boundary circles. So for a closed surface, or a surface with one or two boundary circles, the genus is ⌊dim H₁(S; ℚ) / 2⌋. This file defines that quantity once for every topological space (TauCeti.surfaceGenus), as the common genus convention of Seifert surfaces, slice surfaces, knot cobordisms and surfaces representing a homology class.

Main definitions

• TauCeti.surfaceGenus X: half the dimension of H₁(X; ℚ), rounded down.

Main results

• TauCeti.surfaceGenus_eq_zero_of_contractibleSpace: a contractible space, such as a disc, has genus 0.

noncomputable def TauCeti.surfaceGenus (X : Type) [TopologicalSpace X] : ℕ

The genus of a surface X, read off its rational singular homology: half the dimension of H₁(X; ℚ), rounded down. For a compact, connected, orientable surface which is closed or has at most two boundary circles, this is its genus.

theorem TauCeti.surfaceGenus_def (X : Type) [TopologicalSpace X] : surfaceGenus X = Module.finrank ℚ ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℚ) 1).obj ↧ℚ).obj ↧X) / 2

The genus of a surface is half the dimension of its first rational homology, rounded down.

@[simp]

theorem TauCeti.surfaceGenus_eq_zero_of_contractibleSpace (X : Type) [TopologicalSpace X] [ContractibleSpace X] : surfaceGenus X = 0

A contractible space has genus 0: its first homology vanishes.