Documentation

TauCeti.LowDimTopology.Heegaard.HatDifferential

The combinatorial hat differential of a Heegaard diagram #

The hat chain group \widehat{CF} of a pointed Heegaard diagram is the 𝔽₂-vector space on its generators. Its differential sends a generator x to the sum over generators y of the number, modulo two, of holomorphic disks from x to y of Maslov index one avoiding the basepoints. The domain of such a disk is a nonnegative domain from x to y with multiplicity zero at every basepoint and Maslov index one. Sarkar and Wang show that in a genuine nice Heegaard diagram, one on a surface in which every region containing no basepoint is an embedded disk with two or four corners, every such domain is an empty embedded bigon or an empty embedded rectangle, and each of those is the domain of exactly one holomorphic disk modulo translation. So in a genuine nice diagram the differential counts these domains themselves, which is the combinatorial chain complex of Sarkar–Wang and OzsvΓ‘th–Stipsicz–SzabΓ³.

This file defines that count for the abstract region incidence data TauCeti.HeegaardRegionSystem with region Euler characteristics Ο‡. The counted domains from x to y form the set H.hatDomains Ο‡ x y. It is finite when the diagram is weakly admissible, or merely weakly admissible at y, and the matrix coefficient H.hatCoefficient Ο‡ x y is its cardinality modulo two. The linear map H.hatDifferential Ο‡ on H.Generator β†’β‚€ ZMod 2 has these coefficients. The abstract condition TauCeti.HeegaardRegionSystem.IsNice only records that every region containing no basepoint has Euler characteristic one and two or four corners; it does not say that H and Ο‡ come from regions of an actual surface. The agreement of this count with the holomorphic differential therefore applies only to incidence data realized by a genuine nice Heegaard diagram with these region Euler characteristics, and neither that realization nor the agreement is formalized here. Otherwise the count of domains need not be the count of holomorphic disks. In a diagram that is not weakly admissible at y the set can be infinite, in which case the coefficient is 0 by the convention of Set.ncard; the results below carry the combinatorial hypotheses under which the count is finite and has the properties listed next. That the differential squares to zero on nice diagrams is not proved here.

The basic properties of the count are the following. In a weakly admissible diagram nothing is counted from a generator to itself, since a nonnegative periodic domain vanishes. Without nonzero periodic domains at most one domain is counted between two generators, so each coefficient is 1 exactly when a counted domain exists. In a nice weakly admissible diagram a counted domain changes the points of x on exactly one or two Ξ±-curves, as a bigon or a rectangle does. In a singly pointed diagram the differential lowers the relative grading by one, modulo the Maslov indices of the periodic domains, and on the nose when those vanish.

Main definitions #

Main results #

References #

source
def TauCeti.HeegaardRegionSystem.hatDomains {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) :
Set (Region β†’ β„€)

The domains counted by the hat differential from the generator x to the generator y: the nonnegative domains from x to y with multiplicity zero at every basepoint and Maslov index one, for the region Euler characteristics Ο‡.

Instances For
    source
    @[simp]
    theorem TauCeti.HeegaardRegionSystem.mem_hatDomains_iff {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 β†’ β„€} :
    D ∈ H.hatDomains Ο‡ x y ↔ IsDomainBetween x y D ∧ (βˆ€ (z : Basepoint), D (H.basepoint z) = 0) ∧ 0 ≀ D ∧ (H.maslovIndex Ο‡ x y) D = 1
    source
    theorem TauCeti.HeegaardRegionSystem.WeaklyAdmissibleAt.finite_hatDomains {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] {Ο‡ : Region β†’ β„€} {y : H.Generator} (hW : H.WeaklyAdmissibleAt Ο‡ y) (x : H.Generator) :
    (H.hatDomains Ο‡ x y).Finite

    In a diagram weakly admissible at y only finitely many domains are counted by the hat differential from any generator to y.

    source
    theorem TauCeti.HeegaardRegionSystem.WeaklyAdmissible.finite_hatDomains {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] (hW : H.WeaklyAdmissible) (Ο‡ : Region β†’ β„€) (x y : H.Generator) :
    (H.hatDomains Ο‡ x y).Finite

    In a weakly admissible diagram only finitely many domains are counted by the hat differential between two generators.

    source
    @[simp]
    theorem TauCeti.HeegaardRegionSystem.WeaklyAdmissible.hatDomains_self {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] (hW : H.WeaklyAdmissible) (Ο‡ : Region β†’ β„€) (x : H.Generator) :
    H.hatDomains Ο‡ x x = βˆ…

    In a weakly admissible diagram no domain is counted by the hat differential from a generator to itself: such a domain is a nonnegative periodic domain, hence zero, and the zero domain has Maslov index zero.

    source
    theorem TauCeti.HeegaardRegionSystem.subsingleton_hatDomains_of_periodicDomains_eq_bot {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] (hP : H.periodicDomains = βŠ₯) (Ο‡ : Region β†’ β„€) (x y : H.Generator) :
    (H.hatDomains Ο‡ x y).Subsingleton

    In a diagram without nonzero periodic domains at most one domain is counted by the hat differential between two generators: two of them differ by a periodic domain.

    source
    noncomputable def TauCeti.HeegaardRegionSystem.hatCoefficient {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) :
    ZMod 2

    The coefficient of the generator y in the hat differential of the generator x: the number, modulo two, of nonnegative domains of Maslov index one from x to y avoiding the basepoints. This is meaningful when the set H.hatDomains Ο‡ x y of these domains is finite, for instance in a weakly admissible diagram (WeaklyAdmissible.finite_hatDomains); for an infinite set the coefficient is 0.

    Instances For
      source
      theorem TauCeti.HeegaardRegionSystem.hatCoefficient_def {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} :
      H.hatCoefficient Ο‡ x y = ↑(H.hatDomains Ο‡ x y).ncard
      source
      theorem TauCeti.HeegaardRegionSystem.hatCoefficient_eq_zero_of_hatDomains_eq_empty {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} (h : H.hatDomains Ο‡ x y = βˆ…) :
      H.hatCoefficient Ο‡ x y = 0

      The hat differential has coefficient zero from x to y when no domain from x to y is counted.

      source
      theorem TauCeti.HeegaardRegionSystem.nonempty_hatDomains_of_hatCoefficient_ne_zero {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} (h : H.hatCoefficient Ο‡ x y β‰  0) :
      (H.hatDomains Ο‡ x y).Nonempty

      A nonzero coefficient of the hat differential from x to y comes from a counted domain from x to y.

      source
      @[simp]
      theorem TauCeti.HeegaardRegionSystem.WeaklyAdmissible.hatCoefficient_self {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] (hW : H.WeaklyAdmissible) (Ο‡ : Region β†’ β„€) (x : H.Generator) :
      H.hatCoefficient Ο‡ x x = 0

      In a weakly admissible diagram the hat differential has no diagonal terms.

      source
      theorem TauCeti.HeegaardRegionSystem.hatCoefficient_eq_one_iff_of_periodicDomains_eq_bot {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} (hP : H.periodicDomains = βŠ₯) :
      H.hatCoefficient Ο‡ x y = 1 ↔ (H.hatDomains Ο‡ x y).Nonempty

      In a diagram without nonzero periodic domains, the hat differential has coefficient one from x to y exactly when some domain from x to y is counted.

      source
      theorem TauCeti.HeegaardRegionSystem.IsNice.hammingDist_eq_one_or_eq_two_of_hatCoefficient_ne_zero {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} [DecidableEq Point] (h : H.IsNice Ο‡) (hW : H.WeaklyAdmissible) (hc : H.hatCoefficient Ο‡ x y β‰  0) :
      hammingDist (H.point x) (H.point y) = 1 ∨ hammingDist (H.point x) (H.point y) = 2

      In a nice weakly admissible diagram, the hat differential only joins generators whose points differ on exactly one Ξ±-curve, as across a bigon, or on exactly two, as across a rectangle.

      source
      theorem TauCeti.HeegaardRegionSystem.relativeGrading_eq_one_of_hatCoefficient_ne_zero {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} [Subsingleton Basepoint] (z : Basepoint) (hΟ‡ : βˆ‘ r : Region, Ο‡ r - ↑(Fintype.card Point) = 2 - 2 * ↑n) (hP : βˆ€ P ∈ H.periodicDomains, (H.maslovIndex Ο‡ x x) P = 0) (hc : H.hatCoefficient Ο‡ x y β‰  0) :
      H.relativeGrading Ο‡ z x y = 1

      In a singly pointed diagram of a closed surface of genus n whose periodic domains have Maslov index zero at x, the hat differential lowers the relative Maslov grading by one: a nonzero coefficient from x to y forces gr(x, y) = 1.

      source
      theorem TauCeti.HeegaardRegionSystem.coe_relativeGrading_eq_one_of_hatCoefficient_ne_zero {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} [Subsingleton Basepoint] (z : Basepoint) (hΟ‡ : βˆ‘ r : Region, Ο‡ r - ↑(Fintype.card Point) = 2 - 2 * ↑n) (hc : H.hatCoefficient Ο‡ x y β‰  0) :
      ↑(H.relativeGrading Ο‡ z x y) = ↑1

      In a singly pointed diagram of a closed surface of genus n, the hat differential lowers the relative Maslov grading by one modulo the periodic Maslov indices at x: a nonzero coefficient from x to y forces gr(x, y) = 1 there.

      source
      noncomputable def TauCeti.HeegaardRegionSystem.hatDifferential {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) [Fintype Point] [DecidableEq Region] [Fintype Region] (Ο‡ : Region β†’ β„€) :
      (H.Generator β†’β‚€ ZMod 2) β†’β‚—[ZMod 2] H.Generator β†’β‚€ ZMod 2

      The hat differential of a Heegaard diagram with region Euler characteristics Ο‡: the ZMod 2-linear endomorphism of the free module on generators whose coefficient from x to y is the number, modulo two, of nonnegative domains of Maslov index one from x to y avoiding the basepoints (TauCeti.HeegaardRegionSystem.hatCoefficient).

      Instances For
        source
        @[simp]
        theorem TauCeti.HeegaardRegionSystem.hatDifferential_single_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) (a : ZMod 2) :
        ((H.hatDifferential Ο‡) (Finsupp.single x a)) y = a * H.hatCoefficient Ο‡ x y

        The matrix coefficients of the hat differential are the counts TauCeti.HeegaardRegionSystem.hatCoefficient.

        source
        theorem TauCeti.HeegaardRegionSystem.hatDifferential_apply {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] {Ο‡ : Region β†’ β„€} (c : H.Generator β†’β‚€ ZMod 2) (y : H.Generator) :
        ((H.hatDifferential Ο‡) c) y = c.sum fun (x : H.Generator) (a : ZMod 2) => a * H.hatCoefficient Ο‡ x y

        The coefficient of y in the hat differential of a chain c.

        source
        theorem TauCeti.HeegaardRegionSystem.hatDifferential_eq_zero_iff {n : β„•} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} [Fintype Point] [DecidableEq Region] [Fintype Region] {Ο‡ : Region β†’ β„€} :
        H.hatDifferential Ο‡ = 0 ↔ βˆ€ (x y : H.Generator), H.hatCoefficient Ο‡ x y = 0

        The hat differential vanishes exactly when all of its coefficients vanish.