Lemma 61 in local form: the order bounds at the rational points of the chart

[Kol07, Lemma 61]: for I ≤ Pᵐ with ord_R I = m, the transform π⁻¹_*(I, m) has order ≤ m at every point of the chart over 𝔪 rational over the residue field K. Kollár's proof computes at the origin of the chart and moves the origin by a linear change of coordinates. Here the computation at the origin is done through the completion: the map R̂ → B̂ induced by φ : R → B = R'_{𝔪'}, the local ring of the chart ring R' at the chart origin 𝔪' = (y), is the chart substitution xᵢ ↦ yᵢ y_r (i < r), xⱼ ↦ yⱼ (j ≥ r) under the Cohen isomorphisms of R̂ and B̂ (the predicate HasCohenChart, proved in Hironaka/Algebra/Local/ChartCompletion.lean), and the order bound then follows from ordElem_le_of_completionMap_eq_subst of Hironaka/Algebra/Local/TransformOrder.lean. At the other K-rational points 𝔪'_a of the chart (chartOriginAt), the same statement holds for the shifted coordinates x' = shiftCoords x r a of Hironaka/Algebra/Local/ChartRing.lean, transported along the isomorphism R'_{𝔪'(x')} ≃ R'_{𝔪'_a} of Hironaka/Algebra/Local/ChartShift.lean.

Main results, all under the hypothesis HasCohenChart (for x, or for the shifted coordinates):

• ord_{R'_{𝔪'}} π⁻¹_*(f, m) ≤ m for f ∈ I of order m (ordElem_transformElem_le_of_hasCohenChart);
• ord_{R'_{𝔪'}} π⁻¹_*(I, m) ≤ m (ord_map_transformIdeal_le_of_hasCohenChart);
• the same bound at 𝔪'_a (ord_map_transformIdeal_le_at_of_hasCohenChart) and hence at every K-rational point of the chart over 𝔪 (ord_map_transformIdeal_le_of_rational_of_hasCohenChart).

Also here: R → R'_{𝔪'} and R → R'_{𝔪'_a} are local homomorphisms (isLocalHom_algebraMap_atPrime_chartOrigin, isLocalHom_algebraMap_atPrime_chartOriginAt); the residue field of R'_{𝔪'} is K (residueField_map_bijective_chartOrigin); and the coefficient field of R̂ is transported to a coefficient field of (R'_{𝔪'})^ along the induced map (chartCoefficientField, residue_chartCoefficientField), the datum on which the Cohen isomorphism of (R'_{𝔪'})^ is built in Hironaka/Algebra/Local/ChartCompletion.lean.

The bound at every prime of the fibre, rational or not, is obtained by a different argument in Hironaka/Algebra/Local/ChartFibre.lean. Used in Hironaka/Resolution/Analytic/GoingUp/MaxOrder.lean.

theorem IsLocalRing.isLocalHom_algebraMap_atPrime_chartOrigin {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOrigin x r).IsPrime] : IsLocalHom (algebraMap R (Localization.AtPrime (chartOrigin x r)))

R → R'_{𝔪'} is a local homomorphism: 𝔪' lies over 𝔪.

theorem IsLocalRing.isLocalHom_algebraMap_atPrime_chartOriginAt {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOriginAt x r a).IsPrime] : IsLocalHom (algebraMap R (Localization.AtPrime (chartOriginAt x r a)))

R → R'_{𝔪'_a} is a local homomorphism: 𝔪'_a lies over 𝔪.

theorem IsLocalRing.residueField_map_bijective_chartOrigin {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOrigin x r).IsPrime] : Function.Bijective ⇑(ResidueField.map (algebraMap R (Localization.AtPrime (chartOrigin x r))))

The residue field of the chart's local ring R'_{𝔪'} is K = R/𝔪: R'/𝔪' ≅ R/𝔪 (quotientMap_chartOrigin_bijective), and the residue field of a localization at a maximal ideal is the quotient; so ResidueField.map (R → R'_{𝔪'}) is bijective.

noncomputable def IsLocalRing.chartCoefficientField {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOrigin x r).IsPrime] : ResidueField (Localization.AtPrime (chartOrigin x r)) →+* AdicCompletion (maximalIdeal (Localization.AtPrime (chartOrigin x r))) (Localization.AtPrime (chartOrigin x r))

The coefficient field on the completion of B = R'_{𝔪'} transported from R̂ along the induced map: ι_B := φ̂ ∘ σ_R ∘ e⁻¹, with σ_R the coefficient field of R̂ and e : K ≃ K_B the isomorphism of residue fields.

Equations

• One or more equations did not get rendered due to their size.

theorem IsLocalRing.residue_chartCoefficientField {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOrigin x r).IsPrime] (k : ResidueField (Localization.AtPrime (chartOrigin x r))) : (residue (AdicCompletion (maximalIdeal (Localization.AtPrime (chartOrigin x r))) (Localization.AtPrime (chartOrigin x r)))) ((chartCoefficientField x r hx hn) k) = (residueFieldEquiv (Localization.AtPrime (chartOrigin x r))) k

The transported datum is a coefficient field: it is a section of the residue map of (R'_{𝔪'})^, as the Cohen isomorphism cohenEquivOfResidue requires.

def IsLocalRing.HasCohenChart {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOrigin x r).IsPrime] : Prop

There is a Cohen isomorphism Ψ : K⟦y⟧ ≃ B̂ of the completion of B = R'_{𝔪'} under which the map induced by R → B is the chart substitution xᵢ ↦ yᵢ y_r (i < r), xⱼ ↦ yⱼ (j ≥ r) of [Kol07, (60.3)]. Proved in Hironaka/Algebra/Local/ChartCompletion.lean (hasCohenChart).

Equations

• One or more equations did not get rendered due to their size.

theorem IsLocalRing.ordElem_transformElem_le_of_hasCohenChart {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOrigin x r).IsPrime] (hΨ : HasCohenChart x r hx hn) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) {f : R} (hf : f ∈ I) (hord : ordElem f = ↑m) : ordElem ((algebraMap (↥(chartRing x r)) (Localization.AtPrime (chartOrigin x r))) (transformElem x r f ⋯)) ≤ ↑m

(The proof of [Kol07, Lemma 61].) Given HasCohenChart, for I ≤ Pᵐ and f ∈ I of order m, ord_{R'_{𝔪'}} π⁻¹_*(f, m) ≤ m.

theorem IsLocalRing.ord_map_transformIdeal_le_of_hasCohenChart {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOrigin x r).IsPrime] (hΨ : HasCohenChart x r hx hn) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (hord : ord I = ↑m) : ord (Ideal.map (algebraMap (↥(chartRing x r)) (Localization.AtPrime (chartOrigin x r))) (transformIdeal x r I m)) ≤ ↑m

Kollár's "This shows that ord_{p'} π⁻¹_* I ≤ m" (the proof of [Kol07, Lemma 61]), given HasCohenChart: for I ≤ Pᵐ with ord I = m, ord_{R'_{𝔪'}} π⁻¹_*(I, m) ≤ m.

theorem IsLocalRing.ord_map_transformIdeal_le_at_of_hasCohenChart {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (r : Fin n) (a : Fin n → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) [(chartOriginAt x r a).IsPrime] [(chartOrigin (shiftCoords x r a) r).IsPrime] (hΨ : HasCohenChart (shiftCoords x r a) r ⋯ hn) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (hord : ord I = ↑m) : ord (Ideal.map (algebraMap (↥(chartRing x r)) (Localization.AtPrime (chartOriginAt x r a))) (transformIdeal x r I m)) ≤ ↑m

The same bound at the K-rational point 𝔪'_a of the chart (Kollár's linear change of coordinates moving the origin, in the proof of [Kol07, Lemma 61]), given HasCohenChart for the shifted coordinates x': through the isomorphism R'_{𝔪'(x')} ≃ R'_{𝔪'_a} of Hironaka/Algebra/Local/ChartShift.lean; the transform π⁻¹_*(f, m) satisfies the same equation x_rᵐ g = f in both.

theorem IsLocalRing.ord_map_transformIdeal_le_of_rational_of_hasCohenChart {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (r : Fin n) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (hΨ : ∀ (a : Fin n → R), HasCohenChart (shiftCoords x r a) r ⋯ hn) (q : Ideal ↥(chartRing x r)) [q.IsPrime] (hq : ∃ (a : Fin n → R), q = chartOriginAt x r a) {I : Ideal R} {m : ℕ} (hI : I ≤ chartCenter x r ^ m) (hord : ord I = ↑m) : ord (Ideal.map (algebraMap (↥(chartRing x r)) (Localization.AtPrime q)) (transformIdeal x r I m)) ≤ ↑m

[Kol07, Lemma 61] in local form: the bound at every K-rational point q = 𝔪'_a of the chart over 𝔪, given HasCohenChart for the shifted coordinates.