Documentation

TauCeti.RingTheory.NovikovSeries.Grading

Homogeneous Novikov series #

Let f : H → ι be a degree function on the exponents of Novikov series. A Novikov series is homogeneous of degree i when its support lies in the fibre f ⁻¹' {i}. These series form the submodule TauCeti.NovikovSeries.gradeBy R N f i, the Novikov analogue of Mathlib's AddMonoidAlgebra.gradeBy. For an additive degree function the pieces multiply as a graded monoid, and they are independent.

Unlike the group ring, the Novikov ring is in general not the direct sum of its homogeneous pieces: a series whose support meets infinitely many fibres is not a finite sum of homogeneous series. The homogeneous pieces span exactly the finitely supported series as soon as the period N is bounded above on every fibre of f, for instance when f is injective. In that case the graded ring spanned by homogeneous series is the group ring R[H], and the Novikov ring is its period completion. This is the situation of the coefficient ring of capped Hamiltonian Floer theory on a spherically monotone symplectic manifold, graded by twice the first Chern number.

Main definitions #

Main results #

References #

source
def TauCeti.NovikovSeries.supported (R : Type u_1) {H : Type u_2} [Semiring R] [AddZeroClass H] (N : H →+ ℝ) (s : Set H) :
Submodule R (NovikovSeries R H N)

The Novikov series supported in the set s, the Novikov analogue of Finsupp.supported.

Instances For
    source
    theorem TauCeti.NovikovSeries.mem_supported {R : Type u_1} {H : Type u_2} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} {s : Set H} {a : NovikovSeries R H N} :
    a ∈ supported R N s ↔ a.support ⊆ s

    A series lies in supported R N s exactly when its support lies in s.

    source
    def TauCeti.NovikovSeries.gradeBy (R : Type u_1) {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] (N : H →+ ℝ) (f : H → ι) (i : ι) :
    Submodule R (NovikovSeries R H N)

    The Novikov series of degree i for the degree function f: those whose support lies in the fibre f ⁻¹' {i}.

    Instances For
      source
      theorem TauCeti.NovikovSeries.mem_gradeBy_iff {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} {f : H → ι} {i : ι} {a : NovikovSeries R H N} :
      a ∈ gradeBy R N f i ↔ a.support ⊆ f ⁻¹' {i}

      A series has degree i exactly when its support lies in the fibre over i.

      source
      theorem TauCeti.NovikovSeries.single_mem_gradeBy {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} (f : H → ι) (h : H) (r : R) :
      single h r ∈ gradeBy R N f (f h)

      The monomial r e^h has degree f h.

      source
      theorem TauCeti.NovikovSeries.gradeBy_eq_bot {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} {f : H → ι} {i : ι} (hi : i ∉ Set.range f) :
      gradeBy R N f i = ⊥

      There are no nonzero series of a degree that no exponent has.

      source
      theorem TauCeti.NovikovSeries.gradeBy_eq_top {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} {f : H → ι} {i : ι} (hf : ∀ (h : H), f h = i) :
      gradeBy R N f i = ⊤

      If every exponent has degree i, every series is homogeneous of degree i.

      source
      theorem TauCeti.NovikovSeries.iSupIndep_gradeBy {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} (f : H → ι) :
      iSupIndep (gradeBy R N f)

      Homogeneous series of different degrees span independent submodules.

      source
      theorem TauCeti.NovikovSeries.finite_support_of_mem_gradeBy {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} {f : H → ι} {i : ι} (hf : BddAbove (⇑N '' f ⁻¹' {i})) {a : NovikovSeries R H N} (ha : a ∈ gradeBy R N f i) :
      a.support.Finite

      A homogeneous series is finitely supported if the period is bounded above on its fibre.

      source
      theorem TauCeti.NovikovSeries.ofFinsupp_mem_iSup_gradeBy {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} (f : H → ι) (x : H →₀ R) :
      ofFinsupp x ∈ ⨆ (i : ι), gradeBy R N f i

      A finitely supported series is a finite sum of homogeneous series.

      source
      theorem TauCeti.NovikovSeries.mem_iSup_gradeBy_iff {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} {f : H → ι} (hf : ∀ (i : ι), BddAbove (⇑N '' f ⁻¹' {i})) {a : NovikovSeries R H N} :
      a ∈ ⨆ (i : ι), gradeBy R N f i ↔ a.support.Finite

      If the period is bounded above on every fibre of the degree function, the homogeneous series span exactly the finitely supported series.

      source
      theorem TauCeti.NovikovSeries.eq_single_of_mem_gradeBy {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddZeroClass H] {N : H →+ ℝ} {f : H → ι} (hf : Function.Injective f) {h : H} {a : NovikovSeries R H N} (ha : a ∈ gradeBy R N f (f h)) :
      a = single h (a.coeff h)

      For an injective degree function, a series of the degree of h is the monomial at h with its own coefficient.

      source
      instance TauCeti.NovikovSeries.gradeBy.gradedMonoid {R : Type u_1} {H : Type u_2} {ι : Type u_3} [Semiring R] [AddMonoid H] {N : H →+ ℝ} [AddMonoid ι] (f : H →+ ι) :
      SetLike.GradedMonoid (gradeBy R N ⇑f)

      For an additive degree function, the homogeneous Novikov series form a graded monoid.

      source
      theorem TauCeti.NovikovSeries.ofAddMonoidAlgebra_mem_gradeBy_iff {R : Type u_1} {H : Type u_2} {ι : Type u_3} [CommSemiring R] [AddMonoid H] {N : H →+ ℝ} {f : H → ι} {i : ι} {x : AddMonoidAlgebra R H} :
      ofAddMonoidAlgebra x ∈ gradeBy R N f i ↔ x ∈ AddMonoidAlgebra.gradeBy R f i

      The inclusion of the group ring into the Novikov series preserves and reflects the degree.