Weak admissibility: area forms and finiteness of positive domains

Weak admissibility of a pointed Heegaard diagram (TauCeti.HeegaardRegionSystem.WeaklyAdmissible: every nonzero periodic domain has both positive and negative coefficients) is the hypothesis under which the differential of HF̂ is a finite sum. This file proves two domain-level consequences of it, in terms of the region incidence data of TauCeti.HeegaardRegionSystem.

• Area forms. A diagram is weakly admissible exactly when the regions can be given strictly positive areas for which every periodic domain has signed area zero. For such an area form, all domains connecting x to y with prescribed basepoint multiplicities have the same area.
• Finiteness. In a weakly admissible diagram with finitely many regions, only finitely many nonnegative domains connect x to y with prescribed basepoint multiplicities. Conversely, the diagram is weakly admissible exactly when it has only finitely many nonnegative periodic domains.

These are statements about domains only. Once the energy of a holomorphic disk is identified with the area of its domain, and its domain is known to be nonnegative (both analytic inputs not formalized here), they give the energy bound replacing monotonicity and the finiteness of the homotopy classes that can contribute to the HF̂ differential.

Main results

• TauCeti.HeegaardRegionSystem.weaklyAdmissible_iff_exists_pos_forall_sum_mul_eq_zero: weak admissibility is the existence of a strictly positive area form vanishing on periodic domains.
• TauCeti.HeegaardRegionSystem.IsDomainBetween.sum_mul_eq: for such an area form, the area of a domain connecting x to y depends only on its basepoint multiplicities.
• TauCeti.HeegaardRegionSystem.WeaklyAdmissible.finite_setOf_isDomainBetween_basepoint_eq_nonneg: finitely many nonnegative domains connect x to y with prescribed basepoint multiplicities.
• TauCeti.HeegaardRegionSystem.weaklyAdmissible_iff_finite_setOf_mem_periodicDomains_nonneg: weak admissibility is the finiteness of the set of nonnegative periodic domains.

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 (admissibility, its reformulation by area forms, and the resulting finiteness of positive domains).

theorem TauCeti.HeegaardRegionSystem.weaklyAdmissible_iff_exists_pos_forall_sum_mul_eq_zero {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Region] : H.WeaklyAdmissible ↔ ∃ (A : Region → ℝ), (∀ (r : Region), 0 < A r) ∧ ∀ P ∈ H.periodicDomains, ∑ r : Region, A r * ↑(P r) = 0

A diagram is weakly admissible exactly when its regions carry strictly positive areas A for which every periodic domain has signed area ∑ r, A r * P r equal to zero.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.sum_mul_eq {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Region] {A : Region → ℝ} (hA : ∀ P ∈ H.periodicDomains, ∑ r : Region, A r * ↑(P r) = 0) {x y : H.Generator} {D D' : Region → ℤ} (hD : IsDomainBetween x y D) (hD' : IsDomainBetween x y D') (hz : ∀ (z : Basepoint), D' (H.basepoint z) = D (H.basepoint z)) : ∑ r : Region, A r * ↑(D' r) = ∑ r : Region, A r * ↑(D r)

If an area form A vanishes on the periodic domains, then all domains connecting x to y with the same basepoint multiplicities have the same area.

theorem TauCeti.HeegaardRegionSystem.WeaklyAdmissible.finite_setOf_isDomainBetween_basepoint_eq_nonneg {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Finite Region] (hH : H.WeaklyAdmissible) (x y : H.Generator) (k : Basepoint → ℤ) : {D : Region → ℤ | IsDomainBetween x y D ∧ (∀ (z : Basepoint), D (H.basepoint z) = k z) ∧ 0 ≤ D}.Finite

In a weakly admissible diagram with finitely many regions, only finitely many nonnegative domains connect x to y with prescribed basepoint multiplicities k.

theorem TauCeti.HeegaardRegionSystem.weaklyAdmissible_iff_finite_setOf_mem_periodicDomains_nonneg {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} (H : HeegaardRegionSystem n Point Region Basepoint) : H.WeaklyAdmissible ↔ {P : Region → ℤ | P ∈ H.periodicDomains ∧ 0 ≤ P}.Finite

A diagram is weakly admissible exactly when it has only finitely many nonnegative periodic domains.