R̂ ≅ K⟦X₁, …, X_d⟧ for a regular local ring containing ℚ #
The Cohen structure theorem in the form Kollár uses, Ô_{p,X} ≅ k(p)⟦x₁, …, xₙ⟧
[Kol07, Definition 55]. With the coefficient field
(Hironaka/Algebra/Local/CoefficientField.lean), the map Φ
(Hironaka/Algebra/Local/CohenMap.lean) and its surjectivity (Hironaka/Algebra/Local/Cohen.lean),
what remains is the injectivity of Φ, which is where the regularity of R enters:
R̂is Noetherian, as a quotient ofK⟦X⟧(isNoetherianRing_adicCompletion).dim R̂ = dim R(ringKrullDim_adicCompletion_eq; [TSPA, Tag 07NV]):R → R̂is flat (AdicCompletion.flat_of_isNoetherian), hence satisfies going down (Algebra.HasGoingDown.of_flat); Krull's height formula for a prime lying over a prime (Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown, [TSPA, Tag 00ON]) applied to𝔪̂over𝔪givesheight 𝔪̂ = height 𝔪 + height (𝔪̂/𝔪R̂), and the fibreR̂/𝔪R̂ = Kis a field, so the last term is zero; heights of the maximal ideals are the Krull dimensions (IsLocalRing.maximalIdeal_height_eq_ringKrullDim).- If
Φ(F) = 0withF ≠ 0, thenR̂is a quotient ofK⟦X⟧/(F), whose dimension is at mostd − 1becauseFis a nonzerodivisor of the domainK⟦X⟧(ringKrullDim_quotient_succ_le_of_nonZeroDivisor); butdim R̂ = dim R = dby 2 and the hypothesis thatx₁, …, x_dis a regular system of parameters. SoΦis injective.
Consequences: Φ is a ring isomorphism (cohenEquiv), R̂ is a regular local ring (from the
regularity of K⟦X⟧, Hironaka/Algebra/Local/PowerSeriesRegular.lean, by
IsRegularLocalRing.of_ringEquiv), and the order is multiplicative on R (for [Algebra ℚ R]):
ord_R f = ord_{R̂} (ι f) (Hironaka/Algebra/Local/CompletionCoords.lean) is transported along
Φ⁻¹ to K⟦X⟧, where it is MvPowerSeries.order (MvPowerSeries.ordElem_eq_order) and
order (f g) = order f + order g (MvPowerSeries.order_mul). Neither the general Cohen
structure theorem nor the associated graded ring is used.
Everything is proved for an arbitrary coefficient field [Algebra (ResidueField R) R̂] with
hι : IsCoefficientAlgebra R (the …_of_residue declarations and cohenEquivOfResidue; the only
use of hι is the surjectivity), then specialized to the chosen coefficient field (ℚ ⊆ R).
The completed chart map (Hironaka/Algebra/Local/ChartCompletion.lean) applies the general form to
the chart's local ring R'_{𝔪'} with the coefficient field transported from R̂.
Transport of the order along a ring isomorphism of local rings #
The order of an element is invariant under a ring isomorphism of local rings
(ord_le_ord_map in both directions).
dim R̂ = dim R [TSPA, Tag 07NV], by going down along the flat map R → R̂ and the
zero-dimensional fibre R̂/𝔪R̂ = K.
R̂ is Noetherian, being a quotient of K⟦X₁, …, X_d⟧; for any coefficient field.
Φ is injective when x₁, …, x_d is a regular system of parameters: a nonzero kernel would
drop the dimension of the quotient below d = dim R = dim R̂. For any coefficient field. (The
injectivity half of [Kol07, Definition 55], for which Kollár refers to Shafarevich's textbook.)
Φ : K⟦X₁, …, X_d⟧ ≃ R̂ [Kol07, Definition 55], for any coefficient field (the form used on
the chart's local ring in Hironaka/Algebra/Local/ChartCompletion.lean).
Equations
- IsLocalRing.cohenEquivOfResidue R x hι hx hd = RingEquiv.ofBijective (IsLocalRing.cohenMap' R x hx).toRingHom ⋯
Instances For
The completion of a regular local ring with a regular system of parameters x₁, …, x_d and a
coefficient field is a regular local ring.
The order of a product is the sum of the orders, for R a regular local ring with a regular
system of parameters x₁, …, x_d and a coefficient field (used silently by Kollár in property (3)
of [Kol07, Definition 59] and in [Kol07, Theorem 54.2]; a regular local ring is a domain whose
associated graded ring is a polynomial ring, [AM69, 11.22–11.23]).
The specializations at the chosen coefficient field (ℚ ⊆ R).
R̂ is Noetherian, being a quotient of K⟦X₁, …, X_d⟧.
Φ is injective when x₁, …, x_d is a regular system of parameters.
Φ : K⟦X₁, …, X_d⟧ ≃ R̂, the identification of [Kol07, Definition 55].
Equations
- IsLocalRing.cohenEquiv R x hx hd = IsLocalRing.cohenEquivOfResidue R x ⋯ hx hd
Instances For
The completion of a regular local ring containing ℚ with a regular system of parameters
x₁, …, x_d is a regular local ring.
For R a regular local ring containing ℚ with a regular system of parameters x₁, …, x_d,
the order of a product is the sum of the orders.
The completion of a regular local ring containing ℚ is a regular local ring, as an
instance: the instance argument of RegularCoords.adicCompletion
(Hironaka/Algebra/Local/CompletionCoords.lean).
The order is multiplicative on a regular local ring containing ℚ: the hypothesis hmul of
the order calculus of Hironaka/Algebra/Local/Order.lean, discharged.