The order under local homomorphisms reflecting the powers of the maximal ideal

The order of an ideal does not drop under a local homomorphism φ : A → B (ord_le_ord_map, Hironaka/Algebra/Local/Order.lean). It is preserved when φ reflects the powers of the maximal ideal, φ⁻¹(𝔪_Bʳ) ⊆ 𝔪_Aʳ for every r (OrdFaithful φ; the reverse inclusion holds for every local map): then J B ⊆ 𝔪_Bʳ forces J ⊆ 𝔪_Aʳ, so ord_B (J B) ≤ ord_A J (ord_map_le_of_ordFaithful) and ord_B (J B) = ord_A J (ord_map_eq_of_ordFaithful). The property is stable under composition, transports along isomorphisms, and descends from ψ ∘ φ to φ when ψ is local (OrdFaithful.of_comp).

The main instance is the étale case: a flat local map with 𝔪_A B = 𝔪_B reflects the powers of the maximal ideal (ordFaithful_of_flat_of_map_maximalIdeal_eq), since 𝔪_Bʳ = 𝔪_Aʳ B and 𝔪_Aʳ B ∩ A = 𝔪_Aʳ, a flat local map being faithfully flat (Mathlib's Module.FaithfullyFlat.of_flat_of_isLocalHom and Ideal.comap_map_eq_self_of_faithfullyFlat); hence ord_B (J B) = ord_A J (ord_map_eq_of_flat_of_map_maximalIdeal_eq). Flatness alone does not suffice: k[t]_{(t)} → k[y]_{(y)}, t ↦ y², is flat and local and doubles the order. Two convenient forms: for a flat A-algebra D and a prime Q = 𝔪_A D, the map A → D_Q reflects the powers of the maximal ideal (ordFaithful_algebraMap_atPrime_of_flat), and so does the localization of a bijective ring map at a prime (ordFaithful_localRingHom_of_bijective).

This is the algebra behind the statement of [Hau03, Appendix A] that the order is invariant "with respect to smooth morphisms". The polynomial and smooth cases are Hironaka/Algebra/Local/OrderPolynomial.lean and Hironaka/Algebra/Local/OrderSmooth.lean; the transport of the bound of [Kol07, Lemma 61] along the chart-ring map is Hironaka/Algebra/Local/ChartOrderFaithful.lean; the flat case is used in Hironaka/Scheme/BlowUpSequence/BaseChangeOrder.lean and the vocabulary in Hironaka/Scheme/IdealSheaf/Order/Smooth.lean.

def IsLocalRing.OrdFaithful {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (φ : A →+* B) : Prop

A ring map φ : A → B of local rings reflects the powers of the maximal ideal: φ⁻¹(𝔪_Bʳ) ⊆ 𝔪_Aʳ for every r.

Equations

• IsLocalRing.OrdFaithful φ = ∀ (r : ℕ), Ideal.comap φ (IsLocalRing.maximalIdeal B ^ r) ≤ IsLocalRing.maximalIdeal A ^ r

theorem IsLocalRing.OrdFaithful.comap_pow_eq {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {φ : A →+* B} [IsLocalHom φ] (h : OrdFaithful φ) (r : ℕ) : Ideal.comap φ (maximalIdeal B ^ r) = maximalIdeal A ^ r

theorem IsLocalRing.ord_map_le_of_ordFaithful {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {φ : A →+* B} (h : OrdFaithful φ) (J : Ideal A) : ord (Ideal.map φ J) ≤ ord J

ord_B (J B) ≤ ord_A J when φ reflects the powers of the maximal ideal.

theorem IsLocalRing.ord_map_eq_of_ordFaithful {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {φ : A →+* B} [IsLocalHom φ] (h : OrdFaithful φ) (J : Ideal A) : ord (Ideal.map φ J) = ord J

ord_B (J B) = ord_A J for a local φ reflecting the powers of the maximal ideal.

theorem IsLocalRing.OrdFaithful.comp {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {C : Type u_3} [CommRing C] [IsLocalRing C] {φ : A →+* B} {ψ : B →+* C} (hφ : OrdFaithful φ) (hψ : OrdFaithful ψ) : OrdFaithful (ψ.comp φ)

theorem IsLocalRing.OrdFaithful.of_ringEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] (e : A ≃+* B) : OrdFaithful ↑e

An isomorphism of local rings reflects the powers of the maximal ideal (through its inverse, a local map).

theorem IsLocalRing.OrdFaithful.comp_ringEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {C : Type u_3} [CommRing C] [IsLocalRing C] {φ : A →+* B} (h : OrdFaithful φ) (e : B ≃+* C) : OrdFaithful ((↑e).comp φ)

Composition with an isomorphism on the target.

theorem IsLocalRing.OrdFaithful.ringEquiv_comp {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {C : Type u_3} [CommRing C] [IsLocalRing C] {φ : B →+* C} (h : OrdFaithful φ) (e : A ≃+* B) : OrdFaithful (φ.comp ↑e)

Composition with an isomorphism on the source.

theorem IsLocalRing.OrdFaithful.congr {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {φ ψ : A →+* B} (h : OrdFaithful φ) (e : φ = ψ) : OrdFaithful ψ

theorem IsLocalRing.OrdFaithful.of_comp {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] {C : Type u_3} [CommRing C] [IsLocalRing C] {φ : A →+* B} {ψ : B →+* C} [IsLocalHom ψ] (h : OrdFaithful (ψ.comp φ)) : OrdFaithful φ

If ψ ∘ φ reflects the powers of the maximal ideal and ψ is local, so does φ: φ⁻¹(𝔪_Bʳ) ⊆ (ψ ∘ φ)⁻¹(𝔪_Cʳ) ⊆ 𝔪_Aʳ.

theorem IsLocalRing.ordFaithful_localRingHom_of_bijective {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Bijective ⇑f) {p : Ideal R} [p.IsPrime] (q : Ideal S) [q.IsPrime] (hpq : p = Ideal.comap f q) : OrdFaithful (Localization.localRingHom p q f hpq)

The localization of a bijective ring map at a prime reflects the powers of the maximal ideal: it is inverted by the localization of the inverse map, a local map (OrdFaithful.of_comp).

theorem IsLocalRing.ordFaithful_of_flat_of_map_maximalIdeal_eq {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [Algebra A B] [Module.Flat A B] [IsLocalHom (algebraMap A B)] (h : Ideal.map (algebraMap A B) (maximalIdeal A) = maximalIdeal B) : OrdFaithful (algebraMap A B)

The étale case: a flat local map A → B with 𝔪_A B = 𝔪_B reflects the powers of the maximal ideal, since 𝔪_Bʳ = 𝔪_Aʳ B and 𝔪_Aʳ B ∩ A = 𝔪_Aʳ for the faithfully flat A → B.

theorem IsLocalRing.ord_map_eq_of_flat_of_map_maximalIdeal_eq {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B] [Algebra A B] [Module.Flat A B] [IsLocalHom (algebraMap A B)] (h : Ideal.map (algebraMap A B) (maximalIdeal A) = maximalIdeal B) (J : Ideal A) : ord (Ideal.map (algebraMap A B) J) = ord J

For a flat local map A → B with 𝔪_A B = 𝔪_B, ord_B (J B) = ord_A J.

theorem IsLocalRing.ordFaithful_algebraMap_atPrime_of_flat {A : Type u_1} [CommRing A] [IsLocalRing A] {D : Type u_3} [CommRing D] [Algebra A D] [Module.Flat A D] (Q : Ideal D) [Q.IsPrime] (hQ : Q = Ideal.map (algebraMap A D) (maximalIdeal A)) : OrdFaithful (algebraMap A (Localization.AtPrime Q))

A flat A-algebra D and a prime Q = 𝔪_A D of D: A → D_Q is flat and local with 𝔪_A D_Q = Q D_Q = 𝔪_{D_Q}, hence reflects the powers of the maximal ideal. (The shape of both cases of the one-variable polynomial case in Hironaka/Algebra/Local/OrderPolynomial.lean: D = A[X] with Q = 𝔪_A A[X], and D = A[X]/(G) for a monic G.)