The completed chart map is the chart substitution #
[Kol07, (60.3)] writes the chart map R → R'_{𝔪'} in the coordinates x of R and y of the
chart as the substitution xᵢ ↦ yᵢ y_r (i < r), xⱼ ↦ yⱼ (j ≥ r). This module proves that
statement for the completions (hasCohenChart): the map R̂ → (R'_{𝔪'})^ induced by R → R'_{𝔪'}
is the substitution chartSubst r of Hironaka/Algebra/Local/ChartSubst.lean under the Cohen
isomorphism R̂ ≅ K⟦x⟧ (cohenEquiv, Hironaka/Algebra/Local/CohenIso.lean) and the Cohen
isomorphism (R'_{𝔪'})^ ≅ K⟦y⟧ built on the coefficient field transported from R̂
(chartCoefficientField, Hironaka/Algebra/Local/Lemma61.lean) and on the regular system of
parameters y of R'_{𝔪'} (Hironaka/Algebra/Local/ChartLocal.lean). This is the predicate
HasCohenChart of Hironaka/Algebra/Local/Lemma61.lean, whose order bounds thereby become
unconditional.
The identification is proved level by level (completionMap_cohenMap) for an abstract target: a
Noetherian local ring B with a local homomorphism φ : R → B, a family y in B satisfying the
chart relations φ(xᵢ) = y_r yᵢ (i < r), φ(xⱼ) = yⱼ, and a coefficient field on B̂ compatible
with that of R̂ through a ring map e of residue fields. Modulo 𝔪_B̂ᴺ, both φ̂(Φ_R(F)) and
Φ_B(subst (F.map e)), where Φ_R = cohenMap R x and Φ_B = cohenMap B y, are the evaluation of
the truncation truncTotal N F at the images of the variables (mk_completionMap_cohenMap).
Keeping B abstract keeps every unification away from the concrete chart ring, whose definition
as an Algebra.adjoin Lean would otherwise unfold.
Elementary inputs collected here: the chart relations in R'_{𝔪'} (algebraMap_x_atPrime); the
chart substitution as a polynomial substitution (chartSubstPoly, subst_chartSubst_coe), so
that on truncations it is a polynomial evaluation; its compatibility with a change of
coefficients (map_subst_chartSubst); and the isomorphism of residue fields K ≃ K_B
(chartResidueEquiv).
Used in Hironaka/Resolution/Analytic/GoingUp/MaxOrder.lean;
Hironaka/Algebra/Local/ChartCompletionHom.lean and Hironaka/Algebra/Local/ChartHom.lean build on
it.
φ(xᵢ) = y_r yᵢ in R'_{𝔪'} for i < r.
φ(xⱼ) = yⱼ in R'_{𝔪'} for j ≥ r.
The chart substitution as a polynomial substitution: Xᵢ ↦ Xᵢ X_r (i < r), Xⱼ ↦ Xⱼ.
Equations
- IsLocalRing.chartSubstPoly r i = if i < r then MvPolynomial.X i * MvPolynomial.X r else MvPolynomial.X i
Instances For
On polynomials the chart substitution is the polynomial substitution chartSubstPoly.
The chart substitution commutes with a change of coefficients.
Truncation commutes with a change of coefficients.
The isomorphism e : K ≃ K_B of residue fields induced by R → R'_{𝔪'}.
Equations
Instances For
The transported coefficient field on e k is φ̂ of the coefficient field of R̂ on k.
The chart's local ring is Noetherian, being a localization of the Noetherian chart ring.
The regular system of parameters y of the chart's local ring
(maximalIdeal_localization_chartOrigin).
Equations
- IsLocalRing.chartY' x r i = (algebraMap (↥(IsLocalRing.chartRing x r)) (Localization.AtPrime (IsLocalRing.chartOrigin x r))) (IsLocalRing.chartYR x r i)
Instances For
The completed chart map for an abstract target #
The level-by-level identification is proved for an arbitrary Noetherian local ring B with a local
homomorphism φ : R → B, a family y in B satisfying the chart relations φ(xᵢ) = y_r yᵢ
(i < r), φ(xⱼ) = yⱼ, and a coefficient-field datum on B̂ compatible with that of R̂
through a ring map e of residue fields. Keeping B abstract keeps every unification away
from the concrete chart ring (whose definition as an adjoin Lean would otherwise unfold).
The level-N map R̂/𝔪̂ᴺ → B̂/𝔪_B̂ᴺ induced by φ̂.
Equations
Instances For
Constants: the level map carries the coefficient field of R̂ to the datum on B̂.
Variables: φ̂(ι xᵢ) at level N is the chart substitution evaluated at the levelVar of
y.
Polynomials: the level map of an evaluation at the levelVar of x is the evaluation, at the
levelVar of y, of the chart substitution of the polynomial with coefficients moved by e.
Level N of the identification: modulo 𝔪_B̂ᴺ, φ̂(Φ_R(F)) is the Cohen map of B applied
to the chart substitution of F (coefficients moved by e).
The completed chart map for an abstract target: φ̂ ∘ Φ_R = Φ_B ∘ subst ∘ map e.
The transported coefficient field as an algebra structure on (R'_{𝔪'})^.
Equations
- IsLocalRing.chartCompletionAlgebra x r hx hn = (IsLocalRing.chartCoefficientField x r hx hn).toAlgebra
Instances For
The chart relations in the local ring: φ(xᵢ) = y_r yᵢ (i < r), φ(xⱼ) = yⱼ.
The completed chart map is the chart substitution ([Kol07, (60.3)]): the map induced on
completions by R → R'_{𝔪'} is the chart substitution xᵢ ↦ yᵢ y_r (i < r), xⱼ ↦ yⱼ (j ≥ r)
under the Cohen isomorphism of R̂ and the Cohen isomorphism of (R'_{𝔪'})^ built on the
transported coefficient field chartCoefficientField and the regular system of parameters y of
R'_{𝔪'}, by the level-by-level identification completionMap_cohenMap.