The genus-one Heegaard diagram of S¹ × S²

On the torus ℝ² / ℤ² let α be the circle y = 0 and let β be the circle y = ε sin (2π x) for a small ε > 0, both oriented by increasing x. Two isotopic attaching circles on a torus give S¹ × S²; the perturbation makes them meet transversally in the two points p₀ = (0, 0) and p₁ = (1/2, 0). The complement of α ∪ β has three regions: the bigon B₁ between α and β over 0 < x < 1/2, where β lies above α; the bigon B₂ over 1/2 < x < 1, where β lies below α; and the annulus A making up the rest of the torus.

In TauCeti.HeegaardRegionSystem.circleTimesSphere r the points p₀, p₁ are 0, 1 : Fin 2, the regions A, B₁, B₂ are 0, 1, 2 : Fin 3, and the single basepoint lies in the region r. Both bigons are domains from the generator p₀ to the generator p₁, so their difference B₁ - B₂, whose boundary is α - β, is a periodic domain whenever the basepoint lies in A.

This is a basic example of a diagram with a nonzero periodic domain, on which weak admissibility depends on the placement of the basepoint. With the basepoint in the annulus, the periodic domains are the multiples of B₁ - B₂, and the diagram is weakly admissible. With the basepoint in a bigon, say B₁, the periodic domain A + 2 B₂ has no negative coefficient, so the diagram is not weakly admissible.

The regions have Euler characteristics χ(A) = 0 and χ(B₁) = χ(B₂) = 1; the annulus has four corners and each bigon has two. With these, the combinatorial Maslov index of each bigon is 1, as for the domain of a holomorphic bigon, and that of the periodic domain B₁ - B₂ is 0.

Main definitions

• TauCeti.HeegaardRegionSystem.circleTimesSphere: the diagram, with its basepoint in a given region.
• TauCeti.HeegaardRegionSystem.circleTimesSphereGenerator: its two generators.

Main results

• TauCeti.HeegaardRegionSystem.isDomainBetween_circleTimesSphere_single_one and TauCeti.HeegaardRegionSystem.isDomainBetween_circleTimesSphere_single_two: both bigons are domains from p₀ to p₁.
• TauCeti.HeegaardRegionSystem.mem_periodicDomains_circleTimesSphere_iff: periodic-domain membership for any basepoint placement.
• TauCeti.HeegaardRegionSystem.periodicDomains_circleTimesSphere_zero: with the basepoint in the annulus, the periodic domains are the multiples of B₁ - B₂.
• TauCeti.HeegaardRegionSystem.weaklyAdmissible_circleTimesSphere_iff: the diagram is weakly admissible exactly when its basepoint lies in the annulus.
• TauCeti.HeegaardRegionSystem.not_weaklyAdmissible_circleTimesSphere_one: with the basepoint in a bigon, the diagram is not weakly admissible.
• TauCeti.HeegaardRegionSystem.maslovIndex_circleTimesSphere_single_one, TauCeti.HeegaardRegionSystem.maslovIndex_circleTimesSphere_single_two and TauCeti.HeegaardRegionSystem.maslovIndex_circleTimesSphere_periodic: both bigons have Maslov index one and the periodic domain has Maslov index zero.

References

• P. Ozsváth and Z. Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Ann. of Math. 159 (2004), arXiv:math/0101206, §4.2, where admissibility is introduced.

def TauCeti.HeegaardRegionSystem.circleTimesSphere (r : Fin 3) : HeegaardRegionSystem 1 (Fin 2) (Fin 3) Unit

The genus-one Heegaard diagram of S¹ × S² whose two attaching circles meet in two points, with its basepoint in the region r. The regions 0, 1, 2 are the annulus and the two bigons.

Equations

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

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_alpha (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).alpha p = 0

Both intersection points lie on the unique α-curve.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_beta (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).beta p = 0

Both intersection points lie on the unique β-curve.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_alphaNext (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).alphaNext p = (Equiv.swap 0 1) p

The successor on the α-curve exchanges the two intersection points.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_betaNext (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).betaNext p = (Equiv.swap 0 1) p

The successor on the β-curve exchanges the two intersection points.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_alphaNext_symm (r : Fin 3) (p : Fin 2) : (Equiv.symm (circleTimesSphere r).alphaNext) p = (Equiv.swap 0 1) p

The predecessor on the α-curve exchanges the two intersection points.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_betaNext_symm (r : Fin 3) (p : Fin 2) : (Equiv.symm (circleTimesSphere r).betaNext) p = (Equiv.swap 0 1) p

The predecessor on the β-curve exchanges the two intersection points.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_alphaLeft (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).alphaLeft p = ![1, 0] p

The regions to the left of the two α-arcs.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_alphaRight (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).alphaRight p = ![0, 2] p

The regions to the right of the two α-arcs.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_betaLeft (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).betaLeft p = ![0, 2] p

The regions to the left of the two β-arcs.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_betaRight (r : Fin 3) (p : Fin 2) : (circleTimesSphere r).betaRight p = ![1, 0] p

The regions to the right of the two β-arcs.

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphere_basepoint (r : Fin 3) (z : Unit) : (circleTimesSphere r).basepoint z = r

The basepoint lies in the region r.

def TauCeti.HeegaardRegionSystem.circleTimesSphereGenerator (r : Fin 3) (a : Fin 2) : (circleTimesSphere r).Generator

The generator of circleTimesSphere r at the intersection point a.

Equations

• TauCeti.HeegaardRegionSystem.circleTimesSphereGenerator r a = (TauCeti.HeegaardRegionSystem.circleTimesSphere r).generatorOf 1 (fun (x : Fin 1) => a) ⋯ ⋯

@[simp]

theorem TauCeti.HeegaardRegionSystem.circleTimesSphereGenerator_point (r : Fin 3) (a : Fin 2) (i : Fin 1) : (circleTimesSphere r).point (circleTimesSphereGenerator r a) i = a

The unique point chosen by circleTimesSphereGenerator r a is a.

theorem TauCeti.HeegaardRegionSystem.generatorChain_circleTimesSphereGenerator (r : Fin 3) (a q : Fin 2) : (circleTimesSphere r).generatorChain (circleTimesSphereGenerator r a) q = if a = q then 1 else 0

The generator chain is supported at its chosen intersection point.

theorem TauCeti.HeegaardRegionSystem.mem_periodicDomains_circleTimesSphere_iff (r : Fin 3) (D : Fin 3 → ℤ) : D ∈ (circleTimesSphere r).periodicDomains ↔ D r = 0 ∧ D 1 + D 2 = 2 * D 0

A domain of circleTimesSphere r is periodic exactly when it vanishes at the basepoint and its multiplicities satisfy D B₁ + D B₂ = 2 D A.

theorem TauCeti.HeegaardRegionSystem.isDomainBetween_circleTimesSphere_single_one (r : Fin 3) : IsDomainBetween (circleTimesSphereGenerator r 0) (circleTimesSphereGenerator r 1) (Pi.single 1 1)

The bigon B₁ is a domain from the generator p₀ to the generator p₁.

theorem TauCeti.HeegaardRegionSystem.isDomainBetween_circleTimesSphere_single_two (r : Fin 3) : IsDomainBetween (circleTimesSphereGenerator r 0) (circleTimesSphereGenerator r 1) (Pi.single 2 1)

The bigon B₂ is a domain from the generator p₀ to the generator p₁.

theorem TauCeti.HeegaardRegionSystem.periodicDomains_circleTimesSphere_zero : (circleTimesSphere 0).periodicDomains = AddSubgroup.zmultiples (Pi.single 1 1 - Pi.single 2 1)

With the basepoint in the annulus, the periodic domains of the genus-one diagram of S¹ × S² are the multiples of the difference B₁ - B₂ of the two bigons.

theorem TauCeti.HeegaardRegionSystem.weaklyAdmissible_circleTimesSphere_zero : (circleTimesSphere 0).WeaklyAdmissible

With the basepoint in the annulus, the genus-one diagram of S¹ × S² is weakly admissible.

@[simp]

theorem TauCeti.HeegaardRegionSystem.weaklyAdmissible_circleTimesSphere_iff (r : Fin 3) : (circleTimesSphere r).WeaklyAdmissible ↔ r = 0

The genus-one diagram of S¹ × S² is weakly admissible exactly when its basepoint lies in the annulus.

theorem TauCeti.HeegaardRegionSystem.not_weaklyAdmissible_circleTimesSphere_one : ¬(circleTimesSphere 1).WeaklyAdmissible

With the basepoint in a bigon, the genus-one diagram of S¹ × S² is not weakly admissible: the periodic domain A + 2 B₂ has no negative coefficient.

@[simp]

theorem TauCeti.HeegaardRegionSystem.cornerCount_circleTimesSphere (r s : Fin 3) : (circleTimesSphere r).cornerCount s = ![4, 2, 2] s

The annulus has four corners and each bigon has two.

theorem TauCeti.HeegaardRegionSystem.maslovIndex_circleTimesSphere_single_one (r : Fin 3) : ((circleTimesSphere r).maslovIndex ![0, 1, 1] (circleTimesSphereGenerator r 0) (circleTimesSphereGenerator r 1)) (Pi.single 1 1) = 1

The bigon B₁, a disk with two corners, has Maslov index one.

theorem TauCeti.HeegaardRegionSystem.maslovIndex_circleTimesSphere_single_two (r : Fin 3) : ((circleTimesSphere r).maslovIndex ![0, 1, 1] (circleTimesSphereGenerator r 0) (circleTimesSphereGenerator r 1)) (Pi.single 2 1) = 1

The bigon B₂, a disk with two corners, has Maslov index one.

theorem TauCeti.HeegaardRegionSystem.maslovIndex_circleTimesSphere_periodic (r : Fin 3) (a : Fin 2) : ((circleTimesSphere r).maslovIndex ![0, 1, 1] (circleTimesSphereGenerator r a) (circleTimesSphereGenerator r a)) (Pi.single 1 1 - Pi.single 2 1) = 0

The periodic domain B₁ - B₂ has Maslov index zero at both generators.