The genus-one Heegaard diagrams of lens spaces

Fix p ≥ 1 and a unit q of ZMod p. On the torus ℝ² / ℤ² let α be the circle y = 0, oriented by increasing x, and let β be the closed curve t ↦ (q t, p t) of homology class (q, p), oriented by increasing t. Attaching disks along α and β gives the lens space L(p, q): the meridian β of the second solid torus is glued to p λ + q μ, where μ = α. The two curves meet transversally in the p points x_j = (j / p, 0), j ∈ ZMod p. Going along α the point after x_j is x_{j+1}; going along β it is x_{j+q}. Cutting the torus along α leaves an annulus that the p arcs of β cut into p parallelograms; the region R_j is the one whose bottom edge is the α-arc from x_j to x_{j+1}, its top edge is the α-arc from x_{j-q} to x_{j-q+1}, and its two sides are the β-arcs starting at x_j and x_{j+1}.

TauCeti.HeegaardRegionSystem.lensSpace p q r records this incidence data, with points and regions both indexed by ZMod p and the basepoint in the region R_r. Each point is a generator (TauCeti.HeegaardRegionSystem.lensSpaceGenerator), and every generator is of this form.

The group CurveHomology in which the classes ε(x, y) live is identified with H₁(L(p, q)) = ℤ/p (TauCeti.HeegaardRegionSystem.lensSpaceCurveHomologyEquiv): a cycle of α ∪ β whose β-part has total coefficient s winds s times around the y-direction, and the equivalence sends its class to -q s. Under this identification ε(x_a, x_b) = b - a. So the p generators lie in the p distinct classes, and no domain joins two distinct generators. Since s_z(x) - s_z(y) is Poincaré dual to ε(x, y), this puts one generator in each of the p spin^c structures of L(p, q). The diagram has no nonzero periodic domain, so it is weakly admissible. These are the combinatorial inputs to the computation HF̂(L(p, q)) ≅ 𝔽₂^p: the hat differential only counts disks whose domains join two generators, so it vanishes on this diagram. The Floer complex itself is not constructed here.

Main definitions

• TauCeti.HeegaardRegionSystem.lensSpace: the genus-one diagram of L(p, q), with its basepoint in a given region.
• TauCeti.HeegaardRegionSystem.lensSpaceGenerator: the generator at the intersection point x_a.
• TauCeti.HeegaardRegionSystem.lensSpaceCurveHomologyEquiv: CurveHomology ≃+ ZMod p.

Main results

• TauCeti.HeegaardRegionSystem.lensSpaceCurveHomologyEquiv_epsilon: the identification sends ε(x_a, x_b) to b - a.
• TauCeti.HeegaardRegionSystem.epsilon_lensSpace_eq_zero_iff: ε(x, y) = 0 exactly when x = y, and TauCeti.HeegaardRegionSystem.exists_isDomainBetween_lensSpace_iff: a domain joins x to y exactly when x = y.
• TauCeti.HeegaardRegionSystem.epsilon_lensSpace_bijective: y ↦ ε(x, y) is a bijection from the generators onto CurveHomology.
• TauCeti.HeegaardRegionSystem.addOrderOf_epsilon_lensSpace: ε(x_a, x_{a+1}) has order p.
• TauCeti.HeegaardRegionSystem.periodicDomains_lensSpace and TauCeti.HeegaardRegionSystem.weaklyAdmissible_lensSpace: the only periodic domain is zero, so the diagram is weakly admissible.

References

• P. Ozsváth and Z. Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Ann. of Math. 159 (2004), arXiv:math/0101206, §2.4 for ε(x, y) and periodic domains; their §3 uses these genus-one diagrams of lens spaces.
• D. Rolfsen, Knots and Links, Chapter 9.B, for the lens space L(p, q) as the union of two solid tori glued along the slope p λ + q μ.

def TauCeti.HeegaardRegionSystem.lensSpace (p : ℕ) [NeZero p] (q : (ZMod p)ˣ) (r : ZMod p) : HeegaardRegionSystem 1 (ZMod p) (ZMod p) Unit

The genus-one Heegaard diagram of the lens space L(p, q), with its basepoint in the region r. The point x_j and the region R_j are both indexed by j : ZMod p; the point after x_j is x_{j+1} along α and x_{j+q} along β. The α-arc starting at x_j has R_j on its left and R_{j-q} on its right, and the β-arc starting at x_j has R_{j-1} on its left and R_j on its right.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_alphaNext_apply {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (lensSpace p q r).alphaNext j = j + 1

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_betaNext_apply {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (lensSpace p q r).betaNext j = j + ↑q

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_alphaNext_symm_apply {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (Equiv.symm (lensSpace p q r).alphaNext) j = j - 1

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_betaNext_symm_apply {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (Equiv.symm (lensSpace p q r).betaNext) j = j - ↑q

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_basepoint {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (z : Unit) : (lensSpace p q r).basepoint z = r

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_alphaLeft {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (lensSpace p q r).alphaLeft j = j

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_alphaRight {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (lensSpace p q r).alphaRight j = j - ↑q

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_betaLeft {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (lensSpace p q r).betaLeft j = j - 1

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpace_betaRight {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (j : ZMod p) : (lensSpace p q r).betaRight j = j

def TauCeti.HeegaardRegionSystem.lensSpaceGenerator (p : ℕ) [NeZero p] (q : (ZMod p)ˣ) (r a : ZMod p) : (lensSpace p q r).Generator

The generator of lensSpace p q r at the intersection point x_a.

Equations

• TauCeti.HeegaardRegionSystem.lensSpaceGenerator p q r a = (TauCeti.HeegaardRegionSystem.lensSpace p q r).generatorOf 1 (fun (x : Fin 1) => a) ⋯ ⋯

@[simp]

theorem TauCeti.HeegaardRegionSystem.coe_lensSpaceGenerator_snd {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (a : ZMod p) (i : Fin 1) : ↑((lensSpaceGenerator p q r a).snd i) = a

@[simp]

theorem TauCeti.HeegaardRegionSystem.lensSpaceGenerator_point {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (x : (lensSpace p q r).Generator) : lensSpaceGenerator p q r ↑(x.snd 0) = x

Every generator of lensSpace p q r is the generator at its intersection point.

theorem TauCeti.HeegaardRegionSystem.lensSpaceGenerator_bijective {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} : Function.Bijective (lensSpaceGenerator p q r)

The generators of lensSpace p q r are indexed by the intersection points.

@[simp]

theorem TauCeti.HeegaardRegionSystem.generatorChain_lensSpaceGenerator {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (a : ZMod p) : (lensSpace p q r).generatorChain (lensSpaceGenerator p q r a) = Pi.single a 1

The 0-chain of the generator at x_a is the point x_a.

noncomputable def TauCeti.HeegaardRegionSystem.lensSpaceCurveHomologyEquiv (p : ℕ) [NeZero p] (q : (ZMod p)ˣ) (r : ZMod p) : (lensSpace p q r).CurveHomology ≃+ ZMod p

The group CurveHomology of the lens space diagram is H₁(L(p, q)) = ℤ/p: the class of a cycle of α ∪ β whose β-part has total coefficient s goes to -q s. Under this identification ε(x_a, x_b) = b - a (lensSpaceCurveHomologyEquiv_epsilon).

Equations

• TauCeti.HeegaardRegionSystem.lensSpaceCurveHomologyEquiv p q r = AddEquiv.ofBijective (TauCeti.HeegaardRegionSystem.windingHom✝ p q r) ⋯

theorem TauCeti.HeegaardRegionSystem.lensSpaceCurveHomologyEquiv_mk {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (c : ↥(lensSpace p q r).arcCycles) : (lensSpaceCurveHomologyEquiv p q r) ((CurveHomology.mk (lensSpace p q r)) c) = -(↑q * ∑ j : ZMod p, ↑((↑c).2 j))

The class of a cycle c of α ∪ β is -q times the total coefficient of its β-part.

theorem TauCeti.HeegaardRegionSystem.lensSpaceCurveHomologyEquiv_epsilon {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (x y : (lensSpace p q r).Generator) : (lensSpaceCurveHomologyEquiv p q r) ((lensSpace p q r).epsilon x y) = (lensSpace p q r).point y 0 - (lensSpace p q r).point x 0

The class ε(x, y) of two generators is the difference of their intersection points.

theorem TauCeti.HeegaardRegionSystem.epsilon_lensSpace_eq_zero_iff {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} {x y : (lensSpace p q r).Generator} : (lensSpace p q r).epsilon x y = 0 ↔ x = y

In the lens space diagram ε(x, y) vanishes only when x = y: distinct generators lie in distinct spin^c structures.

theorem TauCeti.HeegaardRegionSystem.exists_isDomainBetween_lensSpace_iff {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} {x y : (lensSpace p q r).Generator} : (∃ (D : ZMod p → ℤ), IsDomainBetween x y D) ↔ x = y

In the lens space diagram a domain joins x to y only when x = y.

theorem TauCeti.HeegaardRegionSystem.epsilon_lensSpace_bijective {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (x : (lensSpace p q r).Generator) : Function.Bijective ((lensSpace p q r).epsilon x)

The generators of the lens space diagram are in bijection with CurveHomology, and so with the spin^c structures of L(p, q), through y ↦ ε(x, y).

theorem TauCeti.HeegaardRegionSystem.addOrderOf_epsilon_lensSpace {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} (a : ZMod p) : addOrderOf ((lensSpace p q r).epsilon (lensSpaceGenerator p q r a) (lensSpaceGenerator p q r (a + 1))) = p

The class ε(x_a, x_{a+1}) of two consecutive generators has order p, as a generator of H₁(L(p, q)) = ℤ/p should.

@[simp]

theorem TauCeti.HeegaardRegionSystem.periodicDomains_lensSpace {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} : (lensSpace p q r).periodicDomains = ⊥

The lens space diagram has no nonzero periodic domain: a domain whose boundary is a combination of whole α- and β-curves and whose multiplicity at the basepoint region R_r is zero must vanish. Hence the diagram is weakly admissible (weaklyAdmissible_lensSpace) for every basepoint, and for each pair of generators there is at most one domain joining them.

theorem TauCeti.HeegaardRegionSystem.weaklyAdmissible_lensSpace {p : ℕ} [NeZero p] {q : (ZMod p)ˣ} {r : ZMod p} : (lensSpace p q r).WeaklyAdmissible

The lens space diagram is weakly admissible.