The order under localizations of polynomial rings

For a prime q of R[X₁, …, Xₙ] over the prime p of R, the local map R_p → R[X₁, …, Xₙ]_q reflects the powers of the maximal ideal (OrdFaithful, Hironaka/Algebra/Local/OrderFlat.lean), so the order of an ideal is preserved (ord_map_eq_of_atPrime_mvPolynomial). This is the polynomial case of the invariance of the order under smooth morphisms ([Hau03, Appendix A]). A retraction Xᵢ ↦ 0 would treat only the primes q at which the Xᵢ reduce to residue-field elements, the points rational over the residue field; the proof here, the library's own, treats every prime, variable by variable:

• One variable over a local base R (ordFaithful_algebraMap_atPrime_polynomial): a prime Q of R[X] containing 𝔪 R[X] reduces to a prime of κ[X], κ = R/𝔪, which is 0 or (ḡ) with ḡ monic. In the first case Q = 𝔪 R[X]; in the second Q = (G) + 𝔪 R[X] for a monic lift G of ḡ, and D = R[X]/(G) is finite free over R with Q D = 𝔪 D a prime. In both cases R → R[X]_Q factors through the flat local map R → D_{QD} with 𝔪 D_{QD} = 𝔪_{D_{QD}} (D = R[X] in the first case), and a flat local map with this property reflects the powers of the maximal ideal by faithful flatness (ordFaithful_algebraMap_atPrime_of_flat, OrdFaithful.of_comp).
• One variable over any base (ordFaithful_localRingHom_C): R_p[X] is the localization of R[X] at C(R ∖ p), so R[X]_Q ≅ R_p[X]_{Q R_p[X]} and the local case applies.
• n variables (ordFaithful_localRingHom_mvPolynomial_C): induction on n through R[X₁, …, Xₙ₊₁] ≅ R[X₁, …, Xₙ][X] (Mathlib's MvPolynomial.finSuccEquiv); the property composes.

Used for the smooth case in Hironaka/Algebra/Local/OrderSmooth.lean.

theorem IsLocalRing.ordFaithful_algebraMap_atPrime_polynomial {R : Type u_1} [CommRing R] [IsLocalRing R] (Q : Ideal (Polynomial R)) [Q.IsPrime] (hQ : Ideal.map Polynomial.C (maximalIdeal R) ≤ Q) : OrdFaithful (algebraMap R (Localization.AtPrime Q))

The polynomial case in one variable over a local base R: for a prime Q of R[X] containing 𝔪 R[X], the local map R → R[X]_Q reflects the powers of the maximal ideal. The image of Q in κ[X] is 0 (then Q = 𝔪 R[X]) or generated by a monic ḡ (then Q = (G) + 𝔪 R[X] for a monic lift G, and R[X]_Q → (R[X]/(G))_{𝔪} is a local map to a flat local R-algebra whose maximal ideal is generated by 𝔪).

theorem IsLocalRing.ordFaithful_localRingHom_C {R : Type u_1} [CommRing R] (Q : Ideal (Polynomial R)) [Q.IsPrime] {p : Ideal R} [p.IsPrime] (hpQ : p = Ideal.comap Polynomial.C Q) : OrdFaithful (Localization.localRingHom p Q Polynomial.C hpQ)

The polynomial case in one variable over any base: for a prime Q of R[X] over the prime p = Q ∩ R, the local map R_p → R[X]_Q reflects the powers of the maximal ideal. R_p[X] is the localization of R[X] at C(R ∖ p), so R[X]_Q ≅ R_p[X]_{Q'} with Q' = Q R_p[X] a prime containing 𝔪_p R_p[X], and the local case applies.

theorem IsLocalRing.ordFaithful_localRingHom_mvPolynomial_C {R : Type u_1} [CommRing R] (n : ℕ) (q : Ideal (MvPolynomial (Fin n) R)) [q.IsPrime] {p : Ideal R} [p.IsPrime] (hpq : p = Ideal.comap MvPolynomial.C q) : OrdFaithful (Localization.localRingHom p q MvPolynomial.C hpq)

The polynomial case in n variables over any base: for a prime q of R[X₁, …, Xₙ] over the prime p = q ∩ R, the local map R_p → R[X₁, …, Xₙ]_q reflects the powers of the maximal ideal. Induction on n through R[X₁, …, Xₙ₊₁] ≅ R[X₁, …, Xₙ][X] (MvPolynomial.finSuccEquiv), the one-variable case (ordFaithful_localRingHom_C) and composition.

theorem IsLocalRing.ord_map_eq_of_atPrime_mvPolynomial {R : Type u_1} [CommRing R] [IsLocalRing R] {n : ℕ} (q : Ideal (MvPolynomial (Fin n) R)) [q.IsPrime] (hq : Ideal.comap (algebraMap R (MvPolynomial (Fin n) R)) q = maximalIdeal R) (J : Ideal R) : ord (Ideal.map (algebraMap R (Localization.AtPrime q)) J) = ord J

The order is preserved by localizations of polynomial rings: for a prime q of R[X₁, …, Xₙ] over the maximal ideal of the local ring R, ord (J R[X₁, …, Xₙ]_q) = ord J. The local map R → R[X₁, …, Xₙ]_q is R ≅ R_𝔪 → R[X₁, …, Xₙ]_q, which reflects the powers of the maximal ideal (ordFaithful_localRingHom_mvPolynomial_C).