The order under the local maps of étale and smooth algebras

For R → S smooth and a prime q of S over p, the local map R_p → S_q reflects the powers of the maximal ideal (OrdFaithful, Hironaka/Algebra/Local/OrderFlat.lean), hence preserves the order of every ideal: the local form of the invariance of the order under smooth morphisms stated in [Hau03, Appendix A].

• The étale case (ordFaithful_localRingHom_of_etale): R_p → S_q is flat (the localization of a flat algebra at a prime lying over a prime), local, and unramified and essentially of finite type, so 𝔪_p S_q = 𝔪_q ([TSPA, Tag 00UW], Mathlib's Algebra.FormallyUnramified.map_maximalIdeal); the flat local lemma ordFaithful_of_flat_of_map_maximalIdeal_eq applies.
• The smooth case (ordFaithful_localRingHom_of_isSmoothAt): a finitely presented algebra smooth at q is, near q, standard étale over a polynomial algebra (Mathlib's Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial): S_q ≅ T_{q'} for T = S[1/f], f ∉ q, and R → T factors as R → R[X₁, …, Xₙ] → T with the second map étale. R_p → T_{q'} is then the composite of the polynomial case (ordFaithful_localRingHom_mvPolynomial_C, Hironaka/Algebra/Local/OrderPolynomial.lean) and the étale case, and OrdFaithful composes and transports along isomorphisms.

Used for the invariance of the order under smooth morphisms of schemes (Hironaka/Scheme/IdealSheaf/Order/Smooth.lean).

theorem IsLocalRing.ordFaithful_localRingHom_of_etale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.Etale R S] (q : Ideal S) [q.IsPrime] {p : Ideal R} [p.IsPrime] (hpq : p = Ideal.comap (algebraMap R S) q) : OrdFaithful (Localization.localRingHom p q (algebraMap R S) hpq)

The étale case: for R → S étale and a prime q of S over p, the local map R_p → S_q reflects the powers of the maximal ideal. It is flat and local with 𝔪_p S_q = 𝔪_q (unramified and essentially of finite type, [TSPA, Tag 00UW]: Mathlib's Algebra.FormallyUnramified.map_maximalIdeal), so ordFaithful_of_flat_of_map_maximalIdeal_eq applies.

theorem IsLocalRing.ordFaithful_localRingHom_of_isSmoothAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] (q : Ideal S) [q.IsPrime] [Algebra.IsSmoothAt R q] {p : Ideal R} [p.IsPrime] (hpq : p = Ideal.comap (algebraMap R S) q) : OrdFaithful (Localization.localRingHom p q (algebraMap R S) hpq)

The order under the local maps of a smooth algebra: for R → S of finite presentation and smooth at the prime q of S over p, the local map R_p → S_q reflects the powers of the maximal ideal. Near q, S is standard étale over a polynomial algebra R[X₁, …, Xₙ]: S_q ≅ S[1/f]_{q'} with f ∉ q, and R_p → S[1/f]_{q'} is the polynomial case followed by the étale case.