Generators from finite Heegaard intersection data

The generators of a pointed Heegaard diagram choose one intersection point on each α-curve and each β-curve. This file records incidence data by assigning each intersection point its α- and β-curve labels. A generator is the matching datum in the domain of TauCeti.Sym.matchingTuple, specialized through TauCeti.Sym.piInterEquiv to the two label fibers: a permutation of the curve indices and an intersection point in each paired fiber.

The curve count n is independent of surface genus. For a multi-pointed diagram of genus g with k basepoints on each side, the usual curve count is g + k - 1; this file records only that count and the incidence data. Abstract region incidence data, basepoints, domains, and admissibility are recorded on top of it in TauCeti.LowDimTopology.Heegaard.Domain; they are needed to define the differential.

Main definitions

• TauCeti.HeegaardIntersectionSystem: finite intersection data with two curve labels.
• TauCeti.HeegaardIntersectionSystem.Generator: a permutation of the curve indices together with one intersection point in each paired α- and β-label fiber.
• TauCeti.HeegaardIntersectionSystem.generatorEquivPiInter: the identification with common points of the two symmetric products.
• TauCeti.HeegaardIntersectionSystem.generator_card: the permanent count of generators.
• TauCeti.HeegaardIntersectionSystem.generatorOf: the low-level constructor from a chosen permutation and point choice.
• TauCeti.HeegaardIntersectionSystem.generatorOfPointChoice: the point-choice constructor from bijective β-labels.
• TauCeti.HeegaardIntersectionSystem.point and TauCeti.HeegaardIntersectionSystem.betaEquiv: accessors for the chosen point and its curve matching; a generator is determined by its chosen points (TauCeti.HeegaardIntersectionSystem.point_injective).
• TauCeti.HeegaardIntersectionSystem.generatorChain: the 0-chain of the points of a generator.

References

The generator convention is the one used in P. Ozsváth and Z. Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Ann. of Math. 159 (2004), arXiv:math/0101206, §2.1.

structure TauCeti.HeegaardIntersectionSystem (n : ℕ) (Point : Type u) : Type u

Finite intersection data for two equally sized curve systems. The finite enumeration records the point set, and each point has one α-curve label and one β-curve label; geometric surface and region data are additional structure.

• pointFintype : Fintype Point

  A finite enumeration of the intersection points.

• alpha : Point → Fin n

  The α-curve containing an intersection point.

• beta : Point → Fin n

  The β-curve containing an intersection point.

theorem TauCeti.HeegaardIntersectionSystem.ext_iff {n : ℕ} {Point : Type u} {x y : HeegaardIntersectionSystem n Point} : x = y ↔ x.pointFintype = y.pointFintype ∧ x.alpha = y.alpha ∧ x.beta = y.beta

theorem TauCeti.HeegaardIntersectionSystem.ext {n : ℕ} {Point : Type u} {x y : HeegaardIntersectionSystem n Point} (pointFintype : x.pointFintype = y.pointFintype) (alpha : x.alpha = y.alpha) (beta : x.beta = y.beta) : x = y

@[reducible, inline]

abbrev TauCeti.HeegaardIntersectionSystem.Generator {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) : Type u

The generators of D as matchings between the fibers of its α- and β-labels.

Equations

• D.Generator = ((σ : Equiv.Perm (Fin n)) × ((i : Fin n) → ↑({p : Point | D.alpha p = i} ∩ {p : Point | D.beta p = σ i})))

@[instance_reducible]

instance TauCeti.HeegaardIntersectionSystem.instFintypeGenerator {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) : Fintype D.Generator

The generators are finite because the intersection point type has a finite enumeration.

Equations

• D.instFintypeGenerator = inferInstance

noncomputable def TauCeti.HeegaardIntersectionSystem.generatorEquivPiInter {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) : D.Generator ≃ ↑((Sym.pi fun (i : Fin n) => {p : Point | D.alpha p = i}) ∩ Sym.pi fun (j : Fin n) => {p : Point | D.beta p = j})

The generators are the common points of the symmetric products of the α- and β-label fibers.

Equations

• D.generatorEquivPiInter = TauCeti.Sym.piInterEquiv ⋯ ⋯

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.generatorEquivPiInter_apply {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) : D.generatorEquivPiInter g = Sym.matchingTuple g

The generator equivalence sends a matching to its unordered tuple of intersection points.

theorem TauCeti.HeegaardIntersectionSystem.generator_card {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) : Fintype.card D.Generator = (Matrix.of fun (i j : Fin n) => Nat.card { p : Point // D.alpha p = i ∧ D.beta p = j }).permanent

The number of generators is the permanent of the matrix of labeled intersection counts.

def TauCeti.HeegaardIntersectionSystem.generatorOf {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (σ : Equiv.Perm (Fin n)) (p : Fin n → Point) (hα : ∀ (i : Fin n), D.alpha (p i) = i) (hβ : ∀ (i : Fin n), D.beta (p i) = σ i) : D.Generator

Construct a generator from a point choice and its two curve-label conditions.

Equations

• D.generatorOf σ p hα hβ = ⟨σ, fun (i : Fin n) => ⟨p i, ⋯⟩⟩

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.generatorOf_fst {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (σ : Equiv.Perm (Fin n)) (p : Fin n → Point) (hα : ∀ (i : Fin n), D.alpha (p i) = i) (hβ : ∀ (i : Fin n), D.beta (p i) = σ i) : (D.generatorOf σ p hα hβ).fst = σ

The curve-index permutation stored by generatorOf.

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.generatorOf_val {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (σ : Equiv.Perm (Fin n)) (p : Fin n → Point) (hα : ∀ (i : Fin n), D.alpha (p i) = i) (hβ : ∀ (i : Fin n), D.beta (p i) = σ i) (i : Fin n) : ↑((D.generatorOf σ p hα hβ).snd i) = p i

The point stored by generatorOf at index i.

noncomputable def TauCeti.HeegaardIntersectionSystem.generatorOfPointChoice {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (p : Fin n → Point) (hα : ∀ (i : Fin n), D.alpha (p i) = i) (hβ : Function.Bijective (D.beta ∘ p)) : D.Generator

Construct a generator from a point choice whose β-labels are bijective.

Equations

• D.generatorOfPointChoice p hα hβ = ⟨Equiv.ofBijective (D.beta ∘ p) hβ, fun (i : Fin n) => ⟨p i, ⋯⟩⟩

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.generatorOfPointChoice_fst {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (p : Fin n → Point) (hα : ∀ (i : Fin n), D.alpha (p i) = i) (hβ : Function.Bijective (D.beta ∘ p)) : (D.generatorOfPointChoice p hα hβ).fst = Equiv.ofBijective (D.beta ∘ p) hβ

The curve-index matching stored by generatorOfPointChoice.

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.generatorOfPointChoice_val {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (p : Fin n → Point) (hα : ∀ (i : Fin n), D.alpha (p i) = i) (hβ : Function.Bijective (D.beta ∘ p)) (i : Fin n) : ↑((D.generatorOfPointChoice p hα hβ).snd i) = p i

The point stored by generatorOfPointChoice at index i.

def TauCeti.HeegaardIntersectionSystem.point {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) (i : Fin n) : Point

The chosen point over i.

Equations

• D.point g i = ↑(g.snd i)

def TauCeti.HeegaardIntersectionSystem.betaEquiv {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) : Equiv.Perm (Fin n)

The curve-index matching stored by a generator.

Equations

• D.betaEquiv g = g.fst

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.point_apply {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) (i : Fin n) : D.point g i = ↑(g.snd i)

The chosen-point accessor is the second projection of a matching.

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.betaEquiv_apply {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) (i : Fin n) : (D.betaEquiv g) i = D.beta (D.point g i)

The matching index is the β-label of the chosen point.

theorem TauCeti.HeegaardIntersectionSystem.point_injective {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) : Function.Injective D.point

A generator is determined by its chosen points: their β-labels recover the matching.

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.alpha_coe {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) (i : Fin n) : D.alpha ↑(g.snd i) = i

The chosen point over i has α-label i.

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.beta_coe {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) (i : Fin n) : D.beta ↑(g.snd i) = g.fst i

The chosen point over i has β-label given by the matching permutation.

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.exists_point_iff {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) (q : Point) : (∃ (i : Fin n), ↑(g.snd i) = q) ↔ D.point g (D.alpha q) = q

An intersection point occurs in a generator exactly when it is the generator's point on its own α-curve.

noncomputable def TauCeti.HeegaardIntersectionSystem.generatorChain {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) (g : D.Generator) : Point → ℤ

The 0-chain of a generator: the indicator function of its intersection points.

Equations

• D.generatorChain g = (Set.range (D.point g)).indicator 1

@[simp]

theorem TauCeti.HeegaardIntersectionSystem.generatorChain_apply {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) [DecidableEq Point] (g : D.Generator) (q : Point) : D.generatorChain g q = if D.point g (D.alpha q) = q then 1 else 0

theorem TauCeti.HeegaardIntersectionSystem.generatorChain_eq_sum_single {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) [DecidableEq Point] (g : D.Generator) : D.generatorChain g = ∑ i : Fin n, Pi.single (D.point g i) 1

The 0-chain of a generator is the sum of the unit chains at its intersection points.

theorem TauCeti.HeegaardIntersectionSystem.sum_generatorChain_smul {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) [Fintype Point] {M : Type u_1} [AddCommGroup M] (g : D.Generator) (f : Point → M) : ∑ q : Point, D.generatorChain g q • f q = ∑ i : Fin n, f (D.point g i)

Pairing the 0-chain of a generator with a function on intersection points sums the function over the points of the generator.

theorem TauCeti.HeegaardIntersectionSystem.Generator.ext {n : ℕ} {Point : Type u} (D : HeegaardIntersectionSystem n Point) {g g' : D.Generator} (h : ∀ (i : Fin n), ↑(g.snd i) = ↑(g'.snd i)) : g = g'

Two generators with the same chosen points are equal.

theorem TauCeti.HeegaardIntersectionSystem.Generator.ext_iff {n : ℕ} {Point : Type u} {D : HeegaardIntersectionSystem n Point} {g g' : D.Generator} : g = g' ↔ ∀ (i : Fin n), ↑(g.snd i) = ↑(g'.snd i)