Finite matrices over Novikov completions

Matrices with Novikov entries act on finite coordinate modules by ordinary matrix-vector multiplication. A common lower period bound on the entries gives a uniform filtration shift for the action. Such bounds exist for every finite matrix, add under composition, and give explicit finite truncations computing the action to any prescribed cutoff.

A group-ring matrix therefore has a unique continuous extension of its action to Novikov coordinate modules. The extension is multiplication by the matrix obtained by including each entry in the completion. Composition uses the native matrix API. When the coefficient and exponent structures are commutative, that API also supplies Novikov linearity. The cutoff estimates apply to matrices whose entries are infinite Novikov series, as arise from supported trajectory counts. No discreteness or injectivity of the period homomorphism is required.

For square matrices, row and column period shifts cancel in the determinant. The weighted determinant and perturbation estimates keep this cancellation explicit, avoiding any loss of cutoff from the choice of a monomial basis in finite extensions of Novikov rings.

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 Matrix.exists_forall_mem_periodFiltration {R : Type u_1} {H : Type u_2} {m : Type u_3} {n : Type u_4} [AddZeroClass H] [AddGroup R] [Finite m] [Finite n] {N : H →+ ℝ} (A : Matrix m n (TauCeti.NovikovSeries R H N)) : ∃ (C : ℝ), ∀ (i : m) (j : n), A i j ∈ TauCeti.NovikovSeries.periodFiltration R N C

Every finite Novikov matrix has a common lower period bound, including a matrix with no entries. Neither the coefficient ring nor the period map needs to be nontrivial.

theorem Matrix.mulVec_mem_periodFiltration {R : Type u_1} {H : Type u_2} {m : Type u_3} {n : Type u_4} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] [Fintype n] (A : Matrix m n (TauCeti.NovikovSeries R H N)) {C D : ℝ} (hA : ∀ (i : m) (j : n), A i j ∈ TauCeti.NovikovSeries.periodFiltration R N C) {v : n → TauCeti.NovikovSeries R H N} (hv : ∀ (j : n), v j ∈ TauCeti.NovikovSeries.periodFiltration R N D) (i : m) : A.mulVec v i ∈ TauCeti.NovikovSeries.periodFiltration R N (C + D)

A common lower period bound on matrix entries shifts the coordinatewise filtration by that bound under matrix-vector multiplication. The output index type need not be finite.

theorem Matrix.mul_mem_periodFiltration {R : Type u_1} {H : Type u_2} {m : Type u_3} {n : Type u_4} {p : Type u_5} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] [Fintype n] (A : Matrix m n (TauCeti.NovikovSeries R H N)) {C D : ℝ} (hA : ∀ (i : m) (j : n), A i j ∈ TauCeti.NovikovSeries.periodFiltration R N C) {B : Matrix n p (TauCeti.NovikovSeries R H N)} (hB : ∀ (j : n) (k : p), B j k ∈ TauCeti.NovikovSeries.periodFiltration R N D) (i : m) (k : p) : (A * B) i k ∈ TauCeti.NovikovSeries.periodFiltration R N (C + D)

Lower bounds for two matrices add under composition, uniformly in both outside indices.

theorem Matrix.mulVec_sub_mulVec_mem_periodFiltration {R : Type u_1} {H : Type u_2} {m : Type u_3} {n : Type u_4} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] [Fintype n] (A : Matrix m n (TauCeti.NovikovSeries R H N)) {A' : Matrix m n (TauCeti.NovikovSeries R H N)} {v v' : n → TauCeti.NovikovSeries R H N} {C D L : ℝ} (hA : ∀ (i : m) (j : n), A i j ∈ TauCeti.NovikovSeries.periodFiltration R N C) (hv' : ∀ (j : n), v' j ∈ TauCeti.NovikovSeries.periodFiltration R N D) (hAA' : ∀ (i : m) (j : n), A i j - A' i j ∈ TauCeti.NovikovSeries.periodFiltration R N (L - D)) (hvv' : ∀ (j : n), v j - v' j ∈ TauCeti.NovikovSeries.periodFiltration R N (L - C)) (i : m) : A.mulVec v i - A'.mulVec v' i ∈ TauCeti.NovikovSeries.periodFiltration R N L

Perturbing a matrix and an input vector at the indicated cutoffs changes their product only above the requested output cutoff. The two unperturbed lower bounds are asymmetric, just as in the scalar identity a * v - a' * v' = a * (v - v') + (a - a') * v'.

theorem Matrix.mulVec_sub_mulVec_trunc_mem_periodFiltration {R : Type u_1} {H : Type u_2} {m : Type u_3} {n : Type u_4} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] [Fintype n] (A : Matrix m n (TauCeti.NovikovSeries R H N)) {v : n → TauCeti.NovikovSeries R H N} {C D : ℝ} (hA : ∀ (i : m) (j : n), A i j ∈ TauCeti.NovikovSeries.periodFiltration R N C) (hv : ∀ (j : n), v j ∈ TauCeti.NovikovSeries.periodFiltration R N D) (L : ℝ) (i : m) : A.mulVec v i - (A.map fun (a : TauCeti.NovikovSeries R H N) => TauCeti.NovikovSeries.ofFinsupp (TauCeti.NovikovSeries.trunc (L - D) a)).mulVec (fun (j : n) => TauCeti.NovikovSeries.ofFinsupp (TauCeti.NovikovSeries.trunc (L - C) (v j))) i ∈ TauCeti.NovikovSeries.periodFiltration R N L

A matrix action below L can be computed using only the finite truncations of its entries below L - D and of its input below L - C. This retains every tied exponent even for a dense or noninjective period map.

theorem Matrix.exists_mulVec_filtration_shift {R : Type u_1} {H : Type u_2} {m : Type u_3} {n : Type u_4} [AddZeroClass H] {N : H →+ ℝ} [NonUnitalNonAssocRing R] [Fintype n] [Finite m] (A : Matrix m n (TauCeti.NovikovSeries R H N)) : ∃ (C : ℝ), ∀ (D : ℝ) (v : n → TauCeti.NovikovSeries R H N), (∀ (j : n), v j ∈ TauCeti.NovikovSeries.periodFiltration R N D) → ∀ (i : m), A.mulVec v i ∈ TauCeti.NovikovSeries.periodFiltration R N (C + D)

A finite matrix has a single filtration shift that works for all input cutoffs and vectors. This supplies the uniform support estimate used for completed differentials and homotopies.

theorem Matrix.continuous_mulVec_extension_iff {R : Type u_1} {H : Type u_2} {m : Type u_3} {n : Type u_4} [AddMonoid H] [Ring R] [Fintype n] (A : Matrix m n (AddMonoidAlgebra R H)) (N : H →+ ℝ) (f : (n → TauCeti.NovikovSeries R H N) → m → TauCeti.NovikovSeries R H N) : (Continuous f ∧ ∀ (v : n → AddMonoidAlgebra R H), (f fun (j : n) => TauCeti.NovikovSeries.ofAddMonoidAlgebra (v j)) = fun (i : m) => TauCeti.NovikovSeries.ofAddMonoidAlgebra (A.mulVec v i)) ↔ f = fun (v : n → TauCeti.NovikovSeries R H N) => (A.map ⇑TauCeti.NovikovSeries.ofAddMonoidAlgebra).mulVec v

A matrix over the group ring has a unique continuous extension of its action to completed coordinate modules. Its entries are included coefficientwise in the Novikov ring. No topology on the group ring is needed to state this uniqueness property.

theorem Matrix.det_mem_periodFiltration_of_weights {R : Type u_1} {H : Type u_2} {n : Type u_4} [AddCommMonoid H] {N : H →+ ℝ} [CommRing R] [Fintype n] [DecidableEq n] (A : Matrix n n (TauCeti.NovikovSeries R H N)) (w : n → ℝ) {D : ℝ} (hA : ∀ (i j : n), A i j ∈ TauCeti.NovikovSeries.periodFiltration R N (D + w j - w i)) : A.det ∈ TauCeti.NovikovSeries.periodFiltration R N (↑(Fintype.card n) * D)

Row and column period shifts cancel in the determinant. Thus an entrywise bound D + w j - w i gives the determinant bound card n * D.

theorem Matrix.det_sub_det_mem_periodFiltration_of_weights {R : Type u_1} {H : Type u_2} {n : Type u_4} [AddCommMonoid H] {N : H →+ ℝ} [CommRing R] [Fintype n] [DecidableEq n] (A B : Matrix n n (TauCeti.NovikovSeries R H N)) (w : n → ℝ) {C D : ℝ} (hA : ∀ (i j : n), A i j ∈ TauCeti.NovikovSeries.periodFiltration R N (D + w j - w i)) (hB : ∀ (i j : n), B i j ∈ TauCeti.NovikovSeries.periodFiltration R N (D + w j - w i)) (hAB : ∀ (i j : n), A i j - B i j ∈ TauCeti.NovikovSeries.periodFiltration R N (C + (D + w j - w i))) : A.det - B.det ∈ TauCeti.NovikovSeries.periodFiltration R N (C + ↑(Fintype.card n) * D)

A weighted entrywise perturbation changes a determinant only above the corresponding cutoff. No sign or nonzero-divisor assumption on the coefficients is needed.