The Floer Novikov ring

Let Γ = PeriodGroup ω c be the period group of a closed symplectic manifold, with symplectic area ω and first Chern number c. Capped Hamiltonian Floer complexes are modules over the Floer Novikov ring Λ: Novikov series ∑ a_γ e^γ in the classes γ ∈ Γ, where the monomial e^γ has

• valuation ν(γ) = -ω(γ): for every bound C only finitely many γ with a_γ ≠ 0 have ν(γ) < C, so infinitely many terms are allowed only as the area tends to -∞;
• degree 2 c(γ), the grading shift of a recapping by γ.

We write Λ as NovikovSeries R Γ (-area), so the ring structure, the period-filtration topology and the completeness of Novikov series apply to it directly, and we grade it by the homomorphism PeriodGroup.degree = 2 • chern. A series whose support meets infinitely many degrees is not a finite sum of homogeneous series, so Λ is not in general the direct sum of its homogeneous pieces; the graded structure is the graded monoid of homogeneous series of TauCeti.RingTheory.NovikovSeries.Grading.

The two classical coefficient regimes are distinguished by this grading.

• If c vanishes on spherical classes, every series has degree 0: the grading of the Floer complex is entirely carried by the generators.
• If every spherical class with vanishing first Chern number has vanishing area, for instance if ω = τ c on spherical classes (spherical monotonicity), each degree is carried by at most one class, so every homogeneous series is a monomial, and the homogeneous series span exactly the group ring R[Γ] of the cyclic group Γ (PeriodGroup.isAddCyclic_of_ker_le): in the monotone case this is the finite Laurent model of the coefficient ring. When moreover ω = τ c with τ > 0, the Novikov condition says exactly that the degrees of the support are bounded above.

Main definitions

• TauCeti.Floer.NovikovRing R ω c: the Floer Novikov ring over R, graded by the degree TauCeti.Floer.PeriodGroup.degree of TauCeti.Geometry.Symplectic.Floer.PeriodGroup.

Main results

• TauCeti.Floer.NovikovRing.gradeBy_degree_eq_bot_of_odd: there are no nonzero series of odd degree.
• TauCeti.Floer.NovikovRing.gradeBy_degree_zero_eq_top_of_chern_eq_zero, TauCeti.Floer.NovikovRing.gradeBy_degree_eq_bot_of_chern_eq_zero: if the first Chern number vanishes, the ring is concentrated in degree 0.
• TauCeti.Floer.NovikovRing.eq_single_of_mem_gradeBy_degree: if ker c ≤ ker ω, for instance for a spherically monotone pair, every homogeneous series is a monomial.
• TauCeti.Floer.NovikovRing.mem_iSup_gradeBy_degree_iff: if ker c ≤ ker ω, the homogeneous series span exactly the finitely supported series, the image of R[Γ].
• TauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree: for a positively monotone pair, a coefficient function is a Floer Novikov series exactly when the degrees of its support are bounded above.

References

• H. Hofer and D. A. Salamon, Floer homology and Novikov rings, in The Floer memorial volume, Progr. Math. 133 (1995), 483–524.
• S. Piunikhin, D. Salamon and M. Schwarz, Symplectic Floer–Donaldson theory and quantum cohomology, in Contact and symplectic geometry, Publ. Newton Inst. 8 (1996), 171–200.
• D. McDuff and D. Salamon, J-holomorphic curves and symplectic topology, the construction of the Novikov ring in the chapter on quantum cohomology.

@[reducible, inline]

abbrev TauCeti.Floer.NovikovRing {S : Type u_1} [AddGroup S] (R : Type u_2) (ω : S →+ ℝ) (c : S →+ ℤ) [Zero R] : Type (max u_1 u_2)

The Floer Novikov ring over R: Novikov series ∑ a_γ e^γ over the period group, with valuation ν(γ) = -ω(γ), so that for every bound C only finitely many classes with nonzero coefficient have area greater than -C. It is graded by PeriodGroup.degree.

theorem TauCeti.Floer.NovikovRing.gradeBy_degree_eq_bot_of_odd {S : Type u_1} [AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Semiring R] {k : ℤ} (hk : Odd k) : NovikovSeries.gradeBy R (-PeriodGroup.area ω c) (⇑(PeriodGroup.degree ω c)) k = ⊥

There are no nonzero Floer Novikov series of odd degree.

theorem TauCeti.Floer.NovikovRing.gradeBy_degree_zero_eq_top_of_chern_eq_zero {S : Type u_1} [AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Semiring R] (h : ∀ (s : S), c s = 0) : NovikovSeries.gradeBy R (-PeriodGroup.area ω c) (⇑(PeriodGroup.degree ω c)) 0 = ⊤

If the first Chern number vanishes on spherical classes, every Floer Novikov series has degree 0.

theorem TauCeti.Floer.NovikovRing.gradeBy_degree_eq_bot_of_chern_eq_zero {S : Type u_1} [AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Semiring R] (h : ∀ (s : S), c s = 0) {k : ℤ} (hk : k ≠ 0) : NovikovSeries.gradeBy R (-PeriodGroup.area ω c) (⇑(PeriodGroup.degree ω c)) k = ⊥

If the first Chern number vanishes on spherical classes, there are no nonzero Floer Novikov series of nonzero degree.

theorem TauCeti.Floer.NovikovRing.eq_single_of_mem_gradeBy_degree {S : Type u_1} [AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Semiring R] (hker : c.ker ≤ ω.ker) {γ : PeriodGroup ω c} {a : NovikovRing R ω c} (ha : a ∈ NovikovSeries.gradeBy R (-PeriodGroup.area ω c) (⇑(PeriodGroup.degree ω c)) ((PeriodGroup.degree ω c) γ)) : a = NovikovSeries.single γ (a.coeff γ)

If every spherical class with vanishing first Chern number has vanishing area, for instance for a spherically monotone pair, a Floer Novikov series of the degree of γ is the monomial a_γ e^γ.

theorem TauCeti.Floer.NovikovRing.mem_iSup_gradeBy_degree_iff {S : Type u_1} [AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Semiring R] (hker : c.ker ≤ ω.ker) {a : NovikovRing R ω c} : a ∈ ⨆ (k : ℤ), NovikovSeries.gradeBy R (-PeriodGroup.area ω c) (⇑(PeriodGroup.degree ω c)) k ↔ (NovikovSeries.support a).Finite

If every spherical class with vanishing first Chern number has vanishing area, for instance for a spherically monotone pair, the homogeneous Floer Novikov series span exactly the finitely supported series, that is, the image of the group ring R[Γ] (TauCeti.NovikovSeries.mem_range_ofFinsupp_iff).

theorem TauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree {S : Type u_1} [AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Zero R] {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) (hτ : 0 < τ) (g : PeriodGroup ω c → R) : (∀ (C : ℝ), {γ : PeriodGroup ω c | g γ ≠ 0 ∧ (-PeriodGroup.area ω c) γ < C}.Finite) ↔ BddAbove (⇑(PeriodGroup.degree ω c) '' Function.support g)

For a positively monotone pair, a coefficient function on the period group satisfies the Novikov condition of the Floer Novikov ring exactly when the degrees of its support are bounded above.

theorem TauCeti.Floer.NovikovRing.bddAbove_degree_image_support {S : Type u_1} [AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Zero R] {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) (hτ : 0 < τ) (a : NovikovRing R ω c) : BddAbove (⇑(PeriodGroup.degree ω c) '' NovikovSeries.support a)

For a positively monotone pair, the degrees of the support of a Floer Novikov series are bounded above.