Continuous Kähler differentials 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. The algebraic Kähler differentials Ω[F⁄K] do
not see the topology of F; in characteristic zero they are much larger than F, since F has
infinite transcendence degree over K(X). The module of continuous differentials Ω¹_cont(F/K)
is the quotient of Ω[F⁄K] by the kernel of the map λ : Ω[F⁄K] → F, f dg ↦ f * D g,
induced by D through the universal property of Kähler differentials.
This file constructs Ω¹_cont(F/K) as TauCeti.ContinuousKaehlerDifferential K, together with
its universal derivation d = TauCeti.ContinuousKaehlerDifferential.D K, and shows:
λinduces anF-linear equivalenceΩ¹_cont(F/K) ≃ FsendingdXto1, so every continuous one-form is uniquelyf dX.Ω¹_cont(F/K)carries the module topology overF, for which this equivalence is a homeomorphism; thus it is the valuation topology ofFtransported along it, anddis continuous.- For every Hausdorff
F-moduleMwith continuous scalar multiplication, aK-derivationδ : F → Mis continuous if and only ifδ f = D f • δ Xfor allf, and then it factors uniquely asℓ ∘ dwithℓ : Ω¹_cont(F/K) → ManF-linear map, which is automatically continuous. Conversely everyℓ ∘ dis continuous, even without Hausdorffness. These continuity statements use the rank-one normal form and require no continuity of addition onM. Sodis the universal continuous derivation.
The classification of such derivations is
Derivation.continuous_iff_exists_apply_eq_laurentSeriesDerivation_smul, from
LaurentSeries.ContinuousDerivation.
Continuous one-forms are covariant under changes of parameter. For a nonzero power series φ with
zero constant coefficient, substitution f dX ↦ f (φ) dφ is a continuous map of Ω¹_cont(F/K),
semilinear over the substitution f ↦ f (φ) of F. Since dφ = Dφ dX, it sends f dX to
f (φ) Dφ dX, and by the chain rule it sends d g to d (g (φ)). Substitutions compose as power
series do, and the residue of ω (φ) is ord φ times the residue of ω. A formal coordinate
φ = u X + ⋯, u ≠ 0, therefore acts by a semilinear automorphism of Ω¹_cont(F/K), inverse to
that of φ⁻¹, which preserves residues.
Main definitions #
TauCeti.ContinuousKaehlerDifferential K: the continuous Kähler differentialsΩ¹_cont(F/K).TauCeti.ContinuousKaehlerDifferential.D K: the universal continuous derivationd.TauCeti.ContinuousKaehlerDifferential.equivLaurentSeries K: the continuousF-linear equivalenceΩ¹_cont(F/K) ≃ Fsendingd Xto1.TauCeti.ContinuousKaehlerDifferential.lift: the factorization of a continuous derivation throughd.TauCeti.ContinuousKaehlerDifferential.subst: substitutionf dX ↦ f (φ) dφinto one-forms.TauCeti.ContinuousKaehlerDifferential.substEquiv: for a formal coordinateφ, substitution into one-forms as a semilinear equivalence.
Main results #
TauCeti.ContinuousKaehlerDifferential.continuous_D: the universal derivation is continuous.TauCeti.ContinuousKaehlerDifferential.continuous_of_linearMap: every linear map from the continuous differentials to a module with continuous scalar multiplication is continuous.TauCeti.ContinuousKaehlerDifferential.existsUnique_compDer_eq: every continuous derivation factors uniquely throughd.TauCeti.ContinuousKaehlerDifferential.derivative_smul_D_single_one:d f = Df dX.TauCeti.ContinuousKaehlerDifferential.subst_D: coordinate covariance,(d g) (φ) = d (g (φ)).TauCeti.ContinuousKaehlerDifferential.subst_subst: substitutingφand thenψis substitutingφ (ψ).TauCeti.ContinuousKaehlerDifferential.coeff_neg_one_equivLaurentSeries_subst: the residue ofω (φ)isord φtimes that ofω.
The map f dg ↦ f * D g from the Kähler differentials is surjective: f dX ↦ f.
The K-module structure on Ω¹_cont(K⸨X⸩/K) restricted from its K⸨X⸩-module structure.
Ω¹_cont(K⸨X⸩/K) carries the module topology over K⸨X⸩. By
TauCeti.ContinuousKaehlerDifferential.equivLaurentSeries this is the valuation topology of
K⸨X⸩ transported to the differentials.
The quotient map from the Kähler differentials to the continuous differentials.
Instances For
A Kähler differential vanishes in Ω¹_cont(K⸨X⸩/K) exactly when its image Σ fᵢ * D gᵢ
under the map induced by the formal derivative vanishes.
The universal continuous derivation d : K⸨X⸩ → Ω¹_cont(K⸨X⸩/K).
Instances For
Continuous one-forms are multiples of dX. The equivalence Ω¹_cont(K⸨X⸩/K) ≃ K⸨X⸩
induced by the formal derivative, sending f dg to f * D g and d X to 1. It is a
homeomorphism for the module topology on the differentials and the valuation topology on
K⸨X⸩.
Instances For
The equivalence sends d f to the formal derivative of f.
The equivalence sends the differential d X of the parameter to 1.
The continuous one-form corresponding to f is f d X.
Every continuous one-form is f d X for the unique f = equivLaurentSeries K ω.
d f = Df dX. The differential of a Laurent series is its formal derivative times d X;
in particular d φ = Dφ dX for a change of parameter φ.
Ω¹_cont(K⸨X⸩/K) has rank one over K⸨X⸩.
The universal derivation d is continuous.
Semilinear maps out of Ω¹_cont(K⸨X⸩/K) agree as soon as they agree on d X.
Every linear map from the continuous differentials to a module with continuous scalar multiplication is continuous.
For a continuous derivation δ, the map Ω[K⸨X⸩⁄K] → M it induces is λ followed by
f ↦ f • δ X, where λ is the map induced by the formal derivative.
The factorization of a continuous derivation through d. A continuous K-derivation
δ : K⸨X⸩ → M factors through Ω¹_cont(K⸨X⸩/K), by the K⸨X⸩-linear map induced by its
Kähler lift.
Instances For
The factorization of a continuous derivation is continuous.
The factorization of δ through d is unique.
Universal property of continuous differentials. Every continuous K-derivation of
K⸨X⸩ into a Hausdorff module with continuous scalar multiplication factors uniquely through
d by a K⸨X⸩-linear map.
Every derivation factoring through d is continuous when scalar multiplication on its
target is continuous.
Substitution into one-forms #
Substitution into continuous one-forms. For a nonzero power series φ with zero constant
coefficient, the map f dX ↦ f (φ) dφ = f (φ) Dφ dX on Ω¹_cont(K⸨X⸩/K). It is semilinear
over the substitution f ↦ f (φ) of TauCeti.LaurentSeries.substAlgHom, and it sends d g to
d (g (φ)) (TauCeti.ContinuousKaehlerDifferential.subst_D).
Instances For
Substitution sends f dX to f (φ) Dφ dX.
Coordinate covariance of the differential. Substitution into one-forms sends d g to
d (g (φ)); this is the chain rule D (g (φ)) = (Dg) (φ) Dφ.
Substitution into one-forms sends d X to d φ.
Substitution into one-forms is the unique f ↦ f (φ)-semilinear map sending d X to d φ.
Substitution into one-forms is continuous.
Residues of substituted one-forms. Substituting φ multiplies the residue of a one-form
by the order of φ: Res (ω (φ)) = ord φ • Res ω, where the residue of f dX is the coefficient
of X⁻¹ in f.
Substituting φ into one-forms and then ψ is substituting φ (ψ).
Equal substitution series give the same pullback of one-forms, independently of the proofs of their substitution hypotheses. This compares the underlying maps even when their semilinearity homomorphisms are not definitionally equal.
Substituting X into one-forms is the identity.
Formal coordinate changes act invertibly on one-forms. For a formal coordinate φ,
substitution f dX ↦ f (φ) dφ into continuous one-forms, as an equivalence that is semilinear
over the substitution automorphism TauCeti.LaurentSeries.substAlgEquiv φ of K⸨X⸩. Its inverse
is substitution of the compositional inverse φ⁻¹.
Instances For
Substituting the composite coordinate φ ∘ ψ into one-forms is substituting φ and then
ψ.
Substituting the identity coordinate X into one-forms is the identity.
Formal coordinate changes preserve residues of one-forms.