Kähler differentials under Laurent expansion

Let e : F → A((X)) be a k-algebra map from a commutative k-algebra F into Laurent series over a commutative k-algebra A, for instance the Laurent expansion of the functions of a curve at a place in a chosen uniformizer. The formal derivative z ↦ (e z)' is a k-derivation of F, so by the universal property of Kähler differentials it factors through d : F → Ω[F⁄k]. In particular every relation dz = c dt in Ω[F⁄k] becomes the identity (e z)' = e c · (e t)' of Laurent series.

If e sends t to the variable X, then (e t)' = 1, so dt ≠ 0. This is how a Laurent expansion certifies that dt ≠ 0; when Ω[F⁄k] is one-dimensional (for instance when a function field F / k is separably generated), this makes t separating.

Main results

• TauCeti.derivative_algHom_eq_mul_of_D_eq_smul: dz = c dt implies (e z)' = e c · (e t)'.
• TauCeti.D_ne_zero_of_algHom_laurentSeries: if e t = X and A is nontrivial, then dt ≠ 0 in Ω[F⁄k].

theorem TauCeti.derivative_algHom_eq_mul_of_D_eq_smul {k : Type u_1} {F : Type u_2} {A : Type u_3} [CommRing k] [CommRing F] [Algebra k F] [CommRing A] [Algebra k A] {e : F →ₐ[k] LaurentSeries A} {z c t : F} (h : (KaehlerDifferential.D k F) z = c • (KaehlerDifferential.D k F) t) : (LaurentSeries.derivative A) (e z) = e c * (LaurentSeries.derivative A) (e t)

Relations between differentials survive Laurent expansion. Let e : F → A((X)) be a k-algebra map into Laurent series over a k-algebra A. If dz = c dt in Ω[F⁄k], then the formal derivatives of the expansions satisfy (e z)' = e c · (e t)': the derivation z ↦ (e z)' factors through the universal derivation d.

theorem TauCeti.D_ne_zero_of_algHom_laurentSeries {k : Type u_1} {F : Type u_2} {A : Type u_3} [CommRing k] [CommRing F] [Algebra k F] [CommRing A] [Nontrivial A] [Algebra k A] {e : F →ₐ[k] LaurentSeries A} {t : F} (he : e t = (HahnSeries.single 1) 1) : (KaehlerDifferential.D k F) t ≠ 0

A Laurent variable has a nonzero differential. If a k-algebra map e : F → A((X)) into Laurent series over a nontrivial k-algebra A sends t to the variable X, then dt ≠ 0 in Ω[F⁄k]: the derivation z ↦ (e z)' takes the value 1 at t.