Four-twist multiplicity weights of square-zero pseudoholomorphic tori

In Taubes's count of embedded pseudoholomorphic curves in a symplectic four-manifold, an embedded square-zero torus C may appear in a curve configuration with any positive multiplicity m. The contribution of C with multiplicity m is the integer [t ^ m] f_(σ, i), the m-th coefficient of one of eight integral power series. The label (σ, i) is read off from the four normal operators of C twisted by the real sign characters π₁(C) → {±1}: σ is the determinant sign of the untwisted operator and i ∈ {0, 1, 2, 3} counts the negative signs among the three nontrivially twisted operators. The series are

• f_(+,0) = 1 / (1 - t), f_(+,1) = 1 + t, f_(+,2) = (1 + t) / (1 + t ^ 2), f_(+,3) = (1 + t) (1 - t ^ 2) / (1 + t ^ 2),
• f_(-,i) = 1 / f_(+,i).

Each has constant term 1, so the divisions take place in the unit group of ℤ⟦X⟧, using the inverse PowerSeries.invOfUnit. For a finite family of pairwise disjoint tori the total weight of the configurations with total multiplicity n is the n-th coefficient of the product of their local series, which TauCeti.coeff_prod_torusWeightSeries expands as a sum of products of local weights.

On the homology ray of a primitive square-zero class A₀, a torus of class m • A₀ enters with its local series evaluated at t ^ m. The ray series ∏_C f_label(C)(t ^ m_C) of a family of such tori, with finitely many tori in each class, is an infinite product in the coefficientwise topology (PowerSeries.WithPiTopology); each of its coefficients is computed by a finite cutoff and expands as a sum over the configurations of these tori of the given total class. A configuration of total class n • A₀ from a finite family s of tori, the torus c having class m c • A₀, is a multiplicity assignment l in the weighted antidiagonal s.weightedFinsuppAntidiag m n, that is, supported in s with ∑ c ∈ s, m c * l c = n. The expansion, cutoff and infinite product hold for any family of power series in place of the local series (PowerSeries.coeff_prod_expand, PowerSeries.coeff_prod_expand_of_subset, PowerSeries.coeff_tprod_expand), and are specialised here to the tori.

Along a generic path of almost complex structures, tori are born and die in pairs of opposite determinant signs, and they undergo period doubling, in which one nontrivially twisted operator changes sign while a torus in twice the class appears or disappears. The local series satisfy the corresponding identities, so the ray series is unchanged by these changes of the family of tori.

This file constructs only this series data and its coefficients; it assumes no geometric regularity and gives no curve-count interpretation.

Main declarations

• TauCeti.torusWeightSeries σ i: the local series f_(σ, i), where σ = true stands for a positive determinant sign and σ = false for a negative one.
• TauCeti.torusWeight σ i m: the local weight w_(σ, i)(m) = [t ^ m] f_(σ, i). The simp lemma TauCeti.torusWeight_def reduces it to the coefficient, so the closed forms below apply to it directly.
• TauCeti.coeff_prod_torusWeightSeries: the weight of a finite configuration of tori with total multiplicity n is the sum, over all distributions of n among the tori, of the products of the local weights.
• TauCeti.torusWeightSeries_not_mul, TauCeti.isUnit_torusWeightSeries: the series of opposite sign and equal index are mutually inverse units.
• TauCeti.torusWeightSeries_true_zero, TauCeti.torusWeightSeries_true_one, TauCeti.torusWeightSeries_true_two_mul, TauCeti.torusWeightSeries_true_three_mul, TauCeti.torusWeightSeries_false_zero, TauCeti.torusWeightSeries_false_one_mul, TauCeti.torusWeightSeries_false_two_mul, TauCeti.torusWeightSeries_false_three_mul: the rational-function identities characterizing the eight series.
• TauCeti.coeff_torusWeightSeries_true_two, TauCeti.coeff_torusWeightSeries_true_three, TauCeti.coeff_torusWeightSeries_false_one, TauCeti.coeff_torusWeightSeries_false_two, TauCeti.coeff_torusWeightSeries_false_three: closed forms for the multiplicity weights of the five series that are neither polynomials nor PowerSeries.mk 1.
• TauCeti.torusWeightSeries_castSucc, TauCeti.torusWeightSeries_succ: the period-doubling identities f_(σ, i)(t) = f_(σ, i + 1)(t) f_(σ, i % 2)(t ^ 2) and f_(σ, i + 1)(t) = f_(σ, i)(t) f_(!σ, i % 2)(t ^ 2).
• TauCeti.rayTorusWeightSeries s m σ i: the ray series ∏ c ∈ s, f_(σ c, i c)(t ^ m c) of a finite family of tori; TauCeti.constantCoeff_rayTorusWeightSeries gives its constant term.
• TauCeti.coeff_rayTorusWeightSeries: the independent-component expansion of the coefficients of the ray series as sums over configurations of products of local weights.
• TauCeti.coeff_rayTorusWeightSeries_of_subset: tori of class larger than n • A₀ do not affect the n-th coefficient.
• TauCeti.rayTorusWeightSeries_insert_insert, TauCeti.rayTorusWeightSeries_insert_eq_update_castSucc, TauCeti.rayTorusWeightSeries_insert_eq_update_succ: the ray series is unchanged by the birth and death of a pair of tori and by period doubling.
• TauCeti.multipliable_expand_torusWeightSeries, TauCeti.coeff_tprod_expand_torusWeightSeries: the infinite ray product over a family with finitely many tori in each class exists, and its coefficients are those of finite cutoffs.

References

• C. H. Taubes, Counting pseudo-holomorphic submanifolds in dimension 4, J. Differential Geom. 44 (1996), 818--893.

noncomputable def TauCeti.torusWeightSeries (σ : Bool) (i : Fin 4) : PowerSeries ℤ

The local multiplicity series f_(σ, i) ∈ ℤ⟦X⟧ attached to an embedded square-zero pseudoholomorphic torus with determinant sign σ (true for +, false for -) and with i negative signs among its three nontrivially twisted normal operators. The positive series are 1 / (1 - X), 1 + X, (1 + X) / (1 + X ^ 2) and (1 + X) (1 - X ^ 2) / (1 + X ^ 2), and each negative series is the inverse of the positive series with the same index. The weight of the torus with multiplicity m is the coefficient coeff m (torusWeightSeries σ i).

noncomputable def TauCeti.torusWeight (σ : Bool) (i : Fin 4) (m : ℕ) : ℤ

The local weight w_(σ, i)(m) ∈ ℤ of an embedded square-zero pseudoholomorphic torus with label (σ, i) appearing with multiplicity m: the m-th coefficient of torusWeightSeries σ i.

@[simp]

theorem TauCeti.torusWeight_def (σ : Bool) (i : Fin 4) (m : ℕ) : torusWeight σ i m = (PowerSeries.coeff m) (torusWeightSeries σ i)

The local weight w_(σ, i)(m) is the m-th coefficient of the local series f_(σ, i).

theorem TauCeti.coeff_prod_torusWeightSeries {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (σ : ι → Bool) (i : ι → Fin 4) (n : ℕ) : (PowerSeries.coeff n) (∏ c ∈ s, torusWeightSeries (σ c) (i c)) = ∑ l ∈ s.finsuppAntidiag n, ∏ c ∈ s, torusWeight (σ c) (i c) (l c)

For a finite family s of tori, the torus c carrying the label (σ c, i c), the n-th coefficient of the product of the local series is the sum, over all ways l of distributing the total multiplicity n among the tori, of the products of the local weights w_(σ c, i c)(l c).

@[simp]

theorem TauCeti.constantCoeff_torusWeightSeries (σ : Bool) (i : Fin 4) : PowerSeries.constantCoeff (torusWeightSeries σ i) = 1

Every local series has constant term 1, so the multiplicity-zero weight is 1.

theorem TauCeti.torusWeight_zero (σ : Bool) (i : Fin 4) : torusWeight σ i 0 = 1

The multiplicity-zero weight of every torus is 1.

theorem TauCeti.torusWeightSeries_true_mul_false (i : Fin 4) : torusWeightSeries true i * torusWeightSeries false i = 1

The negative series is a right inverse of the positive series with the same index.

theorem TauCeti.torusWeightSeries_false_mul_true (i : Fin 4) : torusWeightSeries false i * torusWeightSeries true i = 1

The negative series is a left inverse of the positive series with the same index.

theorem TauCeti.torusWeightSeries_not_mul (σ : Bool) (i : Fin 4) : torusWeightSeries (!σ) i * torusWeightSeries σ i = 1

Reversing the determinant sign inverts the local series.

theorem TauCeti.torusWeightSeries_mul_not (σ : Bool) (i : Fin 4) : torusWeightSeries σ i * torusWeightSeries (!σ) i = 1

Reversing the determinant sign inverts the local series.

theorem TauCeti.isUnit_torusWeightSeries (σ : Bool) (i : Fin 4) : IsUnit (torusWeightSeries σ i)

Every local series is a unit of ℤ⟦X⟧.

theorem TauCeti.torusWeightSeries_false_eq_iff (i : Fin 4) (φ : PowerSeries ℤ) : torusWeightSeries false i = φ ↔ torusWeightSeries true i * φ = 1

A series equals the negative series f_(-, i) exactly when it inverts f_(+, i).

The rational-function identities

@[simp]

theorem TauCeti.torusWeightSeries_true_zero : torusWeightSeries true 0 = PowerSeries.mk 1

f_(+,0) is the geometric series 1 + X + X ^ 2 + ⋯.

@[simp]

theorem TauCeti.torusWeightSeries_true_one : torusWeightSeries true 1 = 1 + PowerSeries.X

f_(+,1) is the polynomial 1 + X.

theorem TauCeti.torusWeightSeries_true_zero_mul : torusWeightSeries true 0 * (1 - PowerSeries.X) = 1

f_(+,0) = 1 / (1 - X).

theorem TauCeti.torusWeightSeries_true_two_mul : torusWeightSeries true 2 * (1 + PowerSeries.X ^ 2) = 1 + PowerSeries.X

f_(+,2) = (1 + X) / (1 + X ^ 2).

theorem TauCeti.torusWeightSeries_true_three_mul : torusWeightSeries true 3 * (1 + PowerSeries.X ^ 2) = (1 + PowerSeries.X) * (1 - PowerSeries.X ^ 2)

f_(+,3) = (1 + X) (1 - X ^ 2) / (1 + X ^ 2).

@[simp]

theorem TauCeti.torusWeightSeries_false_zero : torusWeightSeries false 0 = 1 - PowerSeries.X

f_(-,0) = 1 - X.

theorem TauCeti.torusWeightSeries_false_one_mul : torusWeightSeries false 1 * (1 + PowerSeries.X) = 1

f_(-,1) = 1 / (1 + X).

theorem TauCeti.torusWeightSeries_false_two_mul : torusWeightSeries false 2 * (1 + PowerSeries.X) = 1 + PowerSeries.X ^ 2

f_(-,2) = (1 + X ^ 2) / (1 + X).

theorem TauCeti.torusWeightSeries_false_three_mul : torusWeightSeries false 3 * ((1 + PowerSeries.X) * (1 - PowerSeries.X ^ 2)) = 1 + PowerSeries.X ^ 2

f_(-,3) = (1 + X ^ 2) / ((1 + X) (1 - X ^ 2)).

Closed forms for the multiplicity weights

Each closed form is checked against the coefficient recurrence obtained by multiplying by the denominator of the corresponding rational function, which is a unit of ℤ⟦X⟧.

@[simp]

theorem TauCeti.coeff_torusWeightSeries_true_two (m : ℕ) : (PowerSeries.coeff m) (torusWeightSeries true 2) = (-1) ^ (m / 2)

The multiplicity weights of f_(+,2) = (1 + X) / (1 + X ^ 2) are 1, 1, -1, -1, 1, 1, ….

@[simp]

theorem TauCeti.coeff_torusWeightSeries_true_three (m : ℕ) : (PowerSeries.coeff m) (torusWeightSeries true 3) = if m ≤ 1 then 1 else 2 * (-1) ^ (m / 2)

The multiplicity weights of f_(+,3) = (1 + X) (1 - X ^ 2) / (1 + X ^ 2) are 1, 1, -2, -2, 2, 2, ….

@[simp]

theorem TauCeti.coeff_torusWeightSeries_false_one (m : ℕ) : (PowerSeries.coeff m) (torusWeightSeries false 1) = (-1) ^ m

The multiplicity weights of f_(-,1) = 1 / (1 + X) are 1, -1, 1, -1, ….

@[simp]

theorem TauCeti.coeff_torusWeightSeries_false_two (m : ℕ) : (PowerSeries.coeff m) (torusWeightSeries false 2) = if m ≤ 1 then (-1) ^ m else 2 * (-1) ^ m

The multiplicity weights of f_(-,2) = (1 + X ^ 2) / (1 + X) are 1, -1, 2, -2, 2, -2, ….

@[simp]

theorem TauCeti.coeff_torusWeightSeries_false_three (m : ℕ) : (PowerSeries.coeff m) (torusWeightSeries false 3) = (-1) ^ m * (2 * ↑(m / 2) + 1)

The multiplicity weights of f_(-,3) = (1 + X ^ 2) / ((1 + X) (1 - X ^ 2)) are 1, -1, 3, -3, 5, -5, ….

Bifurcation identities

Along a generic path of almost complex structures the set of embedded square-zero tori changes through bifurcations, and the local series are such that the weighted count does not change.

• Birth and death. Two tori of the same class and index with opposite determinant signs appear or disappear together. Their contributions cancel since f_(σ, i) f_(!σ, i) = 1 (TauCeti.torusWeightSeries_mul_not).

• Period doubling. The operator of a torus C twisted by one nontrivial sign character ι acquires a kernel, so the sign of that twisted operator changes and the index of C moves between i and i + 1, the sign of ι being positive at index i. A torus close to the double cover of C determined by ι, in twice the class of C, appears or disappears with it. The new torus is assigned the index i % 2: of the nontrivial sign characters of the double cover, the one pulled back from C is the common restriction of the two characters of C other than ι, whose signs contain i negative ones, while the other two come from characters of C of order four. The identities

  f_(σ, i)(t) = f_(σ, i + 1)(t) f_(σ, i % 2)(t ^ 2), f_(σ, i + 1)(t) = f_(σ, i)(t) f_(!σ, i % 2)(t ^ 2)

  (TauCeti.torusWeightSeries_castSucc, TauCeti.torusWeightSeries_succ) show that a torus of label (σ, i) contributes as much as a torus of label (σ, i + 1) together with one of label (σ, i % 2) in twice its class, and that a torus of label (σ, i + 1) contributes as much as a torus of label (σ, i) together with one of label (!σ, i % 2) in twice its class.

These are identities of the local series, valid for every multiplicity and both determinant signs. The bifurcation analysis producing the label changes is separate. The ray versions are TauCeti.rayTorusWeightSeries_insert_insert, TauCeti.rayTorusWeightSeries_insert_eq_update_castSucc and TauCeti.rayTorusWeightSeries_insert_eq_update_succ.

theorem TauCeti.torusWeightSeries_castSucc (σ : Bool) (j : Fin 3) : torusWeightSeries σ j.castSucc = torusWeightSeries σ j.succ * (PowerSeries.expand 2 ⋯) (torusWeightSeries σ (j % 2).castSucc)

Period-doubling identity of the local series: for j ∈ {0, 1, 2}, f_(σ, j)(t) = f_(σ, j + 1)(t) f_(σ, j % 2)(t ^ 2), the indices j, j + 1 and j % 2 being j.castSucc, j.succ and (j % 2).castSucc in Fin 4. A torus of label (σ, j) contributes as much as a torus of label (σ, j + 1) together with a torus of label (σ, j % 2) in twice its class.

theorem TauCeti.torusWeightSeries_succ (σ : Bool) (j : Fin 3) : torusWeightSeries σ j.succ = torusWeightSeries σ j.castSucc * (PowerSeries.expand 2 ⋯) (torusWeightSeries (!σ) (j % 2).castSucc)

Period-doubling identity, read in the other direction: for j ∈ {0, 1, 2}, f_(σ, j + 1)(t) = f_(σ, j)(t) f_(!σ, j % 2)(t ^ 2), the indices j + 1, j and j % 2 being j.succ, j.castSucc and (j % 2).castSucc in Fin 4. A torus of label (σ, j + 1) contributes as much as a torus of label (σ, j) together with a torus of the opposite determinant sign and index j % 2 in twice its class.

Tori on a square-zero homology ray

Let A₀ be a primitive square-zero class. A torus whose class is m • A₀ and which appears with multiplicity l contributes the class (m * l) • A₀, so its local series enters the count of configurations on the ray of A₀ with t replaced by t ^ m. The coefficient expansion, the finite cutoff and the infinite product specialise the corresponding results of TauCeti.RingTheory.PowerSeries.Expand for products of expanded power series.

noncomputable def TauCeti.rayTorusWeightSeries {ι : Type u_1} (s : Finset ι) (m : ι → ℕ+) (σ : ι → Bool) (i : ι → Fin 4) : PowerSeries ℤ

The weight series ∏ c ∈ s, f_(σ c, i c)(t ^ m c) of a finite family s of embedded square-zero pseudoholomorphic tori on the homology ray of a primitive class A₀, the torus c having class m c • A₀ and label (σ c, i c). Its n-th coefficient is the sum, over the multiplicity assignments of total class n • A₀, of the products of the local weights (TauCeti.coeff_rayTorusWeightSeries).

theorem TauCeti.rayTorusWeightSeries_def {ι : Type u_1} (s : Finset ι) (m : ι → ℕ+) (σ : ι → Bool) (i : ι → Fin 4) : rayTorusWeightSeries s m σ i = ∏ c ∈ s, (PowerSeries.expand ↑(m c) ⋯) (torusWeightSeries (σ c) (i c))

The ray series is the product of the local series evaluated at t ^ m c.

@[simp]

theorem TauCeti.constantCoeff_rayTorusWeightSeries {ι : Type u_1} (s : Finset ι) (m : ι → ℕ+) (σ : ι → Bool) (i : ι → Fin 4) : PowerSeries.constantCoeff (rayTorusWeightSeries s m σ i) = 1

The ray series has constant term 1.

theorem TauCeti.coeff_rayTorusWeightSeries {ι : Type u_1} (s : Finset ι) (m : ι → ℕ+) (σ : ι → Bool) (i : ι → Fin 4) (n : ℕ) : (PowerSeries.coeff n) (rayTorusWeightSeries s m σ i) = ∑ l ∈ s.weightedFinsuppAntidiag m n, ∏ c ∈ s, torusWeight (σ c) (i c) (l c)

Independent-component expansion of the ray series: its n-th coefficient is the sum, over all configurations l of total class n • A₀ (the elements of s.weightedFinsuppAntidiag m n), of the products of the local weights w_(σ c, i c)(l c).

theorem TauCeti.coeff_rayTorusWeightSeries_of_subset {ι : Type u_1} {s t : Finset ι} (hst : s ⊆ t) {m : ι → ℕ+} (σ : ι → Bool) (i : ι → Fin 4) {n : ℕ} (h : ∀ c ∈ t, c ∉ s → n < ↑(m c)) : (PowerSeries.coeff n) (rayTorusWeightSeries t m σ i) = (PowerSeries.coeff n) (rayTorusWeightSeries s m σ i)

Finite cutoff for the ray series: adjoining tori whose classes are all larger than n • A₀ does not change the n-th coefficient.

@[simp]

theorem TauCeti.rayTorusWeightSeries_insert {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {c : ι} (hc : c ∉ s) (m : ι → ℕ+) (σ : ι → Bool) (i : ι → Fin 4) : rayTorusWeightSeries (insert c s) m σ i = (PowerSeries.expand ↑(m c) ⋯) (torusWeightSeries (σ c) (i c)) * rayTorusWeightSeries s m σ i

Adjoining a torus c ∉ s multiplies the ray series by its factor f_(σ c, i c)(t ^ m c).

theorem TauCeti.rayTorusWeightSeries_insert_insert {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {c d : ι} (hc : c ∉ s) (hd : d ∉ s) {m : ι → ℕ+} (hm : m d = m c) {σ : ι → Bool} (hσ : σ d = !σ c) {i : ι → Fin 4} (hi : i d = i c) : rayTorusWeightSeries (insert c (insert d s)) m σ i = rayTorusWeightSeries s m σ i

Birth and death on the ray: adjoining two tori c and d of the same class, with the same index and opposite determinant signs, does not change the ray series.

theorem TauCeti.rayTorusWeightSeries_insert_eq_update_castSucc {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {c d : ι} (hc : c ∈ s) (hd : d ∉ s) {m : ι → ℕ+} (hm : m d = 2 * m c) {σ : ι → Bool} (hσ : σ d = σ c) {i : ι → Fin 4} {j : Fin 3} (hic : i c = j.succ) (hid : i d = (j % 2).castSucc) : rayTorusWeightSeries (insert d s) m σ i = rayTorusWeightSeries s m σ (Function.update i c j.castSucc)

Period doubling on the ray: let c ∈ s have index j + 1 (i c = j.succ), and adjoin a torus d ∉ s of twice the class of c, with the determinant sign of c and index j % 2 (i d = (j % 2).castSucc). The ray series is that of s with c relabelled with index j (j.castSucc).

theorem TauCeti.rayTorusWeightSeries_insert_eq_update_succ {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {c d : ι} (hc : c ∈ s) (hd : d ∉ s) {m : ι → ℕ+} (hm : m d = 2 * m c) {σ : ι → Bool} (hσ : σ d = !σ c) {i : ι → Fin 4} {j : Fin 3} (hic : i c = j.castSucc) (hid : i d = (j % 2).castSucc) : rayTorusWeightSeries (insert d s) m σ i = rayTorusWeightSeries s m σ (Function.update i c j.succ)

Period doubling on the ray, in the other direction: let c ∈ s have index j (i c = j.castSucc), and adjoin a torus d ∉ s of twice the class of c, with the opposite determinant sign and index j % 2 (i d = (j % 2).castSucc). The ray series is that of s with c relabelled with index j + 1 (j.succ).

theorem TauCeti.multipliable_expand_torusWeightSeries {ι : Type u_1} {m : ι → ℕ+} (hm : ∀ (n : ℕ), {c : ι | ↑(m c) ≤ n}.Finite) (σ : ι → Bool) (i : ι → Fin 4) : Multipliable fun (c : ι) => (PowerSeries.expand ↑(m c) ⋯) (torusWeightSeries (σ c) (i c))

The ray factors f_(σ c, i c)(t ^ m c) of a family of tori with finitely many tori in each class m • A₀ have an infinite product in the coefficientwise topology (PowerSeries.WithPiTopology) on ℤ⟦X⟧.

theorem TauCeti.coeff_tprod_expand_torusWeightSeries {ι : Type u_1} {m : ι → ℕ+} (hm : ∀ (n : ℕ), {c : ι | ↑(m c) ≤ n}.Finite) (σ : ι → Bool) (i : ι → Fin 4) {s : Finset ι} {n : ℕ} (hs : ∀ (c : ι), ↑(m c) ≤ n → c ∈ s) : (PowerSeries.coeff n) (∏' (c : ι), (PowerSeries.expand ↑(m c) ⋯) (torusWeightSeries (σ c) (i c))) = (PowerSeries.coeff n) (rayTorusWeightSeries s m σ i)

The n-th coefficient of the infinite ray product ∏_c f_(σ c, i c)(t ^ m c), over a family of tori with finitely many tori in each class, is that of the ray series of any finite subfamily containing every torus of class at most n • A₀.