Four-twist weights of orbit tori and the signed iterates of the return map

Let φ be an area-preserving diffeomorphism of a closed surface and Y_φ its mapping torus. In the symplectic four-manifold S¹ × Y_φ a periodic orbit γ of φ gives an embedded square-zero torus S¹ × γ, and the normal operator of this torus is governed by the linearized return map P of γ, a 2 × 2 matrix of determinant one. Of the four normal operators of the torus twisted by its real sign characters, the two twisted along the circle factor are expected to have positive determinant sign, while the untwisted operator and the operator twisted only along γ compare with det (1 - P) and det (1 + P). The four-twist label (σ, i) of Taubes's weighted count that these signs prescribe has σ the sign of det (1 - P), and i equal to 1 or 0 according as det (1 + P) is negative or not. Since det (1 ∓ P) = 2 ∓ trace P, a return map all of whose iterates are nondegenerate falls into one of three classes:

• positive hyperbolic (2 < trace P), with label (-, 0) and local series 1 - t;
• negative hyperbolic (trace P < -2), with label (+, 1) and local series 1 + t;
• elliptic (|trace P| < 2), with label (+, 0) and local series 1 / (1 - t).

This file proves that in each class the local series f = f_(σ, i) of TauCeti.torusWeightSeries satisfies the logarithmic derivative identity

t f'(t) = f(t) ∑_{k ≥ 1} ε(P ^ k) t ^ k, ε(Q) = sgn det (1 - Q),

provided every iterate of P is nondegenerate, det (1 - P ^ k) ≠ 0 for k ≥ 1. Here ε(P ^ k) is the Lefschetz index of the fixed point of the k-th iterate of the return map. Over ℚ the identity says that log f = ∑_{k ≥ 1} ε(P ^ k) t ^ k / k, so that f is the factor that the orbit γ contributes to the dynamical zeta function exp ∑_n L(φ ^ n) t ^ n / n. Taubes's weights of the orbit tori thus reproduce the local factors of the Lefschetz zeta function, which is the local input to the comparison of the curve count of S¹ × Y_φ with the zeta function of φ.

That the determinant signs of the twisted normal operators of the orbit torus are those of det (1 ∓ P) is a determinant comparison which this file does not prove; the statements here are about the label that the signs of det (1 ∓ P) prescribe.

Main results

• TauCeti.X_mul_derivative_torusWeightSeries_false_zero_of_two_lt_trace: the identity for a positive hyperbolic return map and the series f_(-, 0) = 1 - t.
• TauCeti.X_mul_derivative_torusWeightSeries_true_one_of_trace_lt_neg_two: the identity for a negative hyperbolic return map and the series f_(+, 1) = 1 + t.
• TauCeti.X_mul_derivative_torusWeightSeries_true_zero_of_abs_trace_le_two: the identity for a nondegenerate elliptic return map and the series f_(+, 0) = 1 / (1 - t).
• TauCeti.X_mul_derivative_torusWeightSeries_of_det_eq_one: the identity for every return map all of whose iterates are nondegenerate, with the label read off from the signs of det (1 - P) and det (1 + P).

References

• C. H. Taubes, Counting pseudo-holomorphic submanifolds in dimension 4, J. Differential Geom. 44 (1996), 818--893.
• E.-N. Ionel and T. H. Parker, Gromov invariants and symplectic maps, Math. Ann. 314 (1999), 127--158.
• M. Hutchings and Y.-J. Lee, Circle-valued Morse theory, Reidemeister torsion, and Seiberg–Witten invariants of 3-manifolds, Topology 38 (1999), 861--888.

theorem TauCeti.X_mul_derivative_torusWeightSeries_false_zero_of_two_lt_trace {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {P : Matrix (Fin 2) (Fin 2) R} (hdet : P.det = 1) (htr : 2 < P.trace) : PowerSeries.X * PowerSeries.derivative (torusWeightSeries false 0) = torusWeightSeries false 0 * PowerSeries.mk fun (k : ℕ) => if k = 0 then 0 else ↑(SignType.sign (1 - P ^ k).det)

For a positive hyperbolic 2 × 2 matrix P of determinant one (2 < trace P), the local series f_(-, 0) = 1 - t satisfies t f' = f ∑_{k ≥ 1} sgn det (1 - P ^ k) t ^ k: every iterate of P has det (1 - P ^ k) < 0, and 1 - t = exp (-∑_{k ≥ 1} t ^ k / k).

theorem TauCeti.X_mul_derivative_torusWeightSeries_true_one_of_trace_lt_neg_two {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {P : Matrix (Fin 2) (Fin 2) R} (hdet : P.det = 1) (htr : P.trace < -2) : PowerSeries.X * PowerSeries.derivative (torusWeightSeries true 1) = torusWeightSeries true 1 * PowerSeries.mk fun (k : ℕ) => if k = 0 then 0 else ↑(SignType.sign (1 - P ^ k).det)

For a negative hyperbolic 2 × 2 matrix P of determinant one (trace P < -2), the local series f_(+, 1) = 1 + t satisfies t f' = f ∑_{k ≥ 1} sgn det (1 - P ^ k) t ^ k: the sign of det (1 - P ^ k) is (-1) ^ (k + 1), and 1 + t = exp ∑_{k ≥ 1} (-1) ^ (k + 1) t ^ k / k.

theorem TauCeti.X_mul_derivative_torusWeightSeries_true_zero_of_abs_trace_le_two {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {P : Matrix (Fin 2) (Fin 2) R} (hdet : P.det = 1) (htr : |P.trace| ≤ 2) (hP : ∀ (k : ℕ), k ≠ 0 → (1 - P ^ k).det ≠ 0) : PowerSeries.X * PowerSeries.derivative (torusWeightSeries true 0) = torusWeightSeries true 0 * PowerSeries.mk fun (k : ℕ) => if k = 0 then 0 else ↑(SignType.sign (1 - P ^ k).det)

For a 2 × 2 matrix P of determinant one with |trace P| ≤ 2, all of whose iterates are nondegenerate (so that P is elliptic), the local series f_(+, 0) = 1 / (1 - t) satisfies t f' = f ∑_{k ≥ 1} sgn det (1 - P ^ k) t ^ k: every iterate has 0 < det (1 - P ^ k), and 1 / (1 - t) = exp ∑_{k ≥ 1} t ^ k / k.

theorem TauCeti.X_mul_derivative_torusWeightSeries_of_det_eq_one {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {P : Matrix (Fin 2) (Fin 2) R} (hdet : P.det = 1) (hP : ∀ (k : ℕ), k ≠ 0 → (1 - P ^ k).det ≠ 0) : PowerSeries.X * PowerSeries.derivative (torusWeightSeries (decide (0 < (1 - P).det)) (if (1 + P).det < 0 then 1 else 0)) = torusWeightSeries (decide (0 < (1 - P).det)) (if (1 + P).det < 0 then 1 else 0) * PowerSeries.mk fun (k : ℕ) => if k = 0 then 0 else ↑(SignType.sign (1 - P ^ k).det)

Orbit-torus weights are local zeta factors. Let P be a 2 × 2 matrix of determinant one all of whose iterates are nondegenerate, det (1 - P ^ k) ≠ 0 for k ≥ 1. Read off the label σ = (0 < det (1 - P)) and i = 1 if det (1 + P) < 0, i = 0 otherwise. Then the local series f = f_(σ, i) satisfies t f' = f ∑_{k ≥ 1} sgn det (1 - P ^ k) t ^ k; over ℚ this says log f = ∑_{k ≥ 1} sgn det (1 - P ^ k) t ^ k / k.