Documentation

TauCeti.LowDimTopology.Heegaard.StrongAdmissibility

Strong admissibility #

Strong admissibility restricts periodic domains using the Maslov index of a chosen generator. For a nonzero periodic domain of nonnegative index 2m, some region must have multiplicity greater than m. We use the rational half-index because the abstract region system accepts an arbitrary Euler-characteristic function; on a geometric Heegaard diagram this is the usual integer-valued condition. In particular, an index-zero periodic domain has both positive and negative coefficients, so strong admissibility at x implies weak admissibility at x (TauCeti.HeegaardRegionSystem.WeaklyAdmissibleAt).

Through weak admissibility at the terminal generator y, this makes nonnegative domains from x to y with fixed basepoint multiplicities and fixed Maslov index finite (HeegaardRegionSystem.WeaklyAdmissibleAt.finite_setOf_isDomainBetween_basepoint_eq_nonneg_index). In a singly pointed diagram of a closed surface, strong admissibility at y gives more: the nonnegative domains from x to y with fixed Maslov index are finite whatever their basepoint multiplicity. A domain from y to itself is a periodic domain plus n_z copies of the whole surface Σ, which has Maslov index two, so strong admissibility at y is the statement that no nonzero nonnegative domain from y to itself has Maslov index zero, and Dickson's lemma turns this into finiteness. This is the finiteness needed for differentials that count holomorphic disks of every basepoint multiplicity, recording n_z as a power of a formal variable U.

Main definitions #

Main results #

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: Definition 4.10 (strong admissibility for a spin^c structure) and Lemmas 4.13–4.14 (finiteness of nonnegative classes in admissible diagrams).

source
def TauCeti.HeegaardRegionSystem.StronglyAdmissible {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [Fintype Region] [DecidableEq Region] (χ : Region → ℤ) (x : H.Generator) :
Prop

Strong admissibility at a generator x: every nonzero periodic domain P of nonnegative Maslov index has a coefficient strictly greater than half its index. The Euler characteristics of the regions are supplied by χ.

Instances For
    source
    theorem TauCeti.HeegaardRegionSystem.stronglyAdmissible_iff {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [Fintype Region] [DecidableEq Region] {χ : Region → ℤ} {x : H.Generator} :
    H.StronglyAdmissible χ x ↔ ∀ P ∈ H.periodicDomains, P ≠ 0 → 0 ≤ (H.maslovIndex χ x x) P → ∃ (r : Region), (H.maslovIndex χ x x) P / 2 < ↑(P r)

    Strong admissibility at x means every nonzero periodic domain of nonnegative Maslov index has a coefficient strictly greater than half its index.

    source
    theorem TauCeti.HeegaardRegionSystem.stronglyAdmissible_iff_of_isDomainBetween {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [Fintype Region] [DecidableEq Region] {χ : Region → ℤ} {x y : H.Generator} {D : Region → ℤ} (hD : IsDomainBetween x y D) :
    H.StronglyAdmissible χ x ↔ H.StronglyAdmissible χ y

    Strong admissibility has the same value at generators joined by a domain: the Maslov index of a periodic domain is independent of the generator within that class.

    source
    theorem TauCeti.HeegaardRegionSystem.StronglyAdmissible.weaklyAdmissibleAt {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [Fintype Region] [DecidableEq Region] {χ : Region → ℤ} {x : H.Generator} (hH : H.StronglyAdmissible χ x) :
    H.WeaklyAdmissibleAt χ x

    A strongly admissible diagram at x is weakly admissible at x: an index-zero periodic domain P must have a coefficient greater than zero, and so must -P.

    source
    theorem TauCeti.HeegaardRegionSystem.StronglyAdmissible.eq_zero_of_isDomainBetween_self {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [Fintype Region] [DecidableEq Region] {χ : Region → ℤ} {y : H.Generator} {E : Region → ℤ} [Subsingleton Basepoint] (hχ : ∑ r : Region, χ r - ↑(Fintype.card Point) = 2 - 2 * ↑n) (hH : H.StronglyAdmissible χ y) (hE : IsDomainBetween y y E) (hE₀ : 0 ≤ E) (hμ : (H.maslovIndex χ y y) E = 0) :
    E = 0

    In a singly pointed diagram of a closed surface of genus n that is strongly admissible at y, the only nonnegative domain from y to itself of Maslov index zero is zero. Unlike weak admissibility at y, which only excludes such domains with multiplicity zero at the basepoint, this excludes them for every basepoint multiplicity.

    source
    theorem TauCeti.HeegaardRegionSystem.stronglyAdmissible_iff_forall_isDomainBetween_self {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [Fintype Region] [DecidableEq Region] {χ : Region → ℤ} {y : H.Generator} [Subsingleton Basepoint] (hχ : ∑ r : Region, χ r - ↑(Fintype.card Point) = 2 - 2 * ↑n) [Nonempty Basepoint] :
    H.StronglyAdmissible χ y ↔ ∀ (E : Region → ℤ), IsDomainBetween y y E → 0 ≤ E → (H.maslovIndex χ y y) E = 0 → E = 0

    A singly pointed diagram of a closed surface of genus n is strongly admissible at y exactly when its only nonnegative domain from y to itself of Maslov index zero is zero. If a nonzero periodic domain P of index 2m ≥ 0 has every coefficient at most m, then a multiple of m Σ - P is a nonzero nonnegative domain of index zero from y to itself.

    source
    theorem TauCeti.HeegaardRegionSystem.StronglyAdmissible.finite_setOf_isDomainBetween_nonneg_index {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [Fintype Region] [DecidableEq Region] {χ : Region → ℤ} {y : H.Generator} [Subsingleton Basepoint] (hχ : ∑ r : Region, χ r - ↑(Fintype.card Point) = 2 - 2 * ↑n) (hH : H.StronglyAdmissible χ y) (x : H.Generator) (m : ℚ) :
    {D : Region → ℤ | IsDomainBetween x y D ∧ 0 ≤ D ∧ (H.maslovIndex χ x y) D = m}.Finite

    In a singly pointed diagram of a closed surface of genus n that is strongly admissible at y, only finitely many nonnegative domains connect x to y with prescribed Maslov index m. Their basepoint multiplicities are not prescribed, in contrast to the finiteness given by weak admissibility at y (WeaklyAdmissibleAt.finite_setOf_isDomainBetween_basepoint_eq_nonneg_index); this is the finiteness behind differentials that record every basepoint multiplicity by a power of a formal variable.

    source
    theorem TauCeti.HeegaardRegionSystem.stronglyAdmissible_iff_forall_finite {n : ℕ} {Point : Type u_1} {Region : Type u_2} {Basepoint : Type u_3} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [Fintype Region] [DecidableEq Region] {χ : Region → ℤ} {y : H.Generator} [Subsingleton Basepoint] (hχ : ∑ r : Region, χ r - ↑(Fintype.card Point) = 2 - 2 * ↑n) [Nonempty Basepoint] :
    H.StronglyAdmissible χ y ↔ ∀ (x : H.Generator) (m : ℚ), {D : Region → ℤ | IsDomainBetween x y D ∧ 0 ≤ D ∧ (H.maslovIndex χ x y) D = m}.Finite

    A singly pointed diagram of a closed surface of genus n is strongly admissible at y exactly when, for every generator x and Maslov index m, only finitely many nonnegative domains connect x to y with this Maslov index. Without strong admissibility at y, the multiples of a nonzero nonnegative domain of index zero from y to itself are infinitely many such domains.