Morse–Novikov homology and dynamical Reidemeister torsion
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
DefinitionTauCeti.NovikovSeries.completionPkg#
The Novikov series are the completion of the group ring H →₀ R for the uniform structure
of its period filtration: they are complete and separated, and the inclusion ofFinsupp is a
uniform inducing map with dense range.
TauCeti.NovikovSeries.completionPkg.{u_1, u_2} (R : Type u_1) (H : Type u_2) [AddZeroClass H]
(N : H →+ ℝ) [AddCommGroup R] : AbstractCompletion.{max u_2 u_1, max u_1 u_2} (H →₀ R)
TheoremTauCeti.NovikovSeries.isDomain_of_fg#
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.
TauCeti.NovikovSeries.isDomain_of_fg.{u_1, u_2} {R : Type u_1} {H : Type u_2} [Ring R] [IsDomain R]
[AddCancelCommMonoid H] [AddMonoid.FG H] [HasUniqueDiv H] (N : H →+ ℝ) :
IsDomain (TauCeti.NovikovSeries R H N)
DefinitionExponential 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.
TauCeti.NovikovSeries.expMulEquiv.{u_1, u_2} {H : Type u_1} (K : Type u_2) [AddCommMonoid H]
(N : H →+ ℝ) [CommRing K] [Algebra ℚ K] :
Multiplicative ↥(TauCeti.NovikovSeries.posIdeal K N) ≃*
↥(TauCeti.NovikovSeries.posIdeal K N).principalUnitGroup
TheoremMultiplicativity of the torsion#
Let 0 → C₁ → C₂ → C₃ → 0 be a short exact sequence of
chain complexes of vector spaces, with C₁ and C₃ acyclic, and with compatible bases: the basis
c₂ i of C₂ᵢ is the image of the basis c₁ i of C₁ᵢ followed by lifts of the basis c₃ i of
C₃ᵢ. Then τ(C₂) = ε · τ(C₁) · τ(C₃), with the sign ε = ∏ⱼ (-1) ^ (dim B₃,ⱼ₊₁ · dim B₁,ⱼ)
given by the dimensions of the boundaries Bₖ,ⱼ ⊆ Cₖ,ⱼ. This also holds when the complexes are
unbounded, both sides being 0.
HomologicalComplex.reidemeisterTorsion_eq_mul_of_shortExact.{u_1, u_2} {F : Type u_1} [Field F]
{S : CategoryTheory.ShortComplex (ChainComplex (ModuleCat F) ℤ)} (hS : S.ShortExact)
(h₁ : HomologicalComplex.Acyclic S.X₁) (h₃ : HomologicalComplex.Acyclic S.X₃) {n₁ n₃ : ℤ → ℕ}
(c₁ : (i : ℤ) → Module.Basis (Fin (n₁ i)) F ↑(S.X₁.X i))
(c₃ : (i : ℤ) → Module.Basis (Fin (n₃ i)) F ↑(S.X₃.X i))
(c₂ : (i : ℤ) → Module.Basis (Fin (n₁ i + n₃ i)) F ↑(S.X₂.X i))
(hc₁ :
∀ (i : ℤ) (k : Fin (n₁ i)),
(c₂ i) (Fin.castAdd (n₃ i) k) = (ModuleCat.Hom.hom (S.f.f i)) ((c₁ i) k))
(hc₃ :
∀ (i : ℤ) (k : Fin (n₃ i)),
(ModuleCat.Hom.hom (S.g.f i)) ((c₂ i) (Fin.natAdd (n₁ i) k)) = (c₃ i) k) :
HomologicalComplex.reidemeisterTorsion S.X₂ c₂ =
(∏ᶠ (j : ℤ),
(-1) ^
(Module.finrank F ↥(ModuleCat.Hom.hom (S.X₃.d (j + 1 + 1) (j + 1))).range *
Module.finrank F ↥(ModuleCat.Hom.hom (S.X₁.d (j + 1) j)).range)) *
(HomologicalComplex.reidemeisterTorsion S.X₁ c₁ *
HomologicalComplex.reidemeisterTorsion S.X₃ c₃)
Lean
Formalized in Tau Ceti as HomologicalComplex.reidemeisterTorsion_eq_mul_of_shortExact.
Sources
TheoremHomologicalComplex.reidemeisterTorsion_eq_zero_iff#
The torsion of a bounded based complex vanishes if and only if the complex is not acyclic.
HomologicalComplex.reidemeisterTorsion_eq_zero_iff.{u_1, u_2} {F : Type u_1} [Field F]
(C : ChainComplex (ModuleCat F) ℤ) {n : ℤ → ℕ} (c : (i : ℤ) → Module.Basis (Fin (n i)) F ↑(C.X i))
(hn : {i | n i ≠ 0}.Finite) :
HomologicalComplex.reidemeisterTorsion C c = 0 ↔ ¬HomologicalComplex.Acyclic C
Lean
Formalized in Tau Ceti as HomologicalComplex.reidemeisterTorsion_eq_zero_iff.
Sources
TheoremHomologicalComplex.reidemeisterTorsion_eq_mul_finprod_det#
The basis-change formula for the torsion: replacing the bases c i of C by c' i
multiplies the torsion by ∏ᵢ [c'ᵢ / cᵢ] ^ ((-1) ^ i), where [c'ᵢ / cᵢ] is the determinant of
c' i with respect to c i. This holds for every complex, both sides being 0 when C is
not acyclic or is unbounded.
HomologicalComplex.reidemeisterTorsion_eq_mul_finprod_det.{u_1, u_2} {F : Type u_1} [Field F]
(C : ChainComplex (ModuleCat F) ℤ) {n : ℤ → ℕ}
(c c' : (i : ℤ) → Module.Basis (Fin (n i)) F ↑(C.X i)) :
HomologicalComplex.reidemeisterTorsion C c' =
HomologicalComplex.reidemeisterTorsion C c * ∏ᶠ (i : ℤ), (c i).det ⇑(c' i) ^ ↑i.negOnePow
Lean
Formalized in Tau Ceti as HomologicalComplex.reidemeisterTorsion_eq_mul_finprod_det.
Sources
DefinitionTauCeti.NovikovSeries.mapRingHom#
The pushforward P_(ρ,φ) of Novikov series along a ring homomorphism ρ of coefficients and
an exponent homomorphism φ rescaling periods by a positive constant, as a ring homomorphism: the
coefficient at h' is the sum of the images under ρ of the coefficients at the exponents h
with φ h = h'.
TauCeti.NovikovSeries.mapRingHom.{u_1, u_2, u_4, u_5} {R : Type u_1} {S : Type u_2} {H : Type u_4}
{H' : Type u_5} [AddMonoid H] [AddMonoid H'] {N : H →+ ℝ} {N' : H' →+ ℝ} [Semiring R] [Semiring S]
(ρ : R →+* S) (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) :
TauCeti.NovikovSeries R H N →+* TauCeti.NovikovSeries S H' N'
DefinitionTauCeti.NovikovSeries.toLaurentSeries#
Novikov series on ℤ for the period map k ↦ k are the Laurent series: the ring isomorphism
which keeps every coefficient.
TauCeti.NovikovSeries.toLaurentSeries.{u_1} {R : Type u_1} [Semiring R] :
TauCeti.NovikovSeries R ℤ (Int.castAddHom ℝ) ≃+* LaurentSeries R
TheoremMatrix.continuous_mulVec_extension_iff#
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.
Matrix.continuous_mulVec_extension_iff.{u_1, u_2, u_3, u_4} {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 => TauCeti.NovikovSeries.ofAddMonoidAlgebra (v j)) = fun i =>
TauCeti.NovikovSeries.ofAddMonoidAlgebra (A.mulVec v i)) ↔
f = fun v => (A.map ⇑TauCeti.NovikovSeries.ofAddMonoidAlgebra).mulVec v
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.