The completion R̂ and its relation to R #
R is a Noetherian local ring, R̂ = AdicCompletion (maximalIdeal R) R and ι : R → R̂ the
canonical map: the completion of [Kol07, Definition 55]. This file collects what the rest of the
library needs about the passage from R to R̂: R̂ is local with the same residue field, the
order of an element or an ideal is preserved, ideals extend faithfully, and the coordinate
derivations extend, so that a coordinate structure on R induces one on R̂.
The completion is local with the same residue field #
Mathlib supplies everything: R̂ is local with maximal ideal 𝔪R̂
(AdicCompletion.maximalIdeal_eq_map), the residue map R/𝔪 → R̂/𝔪R̂ is bijective
(AdicCompletion.residueField_map_bijective) and R̂ is 𝔪R̂-adically complete. The four
statements are restated here under the names used later.
Order is preserved #
(𝔪R̂)ᵃ is the kernel of the evaluation R̂ → R/𝔪ᵃ at level a
(AdicCompletion.pow_smul_top_eq_ker_eval, read through Ideal.smul_top_eq_map), and the
evaluation of ι f is f mod 𝔪ᵃ; so ι f ∈ (𝔪R̂)ᵃ ↔ f ∈ 𝔪ᵃ. Since the order of an element is
sup {a : f ∈ 𝔪ᵃ} (Hironaka/Algebra/Local/Order.lean), ord (ι f) = ord f, and for ideals both
inequalities ord I ≤ ord (I R̂) (ι is a local homomorphism) and ord (I R̂) ≤ ord I
(generators) follow.
Ideals extend faithfully #
R → R̂ is flat (AdicCompletion.flat_of_isNoetherian) and local
(AdicCompletion.algebraMap_isLocalHom_of_fg), hence faithfully flat
(Module.FaithfullyFlat.of_flat_of_isLocalHom, [TSPA, Tag 00MC]), and for a faithfully flat
extension I R̂ ∩ R = I (Ideal.comap_map_eq_self_of_faithfullyFlat); so I R̂ = J R̂ forces
I = J. Finally I R̂ is the image of the completion Î of the module I: the image
contains each ι i (AdicCompletion.map_of), and it is contained in I R̂ because Î is the
image of R̂ ⊗ I (ofTensorProduct_surjective_of_finite, I finitely generated) and, by
naturality of ofTensorProduct, an elementary tensor r ⊗ i maps to r · ι i.
The coordinate derivations extend #
∂̂ᵢ := (∂ᵢ).adicCompletion 𝔪 (Hironaka/Algebra/Local/Completion.lean) restricts to ∂ᵢ along
ι, so ∂̂ᵢ (ι xⱼ) = ι (δᵢⱼ) = δᵢⱼ, and it kills the coefficient field when ∂ᵢ does.
Commutation is checked level by level: the level-n component of ∂̂ᵢ (∂̂ⱼ f) is ∂ᵢ ∂ⱼ h mod 𝔪ⁿ
for any lift h of the level-n + 2 component of f, symmetric in i, j by c.pderiv_comm.
With the regularity of R̂ supplied as an instance (it follows from the Cohen structure theorem,
Hironaka/Algebra/Local/CohenIso.lean), the pair (ι x, ∂̂) is a RegularCoords structure on
R̂: the ι xᵢ generate 𝔪R̂ (maximalIdeal_eq_map, Ideal.map_span), and the dimension field
follows from spanFinrank (𝔪R̂) = spanFinrank 𝔪 (AdicCompletion.spanFinrank_maximalIdeal_eq) and
regularity of both rings.
R̂ is a local ring (Mathlib's instance, restated).
The maximal ideal of R̂ is 𝔪R̂.
The residue field of R̂ is K.
R̂ is 𝔪R̂-adically complete.
ι f ∈ (𝔪R̂)ᵃ ↔ f ∈ 𝔪ᵃ, through the kernel of the evaluation at level a.
f ∈ 𝔪ᵃ ↔ ι f ∈ (𝔪R̂)ᵃ.
The order of an element is preserved under completion.
The order of an ideal is preserved under completion.
R → R̂ is faithfully flat (flat and local, [TSPA, Tag 00MC]).
I R̂ ∩ R = I (Krull's intersection theorem in the form recalled in [Kol07, Definition 55],
here from faithful flatness).
Extension of ideals to R̂ is injective: two subschemes with the same completion at a point
agree near it ([Kol07, Definition 55]).
I R̂ = Î, the image in R̂ of the completion of the module I.
The extended derivation restricts to D along ι (the completed derivations of
[Kol07, Lemma 74(5)]).
The extension kills the coefficient field whenever D does.
∂̂ᵢ (ι xⱼ) = δᵢⱼ.
The extended coordinate derivations commute.
The coordinate structure on R̂ with parameters ι xᵢ and derivations ∂̂ᵢ, given the
regularity of R̂ as an instance argument.
Equations
- One or more equations did not get rendered due to their size.
Instances For
R̂ carries a RegularCoords structure with parameters ι xᵢ and derivations ∂̂ᵢ, given
the regularity of R̂.