Infinitesimal substitutions of power series

Let S be a commutative ring and e ∈ S with e ^ 2 = 0. For every power series a, the substitution X ↦ X + e a is the automorphism f ↦ f + e a f' of the S-algebra S⟦X⟧: this is the first-order Taylor formula PowerSeries.subst_X_add_of_sq_eq_zero. In operator notation it is 1 + e a D, where D is the formal derivative. For a fixed e these automorphisms compose by adding the parameters, (1 + e a D) (1 + e b D) = 1 + e (a + b) D, because the cross term is a multiple of e ^ 2 = 0.

For two square-zero elements e₁, e₂, the group commutator of σ₁ = 1 + e₁ a D and σ₂ = 1 + e₂ b D in the automorphism group, whose multiplication is composition, is

σ₁ σ₂ σ₁⁻¹ σ₂⁻¹ = 1 + e₁ e₂ (a b' - b a') D.

The vector field on the right is the commutator [a D, b D] = (a b' - b a') D of derivations, so this fixes the sign relating composition of substitutions to the bracket of vector fields. Over S = DualNumber (DualNumber K) = K[ε₁, ε₂] / (ε₁², ε₂²) this applies to e₁ = ε₁ and e₂ = ε₂.

Over the dual numbers R[ε] of a commutative ring R, the infinitesimal substitutions are the R[ε]-algebra automorphisms of R[ε]⟦X⟧ that reduce to the identity modulo ε and preserve the ideal (X). They are exactly the automorphisms 1 + ε a D for a ∈ X R⟦X⟧, and a ↦ 1 + ε a D is an isomorphism from the additive group X R⟦X⟧ onto this subgroup. The ε-coefficient of 1 + ε a D on R⟦X⟧ is the derivation a D of R⟦X⟧, so this identifies the infinitesimal substitutions with the derivations X R⟦X⟧ D vanishing at the origin.

Main definitions

• TauCeti.infinitesimalSubstAlgEquiv e he a: the automorphism f ↦ f + e a f' of S⟦X⟧, the substitution X ↦ X + e a.
• TauCeti.infinitesimalSubstitutions R: the subgroup of R[ε]-algebra automorphisms of R[ε]⟦X⟧ reducing to the identity modulo ε and preserving (X).
• TauCeti.infinitesimalSubstitutionsEquiv R: the isomorphism a ↦ 1 + ε a D from the additive group X R⟦X⟧ to TauCeti.infinitesimalSubstitutions R.

Main results

• TauCeti.infinitesimalSubstAlgEquiv_apply_eq_subst: 1 + e a D is the substitution X ↦ X + e a.
• TauCeti.infinitesimalSubstAlgEquiv_add: 1 + e (a + b) D = (1 + e a D) (1 + e b D).
• TauCeti.infinitesimalSubstAlgEquiv_commutator_apply: the commutator formula above.
• TauCeti.infinitesimalSubstitutionsEquiv_apply_map: the ε-coefficient of 1 + ε a D on R⟦X⟧ is the derivation a D.

noncomputable def TauCeti.infinitesimalSubstAlgEquiv {S : Type u_1} [CommRing S] (e : S) (he : e ^ 2 = 0) (a : PowerSeries S) : PowerSeries S ≃ₐ[S] PowerSeries S

For e with e ^ 2 = 0 and a power series a, the infinitesimal substitution 1 + e a D : f ↦ f + e a f' of S⟦X⟧, which is the substitution X ↦ X + e a. Its inverse is 1 - e a D.

@[simp]

theorem TauCeti.infinitesimalSubstAlgEquiv_apply {S : Type u_1} [CommRing S] {e : S} (he : e ^ 2 = 0) (a f : PowerSeries S) : (infinitesimalSubstAlgEquiv e he a) f = f + e • (a * PowerSeries.derivative f)

1 + e a D acts by f ↦ f + e a f'.

theorem TauCeti.infinitesimalSubstAlgEquiv_apply_eq_subst {S : Type u_1} [CommRing S] {e : S} (he : e ^ 2 = 0) (a f : PowerSeries S) : (infinitesimalSubstAlgEquiv e he a) f = PowerSeries.subst (PowerSeries.X + e • a) f

1 + e a D is the substitution X ↦ X + e a.

theorem TauCeti.infinitesimalSubstAlgEquiv_X {S : Type u_1} [CommRing S] {e : S} (he : e ^ 2 = 0) (a : PowerSeries S) : (infinitesimalSubstAlgEquiv e he a) PowerSeries.X = PowerSeries.X + e • a

@[simp]

theorem TauCeti.infinitesimalSubstAlgEquiv_zero {S : Type u_1} [CommRing S] {e : S} (he : e ^ 2 = 0) : infinitesimalSubstAlgEquiv e he 0 = 1

theorem TauCeti.infinitesimalSubstAlgEquiv_add {S : Type u_1} [CommRing S] {e : S} (he : e ^ 2 = 0) (a b : PowerSeries S) : infinitesimalSubstAlgEquiv e he (a + b) = infinitesimalSubstAlgEquiv e he a * infinitesimalSubstAlgEquiv e he b

For a fixed square-zero e, infinitesimal substitutions compose by adding their parameters: 1 + e (a + b) D = (1 + e a D) (1 + e b D).

@[simp]

theorem TauCeti.infinitesimalSubstAlgEquiv_symm {S : Type u_1} [CommRing S] {e : S} (he : e ^ 2 = 0) (a : PowerSeries S) : (infinitesimalSubstAlgEquiv e he a).symm = infinitesimalSubstAlgEquiv e he (-a)

theorem TauCeti.infinitesimalSubstAlgEquiv_commutator_apply {S : Type u_1} [CommRing S] {e₁ e₂ : S} (he₁ : e₁ ^ 2 = 0) (he₂ : e₂ ^ 2 = 0) (a b f : PowerSeries S) : ⁅infinitesimalSubstAlgEquiv e₁ he₁ a, infinitesimalSubstAlgEquiv e₂ he₂ b⁆ f = f + (e₁ * e₂) • ((a * PowerSeries.derivative b - b * PowerSeries.derivative a) * PowerSeries.derivative f)

The commutator of infinitesimal substitutions: for square-zero e₁, e₂, the group commutator ⁅σ₁, σ₂⁆ = σ₁ σ₂ σ₁⁻¹ σ₂⁻¹ of σ₁ = 1 + e₁ a D and σ₂ = 1 + e₂ b D, with multiplication given by composition, is 1 + e₁ e₂ (a b' - b a') D.

noncomputable def TauCeti.infinitesimalSubstitutions (R : Type u_1) [CommRing R] : Subgroup (PowerSeries (DualNumber R) ≃ₐ[DualNumber R] PowerSeries (DualNumber R))

The infinitesimal substitutions over the dual numbers R[ε]: the R[ε]-algebra automorphisms of R[ε]⟦X⟧ that reduce to the identity modulo ε and preserve the ideal (X).

theorem TauCeti.mem_infinitesimalSubstitutions (R : Type u_1) [CommRing R] {σ : PowerSeries (DualNumber R) ≃ₐ[DualNumber R] PowerSeries (DualNumber R)} : σ ∈ infinitesimalSubstitutions R ↔ (∀ (f : PowerSeries (DualNumber R)), (PowerSeries.map (TrivSqZeroExt.fstHom R R R).toRingHom) (σ f) = (PowerSeries.map (TrivSqZeroExt.fstHom R R R).toRingHom) f) ∧ ∀ f ∈ Ideal.span {PowerSeries.X}, σ f ∈ Ideal.span {PowerSeries.X}

An automorphism of R[ε]⟦X⟧ is an infinitesimal substitution exactly when it reduces to the identity modulo ε and preserves the ideal (X).

theorem TauCeti.mem_infinitesimalSubstitutions_iff (R : Type u_1) [CommRing R] {σ : PowerSeries (DualNumber R) ≃ₐ[DualNumber R] PowerSeries (DualNumber R)} : σ ∈ infinitesimalSubstitutions R ↔ ∃ (a : PowerSeries R), PowerSeries.constantCoeff a = 0 ∧ σ = infinitesimalSubstAlgEquiv DualNumber.eps ⋯ ((PowerSeries.map (algebraMap R (DualNumber R))) a)

An automorphism of R[ε]⟦X⟧ is an infinitesimal substitution exactly when it is 1 + ε a D for some a ∈ X R⟦X⟧.

noncomputable def TauCeti.infinitesimalSubstitutionsEquiv (R : Type u_1) [CommRing R] : Multiplicative ↥(Ideal.span {PowerSeries.X}) ≃* ↥(infinitesimalSubstitutions R)

The infinitesimal substitutions over R[ε] are parametrized by the additive group X R⟦X⟧, through a ↦ 1 + ε a D. The inverse reads off the ε-coefficient of the image of X.

@[simp]

theorem TauCeti.coe_infinitesimalSubstitutionsEquiv_apply (R : Type u_1) [CommRing R] (a : Multiplicative ↥(Ideal.span {PowerSeries.X})) : ↑((infinitesimalSubstitutionsEquiv R) a) = infinitesimalSubstAlgEquiv DualNumber.eps ⋯ ((PowerSeries.map (algebraMap R (DualNumber R))) ↑(Multiplicative.toAdd a))

@[simp]

theorem TauCeti.coe_toAdd_infinitesimalSubstitutionsEquiv_symm_apply (R : Type u_1) [CommRing R] (σ : ↥(infinitesimalSubstitutions R)) : ↑(Multiplicative.toAdd ((infinitesimalSubstitutionsEquiv R).symm σ)) = PowerSeries.mk fun (n : ℕ) => TrivSqZeroExt.snd ((PowerSeries.coeff n) (↑σ PowerSeries.X))

The inverse of TauCeti.infinitesimalSubstitutionsEquiv reads off the ε-coefficient of the image of X.

theorem TauCeti.infinitesimalSubstitutionsEquiv_apply_map (R : Type u_1) [CommRing R] (a : Multiplicative ↥(Ideal.span {PowerSeries.X})) (f : PowerSeries R) : ↑((infinitesimalSubstitutionsEquiv R) a) ((PowerSeries.map (algebraMap R (DualNumber R))) f) = (PowerSeries.map (algebraMap R (DualNumber R))) f + DualNumber.eps • (PowerSeries.map (algebraMap R (DualNumber R))) (((PowerSeries.mkDerivation R) ↑(Multiplicative.toAdd a)) f)

The ε-coefficient of the infinitesimal substitution 1 + ε a D on R⟦X⟧ is the derivation a D of R⟦X⟧, which preserves (X) since a ∈ X R⟦X⟧.