Documentation

TauCeti.RingTheory.LaurentSeries.ContinuousDerivation

Continuous derivations of formal Laurent series #

Let K be a field and F = K⸨X⸩, with the valuation topology, and let D be the formal derivative TauCeti.laurentSeriesDerivation K. This file shows that the continuous K-derivations F → F are exactly the multiples a • D with a : F, and that a = δ X is the value of such a derivation δ at the parameter X = single 1 1.

The algebraic part holds for every derivation δ : F → M into an F-module: on the rational functions K(X), it agrees with f ↦ D f • δ X, since both are derivations of the fraction field of K[X] with the same value at X. When M is Hausdorff with continuous scalar multiplication, continuity extends this agreement to F, since K(X) is dense in F (LaurentSeries.coe_range_dense) and continuous maps to a Hausdorff space that agree on a dense subset are equal.

The continuous derivations form an F-submodule TauCeti.continuousDerivations K of Derivation K F F, which TauCeti.continuousDerivationsEquiv K identifies with F itself. Their commutator makes them a Lie subalgebra of the Laurent derivations, whose Lie structure and coefficient formula are defined in LaurentSeries.Derivative. The subalgebras preserving the embedded power-series ring and its maximal ideal are respectively K⟦X⟧ D and X K⟦X⟧ D. These classifications hold in every characteristic.

The vector fields X K⟦X⟧ D are the infinitesimal coordinate changes. The infinitesimal substitutions 1 + ε a D of K[ε]⟦X⟧, for a ∈ X K⟦X⟧ (TauCeti.infinitesimalSubstitutions), correspond to the vector fields a D, and the ε-coefficient of such a substitution on a power series f is the value of its vector field at f. Composition of substitutions corresponds to addition of vector fields.

Main results #

source
theorem Polynomial.aeval_single_one_eq_algebraMap {R : Type u_1} [CommSemiring R] (p : Polynomial R) :
(aeval ((HahnSeries.single 1) 1)) p = (algebraMap (Polynomial R) (LaurentSeries R)) p

A polynomial evaluated at the parameter X = single 1 1 of R⸨X⸩ is its image as a Laurent series.

source
@[simp]
theorem TauCeti.smul_laurentSeriesDerivation_inj {R : Type u_1} [CommRing R] {a b : LaurentSeries R} :
a • laurentSeriesDerivation R = b • laurentSeriesDerivation R ↔ a = b

A multiple of the formal derivative determines the multiplier.

source
theorem TauCeti.continuous_smul_laurentSeriesDerivation {K : Type u_1} [Field K] (a : LaurentSeries K) :
Continuous ⇑(a • laurentSeriesDerivation K)

Every multiple of the formal derivative is continuous for the valuation topology.

source
theorem Derivation.apply_coe_ratFunc {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module (LaurentSeries K) M] [Module K M] [IsScalarTower K (LaurentSeries K) M] (δ : Derivation K (LaurentSeries K) M) (r : RatFunc K) :
δ ((algebraMap (RatFunc K) (LaurentSeries K)) r) = (TauCeti.laurentSeriesDerivation K) ((algebraMap (RatFunc K) (LaurentSeries K)) r) • δ ((HahnSeries.single 1) 1)

On rational functions, every K-derivation δ : K⸨X⸩ → M into a K⸨X⸩-module agrees with f ↦ D f • δ X, where D is the formal derivative.

source
theorem Derivation.apply_eq_laurentSeriesDerivation_smul {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module (LaurentSeries K) M] [Module K M] [IsScalarTower K (LaurentSeries K) M] [TopologicalSpace M] [T2Space M] [ContinuousSMul (LaurentSeries K) M] (δ : Derivation K (LaurentSeries K) M) (hδ : Continuous ⇑δ) (f : LaurentSeries K) :
δ f = (TauCeti.laurentSeriesDerivation K) f • δ ((HahnSeries.single 1) 1)

Continuous derivations of Laurent series into a topological module. A K-derivation δ : K⸨X⸩ → M into a Hausdorff K⸨X⸩-module with continuous scalar multiplication that is continuous for the valuation topology satisfies δ f = D f • δ X, where D is the formal derivative.

source
theorem Derivation.continuous_iff_exists_apply_eq_laurentSeriesDerivation_smul {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module (LaurentSeries K) M] [Module K M] [IsScalarTower K (LaurentSeries K) M] [TopologicalSpace M] [T2Space M] [ContinuousSMul (LaurentSeries K) M] {δ : Derivation K (LaurentSeries K) M} :
Continuous ⇑δ ↔ ∃ (m : M), ∀ (f : LaurentSeries K), δ f = (TauCeti.laurentSeriesDerivation K) f • m

A K-derivation of K⸨X⸩ into a Hausdorff K⸨X⸩-module with continuous scalar multiplication is continuous if and only if it is f ↦ D f • m for some m, where D is the formal derivative.

source
theorem Derivation.eq_smul_laurentSeriesDerivation {K : Type u_1} [Field K] (δ : Derivation K (LaurentSeries K) (LaurentSeries K)) (hδ : Continuous ⇑δ) :
δ = δ ((HahnSeries.single 1) 1) • TauCeti.laurentSeriesDerivation K

Continuous derivations of Laurent series. A K-derivation δ of K⸨X⸩ that is continuous for the valuation topology is the multiple δ X • D of the formal derivative D.

source
theorem Derivation.continuous_iff_exists_eq_smul_laurentSeriesDerivation {K : Type u_1} [Field K] {δ : Derivation K (LaurentSeries K) (LaurentSeries K)} :
Continuous ⇑δ ↔ ∃ (a : LaurentSeries K), δ = a • TauCeti.laurentSeriesDerivation K

A K-derivation of K⸨X⸩ is continuous for the valuation topology if and only if it is a multiple of the formal derivative.

source
def TauCeti.continuousDerivations (K : Type u_1) [Field K] :
Submodule (LaurentSeries K) (Derivation K (LaurentSeries K) (LaurentSeries K))

The K⸨X⸩-submodule of K-derivations of K⸨X⸩ that are continuous for the valuation topology.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_continuousDerivations {K : Type u_1} [Field K] {δ : Derivation K (LaurentSeries K) (LaurentSeries K)} :
    δ ∈ continuousDerivations K ↔ Continuous ⇑δ
    source
    noncomputable def TauCeti.continuousDerivationsEquiv (K : Type u_1) [Field K] :
    LaurentSeries K ≃ₗ[LaurentSeries K] ↥(continuousDerivations K)

    The continuous derivations of K⸨X⸩ form a free module of rank one with basis the formal derivative D: the equivalence sends a to a • D, and its inverse evaluates a derivation at the parameter X.

    Instances For
      source
      @[simp]
      theorem TauCeti.coe_continuousDerivationsEquiv_apply {K : Type u_1} [Field K] (a : LaurentSeries K) :
      ↑((continuousDerivationsEquiv K) a) = a • laurentSeriesDerivation K
      source
      @[simp]
      theorem TauCeti.continuousDerivationsEquiv_symm_apply {K : Type u_1} [Field K] (δ : ↥(continuousDerivations K)) :
      (continuousDerivationsEquiv K).symm δ = ↑δ ((HahnSeries.single 1) 1)
      source
      noncomputable def TauCeti.continuousDerivationsLieSubalgebra (K : Type u_1) [Field K] :
      LieSubalgebra K (Derivation K (LaurentSeries K) (LaurentSeries K))

      Continuous Laurent derivations, with their commutator Lie algebra structure over K.

      Instances For
        source
        @[simp]
        theorem TauCeti.mem_continuousDerivationsLieSubalgebra {K : Type u_1} [Field K] {δ : Derivation K (LaurentSeries K) (LaurentSeries K)} :
        δ ∈ continuousDerivationsLieSubalgebra K ↔ Continuous ⇑δ
        source
        noncomputable def TauCeti.powerSeriesPreservingDerivations (K : Type u_1) [Field K] :
        LieSubalgebra K (Derivation K (LaurentSeries K) (LaurentSeries K))

        Continuous Laurent vector fields preserving the power-series ring K⟦X⟧.

        Instances For
          source
          @[simp]
          theorem TauCeti.mem_powerSeriesPreservingDerivations {K : Type u_1} [Field K] {δ : Derivation K (LaurentSeries K) (LaurentSeries K)} :
          δ ∈ powerSeriesPreservingDerivations K ↔ Continuous ⇑δ ∧ ∀ (f : PowerSeries K), ∃ (g : PowerSeries K), δ ((HahnSeries.ofPowerSeries ℤ K) f) = (HahnSeries.ofPowerSeries ℤ K) g

          Membership in the power-series-preserving Lie subalgebra means continuity and preservation of the embedded power-series ring.

          source
          theorem TauCeti.mem_powerSeriesPreservingDerivations_iff {K : Type u_1} [Field K] {δ : Derivation K (LaurentSeries K) (LaurentSeries K)} :
          δ ∈ powerSeriesPreservingDerivations K ↔ ∃ (a : PowerSeries K), δ = (HahnSeries.ofPowerSeries ℤ K) a • laurentSeriesDerivation K

          A continuous Laurent vector field preserves power series exactly when its coefficient is a power series: the subalgebra is K⟦X⟧ D.

          source
          noncomputable def TauCeti.maximalIdealPreservingDerivations (K : Type u_1) [Field K] :
          LieSubalgebra K (Derivation K (LaurentSeries K) (LaurentSeries K))

          Continuous Laurent vector fields preserving the maximal ideal X K⟦X⟧ of K⟦X⟧. The ideal is presented by its multiples of X, avoiding a new carrier for the embedded ideal.

          Instances For
            source
            @[simp]
            theorem TauCeti.mem_maximalIdealPreservingDerivations {K : Type u_1} [Field K] {δ : Derivation K (LaurentSeries K) (LaurentSeries K)} :
            δ ∈ maximalIdealPreservingDerivations K ↔ Continuous ⇑δ ∧ ∀ (f : PowerSeries K), ∃ (g : PowerSeries K), δ ((HahnSeries.ofPowerSeries ℤ K) (PowerSeries.X * f)) = (HahnSeries.ofPowerSeries ℤ K) (PowerSeries.X * g)

            Membership in the maximal-ideal-preserving Lie subalgebra means continuity and preservation of all power-series multiples of X.

            source
            theorem TauCeti.mem_maximalIdealPreservingDerivations_iff {K : Type u_1} [Field K] {δ : Derivation K (LaurentSeries K) (LaurentSeries K)} :
            δ ∈ maximalIdealPreservingDerivations K ↔ ∃ (a : PowerSeries K), δ = (HahnSeries.ofPowerSeries ℤ K) (PowerSeries.X * a) • laurentSeriesDerivation K

            A continuous Laurent vector field preserves the maximal ideal exactly when its coefficient is a multiple of X in the power-series ring: the subalgebra is X K⟦X⟧ D.

            source
            theorem TauCeti.maximalIdealPreservingDerivations_le_powerSeriesPreservingDerivations {K : Type u_1} [Field K] :
            maximalIdealPreservingDerivations K ≤ powerSeriesPreservingDerivations K

            Maximal-ideal-preserving continuous Laurent vector fields preserve power series.

            source
            noncomputable def TauCeti.powerSeriesPreservingDerivationsEquiv (K : Type u_1) [Field K] :
            PowerSeries K ≃ₗ[K] ↥(powerSeriesPreservingDerivations K)

            The power-series-preserving continuous Laurent vector fields are parametrized by K⟦X⟧, through the K-linear isomorphism a ↦ a D.

            Instances For
              source
              @[simp]
              theorem TauCeti.coe_powerSeriesPreservingDerivationsEquiv_apply {K : Type u_1} [Field K] (a : PowerSeries K) :
              ↑((powerSeriesPreservingDerivationsEquiv K) a) = (HahnSeries.ofPowerSeries ℤ K) a • laurentSeriesDerivation K

              TauCeti.powerSeriesPreservingDerivationsEquiv sends a to the vector field a D.

              source
              @[simp]
              theorem TauCeti.coe_powerSeriesPreservingDerivationsEquiv_symm_apply {K : Type u_1} [Field K] (δ : ↥(powerSeriesPreservingDerivations K)) :
              (HahnSeries.ofPowerSeries ℤ K) ((powerSeriesPreservingDerivationsEquiv K).symm δ) = ↑δ ((HahnSeries.single 1) 1)

              The inverse of TauCeti.powerSeriesPreservingDerivationsEquiv evaluates a vector field at the parameter X = single 1 1.

              source
              theorem TauCeti.smul_laurentSeriesDerivation_mem_maximalIdealPreservingDerivations {K : Type u_1} [Field K] {a : PowerSeries K} (ha : a ∈ Ideal.span {PowerSeries.X}) :
              (HahnSeries.ofPowerSeries ℤ K) a • laurentSeriesDerivation K ∈ maximalIdealPreservingDerivations K

              The vector field a D preserves the maximal ideal of K⟦X⟧ for every a ∈ X K⟦X⟧.

              source
              noncomputable def TauCeti.maximalIdealPreservingDerivationsEquiv (K : Type u_1) [Field K] :
              ↥(Ideal.span {PowerSeries.X}) ≃ₗ[K] ↥(maximalIdealPreservingDerivations K)

              The maximal-ideal-preserving continuous Laurent vector fields are parametrized by the ideal (X) of K⟦X⟧, through the K-linear isomorphism a ↦ a D.

              Instances For
                source
                @[simp]
                theorem TauCeti.coe_maximalIdealPreservingDerivationsEquiv_apply {K : Type u_1} [Field K] (a : ↥(Ideal.span {PowerSeries.X})) :
                ↑((maximalIdealPreservingDerivationsEquiv K) a) = (HahnSeries.ofPowerSeries ℤ K) ↑a • laurentSeriesDerivation K

                TauCeti.maximalIdealPreservingDerivationsEquiv sends a to the vector field a D.

                source
                @[simp]
                theorem TauCeti.coe_maximalIdealPreservingDerivationsEquiv_symm_apply {K : Type u_1} [Field K] (δ : ↥(maximalIdealPreservingDerivations K)) :
                (HahnSeries.ofPowerSeries ℤ K) ↑((maximalIdealPreservingDerivationsEquiv K).symm δ) = ↑δ ((HahnSeries.single 1) 1)

                The inverse of TauCeti.maximalIdealPreservingDerivationsEquiv evaluates a vector field at the parameter X = single 1 1.

                source
                noncomputable def TauCeti.infinitesimalSubstitutionsEquivDerivations (K : Type u_1) [Field K] :
                ↥(infinitesimalSubstitutions K) ≃* Multiplicative ↥(maximalIdealPreservingDerivations K)

                The infinitesimal substitutions of K[ε]⟦X⟧ are identified with the maximal-ideal-preserving continuous vector fields of K⸨X⸩: the substitution 1 + ε a D corresponds to the vector field a D, for a ∈ X K⟦X⟧. Composition of substitutions corresponds to addition of vector fields.

                Instances For
                  source
                  @[simp]
                  theorem TauCeti.coe_toAdd_infinitesimalSubstitutionsEquivDerivations_apply {K : Type u_1} [Field K] (σ : ↥(infinitesimalSubstitutions K)) :
                  ↑(Multiplicative.toAdd ((infinitesimalSubstitutionsEquivDerivations K) σ)) = (HahnSeries.ofPowerSeries ℤ K) (PowerSeries.mk fun (n : ℕ) => TrivSqZeroExt.snd ((PowerSeries.coeff n) (↑σ PowerSeries.X))) • laurentSeriesDerivation K

                  The vector field of an infinitesimal substitution σ is a D, where a is the ε-coefficient of σ X.

                  source
                  @[simp]
                  theorem TauCeti.coe_infinitesimalSubstitutionsEquivDerivations_symm_apply {K : Type u_1} [Field K] (δ : Multiplicative ↥(maximalIdealPreservingDerivations K)) :
                  ↑((infinitesimalSubstitutionsEquivDerivations K).symm δ) = infinitesimalSubstAlgEquiv DualNumber.eps ⋯ ((PowerSeries.map (algebraMap K (DualNumber K))) ↑((maximalIdealPreservingDerivationsEquiv K).symm (Multiplicative.toAdd δ)))

                  The infinitesimal substitution of a vector field a D is 1 + ε a D.

                  source
                  theorem TauCeti.infinitesimalSubstitutions_apply_map_eq_iff {K : Type u_1} [Field K] (σ : ↥(infinitesimalSubstitutions K)) (f g : PowerSeries K) :
                  ↑σ ((PowerSeries.map (algebraMap K (DualNumber K))) f) = (PowerSeries.map (algebraMap K (DualNumber K))) f + DualNumber.eps • (PowerSeries.map (algebraMap K (DualNumber K))) g ↔ (HahnSeries.ofPowerSeries ℤ K) g = ↑(Multiplicative.toAdd ((infinitesimalSubstitutionsEquivDerivations K) σ)) ((HahnSeries.ofPowerSeries ℤ K) f)

                  The ε-coefficient of an infinitesimal substitution σ on a power series f is the image of f under the vector field δ of σ: σ f = f + ε g exactly when g = δ f.