Derivations extend to the adic completion

A derivation D of a commutative ring R lowers the powers of any ideal by one: D(Iᵃ⁺¹) ⊆ Iᵃ (Leibniz on a product of a + 1 elements of I). Hence D induces, for every n, a map R/Iⁿ⁺¹ → R/Iⁿ, and these maps are compatible with the transition maps of the inverse system defining the I-adic completion R̂ = AdicCompletion I R; assembling them gives a derivation D̂ of R̂ with D̂ ∘ ι = ι ∘ D for the canonical map ι : R → R̂ (Derivation.adicCompletion, Derivation.adicCompletion_of). This is the completion of a derivation behind Kollár's identity D(Î) = D(I)^ [Kol07, Lemma 74(5)], needed for the coordinate derivations ∂ᵢ of a regular local ring; it needs no hypothesis on D, I or R, so it is stated for an arbitrary derivation over an arbitrary base ring k.

Conventions

AdicCompletion I R is Mathlib's: compatible families x.val n ∈ R ⧸ (Iⁿ • ⊤). The level-n component of D̂ x is computed from the level-n + 1 component of x: lift x.val (n + 1) to f ∈ R, apply D, and reduce modulo Iⁿ; well defined by Derivation.mem_pow_of_mem_pow_succ. The properties of the completed coordinate derivations of a regular local ring (∂̂ᵢ xⱼ = δᵢⱼ, commutation, linearity over the coefficient field, the RegularCoords structure on R̂) are proved in Hironaka/Algebra/Local/CompletionCoords.lean.

theorem Derivation.mem_pow_of_mem_pow_succ {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (a : ℕ) {f : R} (hf : f ∈ I ^ (a + 1)) : D f ∈ I ^ a

A derivation lowers the powers of an ideal by one: D(Iᵃ⁺¹) ⊆ Iᵃ.

noncomputable def Derivation.adicLevel {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (n : ℕ) (y : R ⧸ I ^ (n + 1) • ⊤) : R ⧸ I ^ n • ⊤

The level-n component of the extended derivation: R/Iⁿ⁺¹ → R/Iⁿ, f mod Iⁿ⁺¹ ↦ D f mod Iⁿ.

Equations

• Derivation.adicLevel I D n y = Quotient.liftOn' y (fun (f : R) => Submodule.Quotient.mk (D f)) ⋯

@[simp]

theorem Derivation.adicLevel_mk {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (n : ℕ) (f : R) : adicLevel I D n (Submodule.Quotient.mk f) = Submodule.Quotient.mk (D f)

theorem Derivation.transitionMap_adicLevel {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) {m n : ℕ} (h : m ≤ n) (y : R ⧸ I ^ (n + 1) • ⊤) : (AdicCompletion.transitionMap I R h) (adicLevel I D n y) = adicLevel I D m ((AdicCompletion.transitionMap I R ⋯) y)

noncomputable def Derivation.adicCompletionFun {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (x : AdicCompletion I R) : AdicCompletion I R

The underlying function of the extended derivation.

Equations

• Derivation.adicCompletionFun I D x = ⟨fun (n : ℕ) => Derivation.adicLevel I D n (↑x (n + 1)), ⋯⟩

@[simp]

theorem Derivation.adicCompletionFun_val {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (x : AdicCompletion I R) (n : ℕ) : ↑(adicCompletionFun I D x) n = adicLevel I D n (↑x (n + 1))

noncomputable def Derivation.adicCompletion {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) : Derivation k (AdicCompletion I R) (AdicCompletion I R)

The extension of a derivation D of R to the I-adic completion R̂, computed level by level from D(Iⁿ⁺¹) ⊆ Iⁿ: the completed derivation of [Kol07, Lemma 74(5)].

Equations

• Derivation.adicCompletion I D = { toFun := Derivation.adicCompletionFun I D, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

@[simp]

theorem Derivation.adicCompletion_val {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (x : AdicCompletion I R) (n : ℕ) : ↑((adicCompletion I D) x) n = adicLevel I D n (↑x (n + 1))

theorem Derivation.adicCompletion_of {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (f : R) : (adicCompletion I D) ((AdicCompletion.of I R) f) = (AdicCompletion.of I R) (D f)

The extended derivation restricts to D along the canonical map R → R̂.

theorem Derivation.adicCompletion_algebraMap {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (I : Ideal R) (D : Derivation k R R) (f : R) : (adicCompletion I D) ((algebraMap R (AdicCompletion I R)) f) = (algebraMap R (AdicCompletion I R)) (D f)

D̂ ∘ ι = ι ∘ D for the algebra map ι : R → R̂.