Documentation

TauCeti.RingTheory.NovikovSeries.Derivation

Degree derivations of Novikov series #

Let ℓ : H →+ R be an additive map from the exponent group into the coefficient ring. Multiplying the coefficient at each exponent h by ℓ h is a derivation of the Novikov ring Nov(R, H, N), the degree derivation TauCeti.NovikovSeries.degreeDerivation ℓ: the Leibniz rule is the identity ℓ (u + v) = ℓ u + ℓ v on the pairs of exponents contributing to a product. Since it does not enlarge supports, the degree derivation preserves every period neighbourhood U_C, so it is continuous and preserves the nonnegative subring. It is compatible with the inclusion of Novikov series on a subgroup and with restriction along exponent homomorphisms.

Over a ℚ-algebra, the degree derivations along the period detect the coefficients of nonzero period: composing N with a ℚ-linear functional f : ℝ → ℚ gives a degree derivation, and a series killed by all of them vanishes at every exponent h with N h ≠ 0 (TauCeti.NovikovSeries.coeff_eq_zero_of_forall_degreeDerivation_eq_zero). This replaces the derivative in the parameter of a one-parameter family: an identity between series supported in positive periods follows from the identity between their degree derivatives.

Main definitions #

Main results #

References #

source
def TauCeti.NovikovSeries.degreeDerivation {R : Type u_1} {H : Type u_2} [CommSemiring R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) :
Derivation R (NovikovSeries R H N) (NovikovSeries R H N)

The degree derivation of Novikov series along an additive map ℓ : H →+ R: it multiplies the coefficient at each exponent h by ℓ h.

Instances For
    source
    @[simp]
    theorem TauCeti.NovikovSeries.coeff_degreeDerivation {R : Type u_1} {H : Type u_2} [CommSemiring R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) (a : NovikovSeries R H N) (h : H) :
    ((degreeDerivation ℓ) a).coeff h = ℓ h * a.coeff h

    The coefficient of the degree derivative at h is ℓ h times the coefficient at h.

    source
    @[simp]
    theorem TauCeti.NovikovSeries.degreeDerivation_single {R : Type u_1} {H : Type u_2} [CommSemiring R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) (g : H) (r : R) :
    (degreeDerivation ℓ) (single g r) = single g (ℓ g * r)

    The degree derivation multiplies the monomial r e^g by ℓ g.

    source
    theorem TauCeti.NovikovSeries.degreeDerivation_mem_periodFiltration {R : Type u_1} {H : Type u_2} [CommRing R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) {C : ℝ} {a : NovikovSeries R H N} (ha : a ∈ periodFiltration R N C) :
    (degreeDerivation ℓ) a ∈ periodFiltration R N C

    The degree derivation preserves each period neighbourhood U_C.

    source
    theorem TauCeti.NovikovSeries.continuous_degreeDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) :
    Continuous ⇑(degreeDerivation ℓ)

    Degree derivations are continuous for the period topology.

    source
    theorem TauCeti.NovikovSeries.degreeDerivation_mem_nonnegSubring {R : Type u_1} {H : Type u_2} [CommRing R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) {a : NovikovSeries R H N} (ha : a ∈ nonnegSubring R N) :
    (degreeDerivation ℓ) a ∈ nonnegSubring R N

    The degree derivation preserves the nonnegative subring.

    source
    noncomputable def TauCeti.NovikovSeries.nonnegDegreeDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) :
    Derivation ℤ ↥(nonnegSubring R N) ↥(nonnegSubring R N)

    The degree derivation along ℓ, restricted to the nonnegative subring.

    Instances For
      source
      @[simp]
      theorem TauCeti.NovikovSeries.coe_nonnegDegreeDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) (a : ↥(nonnegSubring R N)) :
      ↑((nonnegDegreeDerivation ℓ) a) = (degreeDerivation ℓ) ↑a

      The restricted degree derivation agrees with the degree derivation on Novikov series.

      source
      theorem TauCeti.NovikovSeries.continuous_nonnegDegreeDerivation {R : Type u_1} {H : Type u_2} [CommRing R] [AddCommMonoid H] {N : H →+ ℝ} (ℓ : H →+ R) :
      Continuous ⇑(nonnegDegreeDerivation ℓ)

      The restricted degree derivation is continuous for the subspace topology.

      source
      theorem TauCeti.NovikovSeries.degreeDerivation_algebraMap_addSubgroup {R : Type u_1} {H : Type u_2} [CommSemiring R] [AddCommGroup H] {N : H →+ ℝ} {K : AddSubgroup H} (ℓ : H →+ R) (b : NovikovSeries R (↥K) (N.comp K.subtype)) :
      (degreeDerivation ℓ) ((algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) b) = (algebraMap (NovikovSeries R (↥K) (N.comp K.subtype)) (NovikovSeries R H N)) ((degreeDerivation (ℓ.comp K.subtype)) b)

      The degree derivation commutes with the inclusion of Novikov series on a subgroup K, for the restriction of ℓ to K.

      source
      theorem TauCeti.NovikovSeries.comap_degreeDerivation {R : Type u_1} {H : Type u_2} [CommSemiring R] [AddCommGroup H] {N : H →+ ℝ} {H' : Type u_3} [AddCommMonoid H'] {N' : H' →+ ℝ} (φ : H →+ H') (hφ : ∃ c > 0, ∀ (h : H), N' (φ h) = c * N h) (hker : (↑φ.ker).Finite) (ℓ : H' →+ R) (b : NovikovSeries R H' N') :
      (comap φ hφ hker) ((degreeDerivation ℓ) b) = (degreeDerivation (ℓ.comp φ)) ((comap φ hφ hker) b)

      The degree derivation commutes with restriction along φ, for the composite ℓ ∘ φ.

      source
      theorem TauCeti.NovikovSeries.coeff_eq_zero_of_forall_degreeDerivation_eq_zero {R : Type u_1} {H : Type u_2} [CommRing R] [Algebra ℚ R] [AddCommMonoid H] {N : H →+ ℝ} {a : NovikovSeries R H N} (ha : ∀ (f : Module.Dual ℚ ℝ), (degreeDerivation (((algebraMap ℚ R).toAddMonoidHom.comp (LinearMap.toAddMonoidHom f)).comp N)) a = 0) {h : H} (hh : N h ≠ 0) :
      a.coeff h = 0

      Over a ℚ-algebra, the degree derivations along the period detect the coefficients of nonzero period: if a is killed by the degree derivation along f ∘ N for every ℚ-linear functional f : ℝ → ℚ, then a vanishes at every exponent h with N h ≠ 0.