Derivations are continuous for adic topologies #
Let I be an ideal of a commutative ring A and M an A-module. Every derivation
D : A → M is continuous for the I-adic topology on A and the I-adic topology on M, with
no further hypothesis: by the Leibniz rule D maps I ^ (n + 1) into I ^ n • M
(Derivation.apply_mem_pow_smul_top_of_mem_pow_succ), and these sets are bases of neighbourhoods
of zero.
For A = K⟦X⟧ and I = (X) this says that every K-derivation of formal power series is
X-adically continuous, in every characteristic, although K⟦X⟧ is far from being generated by
X as an algebra.
Main results #
Derivation.continuous_adic: a derivationA → Mis continuous for theI-adic topologies.
theorem
Derivation.continuous_adic
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommSemiring R]
[CommRing A]
[Algebra R A]
[AddCommGroup M]
[Module A M]
[Module R M]
(D : Derivation R A M)
(I : Ideal A)
:
Continuous ⇑D
Every derivation D : A → M is continuous for the I-adic topologies on A and on M,
since it maps I ^ (n + 1) into I ^ n • M.