Convolution of Novikov series

Let H be an additive monoid with a period homomorphism N : H →+ ℝ. The product of two Novikov series a and b is their convolution (a * b).coeff h = ∑ a.coeff u * b.coeff v, the sum running over the pairs (u, v) with u + v = h and both coefficients nonzero. There are only finitely many such pairs (NovikovSeries.finite_setOf_add_eq), because the periods of each support are bounded below and only finitely many exponents of a series lie below any period cutoff. With this product the Novikov series form a ring, the Novikov completion of the group ring R[H] along the period filtration: it is the coefficient ring of the Novikov complex of a closed one-form and of capped Hamiltonian Floer complexes.

All ring laws are proved by finite-support arguments. The basic tool is NovikovSeries.coeff_mul_eq_sum: a coefficient of a product may be computed as a sum over any finite set of pairs adding up to the exponent which contains every pair of support exponents. Associativity rests on the uniform cutoff lemma NovikovSeries.finite_setOf_period_add_add_lt for triples of support exponents, from TauCeti.RingTheory.NovikovSeries.Basic.

The arrangement of the instances follows Mathlib's HahnSeries in Mathlib/RingTheory/HahnSeries/Multiplication.lean; the support arguments are different, since H carries no order here.

Main definitions

• TauCeti.NovikovSeries.instMul: the convolution product.
• TauCeti.NovikovSeries.instSemiring, TauCeti.NovikovSeries.instCommRing, ...: the (commutative) (semi)ring structures, with unit the monomial single 0 1.
• TauCeti.NovikovSeries.instAlgebra: for an S-algebra R, Novikov series over R form an S-algebra, with algebraMap S _ s = single 0 (algebraMap S R s).
• TauCeti.NovikovSeries.coeffZeroRingEquiv: over a trivial exponent group, Novikov series are identified with their constant coefficients.
• TauCeti.NovikovSeries.ofAddMonoidAlgebra: the group ring R[H] as a subring of Novikov series, by its coefficient map.

Main results

• TauCeti.NovikovSeries.coeff_mul_eq_sum: computing a coefficient of a product over any finite set of pairs containing the pairs of support exponents.
• TauCeti.NovikovSeries.support_mul_subset: the support of a product lies in the sum of the supports.
• TauCeti.NovikovSeries.single_mul_single and TauCeti.NovikovSeries.single_pow: monomials multiply by adding exponents.
• TauCeti.NovikovSeries.unitsSingle, TauCeti.NovikovSeries.isUnit_single: over an additive group, a monomial u e^g with unit coefficient is a unit, with inverse u⁻¹ e^(-g).
• TauCeti.NovikovSeries.ofAddMonoidAlgebra_injective: the group ring embeds into Novikov series, and TauCeti.NovikovSeries.mem_range_ofAddMonoidAlgebra_iff identifies its image as the series of finite support. Over an additive group H and for nontrivial R, by TauCeti.NovikovSeries.ofFinsupp_surjective_iff this embedding is onto exactly when N = 0.

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.
• H. Hofer and D. A. Salamon, Floer homology and Novikov rings, in The Floer memorial volume, Progr. Math. 133 (1995), 483–524.

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instMul {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] : Mul (NovikovSeries R H N)

The convolution product of Novikov series: the coefficient of a * b at h is the finite sum of a.coeff u * b.coeff v over the pairs (u, v) of support exponents with u + v = h.

theorem TauCeti.NovikovSeries.coeff_mul {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (a b : NovikovSeries R H N) (h : H) : (a * b).coeff h = ∑ p ∈ ⋯.toFinset, a.coeff p.1 * b.coeff p.2

The coefficient of a * b at h, as a sum over the finite set of pairs of support exponents adding up to h.

theorem TauCeti.NovikovSeries.coeff_mul_eq_sum {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] {a b : NovikovSeries R H N} {h : H} {s : Finset (H × H)} (hs : ∀ p ∈ s, p.1 + p.2 = h) (hab : ∀ (u v : H), u + v = h → a.coeff u ≠ 0 → b.coeff v ≠ 0 → (u, v) ∈ s) : (a * b).coeff h = ∑ p ∈ s, a.coeff p.1 * b.coeff p.2

A coefficient of a product is the sum of a.coeff p.1 * b.coeff p.2 over any finite set of pairs p with p.1 + p.2 = h containing every such pair of support exponents.

theorem TauCeti.NovikovSeries.exists_add_eq_of_coeff_mul_ne_zero {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] {a b : NovikovSeries R H N} {h : H} (hab : (a * b).coeff h ≠ 0) : ∃ (u : H) (v : H), u + v = h ∧ a.coeff u ≠ 0 ∧ b.coeff v ≠ 0

A nonzero coefficient of a product comes from a pair of support exponents.

theorem TauCeti.NovikovSeries.support_mul_subset {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (a b : NovikovSeries R H N) : (a * b).support ⊆ a.support + b.support

The support of a product lies in the sum of the supports.

theorem TauCeti.NovikovSeries.coeff_mul_eq_sum_of_injOn {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] {ι : Type u_4} {a b : NovikovSeries R H N} {h : H} {F : Finset ι} {f : ι → H × H} (hf : ∀ t ∈ F, (f t).1 + (f t).2 = h) (hab : ∀ (u v : H), u + v = h → a.coeff u ≠ 0 → b.coeff v ≠ 0 → ∃ t ∈ F, f t = (u, v)) (hinj : Set.InjOn f ↑F) : (a * b).coeff h = ∑ t ∈ F, a.coeff (f t).1 * b.coeff (f t).2

A coefficient of a product as a sum over a finite set F, mapped injectively by f onto a set of pairs adding up to h which contains every pair of support exponents.

@[simp]

theorem TauCeti.NovikovSeries.single_mul_single {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (g g' : H) (r r' : R) : single g r * single g' r' = single (g + g') (r * r')

Monomials multiply by adding exponents.

theorem TauCeti.NovikovSeries.coeff_single_zero_mul {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (r : R) (a : NovikovSeries R H N) (h : H) : (single 0 r * a).coeff h = r * a.coeff h

Multiplying by a constant series single 0 r multiplies each coefficient on the left.

@[simp]

theorem TauCeti.NovikovSeries.single_zero_mul_eq_smul {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (r : R) (a : NovikovSeries R H N) : single 0 r * a = r • a

Multiplying by a constant series is scalar multiplication.

@[simp]

theorem TauCeti.NovikovSeries.coeff_mul_single_zero {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (a : NovikovSeries R H N) (r : R) (h : H) : (a * single 0 r).coeff h = a.coeff h * r

Multiplying by a constant series single 0 r multiplies each coefficient on the right.

theorem TauCeti.NovikovSeries.coeff_single_mul_add {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] [IsLeftCancelAdd H] (g : H) (r : R) (a : NovikovSeries R H N) (h : H) : (single g r * a).coeff (g + h) = r * a.coeff h

Multiplying on the left by the monomial r e^g shifts the exponents by g.

theorem TauCeti.NovikovSeries.coeff_mul_single_add {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] [IsRightCancelAdd H] (a : NovikovSeries R H N) (g : H) (r : R) (h : H) : (a * single g r).coeff (h + g) = a.coeff h * r

Multiplying on the right by the monomial r e^g shifts the exponents by g.

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonUnitalNonAssocSemiring {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (NovikovSeries R H N)

Convolution distributes over addition.

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instOne {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [One R] : One (NovikovSeries R H N)

The unit of convolution is the monomial single 0 1.

theorem TauCeti.NovikovSeries.one_def {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [One R] : 1 = single 0 1

@[simp]

theorem TauCeti.NovikovSeries.single_zero_one {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [One R] : single 0 1 = 1

@[simp]

theorem TauCeti.NovikovSeries.coeff_one {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [Zero R] [One R] [DecidableEq H] (h : H) : coeff 1 h = if h = 0 then 1 else 0

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonAssocSemiring {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonAssocSemiring R] : NonAssocSemiring (NovikovSeries R H N)

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonUnitalNonAssocRing {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (NovikovSeries R H N)

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonAssocRing {R : Type u_1} {H : Type u_3} [AddZeroClass H] {N : H →+ ℝ} [NonAssocRing R] : NonAssocRing (NovikovSeries R H N)

theorem TauCeti.NovikovSeries.coeff_mul_mul_eq_sum {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [NonUnitalSemiring R] (a b c : NovikovSeries R H N) (h : H) : (a * b * c).coeff h = ∑ t ∈ ⋯.toFinset, a.coeff t.1 * b.coeff t.2.1 * c.coeff t.2.2

The coefficient at h of a triple product a * b * c is the sum of a.coeff u * b.coeff v * c.coeff w over the finitely many triples of support exponents with u + v + w = h.

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonUnitalSemiring {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [NonUnitalSemiring R] : NonUnitalSemiring (NovikovSeries R H N)

Convolution is associative, by the uniform cutoff lemma NovikovSeries.finite_setOf_period_add_add_lt.

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instSemiring {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Semiring R] : Semiring (NovikovSeries R H N)

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonUnitalRing {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [NonUnitalRing R] : NonUnitalRing (NovikovSeries R H N)

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instRing {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Ring R] : Ring (NovikovSeries R H N)

@[simp]

theorem TauCeti.NovikovSeries.single_pow {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Semiring R] (g : H) (r : R) (n : ℕ) : single g r ^ n = single (n • g) (r ^ n)

The powers of a monomial: (r e^g) ^ n = r ^ n e^(n • g).

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonUnitalCommSemiring {R : Type u_1} {H : Type u_3} [AddCommMonoid H] {N : H →+ ℝ} [NonUnitalCommSemiring R] : NonUnitalCommSemiring (NovikovSeries R H N)

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instCommSemiring {R : Type u_1} {H : Type u_3} [AddCommMonoid H] {N : H →+ ℝ} [CommSemiring R] : CommSemiring (NovikovSeries R H N)

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instNonUnitalCommRing {R : Type u_1} {H : Type u_3} [AddCommMonoid H] {N : H →+ ℝ} [NonUnitalCommRing R] : NonUnitalCommRing (NovikovSeries R H N)

@[instance_reducible]

noncomputable instance TauCeti.NovikovSeries.instCommRing {R : Type u_1} {H : Type u_3} [AddCommMonoid H] {N : H →+ ℝ} [CommRing R] : CommRing (NovikovSeries R H N)

theorem TauCeti.NovikovSeries.coeff_single_mul {R : Type u_1} {H : Type u_3} [AddGroup H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (g : H) (r : R) (a : NovikovSeries R H N) (h : H) : (single g r * a).coeff h = r * a.coeff (-g + h)

Multiplying on the left by a monomial shifts the exponents.

theorem TauCeti.NovikovSeries.coeff_mul_single {R : Type u_1} {H : Type u_3} [AddGroup H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (a : NovikovSeries R H N) (g : H) (r : R) (h : H) : (a * single g r).coeff h = a.coeff (h - g) * r

Multiplying on the right by a monomial shifts the exponents.

noncomputable def TauCeti.NovikovSeries.unitsSingle {R : Type u_1} {H : Type u_3} [AddGroup H] {N : H →+ ℝ} [Semiring R] (g : H) (u : Rˣ) : (NovikovSeries R H N)ˣ

The monomial u e^g with unit coefficient u, as a unit with inverse u⁻¹ e^(-g).

@[simp]

theorem TauCeti.NovikovSeries.val_unitsSingle {R : Type u_1} {H : Type u_3} [AddGroup H] {N : H →+ ℝ} [Semiring R] (g : H) (u : Rˣ) : ↑(unitsSingle g u) = single g ↑u

The underlying series of unitsSingle g u is the monomial u e^g.

@[simp]

theorem TauCeti.NovikovSeries.val_inv_unitsSingle {R : Type u_1} {H : Type u_3} [AddGroup H] {N : H →+ ℝ} [Semiring R] (g : H) (u : Rˣ) : ↑(unitsSingle g u)⁻¹ = single (-g) ↑u⁻¹

The inverse of unitsSingle g u is the monomial u⁻¹ e^(-g).

theorem TauCeti.NovikovSeries.isUnit_single {R : Type u_1} {H : Type u_3} [AddGroup H] {N : H →+ ℝ} [Semiring R] (g : H) {r : R} (hr : IsUnit r) : IsUnit (single g r)

A monomial r e^g with unit coefficient is a unit.

@[instance_reducible]

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

For an S-algebra R, Novikov series over R form an S-algebra: a scalar s acts as the constant series single 0 (algebraMap S R s).

@[simp]

theorem TauCeti.NovikovSeries.algebraMap_apply {R : Type u_1} {S : Type u_2} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [CommSemiring S] [Semiring R] [Algebra S R] (s : S) : (algebraMap S (NovikovSeries R H N)) s = single 0 ((algebraMap S R) s)

def TauCeti.NovikovSeries.ofAddMonoidAlgebra {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Semiring R] : AddMonoidAlgebra R H →+* NovikovSeries R H N

The group ring R[H] as a subring of Novikov series: an element is sent to the Novikov series with the same (finitely supported) coefficients.

@[simp]

theorem TauCeti.NovikovSeries.coeff_ofAddMonoidAlgebra {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Semiring R] (x : AddMonoidAlgebra R H) : (ofAddMonoidAlgebra x).coeff = ⇑x.coeff

@[simp]

theorem TauCeti.NovikovSeries.ofAddMonoidAlgebra_single {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Semiring R] (h : H) (r : R) : ofAddMonoidAlgebra (AddMonoidAlgebra.single h r) = single h r

theorem TauCeti.NovikovSeries.ofAddMonoidAlgebra_injective {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Semiring R] : Function.Injective ⇑ofAddMonoidAlgebra

theorem TauCeti.NovikovSeries.mem_range_ofAddMonoidAlgebra_iff {R : Type u_1} {H : Type u_3} [AddMonoid H] {N : H →+ ℝ} [Semiring R] {a : NovikovSeries R H N} : a ∈ Set.range ⇑ofAddMonoidAlgebra ↔ a.support.Finite

A Novikov series comes from the group ring exactly when its support is finite.

noncomputable def TauCeti.NovikovSeries.coeffZeroRingEquiv {R : Type u_1} {H : Type u_3} [AddZeroClass H] [Subsingleton H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] : NovikovSeries R H N ≃+* R

Novikov series over a trivial exponent group are their constant coefficients. Taking the coefficient at 0 is a ring isomorphism onto R, with inverse r ↦ single 0 r.

@[simp]

theorem TauCeti.NovikovSeries.coeffZeroRingEquiv_apply {R : Type u_1} {H : Type u_3} [AddZeroClass H] [Subsingleton H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (a : NovikovSeries R H N) : coeffZeroRingEquiv a = a.coeff 0

@[simp]

theorem TauCeti.NovikovSeries.coeffZeroRingEquiv_symm_apply {R : Type u_1} {H : Type u_3} [AddZeroClass H] [Subsingleton H] {N : H →+ ℝ} [NonUnitalNonAssocSemiring R] (r : R) : coeffZeroRingEquiv.symm r = single 0 r