Domains and periodic domains of a pointed Heegaard diagram

The attaching curves of a pointed Heegaard diagram (Σ, α, β, z) cut the surface into regions, the closures of the components of Σ - α - β. A domain is an integral combination of regions. This file records the incidence data that domains need, with no surface in sight, and develops domains, periodic domains and weak admissibility on top of it.

HeegaardRegionSystem is abstract incidence data: Region is supplied by the caller. Its local incidence conditions do not identify the connected components of the complement of a specified surface diagram. To use these definitions for such a diagram, one must separately show that its supplied labels are exactly those components; identifying two components changes the incidence system and can change its periodic domains and admissibility. All results below concern the supplied incidence system.

The data extends TauCeti.HeegaardIntersectionSystem, which labels each intersection point by its α- and β-curve. Orient every attaching curve. The intersection points on the α-curve α_i cut it into arcs, one starting at each point p on α_i and ending at the next point along α_i, alphaNext p; when that curve has intersection points, they form a single cycle of alphaNext. Empty curve fibres satisfy the cycle condition vacuously. Each such arc has a region on its left and one on its right. The β-curves are recorded in the same way, with compatible region labels at each crossing and every region incident to an arc unless there are no intersection arcs. Each basepoint lies in a region. A generator supplies an intersection point on every curve, so curves in a diagram with a generator are subdivided into arcs.

In these terms the α-part of the boundary of a domain D is the 1-chain on α-arcs whose coefficient on the arc starting at p is D (alphaLeft p) - D (alphaRight p), and the boundary of the arc starting at p is alphaNext p - p. A domain D connects a generator x to a generator y when ∂(∂D ∩ α) = y - x and ∂(∂D ∩ β) = x - y; the domain of every Whitney disk from x to y connects x to y in this sense. A domain is periodic when it has multiplicity zero at every basepoint and its boundary is a sum of whole α- and β-curves. The periodic domains form a subgroup, and the domains connecting x to y with prescribed basepoint multiplicities form a coset of it. A diagram is weakly admissible when every nonzero periodic domain has both positive and negative coefficients: the finiteness hypothesis under which the differential of HF̂ is a finite count.

Main definitions

• TauCeti.HeegaardRegionSystem: intersection data together with the cyclic order of the intersection points along each curve, the regions on the two sides of each arc, and the regions containing the basepoints.
• TauCeti.HeegaardRegionSystem.alphaBoundary, TauCeti.HeegaardRegionSystem.betaBoundary: the α- and β-parts of the boundary of a domain.
• TauCeti.HeegaardRegionSystem.alphaArcBoundary, TauCeti.HeegaardRegionSystem.betaArcBoundary: the boundary of a 1-chain on the α- or β-arcs.
• TauCeti.HeegaardRegionSystem.IsDomainBetween: D is a domain connecting x to y.
• TauCeti.HeegaardRegionSystem.periodicDomains: the subgroup of periodic domains.
• TauCeti.HeegaardRegionSystem.WeaklyAdmissible: every nonzero periodic domain has both positive and negative coefficients.

Main results

• TauCeti.HeegaardRegionSystem.boundary_boundary_eq_zero: the full boundary of every region chain is a cycle.
• TauCeti.HeegaardRegionSystem.alphaArcBoundary_eq_zero_iff: a 1-chain on the α-arcs is a cycle exactly when it is a combination of whole α-curves.
• TauCeti.HeegaardRegionSystem.mem_periodicDomains_iff_exists_curves: a domain is periodic exactly when it avoids the basepoints and its boundary is a combination of whole curves.
• TauCeti.HeegaardRegionSystem.IsDomainBetween.add: domains connecting x to y and y to w add to a domain connecting x to w.
• TauCeti.HeegaardRegionSystem.IsDomainBetween.sub_mem_periodicDomains_iff: the domains connecting x to y with the basepoint multiplicities of a given one form a coset of the periodic domains.
• TauCeti.HeegaardRegionSystem.weaklyAdmissible_iff: weak admissibility says that the only nonnegative periodic domain is 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, §2.4 (domains and periodic domains) and §4.2 (admissibility). Their weak admissibility for a spin^c structure 𝔰 quantifies only over the periodic domains P with ⟨c₁(𝔰), H(P)⟩ = 0; the condition here quantifies over all periodic domains, so it implies weak admissibility for every spin^c structure.
• R. Lipshitz, A cylindrical reformulation of Heegaard Floer homology, Geom. Topol. 10 (2006), arXiv:math/0502404, for the corner conditions ∂(∂D ∩ α) = y - x and ∂(∂D ∩ β) = x - y.

structure TauCeti.HeegaardRegionSystem (n : ℕ) (Point : Type u) (Region : Type v) (Basepoint : Type w) extends TauCeti.HeegaardIntersectionSystem n Point : Type (max (max u v) w)

The incidence data of a pointed Heegaard diagram needed for domains. On top of the intersection data it records, for each intersection point p, the next intersection point along the oriented α- and β-curve through p, the regions to the left and to the right of the arcs starting at p, and the region containing each basepoint. The points on each curve form a single cycle of the corresponding successor permutation when nonempty. Region labels agree around each crossing. Each region is incident to an arc, apart from the one-region case with no arcs. The data does not assert that the labels are the connected complementary regions of a particular surface realization; that requires a separate identification.

• pointFintype : Fintype Point
• alpha : Point → Fin n
• beta : Point → Fin n
• alphaNext : Equiv.Perm Point

  The next intersection point along the oriented α-curve.

• alphaNext_isCycleOn (i : Fin n) : self.alphaNext.IsCycleOn {p : Point | self.alpha p = i}

  The intersection points on a nonempty α-curve fibre form one cycle of alphaNext; empty fibres satisfy this condition vacuously.

• betaNext : Equiv.Perm Point

  The next intersection point along the oriented β-curve.

• betaNext_isCycleOn (j : Fin n) : self.betaNext.IsCycleOn {p : Point | self.beta p = j}

  The intersection points on a nonempty β-curve fibre form one cycle of betaNext; empty fibres satisfy this condition vacuously.

• alphaLeft : Point → Region

  The region to the left of the α-arc starting at an intersection point.

• alphaRight : Point → Region

  The region to the right of the α-arc starting at an intersection point.

• betaLeft : Point → Region

  The region to the left of the β-arc starting at an intersection point.

• betaRight : Point → Region

  The region to the right of the β-arc starting at an intersection point.

• regionNonempty : Nonempty Region

  The diagram has a complementary region.

• crossingCompatible (p : Point) : self.alphaLeft ((Equiv.symm self.alphaNext) p) = self.betaLeft p ∧ self.alphaRight ((Equiv.symm self.alphaNext) p) = self.betaLeft ((Equiv.symm self.betaNext) p) ∧ self.alphaLeft p = self.betaRight p ∧ self.alphaRight p = self.betaRight ((Equiv.symm self.betaNext) p) ∨ self.alphaLeft ((Equiv.symm self.alphaNext) p) = self.betaRight ((Equiv.symm self.betaNext) p) ∧ self.alphaRight ((Equiv.symm self.alphaNext) p) = self.betaRight p ∧ self.alphaLeft p = self.betaLeft ((Equiv.symm self.betaNext) p) ∧ self.alphaRight p = self.betaLeft p

  The four region labels around each transverse crossing agree on the α- and β-arc sides. The two alternatives are the two possible local crossing orientations.

• regionCovered (r : Region) : (∃ (p : Point), self.alphaLeft p = r ∨ self.alphaRight p = r ∨ self.betaLeft p = r ∨ self.betaRight p = r) ∨ IsEmpty Point ∧ Subsingleton Region

  Every region meets an arc, except for the unique region of a diagram with no intersection arcs.

• basepoint : Basepoint → Region

  The region containing a basepoint.

theorem TauCeti.HeegaardRegionSystem.ext {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {x y : HeegaardRegionSystem n Point Region Basepoint} (pointFintype : x.pointFintype = y.pointFintype) (alpha : x.alpha = y.alpha) (beta : x.beta = y.beta) (alphaNext : x.alphaNext = y.alphaNext) (betaNext : x.betaNext = y.betaNext) (alphaLeft : x.alphaLeft = y.alphaLeft) (alphaRight : x.alphaRight = y.alphaRight) (betaLeft : x.betaLeft = y.betaLeft) (betaRight : x.betaRight = y.betaRight) (basepoint : x.basepoint = y.basepoint) : x = y

theorem TauCeti.HeegaardRegionSystem.ext_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {x y : HeegaardRegionSystem n Point Region Basepoint} : x = y ↔ x.pointFintype = y.pointFintype ∧ x.alpha = y.alpha ∧ x.beta = y.beta ∧ x.alphaNext = y.alphaNext ∧ x.betaNext = y.betaNext ∧ x.alphaLeft = y.alphaLeft ∧ x.alphaRight = y.alphaRight ∧ x.betaLeft = y.betaLeft ∧ x.betaRight = y.betaRight ∧ x.basepoint = y.basepoint

@[simp]

theorem TauCeti.HeegaardRegionSystem.alpha_alphaNext {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (p : Point) : H.alpha (H.alphaNext p) = H.alpha p

The successor along an α-curve stays on that curve.

@[simp]

theorem TauCeti.HeegaardRegionSystem.alpha_alphaNext_symm {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (p : Point) : H.alpha ((Equiv.symm H.alphaNext) p) = H.alpha p

The predecessor along an α-curve stays on that curve.

@[simp]

theorem TauCeti.HeegaardRegionSystem.beta_betaNext {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (p : Point) : H.beta (H.betaNext p) = H.beta p

The successor along a β-curve stays on that curve.

@[simp]

theorem TauCeti.HeegaardRegionSystem.beta_betaNext_symm {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (p : Point) : H.beta ((Equiv.symm H.betaNext) p) = H.beta p

The predecessor along a β-curve stays on that curve.

def TauCeti.HeegaardRegionSystem.alphaBoundary {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : (Region → ℤ) →+ Point → ℤ

The α-part ∂D ∩ α of the boundary of a domain, as a 1-chain on the α-arcs: its coefficient on the arc starting at p is the multiplicity of D to the left of the arc minus the multiplicity to its right.

Equations

• H.alphaBoundary = { toFun := fun (D : Region → ℤ) (p : Point) => D (H.alphaLeft p) - D (H.alphaRight p), map_zero' := ⋯, map_add' := ⋯ }

def TauCeti.HeegaardRegionSystem.betaBoundary {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : (Region → ℤ) →+ Point → ℤ

The β-part ∂D ∩ β of the boundary of a domain, as a 1-chain on the β-arcs: its coefficient on the arc starting at p is the multiplicity of D to the left of the arc minus the multiplicity to its right.

Equations

• H.betaBoundary = { toFun := fun (D : Region → ℤ) (p : Point) => D (H.betaLeft p) - D (H.betaRight p), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.HeegaardRegionSystem.alphaBoundary_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) (p : Point) : H.alphaBoundary D p = D (H.alphaLeft p) - D (H.alphaRight p)

@[simp]

theorem TauCeti.HeegaardRegionSystem.betaBoundary_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) (p : Point) : H.betaBoundary D p = D (H.betaLeft p) - D (H.betaRight p)

def TauCeti.HeegaardRegionSystem.alphaArcBoundary {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : (Point → ℤ) →+ Point → ℤ

The boundary of a 1-chain on the α-arcs, indexed by starting points. The arc starting at p ends at alphaNext p, so the coefficient at q is that of the arc ending at q minus that of the arc starting at q.

Equations

• H.alphaArcBoundary = { toFun := fun (c : Point → ℤ) (q : Point) => c ((Equiv.symm H.alphaNext) q) - c q, map_zero' := ⋯, map_add' := ⋯ }

def TauCeti.HeegaardRegionSystem.betaArcBoundary {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : (Point → ℤ) →+ Point → ℤ

The boundary of a 1-chain on the β-arcs, indexed by starting points. The arc starting at p ends at betaNext p, so the coefficient at q is that of the arc ending at q minus that of the arc starting at q.

Equations

• H.betaArcBoundary = { toFun := fun (c : Point → ℤ) (q : Point) => c ((Equiv.symm H.betaNext) q) - c q, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.HeegaardRegionSystem.alphaArcBoundary_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (c : Point → ℤ) (q : Point) : H.alphaArcBoundary c q = c ((Equiv.symm H.alphaNext) q) - c q

@[simp]

theorem TauCeti.HeegaardRegionSystem.betaArcBoundary_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (c : Point → ℤ) (q : Point) : H.betaArcBoundary c q = c ((Equiv.symm H.betaNext) q) - c q

theorem TauCeti.HeegaardRegionSystem.boundary_boundary_eq_zero {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) : H.alphaArcBoundary (H.alphaBoundary D) + H.betaArcBoundary (H.betaBoundary D) = 0

The full boundary of a region chain is a cycle.

theorem TauCeti.HeegaardRegionSystem.alphaArcBoundary_eq_zero_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (c : Point → ℤ) : H.alphaArcBoundary c = 0 ↔ ∃ (a : Fin n → ℤ), ∀ (p : Point), c p = a (H.alpha p)

A 1-chain on the α-arcs is a cycle exactly when it is a combination of whole α-curves, that is, constant along each α-curve.

theorem TauCeti.HeegaardRegionSystem.betaArcBoundary_eq_zero_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (c : Point → ℤ) : H.betaArcBoundary c = 0 ↔ ∃ (b : Fin n → ℤ), ∀ (p : Point), c p = b (H.beta p)

A 1-chain on the β-arcs is a cycle exactly when it is a combination of whole β-curves, that is, constant along each β-curve.

def TauCeti.HeegaardRegionSystem.IsDomainBetween {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} (x y : H.Generator) (D : Region → ℤ) : Prop

D is a domain connecting the generator x to the generator y: the boundary of its α-part is y - x and the boundary of its β-part is x - y. The domain of every Whitney disk from x to y satisfies these corner conditions.

Equations

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

@[simp]

theorem TauCeti.HeegaardRegionSystem.isDomainBetween_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {D : Region → ℤ} : IsDomainBetween x y D ↔ H.alphaArcBoundary (H.alphaBoundary D) = H.generatorChain y - H.generatorChain x ∧ H.betaArcBoundary (H.betaBoundary D) = H.generatorChain x - H.generatorChain y

theorem TauCeti.HeegaardRegionSystem.isDomainBetween_zero {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} (x : H.Generator) : IsDomainBetween x x 0

The zero domain connects every generator to itself.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.add {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y w : H.Generator} {D E : Region → ℤ} (hD : IsDomainBetween x y D) (hE : IsDomainBetween y w E) : IsDomainBetween x w (D + E)

Juxtaposing a domain from x to y with one from y to w gives a domain from x to w.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.neg {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {D : Region → ℤ} (hD : IsDomainBetween x y D) : IsDomainBetween y x (-D)

Reversing a domain from x to y gives a domain from y to x.

def TauCeti.HeegaardRegionSystem.periodicDomains {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : AddSubgroup (Region → ℤ)

The periodic domains: the domains with multiplicity zero at every basepoint whose boundary is a sum of whole α- and β-curves, that is, whose α- and β-parts are cycles.

Equations

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

@[simp]

theorem TauCeti.HeegaardRegionSystem.mem_periodicDomains_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {P : Region → ℤ} : P ∈ H.periodicDomains ↔ (∀ (z : Basepoint), P (H.basepoint z) = 0) ∧ H.alphaArcBoundary (H.alphaBoundary P) = 0 ∧ H.betaArcBoundary (H.betaBoundary P) = 0

theorem TauCeti.HeegaardRegionSystem.mem_periodicDomains_iff_exists_curves {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {P : Region → ℤ} : P ∈ H.periodicDomains ↔ (∀ (z : Basepoint), P (H.basepoint z) = 0) ∧ (∃ (a : Fin n → ℤ), ∀ (p : Point), P (H.alphaLeft p) - P (H.alphaRight p) = a (H.alpha p)) ∧ ∃ (b : Fin n → ℤ), ∀ (p : Point), P (H.betaLeft p) - P (H.betaRight p) = b (H.beta p)

A domain is periodic exactly when it has multiplicity zero at every basepoint and its boundary is ∑ aᵢ αᵢ + ∑ bⱼ βⱼ for some integers aᵢ, bⱼ.

theorem TauCeti.HeegaardRegionSystem.isDomainBetween_self_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x : H.Generator} {P : Region → ℤ} : (IsDomainBetween x x P ∧ ∀ (z : Basepoint), P (H.basepoint z) = 0) ↔ P ∈ H.periodicDomains

A domain connects every generator to itself and avoids the basepoints exactly when it is periodic.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.sub_mem_periodicDomains_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {D D' : Region → ℤ} (hD : IsDomainBetween x y D) : D' - D ∈ H.periodicDomains ↔ IsDomainBetween x y D' ∧ ∀ (z : Basepoint), D' (H.basepoint z) = D (H.basepoint z)

Given a domain D connecting x to y, another domain D' connects x to y with the same basepoint multiplicities as D exactly when D' - D is periodic. So the domains connecting x to y with prescribed basepoint multiplicities form a coset of the periodic domains.

def TauCeti.HeegaardRegionSystem.WeaklyAdmissible {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : Prop

The supplied region incidence system is weakly admissible when every nonzero periodic domain has both positive and negative coefficients. Interpreting this for a geometric diagram requires identifying its actual complementary regions with Region.

Equations

• H.WeaklyAdmissible = ∀ P ∈ H.periodicDomains, P ≠ 0 → (∃ (r : Region), 0 < P r) ∧ ∃ (r : Region), P r < 0

theorem TauCeti.HeegaardRegionSystem.weaklyAdmissible_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} : H.WeaklyAdmissible ↔ ∀ P ∈ H.periodicDomains, 0 ≤ P → P = 0

A diagram is weakly admissible exactly when its only nonnegative periodic domain is zero.