The period-filtration topology on Novikov series

Let H be an additive group, N : H →+ ℝ a period homomorphism and R an additive commutative group of coefficients. For a real cutoff C, the Novikov series whose coefficients vanish at every exponent of period < C form an additive subgroup U_C (TauCeti.NovikovSeries.periodFiltration). These subgroups decrease as C grows and meet only in 0; they form a basis of neighbourhoods of 0 for a separated group topology, the period topology. A sequence of Novikov series converges in it when, below every period cutoff, its coefficients are eventually constant.

The Novikov series are complete for this topology, and the finitely supported ones are dense: the truncation TauCeti.NovikovSeries.trunc C a of a series a, which keeps the coefficients of period < C, differs from a by an element of U_C. Consequently the Novikov series are the completion of the group ring H →₀ R for the uniform structure of its period filtration (TauCeti.NovikovSeries.completionPkg), and every uniformly continuous map from the group ring to a complete separated uniform space extends uniquely to the Novikov series. The packaging as an AbstractCompletion follows Mathlib's LaurentSeries.LaurentSeriesPkg in Mathlib/RingTheory/LaurentSeries.lean; no code is copied from there.

Main definitions

• TauCeti.NovikovSeries.periodFiltration C: the additive subgroup U_C of Novikov series with no nonzero coefficient of period < C.
• The instances TopologicalSpace, IsTopologicalAddGroup, UniformSpace and IsUniformAddGroup on TauCeti.NovikovSeries R H N: the period topology.
• TauCeti.NovikovSeries.groupRingUniformSpace: the uniform structure of the period filtration on the group ring H →₀ R.
• TauCeti.NovikovSeries.completionPkg: the Novikov series as an abstract completion of the group ring.

Main results

• TauCeti.NovikovSeries.exists_mem_periodFiltration: every series lies in some U_C.
• TauCeti.NovikovSeries.mem_periodFiltration_iff_le_order: a nonzero series lies in U_C exactly when C is at most its order.
• TauCeti.NovikovSeries.exists_pos_mem_periodFiltration_iff: a series vanishes at every exponent of period ≤ 0 exactly when it lies in U_C for some C > 0.
• TauCeti.NovikovSeries.hasBasis_nhds_zero and TauCeti.NovikovSeries.hasBasis_uniformity: the subgroups U_C form a basis of the period topology and its uniformity.
• TauCeti.NovikovSeries.tendsto_nhds_iff: convergence in the period topology means eventual agreement of coefficients below every cutoff.
• The instances T2Space and CompleteSpace: the period topology is separated and complete.
• The instances NonarchimedeanAddGroup and ContinuousConstSMul: the period topology has a basis of open subgroups, and coefficientwise scalar multiplication is continuous.
• TauCeti.NovikovSeries.tendsto_ofFinsupp_trunc and TauCeti.NovikovSeries.denseRange_ofFinsupp: the truncations of a series converge to it, so the finitely supported series are dense.
• TauCeti.NovikovSeries.isUniformInducing_ofFinsupp: the period filtration uniformity of the group ring is induced from the Novikov series.

References

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

def TauCeti.NovikovSeries.periodFiltration (R : Type u_1) {H : Type u_2} [AddZeroClass H] (N : H →+ ℝ) [AddGroup R] (C : ℝ) : AddSubgroup (NovikovSeries R H N)

The additive subgroup U_C of Novikov series whose coefficients vanish at every exponent of period < C. These subgroups form a basis of neighbourhoods of 0 in the period topology.

@[simp]

theorem TauCeti.NovikovSeries.mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] {C : ℝ} {a : NovikovSeries R H N} : a ∈ periodFiltration R N C ↔ ∀ (h : H), N h < C → a.coeff h = 0

theorem TauCeti.NovikovSeries.mem_periodFiltration_iff_le_order {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] {C : ℝ} {a : NovikovSeries R H N} (ha : a ≠ 0) : a ∈ periodFiltration R N C ↔ C ≤ a.order

A nonzero Novikov series lies in the period neighbourhood U_C exactly when C is at most its order.

theorem TauCeti.NovikovSeries.antitone_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] : Antitone (periodFiltration R N)

theorem TauCeti.NovikovSeries.exists_pos_mem_periodFiltration_iff {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] {a : NovikovSeries R H N} : (∃ (C : ℝ), 0 < C ∧ a ∈ periodFiltration R N C) ↔ ∀ (h : H), N h ≤ 0 → a.coeff h = 0

A Novikov series vanishes at every exponent of period ≤ 0 exactly when it lies in U_C for some positive cutoff C: a nonzero such series lies in U_C for its least support period C.

theorem TauCeti.NovikovSeries.eq_zero_of_forall_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] {a : NovikovSeries R H N} (ha : ∀ (C : ℝ), a ∈ periodFiltration R N C) : a = 0

An element of every U_C is zero.

theorem TauCeti.NovikovSeries.exists_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (a : NovikovSeries R H N) : ∃ (C : ℝ), a ∈ periodFiltration R N C

Every Novikov series lies in some U_C, since the periods of its support are bounded below.

theorem TauCeti.NovikovSeries.single_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddGroup R] (h : H) (r : R) : single h r ∈ periodFiltration R N (N h)

The monomial r e^h lies in U_(N h).

theorem TauCeti.NovikovSeries.iInf_periodFiltration (R : Type u_1) {H : Type u_2} [AddZeroClass H] (N : H →+ ℝ) [AddGroup R] : ⨅ (C : ℝ), periodFiltration R N C = ⊥

@[instance_reducible]

def TauCeti.NovikovSeries.periodFilterBasis (R : Type u_1) (H : Type u_2) [AddZeroClass H] (N : H →+ ℝ) [AddCommGroup R] : AddGroupFilterBasis (NovikovSeries R H N)

The additive group filter basis made of the subgroups U_C, which defines the period topology.

@[instance_reducible]

instance TauCeti.NovikovSeries.instTopologicalSpace {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : TopologicalSpace (NovikovSeries R H N)

The period topology on Novikov series: the subgroups U_C form a basis of neighbourhoods of 0.

instance TauCeti.NovikovSeries.instIsTopologicalAddGroup {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : IsTopologicalAddGroup (NovikovSeries R H N)

@[instance_reducible]

instance TauCeti.NovikovSeries.instUniformSpace {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : UniformSpace (NovikovSeries R H N)

The uniform structure of the period topology, for which a and b are close when b - a lies in some U_C.

instance TauCeti.NovikovSeries.instIsUniformAddGroup {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : IsUniformAddGroup (NovikovSeries R H N)

theorem TauCeti.NovikovSeries.hasBasis_nhds_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : (nhds 0).HasBasis (fun (x : ℝ) => True) fun (C : ℝ) => ↑(periodFiltration R N C)

The subgroups U_C form a basis of neighbourhoods of 0 in the period topology.

theorem TauCeti.NovikovSeries.periodFiltration_mem_nhds_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] (C : ℝ) : ↑(periodFiltration R N C) ∈ nhds 0

theorem TauCeti.NovikovSeries.isOpen_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] (C : ℝ) : IsOpen ↑(periodFiltration R N C)

theorem TauCeti.NovikovSeries.isClosed_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] (C : ℝ) : IsClosed ↑(periodFiltration R N C)

theorem TauCeti.NovikovSeries.hasBasis_nhds {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] (a : NovikovSeries R H N) : (nhds a).HasBasis (fun (x : ℝ) => True) fun (C : ℝ) => {b : NovikovSeries R H N | b - a ∈ periodFiltration R N C}

The sets {b | b - a ∈ U_C} form a basis of neighbourhoods of a in the period topology.

theorem TauCeti.NovikovSeries.hasBasis_uniformity {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : (uniformity (NovikovSeries R H N)).HasBasis (fun (x : ℝ) => True) fun (C : ℝ) => {p : NovikovSeries R H N × NovikovSeries R H N | p.2 - p.1 ∈ periodFiltration R N C}

The entourages {(a, b) | b - a ∈ U_C} form a basis of the period uniformity.

theorem TauCeti.NovikovSeries.tendsto_nhds_iff {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] {ι : Type u_3} {l : Filter ι} {f : ι → NovikovSeries R H N} {a : NovikovSeries R H N} : Filter.Tendsto f l (nhds a) ↔ ∀ (C : ℝ), ∀ᶠ (i : ι) in l, ∀ (h : H), N h < C → (f i).coeff h = a.coeff h

A family of Novikov series converges to a in the period topology if and only if, below every period cutoff, its coefficients eventually agree with those of a.

instance TauCeti.NovikovSeries.instT2Space {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : T2Space (NovikovSeries R H N)

instance TauCeti.NovikovSeries.instNonarchimedeanAddGroup {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : NonarchimedeanAddGroup (NovikovSeries R H N)

The period topology is nonarchimedean: the open subgroups U_C form a basis of neighbourhoods of 0.

instance TauCeti.NovikovSeries.instContinuousConstSMul {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] {S : Type u_3} [DistribSMul S R] : ContinuousConstSMul S (NovikovSeries R H N)

Coefficientwise scalar multiplication is continuous in the period topology.

theorem TauCeti.NovikovSeries.isLocallyConstant_coeff {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] (h : H) : IsLocallyConstant fun (a : NovikovSeries R H N) => a.coeff h

The coefficient of a series at the exponent h is locally constant in the period topology.

instance TauCeti.NovikovSeries.instCompleteSpace {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : CompleteSpace (NovikovSeries R H N)

The Novikov series are complete for the period topology: the limit of a Cauchy filter has, at each exponent, the coefficient on which the filter eventually agrees.

theorem TauCeti.NovikovSeries.sub_ofFinsupp_trunc_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] (C : ℝ) (a : NovikovSeries R H N) : a - ofFinsupp (trunc C a) ∈ periodFiltration R N C

A Novikov series differs from its truncation below C by an element of U_C.

theorem TauCeti.NovikovSeries.ofFinsupp_trunc_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] {D : ℝ} (C : ℝ) {a : NovikovSeries R H N} (ha : a ∈ periodFiltration R N D) : ofFinsupp (trunc C a) ∈ periodFiltration R N D

Truncation preserves membership in U_D.

theorem TauCeti.NovikovSeries.tendsto_ofFinsupp_trunc {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] (a : NovikovSeries R H N) : Filter.Tendsto (fun (C : ℝ) => ofFinsupp (trunc C a)) Filter.atTop (nhds a)

The truncations of a Novikov series converge to it as the cutoff tends to +∞.

theorem TauCeti.NovikovSeries.denseRange_ofFinsupp {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : DenseRange ⇑ofFinsupp

The finitely supported Novikov series are dense in the period topology.

@[instance_reducible]

def TauCeti.NovikovSeries.groupRingUniformSpace (R : Type u_1) (H : Type u_2) [AddZeroClass H] (N : H →+ ℝ) [AddCommGroup R] : UniformSpace (H →₀ R)

The uniform structure of the period filtration on the group ring H →₀ R: the subgroups of finitely supported functions vanishing at every exponent of period < C form a basis of neighbourhoods of 0 (TauCeti.NovikovSeries.hasBasis_groupRingUniformSpace). It is the uniform structure induced by the inclusion into the Novikov series.

theorem TauCeti.NovikovSeries.hasBasis_groupRingUniformSpace {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : (uniformity (H →₀ R)).HasBasis (fun (x : ℝ) => True) fun (C : ℝ) => {p : (H →₀ R) × (H →₀ R) | ∀ (h : H), N h < C → p.1 h = p.2 h}

The entourages of pairs of finitely supported functions that agree at every exponent of period < C form a basis of the period filtration uniformity on the group ring.

theorem TauCeti.NovikovSeries.isUniformInducing_ofFinsupp {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : IsUniformInducing ⇑ofFinsupp

The group ring carries the uniform structure induced by the inclusion into the Novikov series.

def TauCeti.NovikovSeries.completionPkg (R : Type u_1) (H : Type u_2) [AddZeroClass H] (N : H →+ ℝ) [AddCommGroup R] : AbstractCompletion.{max u_2 u_1, max u_1 u_2} (H →₀ R)

The Novikov series are the completion of the group ring H →₀ R for the uniform structure of its period filtration: they are complete and separated, and the inclusion ofFinsupp is a uniform inducing map with dense range.

@[simp]

theorem TauCeti.NovikovSeries.completionPkg_coe {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [AddCommGroup R] : (completionPkg R H N).coe = ⇑ofFinsupp