Exponential and logarithm of Novikov series

Let K be a commutative ℚ-algebra, H an additive commutative monoid and N : H →+ ℝ a period homomorphism. The nonnegative subring of the Novikov ring Nov(K, H, N) is a complete, separated, linearly topologized ℚ-algebra, and the series of its positive ideal are topologically nilpotent. So the general theory of the exponential and logarithm of topologically nilpotent elements applies (TauCeti/Topology/Algebra/TopologicallyNilpotent/ExpLog.lean): for a in the positive ideal, the series of Mathlib's exponential NormedSpace.exp and logarithm NormedSpace.log

exp a = ∑ aⁿ / n!, log (1 + a) = ∑ (-1)ⁿ⁺¹ aⁿ / n

converge in the period topology, and the exponential is an isomorphism from the additive group of the positive ideal onto its principal unit group of units u with u - 1 in the positive ideal, with inverse the logarithm (TauCeti.NovikovSeries.expMulEquiv). The dynamical zeta function of a closed one-form is defined as the exponential of a rational logarithmic series of periodic orbits lying in the positive ideal; by this isomorphism it is a principal unit.

The degree derivations of TauCeti/RingTheory/NovikovSeries/Derivation.lean are continuous, so they differentiate the logarithm of a principal unit logarithmically: u * D (log u) = D u (TauCeti.NovikovSeries.mul_degreeDerivation_log).

Main definitions

• TauCeti.NovikovSeries.expMulEquiv: the exponential, as an isomorphism from the additive group of the positive ideal onto its principal unit group, with inverse the logarithm.

Main results

• TauCeti.NovikovSeries.coe_exp_of_mem_posIdeal: the exponential of a series of the positive ideal does not depend on whether it is computed in the nonnegative subring or in the Novikov ring.
• TauCeti.NovikovSeries.mul_degreeDerivation_log: the logarithmic derivative of the logarithm along a degree derivation.

References

• M. Hutchings and Y.-J. Lee, Circle-valued Morse theory and Reidemeister torsion, Geom. Topol. 3 (1999), Section 2.

noncomputable def TauCeti.NovikovSeries.expMulEquiv {H : Type u_1} (K : Type u_2) [AddCommMonoid H] (N : H →+ ℝ) [CommRing K] [Algebra ℚ K] : Multiplicative ↥(posIdeal K N) ≃* ↥(posIdeal K N).principalUnitGroup

Exponential and logarithm of Novikov series: over a ℚ-algebra K, the exponential is an isomorphism from the additive group of the positive ideal onto its principal unit group in the nonnegative subring, with inverse the logarithm. This is Ideal.expMulEquiv for the positive ideal, whose series are topologically nilpotent.

@[simp]

theorem TauCeti.NovikovSeries.coe_expMulEquiv_apply {H : Type u_1} {K : Type u_2} [AddCommMonoid H] {N : H →+ ℝ} [CommRing K] [Algebra ℚ K] (a : ↥(posIdeal K N)) : ↑↑((expMulEquiv K N) (Multiplicative.ofAdd a)) = NormedSpace.exp ↑a

TauCeti.NovikovSeries.expMulEquiv sends a to the unit exp a.

@[simp]

theorem TauCeti.NovikovSeries.coe_expMulEquiv_symm_apply {H : Type u_1} {K : Type u_2} [AddCommMonoid H] {N : H →+ ℝ} [CommRing K] [Algebra ℚ K] (u : ↥(posIdeal K N).principalUnitGroup) : ↑(Multiplicative.toAdd ((expMulEquiv K N).symm u)) = NormedSpace.log ↑↑u

The inverse of TauCeti.NovikovSeries.expMulEquiv sends a unit u to log u.

theorem TauCeti.NovikovSeries.coe_exp_of_mem_posIdeal {H : Type u_1} {K : Type u_2} [AddCommMonoid H] {N : H →+ ℝ} [CommRing K] [Algebra ℚ K] {a : ↥(nonnegSubring K N)} (ha : a ∈ posIdeal K N) : ↑(NormedSpace.exp a) = NormedSpace.exp ↑a

The exponential of a series of the positive ideal is the same whether it is computed in the nonnegative subring or in the Novikov ring.

theorem TauCeti.NovikovSeries.mul_degreeDerivation_log {H : Type u_1} {K : Type u_2} [AddCommMonoid H] {N : H →+ ℝ} [CommRing K] [Algebra ℚ K] (ℓ : H →+ K) {u : ↥(nonnegSubring K N)} (hu : u - 1 ∈ posIdeal K N) : ↑u * (degreeDerivation ℓ) ↑(NormedSpace.log u) = (degreeDerivation ℓ) ↑u

A degree derivation differentiates the logarithm of a principal unit of the nonnegative subring logarithmically: u * D (log u) = D u, read in the Novikov series.