Completed combinations of torsor elements

For a potential F : S → ℝ, NovikovModule R F consists of coefficient functions on S with finite support above every potential threshold. It is a submodule of S → R, with the usual pointwise addition and ground-ring scalar multiplication. Finite combinations embed by NovikovModule.ofFinsupp, and NovikovModule.trunc C a is the finite combination keeping the coefficients of a at generators of potential > C. These two constructions adapt the approach of the unmerged TauCeti PR https://github.com/TauCetiProject/TauCeti/pull/20410.

Suppose S is a finite disjoint union of torsors P i under an additive group H, and F (h +ᵥ p) = F p - N h. Choosing one lift in each torsor identifies this completion with one Novikov series per orbit. Changing the lifts multiplies each coordinate on the right by the monomial of the old lift minus the new lift. In particular the completion retains the actual lifted generators, while the coordinate description depends on the chosen lifts. The transported Novikov scalar action is independent of those lifts. Its module laws and basis use Mathlib's AddEquiv.module and Pi.basisFun.

If H is trivial, each torsor is a single generator and no completion is needed (NovikovModule.eq_top_of_subsingleton).

The cutoff formulas include the potential of each chosen lift; they do not require an injective or discrete period map. These are the coefficient coordinates used for completed chains on an abelian cover, or for capped generators with an action functional.

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.NovikovModule (R : Type u_1) [Semiring R] {S : Type u_2} (F : S → ℝ) : Submodule R (S → R)

Completed R-linear combinations of S, finite above each threshold of the potential F. The scalar multiplication in this submodule is the ground-ring action.

@[simp]

theorem TauCeti.NovikovModule.mem_iff {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} {a : S → R} : a ∈ NovikovModule R F ↔ ∀ (C : ℝ), {s : S | a s ≠ 0 ∧ C < F s}.Finite

Membership is precisely finiteness of the nonzero coefficients above every potential threshold.

theorem TauCeti.NovikovModule.mem_of_finite_support {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} {a : S → R} (ha : (Function.support a).Finite) : a ∈ NovikovModule R F

A coefficient function with finite support is a completed combination.

theorem TauCeti.NovikovModule.eq_top_of_finite {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} [Finite S] : NovikovModule R F = ⊤

With finitely many generators no completion is needed: every coefficient function is a completed combination.

theorem TauCeti.NovikovModule.pi_single_mem {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} [DecidableEq S] (s : S) (r : R) : Pi.single s r ∈ NovikovModule R F

A point mass at a generator is a completed combination.

def TauCeti.NovikovModule.single {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} [DecidableEq S] (s : S) (r : R) : ↥(NovikovModule R F)

The point mass r at a generator s, as a completed combination.

@[simp]

theorem TauCeti.NovikovModule.single_val {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} [DecidableEq S] (s : S) (r : R) : ↑(single s r) = Pi.single s r

The coefficients of a point mass.

theorem TauCeti.NovikovModule.finite_gt {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (a : ↥(NovikovModule R F)) (C : ℝ) : {s : S | ↑a s ≠ 0 ∧ C < F s}.Finite

Only finitely many nonzero coefficients occur above any fixed potential threshold.

theorem TauCeti.NovikovModule.mem_iff_finite_ge {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} {a : S → R} : a ∈ NovikovModule R F ↔ ∀ (C : ℝ), {s : S | a s ≠ 0 ∧ C ≤ F s}.Finite

The support condition is unchanged if the potential cutoff is inclusive.

theorem TauCeti.NovikovModule.finite_ge {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (a : ↥(NovikovModule R F)) (C : ℝ) : {s : S | ↑a s ≠ 0 ∧ C ≤ F s}.Finite

A completed combination has only finitely many nonzero coefficients at or above a fixed potential threshold.

theorem TauCeti.NovikovModule.bddAbove_image_support {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (a : ↥(NovikovModule R F)) : BddAbove (F '' Function.support ↑a)

The potential is bounded above on the support of a completed combination.

def TauCeti.NovikovModule.ofFinsupp {R : Type u_1} [Semiring R] {S : Type u_2} (F : S → ℝ) : (S →₀ R) →ₗ[R] ↥(NovikovModule R F)

Finite combinations, viewed as completed combinations with the same coefficients.

@[simp]

theorem TauCeti.NovikovModule.ofFinsupp_apply_val {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (a : S →₀ R) (s : S) : ↑((ofFinsupp F) a) s = a s

theorem TauCeti.NovikovModule.ofFinsupp_injective {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} : Function.Injective ⇑(ofFinsupp F)

theorem TauCeti.NovikovModule.mem_range_ofFinsupp_iff {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} {a : ↥(NovikovModule R F)} : a ∈ (ofFinsupp F).range ↔ (Function.support ↑a).Finite

A completed combination is a finite combination exactly when it has finitely many nonzero coefficients.

noncomputable def TauCeti.NovikovModule.trunc {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (C : ℝ) (a : ↥(NovikovModule R F)) : S →₀ R

The truncation of a completed combination above the potential cutoff C: the finite combination keeping the coefficients of the generators of potential > C.

@[simp]

theorem TauCeti.NovikovModule.trunc_apply {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (C : ℝ) (a : ↥(NovikovModule R F)) (s : S) : (trunc C a) s = if C < F s then ↑a s else 0

theorem TauCeti.NovikovModule.trunc_apply_of_lt {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} {C : ℝ} {a : ↥(NovikovModule R F)} {s : S} (hs : C < F s) : (trunc C a) s = ↑a s

theorem TauCeti.NovikovModule.trunc_apply_of_le {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} {C : ℝ} {a : ↥(NovikovModule R F)} {s : S} (hs : F s ≤ C) : (trunc C a) s = 0

@[simp]

theorem TauCeti.NovikovModule.trunc_zero {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (C : ℝ) : trunc C 0 = 0

@[simp]

theorem TauCeti.NovikovModule.trunc_add {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (C : ℝ) (a b : ↥(NovikovModule R F)) : trunc C (a + b) = trunc C a + trunc C b

@[simp]

theorem TauCeti.NovikovModule.trunc_smul {R : Type u_1} [Semiring R] {S : Type u_2} {F : S → ℝ} (C : ℝ) (c : R) (a : ↥(NovikovModule R F)) : trunc C (c • a) = c • trunc C a

@[simp]

theorem TauCeti.NovikovModule.trunc_neg {S : Type u_2} {F : S → ℝ} {R : Type u_3} [Ring R] (C : ℝ) (a : ↥(NovikovModule R F)) : trunc C (-a) = -trunc C a

@[simp]

theorem TauCeti.NovikovModule.trunc_sub {S : Type u_2} {F : S → ℝ} {R : Type u_3} [Ring R] (C : ℝ) (a b : ↥(NovikovModule R F)) : trunc C (a - b) = trunc C a - trunc C b

theorem TauCeti.NovikovModule.eq_top_of_subsingleton {R : Type u_1} [Semiring R] (H : Type u_3) {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {F : (i : ι) × P i → ℝ} [Subsingleton H] : NovikovModule R F = ⊤

No completion is needed over a trivial group. With finitely many orbits, each a torsor under a trivial group and so a single generator, every coefficient function is a completed combination, whatever the potential F.

theorem TauCeti.NovikovModule.potential_eq_sub_vsub {H : Type u_3} {ι : Type u_4} [AddGroup H] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (i : ι) (p : P i) : F ⟨i, p⟩ = F ⟨i, r i⟩ - N (p -ᵥ r i)

The potential of a generator is its reference potential minus the period of its displacement.

theorem TauCeti.NovikovModule.mem_iff_forall_finite_vadd_lt {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (a : (i : ι) × P i → R) : a ∈ NovikovModule R F ↔ ∀ (i : ι) (C : ℝ), {h : H | a ⟨i, h +ᵥ r i⟩ ≠ 0 ∧ N h < C}.Finite

Finiteness above potential thresholds is equivalent to the Novikov support condition in every orbit, for any chosen lifts.

def TauCeti.NovikovModule.coordinates {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) : ↥(NovikovModule R F) ≃ₗ[R] ι → NovikovSeries R H N

Coordinates of a completed combination relative to one lift in each orbit. This is a ground-ring linear equivalence with a finite family of Novikov series.

@[simp]

theorem TauCeti.NovikovModule.coordinates_coeff {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (a : ↥(NovikovModule R F)) (i : ι) (h : H) : ((coordinates hF r) a i).coeff h = ↑a ⟨i, h +ᵥ r i⟩

The coefficient at exponent h is the coefficient of the generator h +ᵥ r i.

@[simp]

theorem TauCeti.NovikovModule.coordinates_symm_apply {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (b : ι → NovikovSeries R H N) (i : ι) (p : P i) : ↑((coordinates hF r).symm b) ⟨i, p⟩ = (b i).coeff (p -ᵥ r i)

Recover the coefficient of a lifted generator by subtracting its reference lift.

theorem TauCeti.NovikovModule.coordinates_coeff_eq_zero_iff {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (a : ↥(NovikovModule R F)) (C : ℝ) : (∀ (i : ι) (h : H), N h < F ⟨i, r i⟩ - C → ((coordinates hF r) a i).coeff h = 0) ↔ ∀ (s : (i : ι) × P i), C < F s → ↑a s = 0

The potential cutoff in an orbit is the period cutoff measured from its chosen lift.

theorem TauCeti.NovikovModule.coordinates_apply_eq_mul_single {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r r' : (i : ι) → P i) (a : ↥(NovikovModule R F)) (i : ι) : (coordinates hF r') a i = (coordinates hF r) a i * NovikovSeries.single (r i -ᵥ r' i) 1

Changing the reference lift translates the exponent by the old lift minus the new lift. Thus the matrix of a lift change is diagonal with monomial entries.

@[instance_reducible]

noncomputable def TauCeti.NovikovModule.module {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) : Module (NovikovSeries R H N) ↥(NovikovModule R F)

The Novikov module structure, transported using arbitrary orbit lifts. Install it with letI := NovikovModule.module (R := R) hF. Every choice of lifts is linear for this one structure by coordinates_smul.

theorem TauCeti.NovikovModule.coordinates_smul {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (b : NovikovSeries R H N) (a : ↥(NovikovModule R F)) : (coordinates hF r) (b • a) = b • (coordinates hF r) a

Novikov scalar multiplication is componentwise multiplication in any lift coordinates.

def TauCeti.NovikovModule.coordinatesLinearEquiv {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) : ↥(NovikovModule R F) ≃ₗ[NovikovSeries R H N] ι → NovikovSeries R H N

Coordinates in any chosen lifts form a Novikov-linear equivalence for the shared module structure.

@[simp]

theorem TauCeti.NovikovModule.coordinatesLinearEquiv_apply {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (a : ↥(NovikovModule R F)) : (coordinatesLinearEquiv hF r) a = (coordinates hF r) a

The Novikov-linear coordinate equivalence evaluates to the original coefficient coordinates.

@[simp]

theorem TauCeti.NovikovModule.coordinatesLinearEquiv_symm_apply {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (b : ι → NovikovSeries R H N) : (coordinatesLinearEquiv hF r).symm b = (coordinates hF r).symm b

The inverse Novikov-linear equivalence reconstructs the same coefficient function.

theorem TauCeti.NovikovModule.single_smul_apply {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (h : H) (c : R) (a : ↥(NovikovModule R F)) (i : ι) (p : P i) : ↑(NovikovSeries.single h c • a) ⟨i, p⟩ = c * ↑a ⟨i, -h +ᵥ p⟩

A monomial acts by deck translation, with its coefficient multiplying on the left.

noncomputable def TauCeti.NovikovModule.basis {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) : Module.Basis ι (NovikovSeries R H N) ↥(NovikovModule R F)

The basis of the completed module consisting of the chosen orbit lifts. This exhibits it as a finite free Novikov module.

@[simp]

theorem TauCeti.NovikovModule.coordinates_basis {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) [DecidableEq ι] (r : (i : ι) → P i) (i : ι) : (coordinates hF r) ((basis hF r) i) = Pi.single i 1

In lift coordinates, the basis vector for an orbit is the unit series in that orbit and zero in every other orbit.

@[simp]

theorem TauCeti.NovikovModule.basis_repr_apply {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r : (i : ι) → P i) (a : ↥(NovikovModule R F)) (i : ι) : ((basis hF r).repr a) i = (coordinates hF r) a i

Basis representation is precisely the Novikov coordinate series in each orbit.

theorem TauCeti.NovikovModule.basis_eq_single_smul {R : Type u_1} [Semiring R] {H : Type u_3} {ι : Type u_4} [AddGroup H] [Finite ι] {P : ι → Type u_5} [(i : ι) → AddTorsor H (P i)] {N : H →+ ℝ} {F : (i : ι) × P i → ℝ} (hF : ∀ (i : ι) (h : H) (p : P i), F ⟨i, h +ᵥ p⟩ = F ⟨i, p⟩ - N h) (r r' : (i : ι) → P i) (i : ι) : (basis hF r') i = NovikovSeries.single (r' i -ᵥ r i) 1 • (basis hF r) i

Changing a basis lift multiplies its basis vector on the left by the monomial of the new lift minus the old lift. Both bases belong to the same Novikov module.