Derivatives commute with completion

Kollár's D(Î) = \widehat{D(I)}, where ^ denotes completion [Kol07, Lemma 74(5)]. With the extended coordinate derivations ∂̂ᵢ of Hironaka/Algebra/Local/CompletionCoords.lean (∂̂ᵢ ∘ ι = ι ∘ ∂ᵢ, so that R̂ carries the coordinate structure c.adicCompletion, given its regularity) and the identification I R̂ = Î, this is the case e = id of the base-change formula D(φ(I)) = φ(D(I)) of Hironaka/Algebra/Local/Derivative.lean (D_map): D(I R̂) = D(I) R̂. Iterating, Dʳ(I R̂) = Dʳ(I) R̂, in particular MC(Î) = \widehat{MC(I)} (Kollár's "since taking derivatives commutes with completion (74.5), we see that \widehat{MC(I)} = MC(Î)" in the discussion preceding [Kol07, Theorem 92]), and, since I R̂ ∩ R = I, I is MC-invariant iff Î is — the transfer used in the proof of [Kol07, Theorem 92].

theorem IsLocalRing.map_adicCompletion_le_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {I J : Ideal R} : Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I ≤ Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) J ↔ I ≤ J

Extension of ideals to R̂ reflects inclusions (from I R̂ ∩ R = I).

theorem IsLocalRing.RegularCoords.adicCompletion_pderiv_algebraMap {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (i : Fin n) (f : R) : (c.adicCompletion.pderiv i) ((algebraMap R (AdicCompletion (maximalIdeal R) R)) f) = (algebraMap R (AdicCompletion (maximalIdeal R) R)) ((c.pderiv i) f)

The extended coordinate derivations restrict to the originals, read through c.adicCompletion: ∂̂ᵢ (ι f) = ι (∂ᵢ f).

theorem IsLocalRing.RegularCoords.D_adicCompletion {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (I : Ideal R) : c.adicCompletion.D (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I) = Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (c.D I)

Derivatives commute with completion [Kol07, Lemma 74(5)]: D(I R̂) = D(I) R̂, the case e = id of D_map applied to ι : R → R̂ and the extended derivations.

theorem IsLocalRing.RegularCoords.Dpow_adicCompletion {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (r : ℕ) (I : Ideal R) : c.adicCompletion.Dpow r (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I) = Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (c.Dpow r I)

Iterated: Dʳ(I R̂) = Dʳ(I) R̂.

theorem IsLocalRing.RegularCoords.D_range_adicCompletion_map_subtype {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (I : Ideal R) : c.adicCompletion.D ((AdicCompletion.map (maximalIdeal R)) (Submodule.subtype I)).range = ((AdicCompletion.map (maximalIdeal R)) (Submodule.subtype (c.D I))).range

Kollár's notation D(Î) = \widehat{D(I)} [Kol07, Lemma 74(5)], with Î the image in R̂ of the completion of the module I (range_adicCompletion_map_subtype).

theorem IsLocalRing.RegularCoords.MC_adicCompletion {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (I : Ideal R) (m : ℕ) : c.adicCompletion.MC (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I) m = Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (c.MC I m)

MC(Î) = \widehat{MC(I)}, i.e. D^{m-1}(I R̂) = D^{m-1}(I) R̂ (the discussion preceding [Kol07, Theorem 92]).

theorem IsLocalRing.RegularCoords.comap_D_adicCompletion {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (I : Ideal R) : Ideal.comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (c.adicCompletion.D (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I)) = c.D I

D(I R̂) ∩ R = D(I).

theorem IsLocalRing.RegularCoords.comap_MC_adicCompletion {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (I : Ideal R) (m : ℕ) : Ideal.comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (c.adicCompletion.MC (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I) m) = c.MC I m

MC(Î) ∩ R = MC(I).

theorem IsLocalRing.RegularCoords.isMCInvariant_adicCompletion_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) [IsRegularLocalRing (AdicCompletion (maximalIdeal R) R)] (I : Ideal R) (m : ℕ) : c.adicCompletion.IsMCInvariant (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) I) m ↔ c.IsMCInvariant I m

I is MC-invariant with respect to m iff I R̂ is: the transfer of MC-invariance to the completion in the discussion preceding [Kol07, Theorem 92], with the definition (53.1) of [Kol07, 53].