Novikov series form a topological ring, and geometric series

Let H be an additive monoid with a period homomorphism N : H →+ ℝ. The period filtration U_C of TauCeti.RingTheory.NovikovSeries.Topology is compatible with the convolution product: periods add under multiplication, so U_C * U_D ⊆ U_(C + D) (TauCeti.NovikovSeries.mul_mem_periodFiltration). Since every Novikov series lies in some U_C, multiplication is continuous for the period topology and the Novikov series form a nonarchimedean topological ring. Iterating the estimate, a series supported in periods ≥ C with C > 0 is topologically nilpotent; this is what makes geometric series ∑ aⁿ of positive-period series converge in the complete ring of Novikov series, and likewise exponential series when the coefficients form a ℚ-algebra.

The same estimate makes products computable from finite truncations: below the cutoff C, the product of two series with periods bounded below by A and B only involves their coefficients of period < C - B and < C - A (TauCeti.NovikovSeries.mul_sub_mul_trunc_mem_periodFiltration). Multiplying by a monomial u e^g with unit coefficient shifts the filtration by the period N g when exponents satisfy left cancellation (TauCeti.NovikovSeries.single_mul_mem_periodFiltration_iff).

The series supported in nonnegative periods form a subring, whose underlying set is the basic neighbourhood U_0, and the series supported in strictly positive periods form an ideal of it. A series a of the positive ideal lies in U_C for some C > 0, so it is topologically nilpotent, and in the complete nonarchimedean Novikov ring the geometric series ∑ aⁿ converges to a two-sided inverse of 1 - a in the nonnegative subring. For a monomial e^g with N g > 0 this is the expansion (1 - e^g)⁻¹ = ∑ₖ e^(k • g). Such geometric series are the factors in the product formula for dynamical zeta functions, and they appear in the torsion of circle-valued Morse complexes. They also show that the completed ring has no augmentation: a ring homomorphism to a nontrivial ring cannot send a monomial e^g of nonzero period to 1, since it would send the unit 1 - e^g (or 1 - e^(-g)) to 0, although the group ring of finitely supported series maps every monomial to 1.

The nonnegative subring is closed, hence complete, and the traces of the subgroups U_C are ideals of it, so it is linearly topologized. For an S-algebra of coefficients it is an S-algebra. These are the hypotheses of Mathlib's continuous evaluation of power series (PowerSeries.aeval) at its topologically nilpotent elements, such as those of the positive ideal.

Main definitions

• TauCeti.NovikovSeries.nonnegSubring: the subring of series supported in periods ≥ 0.
• TauCeti.NovikovSeries.posIdeal: the ideal of the nonnegative subring formed by the series supported in periods > 0.
• TauCeti.NovikovSeries.unitsOneSub: for a in the positive ideal, 1 - a as a unit of the nonnegative subring, with inverse the geometric series ∑ aⁿ.
• TauCeti.NovikovSeries.unitsOneSubSingle: for N g > 0, the unit 1 - r e^g of the nonnegative subring, with inverse the geometric series ∑ₖ rᵏ e^(k • g).
• TauCeti.NovikovSeries.periodIdeal: the series of the nonnegative subring lying in U_C, an ideal of it.

Main results

• TauCeti.NovikovSeries.mul_mem_periodFiltration: U_C * U_D ⊆ U_(C + D).
• TauCeti.NovikovSeries.mul_sub_mul_mem_periodFiltration and TauCeti.NovikovSeries.mul_sub_mul_trunc_mem_periodFiltration: cutoff compatibility of the convolution.
• TauCeti.NovikovSeries.single_mul_mem_periodFiltration_iff: multiplication by a monomial with unit coefficient shifts the period filtration for left-cancellative exponents.
• The instances IsTopologicalRing and NonarchimedeanRing: the period topology is a nonarchimedean ring topology.
• TauCeti.NovikovSeries.pow_mem_periodFiltration and TauCeti.NovikovSeries.isTopologicallyNilpotent_of_mem_periodFiltration: a series supported in periods ≥ C has its n-th power supported in periods ≥ n • C, so it is topologically nilpotent when C > 0.
• TauCeti.NovikovSeries.isTopologicallyNilpotent_of_mem_posIdeal: a series of the positive ideal is topologically nilpotent.
• TauCeti.NovikovSeries.tsum_pow_mem_nonnegSubring and TauCeti.NovikovSeries.isUnit_one_sub_of_mem_posIdeal: for a in the positive ideal, the geometric series ∑ aⁿ lies in the nonnegative subring and 1 - a is a unit there.
• TauCeti.NovikovSeries.one_sub_single_mul_tsum and TauCeti.NovikovSeries.tsum_mul_one_sub_single: the two inverse identities of the monomial geometric series ∑ₖ rᵏ e^(k • g) for N g > 0.
• TauCeti.NovikovSeries.isUnit_one_sub_single: 1 - r e^g is a unit for N g > 0.
• TauCeti.NovikovSeries.map_single_one_ne_one_of_pos and TauCeti.NovikovSeries.map_single_one_ne_one: a ring homomorphism to a nontrivial ring does not send a monomial e^g of nonzero period to 1.
• TauCeti.NovikovSeries.unitsOneSubSingle_mem_principalUnitGroup_posIdeal and TauCeti.NovikovSeries.unitsOneSubSingle_mem_principalUnitGroup_periodIdeal: 1 - r e^g is a principal unit for the positive ideal and for the ideal of series above the period N g.
• TauCeti.NovikovSeries.coe_zpow_unitsOneSubSingle_sub_one_mem_periodFiltration: every integer power of 1 - r e^g is congruent to 1 above the period N g.
• The instances CompleteSpace, IsLinearTopology and Algebra on the nonnegative subring.

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.

theorem TauCeti.NovikovSeries.mul_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] {C D : ℝ} {a b : NovikovSeries R H N} (ha : a ∈ periodFiltration R N C) (hb : b ∈ periodFiltration R N D) : a * b ∈ periodFiltration R N (C + D)

Periods add under multiplication: if the coefficients of a vanish below the period C and those of b below D, then those of a * b vanish below C + D.

theorem TauCeti.NovikovSeries.mul_sub_mul_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] {A B C : ℝ} {a a' b b' : NovikovSeries R H N} (ha : a ∈ periodFiltration R N A) (hb' : b' ∈ periodFiltration R N B) (haa' : a - a' ∈ periodFiltration R N (C - B)) (hbb' : b - b' ∈ periodFiltration R N (C - A)) : a * b - a' * b' ∈ periodFiltration R N C

Products are determined modulo U_C by approximations of their factors: if a ∈ U_A and b' ∈ U_B, and a' and b' agree with a and b modulo U_(C - B) and U_(C - A), then a * b and a' * b' agree modulo U_C.

theorem TauCeti.NovikovSeries.mul_sub_mul_trunc_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] {A B : ℝ} {a b : NovikovSeries R H N} (ha : a ∈ periodFiltration R N A) (hb : b ∈ periodFiltration R N B) (C : ℝ) : a * b - ofFinsupp (trunc (C - B) a) * ofFinsupp (trunc (C - A) b) ∈ periodFiltration R N C

Cutoff compatibility of the convolution: if the coefficients of a vanish below A and those of b below B, then below the cutoff C the product a * b agrees with the product of the truncations of a below C - B and of b below C - A.

instance TauCeti.NovikovSeries.instIsTopologicalRing {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] : IsTopologicalRing (NovikovSeries R H N)

Multiplication of Novikov series is continuous for the period topology.

theorem TauCeti.NovikovSeries.denseRange_ofAddMonoidAlgebra {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : DenseRange ⇑ofAddMonoidAlgebra

The coefficientwise inclusion of the group ring has dense image in its Novikov completion.

instance TauCeti.NovikovSeries.instNonarchimedeanRing {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : NonarchimedeanRing (NovikovSeries R H N)

The period topology is a nonarchimedean ring topology.

theorem TauCeti.NovikovSeries.one_mem_periodFiltration_zero {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : 1 ∈ periodFiltration R N 0

The unit series 1 = e^0 lies in U_0.

instance TauCeti.NovikovSeries.instGradedMonoidRealAddSubgroupPeriodFiltration {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : SetLike.GradedMonoid (periodFiltration R N)

The period filtration is multiplicatively graded by real lower bounds.

theorem TauCeti.NovikovSeries.pow_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {C : ℝ} {a : NovikovSeries R H N} (ha : a ∈ periodFiltration R N C) (n : ℕ) : a ^ n ∈ periodFiltration R N (n • C)

If the coefficients of a vanish below the period C, then those of a ^ n vanish below n • C.

theorem TauCeti.NovikovSeries.isTopologicallyNilpotent_of_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {C : ℝ} {a : NovikovSeries R H N} (hC : 0 < C) (ha : a ∈ periodFiltration R N C) : IsTopologicallyNilpotent a

A Novikov series whose coefficients vanish below some positive period is topologically nilpotent: its powers tend to 0 in the period topology.

theorem TauCeti.NovikovSeries.isTopologicallyNilpotent_single {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : IsTopologicallyNilpotent (single g r)

A monomial r e^g of positive period N g is topologically nilpotent.

theorem TauCeti.NovikovSeries.one_sub_single_mul_tsum {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : (1 - single g r) * ∑' (k : ℕ), single (k • g) (r ^ k) = 1

Geometric series of a monomial, left inverse identity: for N g > 0, (1 - r e^g) * ∑ₖ rᵏ e^(k • g) = 1.

theorem TauCeti.NovikovSeries.tsum_mul_one_sub_single {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : (∑' (k : ℕ), single (k • g) (r ^ k)) * (1 - single g r) = 1

Geometric series of a monomial, right inverse identity: for N g > 0, (∑ₖ rᵏ e^(k • g)) * (1 - r e^g) = 1.

def TauCeti.NovikovSeries.nonnegSubring (R : Type u_1) {H : Type u_2} [AddMonoid H] (N : H →+ ℝ) [Ring R] : Subring (NovikovSeries R H N)

The subring of Novikov series supported in nonnegative periods. Its underlying additive subgroup is the basic neighbourhood U_0 of the period topology.

@[simp]

theorem TauCeti.NovikovSeries.mem_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : NovikovSeries R H N} : a ∈ nonnegSubring R N ↔ ∀ (h : H), N h < 0 → a.coeff h = 0

theorem TauCeti.NovikovSeries.toAddSubgroup_nonnegSubring (R : Type u_1) {H : Type u_2} [AddMonoid H] (N : H →+ ℝ) [Ring R] : (nonnegSubring R N).toAddSubgroup = periodFiltration R N 0

The underlying additive subgroup of the nonnegative subring is U_0.

theorem TauCeti.NovikovSeries.isOpen_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : IsOpen ↑(nonnegSubring R N)

The nonnegative subring is open, hence also closed, in the period topology.

theorem TauCeti.NovikovSeries.isClosed_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : IsClosed ↑(nonnegSubring R N)

theorem TauCeti.NovikovSeries.single_mem_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 ≤ N g) (r : R) : single g r ∈ nonnegSubring R N

The monomial r e^g lies in the nonnegative subring when N g ≥ 0.

def TauCeti.NovikovSeries.posIdeal (R : Type u_1) {H : Type u_2} [AddMonoid H] (N : H →+ ℝ) [Ring R] : Ideal ↥(nonnegSubring R N)

The ideal of the nonnegative subring formed by the series supported in strictly positive periods. Its elements are the series lying in U_C for some C > 0 (TauCeti.NovikovSeries.exists_pos_mem_periodFiltration_iff).

@[simp]

theorem TauCeti.NovikovSeries.mem_posIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : ↥(nonnegSubring R N)} : a ∈ posIdeal R N ↔ ∀ (h : H), N h ≤ 0 → (↑a).coeff h = 0

instance TauCeti.NovikovSeries.instIsTwoSidedSubtypeMemSubringNonnegSubringPosIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : (posIdeal R N).IsTwoSided

The positive ideal is two-sided, also for noncommutative coefficients.

theorem TauCeti.NovikovSeries.isTopologicallyNilpotent_of_mem_posIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : ↥(nonnegSubring R N)} (ha : a ∈ posIdeal R N) : IsTopologicallyNilpotent ↑a

A series of the positive ideal is topologically nilpotent.

theorem TauCeti.NovikovSeries.tsum_pow_mem_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] (a : ↥(nonnegSubring R N)) : ∑' (n : ℕ), ↑a ^ n ∈ nonnegSubring R N

For a in the nonnegative subring, the geometric series ∑ aⁿ lies in the nonnegative subring.

noncomputable def TauCeti.NovikovSeries.unitsOneSub {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : ↥(nonnegSubring R N)} (ha : a ∈ posIdeal R N) : (↥(nonnegSubring R N))ˣ

For a in the positive ideal, 1 - a as a unit of the nonnegative subring. Its inverse is the geometric series ∑ aⁿ (TauCeti.NovikovSeries.coe_inv_unitsOneSub).

@[simp]

theorem TauCeti.NovikovSeries.val_unitsOneSub {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : ↥(nonnegSubring R N)} (ha : a ∈ posIdeal R N) : ↑(unitsOneSub ha) = 1 - a

@[simp]

theorem TauCeti.NovikovSeries.coe_inv_unitsOneSub {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : ↥(nonnegSubring R N)} (ha : a ∈ posIdeal R N) : ↑↑(unitsOneSub ha)⁻¹ = ∑' (n : ℕ), ↑a ^ n

theorem TauCeti.NovikovSeries.isUnit_one_sub_of_mem_posIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : ↥(nonnegSubring R N)} (ha : a ∈ posIdeal R N) : IsUnit (1 - a)

For a in the positive ideal, 1 - a is a unit of the nonnegative subring.

theorem TauCeti.NovikovSeries.single_mem_posIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : ⟨single g r, ⋯⟩ ∈ posIdeal R N

A monomial of positive period lies in the positive ideal.

noncomputable def TauCeti.NovikovSeries.unitsOneSubSingle {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : (↥(nonnegSubring R N))ˣ

For N g > 0, the factor 1 - r e^g as a unit of the nonnegative subring. Its inverse is the geometric series ∑ₖ rᵏ e^(k • g) (TauCeti.NovikovSeries.coe_inv_unitsOneSubSingle).

theorem TauCeti.NovikovSeries.val_unitsOneSubSingle {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : ↑(unitsOneSubSingle hg r) = 1 - ⟨single g r, ⋯⟩

The unit 1 - r e^g is 1 - a for the monomial a = r e^g of the nonnegative subring.

@[simp]

theorem TauCeti.NovikovSeries.coe_unitsOneSubSingle {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : ↑↑(unitsOneSubSingle hg r) = 1 - single g r

@[simp]

theorem TauCeti.NovikovSeries.coe_inv_unitsOneSubSingle {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : ↑↑(unitsOneSubSingle hg r)⁻¹ = ∑' (k : ℕ), single (k • g) (r ^ k)

theorem TauCeti.NovikovSeries.unitsOneSubSingle_mem_principalUnitGroup_posIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : unitsOneSubSingle hg r ∈ (posIdeal R N).principalUnitGroup

The unit 1 - r e^g is a principal unit for the positive ideal.

theorem TauCeti.NovikovSeries.isUnit_one_sub_single {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : IsUnit (1 - single g r)

For N g > 0, the series 1 - r e^g is a unit of the ring of Novikov series.

theorem TauCeti.NovikovSeries.map_single_one_ne_one_of_pos {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {F : Type u_3} {A : Type u_4} [Ring A] [Nontrivial A] [FunLike F (NovikovSeries R H N) A] [RingHomClass F (NovikovSeries R H N) A] (φ : F) {g : H} (hg : 0 < N g) : φ (single g 1) ≠ 1

A ring homomorphism out of the Novikov series to a nontrivial ring does not send a monomial e^g of positive period to 1: it would send the unit 1 - e^g to 0.

The nonnegative subring as a complete linearly topologized algebra

instance TauCeti.NovikovSeries.instCompleteSpaceSubtypeMemSubringNonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : CompleteSpace ↥(nonnegSubring R N)

The nonnegative subring is complete, being closed in the complete ring of Novikov series.

theorem TauCeti.NovikovSeries.hasBasis_nhds_zero_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : (nhds 0).HasBasis (fun (x : ℝ) => True) fun (C : ℝ) => {a : ↥(nonnegSubring R N) | ↑a ∈ periodFiltration R N C}

In the nonnegative subring, the traces of the subgroups U_C form a basis of neighbourhoods of 0.

def TauCeti.NovikovSeries.periodIdeal (R : Type u_1) {H : Type u_2} [AddMonoid H] (N : H →+ ℝ) [Ring R] (C : ℝ) : Ideal ↥(nonnegSubring R N)

The ideal of the nonnegative subring formed by the series in U_C: multiplying by a series of nonnegative periods does not lower periods. These ideals form a basis of neighbourhoods of 0 (TauCeti.NovikovSeries.hasBasis_nhds_zero_nonnegSubring).

@[simp]

theorem TauCeti.NovikovSeries.mem_periodIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {C : ℝ} {a : ↥(nonnegSubring R N)} : a ∈ periodIdeal R N C ↔ ↑a ∈ periodFiltration R N C

theorem TauCeti.NovikovSeries.unitsOneSubSingle_mem_principalUnitGroup_periodIdeal {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) : unitsOneSubSingle hg r ∈ (periodIdeal R N (N g)).principalUnitGroup

The unit 1 - r e^g is a principal unit for the ideal periodIdeal R N (N g).

theorem TauCeti.NovikovSeries.coe_zpow_unitsOneSubSingle_sub_one_mem_periodFiltration {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {g : H} (hg : 0 < N g) (r : R) (m : ℤ) : ↑↑(unitsOneSubSingle hg r ^ m) - 1 ∈ periodFiltration R N (N g)

Every integer power of 1 - r e^g is congruent to 1 above the period N g.

instance TauCeti.NovikovSeries.instIsLinearTopologySubtypeMemSubringNonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] : IsLinearTopology ↥(nonnegSubring R N) ↥(nonnegSubring R N)

The nonnegative subring is linearly topologized: the ideals periodIdeal R N C form a basis of neighbourhoods of 0. This is what makes power series evaluable at its topologically nilpotent elements (PowerSeries.aeval).

theorem TauCeti.NovikovSeries.isTopologicallyNilpotent_of_mem_posIdeal' {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {a : ↥(nonnegSubring R N)} (ha : a ∈ posIdeal R N) : IsTopologicallyNilpotent a

A series of the positive ideal is topologically nilpotent in the nonnegative subring.

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instAlgebraSubtypeMemSubringNonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {S : Type u_3} [CommSemiring S] [Algebra S R] : Algebra S ↥(nonnegSubring R N)

For an S-algebra R, the nonnegative subring is an S-algebra, with coefficientwise scalar multiplication.

@[simp]

theorem TauCeti.NovikovSeries.coe_smul_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {S : Type u_3} [CommSemiring S] [Algebra S R] (s : S) (a : ↥(nonnegSubring R N)) : ↑(s • a) = s • ↑a

@[simp]

theorem TauCeti.NovikovSeries.coe_algebraMap_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {S : Type u_3} [CommSemiring S] [Algebra S R] (s : S) : ↑((algebraMap S ↥(nonnegSubring R N)) s) = (algebraMap S (NovikovSeries R H N)) s

@[simp]

theorem TauCeti.NovikovSeries.coe_aeval_nonnegSubring {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] {S : Type u_3} [CommSemiring S] [Algebra S R] (a : ↥(nonnegSubring R N)) (p : Polynomial S) : ↑((Polynomial.aeval a) p) = (Polynomial.aeval ↑a) p

Evaluating a polynomial in the nonnegative subring commutes with the inclusion into the Novikov series.

theorem TauCeti.NovikovSeries.prod_sub_prod_mem_periodFiltration_of_bounds {R : Type u_1} {H : Type u_2} [AddCommMonoid H] {N : H →+ ℝ} [CommRing R] {ι : Type u_3} (s : Finset ι) {a b : ι → NovikovSeries R H N} {w : ι → ℝ} {C : ℝ} (ha : ∀ i ∈ s, a i ∈ periodFiltration R N (w i)) (hb : ∀ i ∈ s, b i ∈ periodFiltration R N (w i)) (hab : ∀ i ∈ s, a i - b i ∈ periodFiltration R N (C + w i)) : ∏ i ∈ s, a i - ∏ i ∈ s, b i ∈ periodFiltration R N (C + ∑ i ∈ s, w i)

Perturbing each factor above its lower bound by C perturbs the product above the sum of the lower bounds by C. The empty product has zero difference, at every cutoff.

theorem TauCeti.NovikovSeries.single_mul_mem_periodFiltration_iff {R : Type u_1} {H : Type u_2} [AddZeroClass H] [IsLeftCancelAdd H] {N : H →+ ℝ} [Ring R] (g : H) (u : Rˣ) {C : ℝ} {a : NovikovSeries R H N} : single g ↑u * a ∈ periodFiltration R N (N g + C) ↔ a ∈ periodFiltration R N C

Multiplication by a monomial u e^g with unit coefficient shifts the period filtration by N g: when exponents satisfy left cancellation, the coefficients of single g u * a vanish below N g + C exactly when those of a vanish below C.

theorem TauCeti.NovikovSeries.map_single_one_ne_one {R : Type u_1} {H : Type u_2} [AddGroup H] {N : H →+ ℝ} [Ring R] {F : Type u_3} {A : Type u_4} [Ring A] [Nontrivial A] [FunLike F (NovikovSeries R H N) A] [RingHomClass F (NovikovSeries R H N) A] (φ : F) {g : H} (hg : N g ≠ 0) : φ (single g 1) ≠ 1

No augmentation of a completed Novikov ring. A ring homomorphism out of the Novikov series to a nontrivial ring does not send a monomial e^g of nonzero period to 1. For N g > 0 it would send the unit 1 - e^g to 0; for N g < 0 it would also send the inverse monomial e^(-g), of positive period, to 1. In particular, as soon as the period map is nonzero, no ring homomorphism to a nontrivial ring sends every monomial to 1, even though the group ring of finitely supported series has such a homomorphism.