The combinatorial Maslov index of a domain

Lipshitz's index formula computes the expected dimension of the moduli space of holomorphic disks in a Whitney class φ from its domain D alone: μ(φ) = e(D) + n_x(D) + n_y(D). This file defines the right-hand side for the abstract region incidence data TauCeti.HeegaardRegionSystem and proves that it is additive under juxtaposition of domains, a property needed for a relative grading once independence of the choice of domain is established.

Every intersection point p is a corner of four regions (with repetition): the regions on the two sides of the α-arc ending at p and of the α-arc starting at p. The point measure n_p(D) is the average of the multiplicities of D at these four corners, and for a generator x = {x₁, …, xₙ} one puts n_x(D) = ∑ n_{xᵢ}(D). With the standard combinatorial convention that every corner contributes one quarter, the Euler measure of a region R with k corners is χ(R) - k / 4; it is extended linearly to domains. The Euler characteristics χ(R) of the regions are not determined by the incidence data, so they are an explicit argument.

The key combinatorial fact is that for a domain D from x to y and a domain E from y to w, n_x(E) + n_w(D) = n_y(D) + n_y(E). Both sides differ by a corner-averaged intersection number of ∂D ∩ α with ∂E ∩ β, computed once along the α-curves and once along the β-curves, and the two computations agree up to sign at every crossing.

Main definitions

• TauCeti.HeegaardRegionSystem.cornerRegion: the four regions with a corner at a point.
• TauCeti.HeegaardRegionSystem.pointMeasure: the point measure n_p(D).
• TauCeti.HeegaardRegionSystem.generatorPointMeasure: the point measure n_x(D) of a generator.
• TauCeti.HeegaardRegionSystem.cornerCount: the number of corners of a region.
• TauCeti.HeegaardRegionSystem.eulerMeasure: the Euler measure e(D).
• TauCeti.HeegaardRegionSystem.maslovIndex: the combinatorial Maslov index e(D) + n_x(D) + n_y(D).

Main results

• TauCeti.HeegaardRegionSystem.pointMeasure_apply_beta: the point measure is also the average over the corners on the two sides of the β-arcs.
• TauCeti.HeegaardRegionSystem.eulerMeasure_eq_sub_sum_pointMeasure: the Euler measure is ∑ χ(R) D(R) - ∑ₚ n_p(D).
• TauCeti.HeegaardRegionSystem.IsDomainBetween.generatorPointMeasure_add_generatorPointMeasure: n_x(E) + n_w(D) = n_y(D) + n_y(E) for D from x to y and E from y to w.
• TauCeti.HeegaardRegionSystem.IsDomainBetween.maslovIndex_add: the Maslov index is additive under juxtaposition.
• TauCeti.HeegaardRegionSystem.IsDomainBetween.maslovIndex_self_eq: a domain whose boundary is a sum of whole curves has the same Maslov index at any two generators joined by a domain.

References

• R. Lipshitz, A cylindrical reformulation of Heegaard Floer homology, Geom. Topol. 10 (2006), arXiv:math/0502404, §4, where the index formula and its additivity are proved; see also the erratum arXiv:1301.4919.
• S. Sarkar, Maslov index formulas for Whitney n-gons, J. Topol. 4 (2011), arXiv:math/0609673, for the combinatorial proof of the additivity of point measures.

def TauCeti.HeegaardRegionSystem.cornerRegion {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (p : Point) : Fin 4 → Region

The four regions with a corner at the intersection point p, with repetition: the regions to the left and to the right of the α-arc ending at p, then those of the α-arc starting at p.

Equations

• H.cornerRegion p = ![H.alphaLeft ((Equiv.symm H.alphaNext) p), H.alphaRight ((Equiv.symm H.alphaNext) p), H.alphaLeft p, H.alphaRight p]

theorem TauCeti.HeegaardRegionSystem.cornerRegion_eq {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (p : Point) : H.cornerRegion p = ![H.alphaLeft ((Equiv.symm H.alphaNext) p), H.alphaRight ((Equiv.symm H.alphaNext) p), H.alphaLeft p, H.alphaRight p]

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

The point measure n_p(D): the average multiplicity of the domain D at the four corners at the intersection point p.

Equations

• H.pointMeasure = { toFun := fun (D : Region → ℤ) (p : Point) => (∑ i : Fin 4, ↑(D (H.cornerRegion p i))) / 4, map_zero' := ⋯, map_add' := ⋯ }

theorem TauCeti.HeegaardRegionSystem.pointMeasure_apply_eq_sum {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) (p : Point) : H.pointMeasure D p = (∑ i : Fin 4, ↑(D (H.cornerRegion p i))) / 4

@[simp]

theorem TauCeti.HeegaardRegionSystem.pointMeasure_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) (p : Point) : H.pointMeasure D p = (↑(D (H.alphaLeft ((Equiv.symm H.alphaNext) p))) + ↑(D (H.alphaRight ((Equiv.symm H.alphaNext) p))) + ↑(D (H.alphaLeft p)) + ↑(D (H.alphaRight p))) / 4

theorem TauCeti.HeegaardRegionSystem.pointMeasure_apply_beta {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) (p : Point) : H.pointMeasure D p = (↑(D (H.betaLeft ((Equiv.symm H.betaNext) p))) + ↑(D (H.betaRight ((Equiv.symm H.betaNext) p))) + ↑(D (H.betaLeft p)) + ↑(D (H.betaRight p))) / 4

The four corners at a crossing are also the regions on the two sides of the β-arc ending there and of the β-arc starting there, so the point measure can be read off along β.

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

The point measure n_x(D) = ∑ᵢ n_{xᵢ}(D) of a domain D at a generator x.

Equations

• H.generatorPointMeasure x = { toFun := fun (D : Region → ℤ) => ∑ i : Fin n, H.pointMeasure D (H.point x i), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.HeegaardRegionSystem.generatorPointMeasure_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (x : H.Generator) (D : Region → ℤ) : (H.generatorPointMeasure x) D = ∑ i : Fin n, H.pointMeasure D (H.point x i)

theorem TauCeti.HeegaardRegionSystem.generatorPointMeasure_eq_sum_generatorChain {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] (x : H.Generator) (D : Region → ℤ) : (H.generatorPointMeasure x) D = ∑ q : Point, ↑(H.generatorChain x q) * H.pointMeasure D q

The point measure of a generator is the pairing of its 0-chain with the point measures.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.generatorPointMeasure_add_generatorPointMeasure {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) : (H.generatorPointMeasure x) E + (H.generatorPointMeasure w) D = (H.generatorPointMeasure y) D + (H.generatorPointMeasure y) E

The point measures of two juxtaposable domains satisfy n_x(E) + n_w(D) = n_y(D) + n_y(E) when D connects x to y and E connects y to w.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.generatorPointMeasure_eq {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {D P : Region → ℤ} (hD : IsDomainBetween x y D) (hP : IsDomainBetween y y P) : (H.generatorPointMeasure x) P = (H.generatorPointMeasure y) P

A domain whose boundary is a sum of whole curves has the same point measure at any two generators joined by a domain.

def TauCeti.HeegaardRegionSystem.cornerCount {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] (r : Region) : ℕ

The number of corners of the region r, counted with multiplicity over the four corners at every intersection point.

Equations

• H.cornerCount r = {c : Point × Fin 4 | H.cornerRegion c.1 c.2 = r}.card

theorem TauCeti.HeegaardRegionSystem.cornerCount_eq_card {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] (r : Region) : H.cornerCount r = {c : Point × Fin 4 | H.cornerRegion c.1 c.2 = r}.card

def TauCeti.HeegaardRegionSystem.eulerMeasure {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (χ : Region → ℤ) : (Region → ℤ) →+ ℚ

The Euler measure e(D) = ∑ D(R) (χ(R) - k(R) / 4) of a domain, where χ(R) is the Euler characteristic of the region R, supplied as χ, and k(R) is its number of corners.

Equations

• H.eulerMeasure χ = { toFun := fun (D : Region → ℤ) => ∑ r : Region, ↑(D r) * (↑(χ r) - ↑(H.cornerCount r) / 4), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.HeegaardRegionSystem.eulerMeasure_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (χ D : Region → ℤ) : (H.eulerMeasure χ) D = ∑ r : Region, ↑(D r) * (↑(χ r) - ↑(H.cornerCount r) / 4)

theorem TauCeti.HeegaardRegionSystem.eulerMeasure_single {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (χ : Region → ℤ) (r : Region) : (H.eulerMeasure χ) (Pi.single r 1) = ↑(χ r) - ↑(H.cornerCount r) / 4

The Euler measure of a single region R is χ(R) - k(R) / 4.

theorem TauCeti.HeegaardRegionSystem.eulerMeasure_eq_sub_sum_pointMeasure {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (χ D : Region → ℤ) : (H.eulerMeasure χ) D = ∑ r : Region, ↑(χ r) * ↑(D r) - ∑ p : Point, H.pointMeasure D p

Each corner contributes a quarter of the multiplicity at its region to the point measure at its vertex, so the Euler measure is ∑ χ(R) D(R) - ∑ₚ n_p(D).

def TauCeti.HeegaardRegionSystem.maslovIndex {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (χ : Region → ℤ) (x y : H.Generator) : (Region → ℤ) →+ ℚ

The combinatorial Maslov index μ(D) = e(D) + n_x(D) + n_y(D) of a domain D from the generator x to the generator y, for the Euler characteristics χ of the regions.

Equations

• H.maslovIndex χ x y = H.eulerMeasure χ + H.generatorPointMeasure x + H.generatorPointMeasure y

@[simp]

theorem TauCeti.HeegaardRegionSystem.maslovIndex_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (χ : Region → ℤ) (x y : H.Generator) (D : Region → ℤ) : (H.maslovIndex χ x y) D = (H.eulerMeasure χ) D + (H.generatorPointMeasure x) D + (H.generatorPointMeasure y) D

theorem TauCeti.HeegaardRegionSystem.maslovIndex_neg {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (χ : Region → ℤ) (x y : H.Generator) (D : Region → ℤ) : (H.maslovIndex χ y x) (-D) = -(H.maslovIndex χ x y) D

Reversing a domain negates its Maslov index.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.maslovIndex_add {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] {x y w : H.Generator} {D E : Region → ℤ} (χ : Region → ℤ) (hD : IsDomainBetween x y D) (hE : IsDomainBetween y w E) : (H.maslovIndex χ x w) (D + E) = (H.maslovIndex χ x y) D + (H.maslovIndex χ y w) E

The Maslov index is additive under juxtaposition of domains: if D connects x to y and E connects y to w, then μ(D + E) = μ(D) + μ(E).

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.maslovIndex_self_eq {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] {x y : H.Generator} {D : Region → ℤ} (χ : Region → ℤ) {P : Region → ℤ} (hD : IsDomainBetween x y D) (hP : IsDomainBetween y y P) : (H.maslovIndex χ x x) P = (H.maslovIndex χ y y) P

A domain whose boundary is a sum of whole curves has the same Maslov index at any two generators joined by a domain.