Novikov series on the integers are Laurent series

For the exponent group ℤ with the period map k ↦ k (Int.castAddHom ℝ), the Novikov support condition says exactly that the support is bounded below (TauCeti.NovikovSeries.forall_finite_lt_iff_bddBelow_support). Hence the Novikov series are the formal Laurent series R⸨X⸩ = HahnSeries ℤ R of Mathlib, with the same coefficients. This file constructs that comparison as a ring isomorphism TauCeti.NovikovSeries.toLaurentSeries. It sends the monomial r e^n to r Xⁿ, and it restricts on finitely supported series to the inclusion LaurentPolynomial.toLaurentSeries of Laurent polynomials, the group ring R[ℤ].

Over a field K, the comparison also matches the topologies: the period filtration U_D is the closed ball v ≤ exp (-D) of the X-adic valuation (TauCeti.NovikovSeries.valuation_toLaurentSeries_le_exp_iff), and the comparison is a uniform equivalence between the period topology and the valuation topology (TauCeti.NovikovSeries.toLaurentSeriesUniformEquiv). Through it, the circle-valued Novikov complexes with coefficients in Nov(ℤ, ℤ, id) can be computed with the Laurent-series API of Mathlib.

Main definitions

• TauCeti.NovikovSeries.toLaurentSeries: the coefficient-preserving ring isomorphism between Novikov series on ℤ for the period map k ↦ k and Laurent series.
• TauCeti.NovikovSeries.toLaurentSeriesUniformEquiv: over a field, the same map as a uniform equivalence for the period and valuation topologies.

Main results

• TauCeti.NovikovSeries.toLaurentSeries_single and TauCeti.NovikovSeries.toLaurentSeries_ofAddMonoidAlgebra: the comparison sends monomials to monomials and restricts to the inclusion of Laurent polynomials.
• TauCeti.NovikovSeries.toLaurentSeries_algebraMap: for an S-algebra R, the comparison commutes with algebraMap S.
• TauCeti.NovikovSeries.valuation_toLaurentSeries_le_exp_iff: the period filtration corresponds to the valuation filtration.
• TauCeti.NovikovSeries.tendsto_toLaurentSeries_iff: the comparison and its inverse preserve convergence.

References

• A. Pajitnov, Circle-valued Morse Theory, de Gruyter 2006, Chapter 3.
• M. Hutchings and Y.-J. Lee, Circle-valued Morse theory and Reidemeister torsion, Geom. Topol. 3 (1999), Section 2.

def TauCeti.NovikovSeries.toLaurentSeries {R : Type u_1} [Semiring R] : NovikovSeries R ℤ (Int.castAddHom ℝ) ≃+* LaurentSeries R

Novikov series on ℤ for the period map k ↦ k are the Laurent series: the ring isomorphism which keeps every coefficient.

@[simp]

theorem TauCeti.NovikovSeries.coeff_toLaurentSeries {R : Type u_1} [Semiring R] (a : NovikovSeries R ℤ (Int.castAddHom ℝ)) : (toLaurentSeries a).coeff = a.coeff

@[simp]

theorem TauCeti.NovikovSeries.coeff_toLaurentSeries_symm {R : Type u_1} [Semiring R] (f : LaurentSeries R) : (toLaurentSeries.symm f).coeff = f.coeff

@[simp]

theorem TauCeti.NovikovSeries.support_toLaurentSeries {R : Type u_1} [Semiring R] (a : NovikovSeries R ℤ (Int.castAddHom ℝ)) : HahnSeries.support (toLaurentSeries a) = a.support

@[simp]

theorem TauCeti.NovikovSeries.toLaurentSeries_single {R : Type u_1} [Semiring R] (n : ℤ) (r : R) : toLaurentSeries (single n r) = (HahnSeries.single n) r

The comparison sends the monomial r e^n to the Laurent monomial r Xⁿ.

theorem TauCeti.NovikovSeries.toLaurentSeries_algebraMap {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] [Algebra S R] (s : S) : toLaurentSeries ((algebraMap S (NovikovSeries R ℤ (Int.castAddHom ℝ))) s) = (algebraMap S (LaurentSeries R)) s

For an S-algebra R, the comparison is compatible with the S-algebra structures: it sends the constant series algebraMap S _ s to the constant Laurent series.

@[simp]

theorem TauCeti.NovikovSeries.toLaurentSeries_ofAddMonoidAlgebra {R : Type u_1} [Semiring R] (p : LaurentPolynomial R) : toLaurentSeries (ofAddMonoidAlgebra p) = LaurentPolynomial.toLaurentSeries p

On the group ring R[ℤ] = R[T;T⁻¹], the comparison restricts to the inclusion of Laurent polynomials into Laurent series.

theorem TauCeti.NovikovSeries.valuation_toLaurentSeries_le_exp_iff {K : Type u_2} [Field K] {a : NovikovSeries K ℤ (Int.castAddHom ℝ)} {D : ℤ} : Valued.v (toLaurentSeries a) ≤ WithZero.exp (-D) ↔ a ∈ periodFiltration K (Int.castAddHom ℝ) ↑D

The period filtration U_D corresponds to the closed ball v ≤ exp (-D) of the X-adic valuation on Laurent series.

theorem TauCeti.NovikovSeries.tendsto_toLaurentSeries_iff {K : Type u_2} [Field K] {ι : Type u_3} {l : Filter ι} {f : ι → NovikovSeries K ℤ (Int.castAddHom ℝ)} {a : NovikovSeries K ℤ (Int.castAddHom ℝ)} : Filter.Tendsto (fun (i : ι) => toLaurentSeries (f i)) l (nhds (toLaurentSeries a)) ↔ Filter.Tendsto f l (nhds a)

A family of Novikov series on ℤ converges in the period topology if and only if its image converges in the valuation topology on Laurent series.

theorem TauCeti.NovikovSeries.continuous_toLaurentSeries {K : Type u_2} [Field K] : Continuous ⇑toLaurentSeries

Over a field, the comparison is continuous for the period and valuation topologies.

theorem TauCeti.NovikovSeries.continuous_toLaurentSeries_symm {K : Type u_2} [Field K] : Continuous ⇑toLaurentSeries.symm

Over a field, the inverse comparison is continuous for the valuation and period topologies.

def TauCeti.NovikovSeries.toLaurentSeriesUniformEquiv {K : Type u_2} [Field K] : NovikovSeries K ℤ (Int.castAddHom ℝ) ≃ᵤ LaurentSeries K

Over a field, the comparison between Novikov series on ℤ and Laurent series is a uniform equivalence for the period topology and the X-adic valuation topology.

@[simp]

theorem TauCeti.NovikovSeries.coe_toLaurentSeriesUniformEquiv {K : Type u_2} [Field K] : ⇑toLaurentSeriesUniformEquiv = ⇑toLaurentSeries

@[simp]

theorem TauCeti.NovikovSeries.coe_toLaurentSeriesUniformEquiv_symm {K : Type u_2} [Field K] : ⇑toLaurentSeriesUniformEquiv.symm = ⇑toLaurentSeries.symm