Leading terms of Novikov series, and Novikov rings without zero divisors

Let H be an additive monoid with a period homomorphism N : H →+ ℝ. A nonzero Novikov series a attains a least period on its support; this is its order a.order (TauCeti.NovikovSeries.order). Since N need not be injective, finitely many nonzero coefficients may share this least period. The leading term a.leadingTerm keeps all of them: it is the element of the group ring R[H] with the coefficients of a at the exponents of period a.order, and 0 elsewhere. Its exponents all have the same period, so when H is a group they lie in a single coset h + ker N, and the leading term is a monomial e^h times an element of the group ring of the period kernel.

Periods add under convolution, so the product a * b has no nonzero coefficient below the period a.order + b.order, and at that period its coefficients are those of the group-ring product a.leadingTerm * b.leadingTerm. Hence, whenever this product of leading terms is nonzero, it is the leading term of a * b, and orders add. If the group ring R[H] has no zero divisors, then neither has the Novikov ring. By Mathlib's AffineAddMonoid.to_twoUniqueSums, this applies when R is a domain and H is a finitely generated torsion-free abelian group, so the Novikov ring is then a domain. Ties in the period are retained throughout: nothing here assumes that N is injective.

Main definitions

• TauCeti.NovikovSeries.leadingTerm: the coefficients of least period, as an element of the group ring.

Main results

• TauCeti.NovikovSeries.coeff_mul_eq_zero_of_lt_order_add and TauCeti.NovikovSeries.coeff_mul_of_period_eq_order_add: below the period a.order + b.order the product a * b vanishes, and at that period its coefficients are those of the product of the leading terms.
• TauCeti.NovikovSeries.leadingTerm_mul_of_ne_zero and TauCeti.NovikovSeries.order_mul_of_leadingTerm_mul_ne_zero: a nonzero product of leading terms is the leading term of the product, and then orders add.
• TauCeti.NovikovSeries.leadingTerm_mul and TauCeti.NovikovSeries.order_mul: when R[H] has no zero divisors, the leading term is multiplicative without side condition, and the orders of two nonzero series add.
• The instances NoZeroDivisors and IsDomain: the Novikov ring inherits the absence of zero divisors from the group ring.
• TauCeti.NovikovSeries.isDomain_of_fg: over a domain, the Novikov ring of a finitely generated torsion-free abelian group, or more generally of a finitely generated cancellative torsion-free commutative monoid, is a domain.

References

• A. Pajitnov, Circle-valued Morse Theory, de Gruyter 2006, Chapter 3.
• M. Hutchings, Reidemeister torsion in generalized Morse theory, Forum Math. 14 (2002), Section 2.

noncomputable def TauCeti.NovikovSeries.leadingTerm {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Semiring R] (a : NovikovSeries R H N) : AddMonoidAlgebra R H

The leading term of a Novikov series: the element of the group ring R[H] with the coefficients of the series at the exponents whose period is the order, and 0 elsewhere. Since the period map need not be injective, it may have several nonzero coefficients.

@[simp]

theorem TauCeti.NovikovSeries.coeff_leadingTerm {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Semiring R] (a : NovikovSeries R H N) (h : H) : a.leadingTerm.coeff h = if N h = a.order then a.coeff h else 0

theorem TauCeti.NovikovSeries.period_eq_order_of_coeff_leadingTerm_ne_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Semiring R] {a : NovikovSeries R H N} {h : H} (hh : a.leadingTerm.coeff h ≠ 0) : N h = a.order

The exponents of the leading term all have period equal to the order.

theorem TauCeti.NovikovSeries.coeff_ne_zero_of_coeff_leadingTerm_ne_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Semiring R] {a : NovikovSeries R H N} {h : H} (hh : a.leadingTerm.coeff h ≠ 0) : a.coeff h ≠ 0

@[simp]

theorem TauCeti.NovikovSeries.leadingTerm_eq_zero_iff {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Semiring R] {a : NovikovSeries R H N} : a.leadingTerm = 0 ↔ a = 0

@[simp]

theorem TauCeti.NovikovSeries.leadingTerm_zero {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Semiring R] : leadingTerm 0 = 0

@[simp]

theorem TauCeti.NovikovSeries.leadingTerm_single {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Semiring R] (h : H) (r : R) : (single h r).leadingTerm = AddMonoidAlgebra.single h r

@[simp]

theorem TauCeti.NovikovSeries.leadingTerm_neg {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [Ring R] (a : NovikovSeries R H N) : (-a).leadingTerm = -a.leadingTerm

theorem TauCeti.NovikovSeries.coeff_mul_eq_zero_of_lt_order_add {R : Type u_1} {H : Type u_2} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] {a b : NovikovSeries R H N} {h : H} (hh : N h < a.order + b.order) : (a * b).coeff h = 0

A product of Novikov series has no nonzero coefficient below the sum of the orders.

theorem TauCeti.NovikovSeries.coeff_mul_of_period_eq_order_add {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Semiring R] {a b : NovikovSeries R H N} {h : H} (hh : N h = a.order + b.order) : (a * b).coeff h = (a.leadingTerm * b.leadingTerm).coeff h

At an exponent of period a.order + b.order, the coefficient of a * b is that of the group-ring product of the leading terms.

theorem TauCeti.NovikovSeries.order_mul_of_leadingTerm_mul_ne_zero {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Semiring R] {a b : NovikovSeries R H N} (hab : a.leadingTerm * b.leadingTerm ≠ 0) : (a * b).order = a.order + b.order

If the product of the leading terms of a and b is nonzero, the orders add.

theorem TauCeti.NovikovSeries.leadingTerm_mul_of_ne_zero {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Semiring R] {a b : NovikovSeries R H N} (hab : a.leadingTerm * b.leadingTerm ≠ 0) : (a * b).leadingTerm = a.leadingTerm * b.leadingTerm

If the product of the leading terms of a and b is nonzero, it is the leading term of a * b.

@[simp]

theorem TauCeti.NovikovSeries.leadingTerm_mul {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Semiring R] [NoZeroDivisors (AddMonoidAlgebra R H)] (a b : NovikovSeries R H N) : (a * b).leadingTerm = a.leadingTerm * b.leadingTerm

If the group ring has no zero divisors, the leading term is multiplicative.

theorem TauCeti.NovikovSeries.order_mul {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Semiring R] {a b : NovikovSeries R H N} [NoZeroDivisors (AddMonoidAlgebra R H)] (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).order = a.order + b.order

If the group ring has no zero divisors, the orders of nonzero Novikov series add under multiplication.

instance TauCeti.NovikovSeries.instNoZeroDivisors {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Semiring R] [NoZeroDivisors (AddMonoidAlgebra R H)] : NoZeroDivisors (NovikovSeries R H N)

If the group ring R[H] has no zero divisors, then neither has the Novikov ring.

instance TauCeti.NovikovSeries.instIsDomain {R : Type u_1} {H : Type u_2} [AddMonoid H] {N : H →+ ℝ} [Ring R] [Nontrivial R] [NoZeroDivisors (AddMonoidAlgebra R H)] : IsDomain (NovikovSeries R H N)

If the group ring R[H] over a nontrivial ring has no zero divisors, the Novikov ring is a domain.

theorem TauCeti.NovikovSeries.isDomain_of_fg {R : Type u_1} {H : Type u_2} [Ring R] [IsDomain R] [AddCancelCommMonoid H] [AddMonoid.FG H] [HasUniqueDiv H] (N : H →+ ℝ) : IsDomain (NovikovSeries R H N)

Over a domain, the Novikov ring of a finitely generated cancellative torsion-free commutative monoid, for instance of a finitely generated torsion-free abelian group, is a domain for every period homomorphism.