The class ε(x, y) of a pair of generators

Let (Σ, α, β, z) be a pointed Heegaard diagram of a closed 3-manifold Y, with generators x, y. Ozsváth and Szabó attach to them a class ε(x, y) ∈ H₁(Y; ℤ): join the points of x to those of y by paths in the α-curves, join the points of y back to those of x by paths in the β-curves, and take the class of the resulting loop in H₁(Σ) / ⟨[α₁], …, [β₁], …⟩ ≅ H₁(Y). Changing the paths changes the loop by whole curves, so the class is well defined. It vanishes exactly when some domain connects x to y, and s_z(x) - s_z(y) is the Poincaré dual of ε(x, y) (Ozsváth–Szabó, Lemma 2.19). So ε sorts the generators into the spin^c summands of the Heegaard Floer chain complex, and the differential only counts disks between generators in the same summand.

This file develops ε for the incidence data TauCeti.HeegaardRegionSystem. A 1-chain on α ∪ β is a pair of integer functions on intersection points: a coefficient on the α-arc and one on the β-arc starting at each point. The class ε(x, y) lives in TauCeti.HeegaardRegionSystem.CurveHomology, the group of 1-cycles of α ∪ β modulo boundaries of domains and the cycles supported on whole curves. For the incidence data of an actual diagram in which every attaching curve meets the other family, so that the arcs cover α ∪ β, the boundaries of domains are exactly the cycles of α ∪ β that bound in Σ, so this group is the image of H₁(α ∪ β) in H₁(Σ) / ⟨[αᵢ], [βⱼ]⟩ ≅ H₁(Y) and embeds in H₁(Y); that identification is geometric and is not formalized here. The embedding need not be onto: for the genus-one diagram of S¹ × S² in TauCeti.LowDimTopology.Heegaard.CircleTimesSphere, the core of the annulus is not homologous to a cycle in α ∪ β, and the group is trivial although H₁(S¹ × S²) = ℤ. Since ε(x, y) is the class of a cycle in α ∪ β, nothing is lost for it.

Main definitions

• TauCeti.HeegaardRegionSystem.arcBoundary: the boundary of a 1-chain on α ∪ β.
• TauCeti.HeegaardRegionSystem.domainBoundary: the boundary of a domain, as a 1-chain.
• TauCeti.HeegaardRegionSystem.arcCycles: the 1-cycles of α ∪ β.
• TauCeti.HeegaardRegionSystem.curveCycles: the 1-chains that are combinations of whole α- and β-curves.
• TauCeti.HeegaardRegionSystem.arcRelations: boundaries of domains plus whole curves.
• TauCeti.HeegaardRegionSystem.CurveHomology: the 1-cycles modulo arcRelations, with its class map CurveHomology.mk and universal property CurveHomology.lift.
• TauCeti.HeegaardRegionSystem.IsConnectingChain: a 1-chain made of paths from x to y along α and from y to x along β.
• TauCeti.HeegaardRegionSystem.epsilon: the class ε(x, y).

Main results

• TauCeti.HeegaardRegionSystem.exists_isConnectingChain: any two generators are joined by a connecting chain.
• TauCeti.HeegaardRegionSystem.IsConnectingChain.epsilon_eq: ε(x, y) is the class of every connecting chain.
• TauCeti.HeegaardRegionSystem.epsilon_add_epsilon: ε(x, y) + ε(y, w) = ε(x, w).
• TauCeti.HeegaardRegionSystem.epsilon_eq_zero_iff: ε(x, y) = 0 exactly when some domain connects x to y.

References

• P. Ozsváth and Z. Szabó, Holomorphic disks and topological invariants for closed three-manifolds, Ann. of Math. 159 (2004), arXiv:math/0101206, §2.4: Definition 2.11 of ε(x, y), Proposition 2.15 (π₂(x, y) is nonempty exactly when ε(x, y) = 0) and Lemma 2.19.

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

The boundary of a 1-chain on α ∪ β, given as its α-part and its β-part.

Equations

• H.arcBoundary = H.alphaArcBoundary.coprod H.betaArcBoundary

@[simp]

theorem TauCeti.HeegaardRegionSystem.arcBoundary_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (c : (Point → ℤ) × (Point → ℤ)) : H.arcBoundary c = H.alphaArcBoundary c.1 + H.betaArcBoundary c.2

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

The boundary of a domain as a 1-chain on α ∪ β: its α-part ∂D ∩ α and its β-part ∂D ∩ β.

Equations

• H.domainBoundary = H.alphaBoundary.prod H.betaBoundary

@[simp]

theorem TauCeti.HeegaardRegionSystem.domainBoundary_apply {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) : H.domainBoundary D = (H.alphaBoundary D, H.betaBoundary D)

theorem TauCeti.HeegaardRegionSystem.arcBoundary_domainBoundary {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) : H.arcBoundary (H.domainBoundary D) = 0

The boundary of a domain is a cycle.

def TauCeti.HeegaardRegionSystem.arcCycles {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : AddSubgroup ((Point → ℤ) × (Point → ℤ))

The 1-cycles of α ∪ β.

Equations

• H.arcCycles = H.arcBoundary.ker

@[simp]

theorem TauCeti.HeegaardRegionSystem.mem_arcCycles_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {c : (Point → ℤ) × (Point → ℤ)} : c ∈ H.arcCycles ↔ H.alphaArcBoundary c.1 + H.betaArcBoundary c.2 = 0

def TauCeti.HeegaardRegionSystem.curveCycles {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : AddSubgroup ((Point → ℤ) × (Point → ℤ))

The 1-chains that are combinations ∑ aᵢ αᵢ + ∑ bⱼ βⱼ of whole curves, that is, whose α- and β-parts are both cycles.

Equations

• H.curveCycles = H.alphaArcBoundary.ker.prod H.betaArcBoundary.ker

@[simp]

theorem TauCeti.HeegaardRegionSystem.mem_curveCycles_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {c : (Point → ℤ) × (Point → ℤ)} : c ∈ H.curveCycles ↔ H.alphaArcBoundary c.1 = 0 ∧ H.betaArcBoundary c.2 = 0

A 1-chain is a combination of whole curves exactly when its α- and β-parts are cycles.

theorem TauCeti.HeegaardRegionSystem.mem_curveCycles_iff_exists {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {c : (Point → ℤ) × (Point → ℤ)} : c ∈ H.curveCycles ↔ (∃ (a : Fin n → ℤ), ∀ (p : Point), c.1 p = a (H.alpha p)) ∧ ∃ (b : Fin n → ℤ), ∀ (p : Point), c.2 p = b (H.beta p)

A 1-chain is a combination of whole curves exactly when its α-part is constant along each α-curve and its β-part is constant along each β-curve.

def TauCeti.HeegaardRegionSystem.arcRelations {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : AddSubgroup ((Point → ℤ) × (Point → ℤ))

The relations defining CurveHomology: boundaries of domains plus combinations of whole curves.

Equations

• H.arcRelations = H.domainBoundary.range ⊔ H.curveCycles

theorem TauCeti.HeegaardRegionSystem.mem_arcRelations_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {c : (Point → ℤ) × (Point → ℤ)} : c ∈ H.arcRelations ↔ ∃ (D : Region → ℤ), c - H.domainBoundary D ∈ H.curveCycles

A 1-chain is a relation exactly when it differs from the boundary of some domain by a combination of whole curves.

theorem TauCeti.HeegaardRegionSystem.domainBoundary_mem_arcRelations {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (D : Region → ℤ) : H.domainBoundary D ∈ H.arcRelations

The boundary of a domain is a relation.

theorem TauCeti.HeegaardRegionSystem.curveCycles_le_arcRelations {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : H.curveCycles ≤ H.arcRelations

Combinations of whole curves are relations.

theorem TauCeti.HeegaardRegionSystem.arcRelations_le_arcCycles {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : H.arcRelations ≤ H.arcCycles

Every relation is a cycle.

def TauCeti.HeegaardRegionSystem.CurveHomology {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : Type u

The 1-cycles of α ∪ β modulo boundaries of domains and combinations of whole curves. For the incidence data of a pointed Heegaard diagram of Y whose arcs cover α ∪ β, this is the image of H₁(α ∪ β) in H₁(Σ) / ⟨[αᵢ], [βⱼ]⟩ ≅ H₁(Y; ℤ), the group in which the classes ε(x, y) live.

Equations

• H.CurveHomology = (↥H.arcCycles ⧸ H.arcRelations.addSubgroupOf H.arcCycles)

@[instance_reducible]

instance TauCeti.HeegaardRegionSystem.instAddCommGroupCurveHomology {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : AddCommGroup H.CurveHomology

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.HeegaardRegionSystem.CurveHomology.mk {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : ↥H.arcCycles →+ H.CurveHomology

The class of a 1-cycle of α ∪ β in CurveHomology.

Equations

• TauCeti.HeegaardRegionSystem.CurveHomology.mk H = QuotientAddGroup.mk' (H.arcRelations.addSubgroupOf H.arcCycles)

theorem TauCeti.HeegaardRegionSystem.CurveHomology.mk_surjective {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) : Function.Surjective ⇑(mk H)

Every element of CurveHomology is the class of a cycle.

@[simp]

theorem TauCeti.HeegaardRegionSystem.CurveHomology.mk_eq_zero_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) {c : ↥H.arcCycles} : (mk H) c = 0 ↔ ↑c ∈ H.arcRelations

A cycle has class zero exactly when it is a relation.

@[simp]

theorem TauCeti.HeegaardRegionSystem.CurveHomology.mk_eq_mk_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) {c d : ↥H.arcCycles} : (mk H) c = (mk H) d ↔ ↑c - ↑d ∈ H.arcRelations

Two cycles have the same class exactly when they differ by a relation.

theorem TauCeti.HeegaardRegionSystem.CurveHomology.hom_ext {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) {A : Type u_1} [AddMonoid A] {f g : H.CurveHomology →+ A} (h : f.comp (mk H) = g.comp (mk H)) : f = g

Two additive homomorphisms out of CurveHomology agree once they agree on classes of cycles.

theorem TauCeti.HeegaardRegionSystem.CurveHomology.hom_ext_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {A : Type u_1} [AddMonoid A] {f g : H.CurveHomology →+ A} : f = g ↔ f.comp (mk H) = g.comp (mk H)

def TauCeti.HeegaardRegionSystem.CurveHomology.lift {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) {A : Type u_1} [AddMonoid A] (f : ↥H.arcCycles →+ A) (hf : ∀ (c : ↥H.arcCycles), ↑c ∈ H.arcRelations → f c = 0) : H.CurveHomology →+ A

An additive homomorphism on 1-cycles that vanishes on the relations descends to CurveHomology.

Equations

• TauCeti.HeegaardRegionSystem.CurveHomology.lift H f hf = QuotientAddGroup.lift (H.arcRelations.addSubgroupOf H.arcCycles) f ⋯

@[simp]

theorem TauCeti.HeegaardRegionSystem.CurveHomology.lift_mk {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) {A : Type u_1} [AddMonoid A] (f : ↥H.arcCycles →+ A) (hf : ∀ (c : ↥H.arcCycles), ↑c ∈ H.arcRelations → f c = 0) (c : ↥H.arcCycles) : (lift H f hf) ((mk H) c) = f c

def TauCeti.HeegaardRegionSystem.IsConnectingChain {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} (x y : H.Generator) (c : (Point → ℤ) × (Point → ℤ)) : Prop

c connects the generator x to the generator y: its α-part is a 1-chain on the α-arcs with boundary y - x and its β-part a 1-chain on the β-arcs with boundary x - y. Concretely, c runs from the points of x to those of y along the α-curves and back along the β-curves.

Equations

• TauCeti.HeegaardRegionSystem.IsConnectingChain x y c = (H.alphaArcBoundary c.1 = H.generatorChain y - H.generatorChain x ∧ H.betaArcBoundary c.2 = H.generatorChain x - H.generatorChain y)

@[simp]

theorem TauCeti.HeegaardRegionSystem.isConnectingChain_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {c : (Point → ℤ) × (Point → ℤ)} : IsConnectingChain x y c ↔ H.alphaArcBoundary c.1 = H.generatorChain y - H.generatorChain x ∧ H.betaArcBoundary c.2 = H.generatorChain x - H.generatorChain y

Unfolding IsConnectingChain into its two boundary conditions.

theorem TauCeti.HeegaardRegionSystem.isConnectingChain_domainBoundary_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {D : Region → ℤ} : IsConnectingChain x y (H.domainBoundary D) ↔ IsDomainBetween x y D

The boundary of a domain connects x to y exactly when the domain does.

theorem TauCeti.HeegaardRegionSystem.IsDomainBetween.isConnectingChain {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {D : Region → ℤ} : IsDomainBetween x y D → IsConnectingChain x y (H.domainBoundary D)

Alias of the reverse direction of TauCeti.HeegaardRegionSystem.isConnectingChain_domainBoundary_iff.

---

The boundary of a domain connects x to y exactly when the domain does.

theorem TauCeti.HeegaardRegionSystem.isConnectingChain_self_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x : H.Generator} {c : (Point → ℤ) × (Point → ℤ)} : IsConnectingChain x x c ↔ c ∈ H.curveCycles

The chains connecting a generator to itself are the combinations of whole curves.

theorem TauCeti.HeegaardRegionSystem.IsConnectingChain.mem_arcCycles {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {c : (Point → ℤ) × (Point → ℤ)} (hc : IsConnectingChain x y c) : c ∈ H.arcCycles

A connecting chain is a cycle.

theorem TauCeti.HeegaardRegionSystem.IsConnectingChain.add {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y w : H.Generator} {c d : (Point → ℤ) × (Point → ℤ)} (hc : IsConnectingChain x y c) (hd : IsConnectingChain y w d) : IsConnectingChain x w (c + d)

Concatenating a chain from x to y with one from y to w gives a chain from x to w.

theorem TauCeti.HeegaardRegionSystem.IsConnectingChain.neg {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {c : (Point → ℤ) × (Point → ℤ)} (hc : IsConnectingChain x y c) : IsConnectingChain y x (-c)

Reversing a chain from x to y gives a chain from y to x.

theorem TauCeti.HeegaardRegionSystem.IsConnectingChain.sub_mem_curveCycles {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {c d : (Point → ℤ) × (Point → ℤ)} (hc : IsConnectingChain x y c) (hd : IsConnectingChain x y d) : c - d ∈ H.curveCycles

Two chains connecting x to y differ by a combination of whole curves.

theorem TauCeti.HeegaardRegionSystem.exists_isConnectingChain {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} (x y : H.Generator) : ∃ (c : (Point → ℤ) × (Point → ℤ)), IsConnectingChain x y c

Any two generators are connected by a chain.

noncomputable def TauCeti.HeegaardRegionSystem.epsilon {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} (H : HeegaardRegionSystem n Point Region Basepoint) (x y : H.Generator) : H.CurveHomology

The class ε(x, y) of Ozsváth and Szabó: the class in CurveHomology of any chain connecting x to y (see IsConnectingChain.epsilon_eq).

Equations

• H.epsilon x y = (TauCeti.HeegaardRegionSystem.CurveHomology.mk H) ⟨⋯.choose, ⋯⟩

theorem TauCeti.HeegaardRegionSystem.IsConnectingChain.epsilon_eq {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} {c : (Point → ℤ) × (Point → ℤ)} (hc : IsConnectingChain x y c) : H.epsilon x y = (CurveHomology.mk H) ⟨c, ⋯⟩

ε(x, y) is the class of every chain connecting x to y.

@[simp]

theorem TauCeti.HeegaardRegionSystem.epsilon_self {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} (x : H.Generator) : H.epsilon x x = 0

ε(x, x) = 0.

@[simp]

theorem TauCeti.HeegaardRegionSystem.epsilon_add_epsilon {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} (x y w : H.Generator) : H.epsilon x y + H.epsilon y w = H.epsilon x w

The classes ε are additive along a chain of generators: ε(x, y) + ε(y, w) = ε(x, w).

@[simp]

theorem TauCeti.HeegaardRegionSystem.neg_epsilon {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} (x y : H.Generator) : -H.epsilon x y = H.epsilon y x

Exchanging the generators negates ε: -ε(x, y) = ε(y, x).

@[simp]

theorem TauCeti.HeegaardRegionSystem.epsilon_eq_zero_iff {n : ℕ} {Point : Type u} {Region : Type v} {Basepoint : Type w} {H : HeegaardRegionSystem n Point Region Basepoint} {x y : H.Generator} : H.epsilon x y = 0 ↔ ∃ (D : Region → ℤ), IsDomainBetween x y D

ε(x, y) vanishes exactly when some domain connects x to y.

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

If a domain connects x to y, then ε(x, y) = 0.