Dividing an ideal by a principal prime: the order along divisors

The algebra behind the exponents after a step of the monomial phase (the controlled transform (M/𝓘(D)) · N of the remarks after [Wlo09, Theorem 2.0.3]; the cosupport of N(I) contains no E^i, [Kol07, Definition–Lemma 110]). In a domain R, for an ideal I ⊆ (g):

• I = g · (I : g) (Ideal.span_singleton_mul_colon_of_le, from BMO/SplitOrder.lean);
• along the divisor (g) itself the colon drops the order by exactly one: (I : g) ⊆ (g)^p ↔ I ⊆ (g)^{p+1} (Ideal.colon_span_singleton_le_pow_iff, cancelling g ≠ 0);
• along another prime divisor (f) with f ∤ g the colon does not change the order: (I : g) ⊆ (f)^p ↔ I ⊆ (f)^p (Ideal.colon_span_singleton_le_pow_iff_of_prime, from Prime.pow_dvd_of_dvd_mul_left).

Read on the stalks of ideal sheaves (ordAlongIdeal), these give ord_D (J : D) + 1 = ord_D J for the principal centre D and ord_{D'} (J : D) = ord_{D'} J for a transversal prime divisor D' (IdealSheaf.ordAlongIdeal_colon_add_one, IdealSheaf.ordAlongIdeal_colon_of_prime). The stalks of the structure sheaf are domains (isDomain_stalk) and the coordinates of a chart with simple normal crossings are pairwise non-dividing primes (IsSncChartAt.prime_coord, IsSncChartAt.not_coord_dvd), which is how Step2bExponent.lean applies them.

theorem Ideal.colon_span_singleton_le_pow_iff {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} {g : R} (hg : g ≠ 0) (hI : I ≤ span {g}) (p : ℕ) : Submodule.colon I ↑(span {g}) ≤ span {g} ^ p ↔ I ≤ span {g} ^ (p + 1)

Along the principal divisor (g) itself, dividing by g drops the order by one: (I : g) ⊆ (g)^p ↔ I ⊆ (g)^{p+1} (for I ⊆ (g), g ≠ 0).

theorem Ideal.colon_span_singleton_le_pow_iff_of_prime {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} {f g : R} (hf : Prime f) (hfg : ¬f ∣ g) (hI : I ≤ span {g}) (p : ℕ) : Submodule.colon I ↑(span {g}) ≤ span {f} ^ p ↔ I ≤ span {f} ^ p

Along a prime divisor (f) with f ∤ g, dividing by g does not change the order: (I : g) ⊆ (f)^p ↔ I ⊆ (f)^p (for I ⊆ (g)).

theorem Hironaka.Manifold.ENat.eq_add_one_of_forall_succ_le_iff {a b : ℕ∞} (h : ∀ (p : ℕ), ↑p ≤ a ↔ ↑p + 1 ≤ b) : a + 1 = b

p ≤ a for every natural p with p ≤ b, and conversely, gives a = b in ℕ∞ (ENat.eq_of_forall_natCast_le_iff); the shifted form used below.

theorem Manifold.IdealSheaf.ordAlongIdeal_colon_add_one {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J J' : IdealSheaf 𝒪) {a : ↑X} {g : ↑(𝒪.presheaf.stalk a)} [IsDomain ↑(𝒪.presheaf.stalk a)] (hD : D.stalkIdeal a = Ideal.span {g}) (hg : g ≠ 0) (hJ : J.stalkIdeal a ≤ Ideal.span {g}) (hJ' : J'.stalkIdeal a = Submodule.colon (J.stalkIdeal a) ↑(Ideal.span {g})) : D.ordAlongIdeal J' a + 1 = D.ordAlongIdeal J a

Along the principal centre D with stalk (g), the order of the colon J : D is one less than the order of J (for J_a ⊆ (g), g ≠ 0): ord_D (J : D) + 1 = ord_D J.

theorem Manifold.IdealSheaf.ordAlongIdeal_colon_of_prime {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D' J J' : IdealSheaf 𝒪) {a : ↑X} {f g : ↑(𝒪.presheaf.stalk a)} [IsDomain ↑(𝒪.presheaf.stalk a)] (hD' : D'.stalkIdeal a = Ideal.span {f}) (hf : Prime f) (hfg : ¬f ∣ g) (hJ : J.stalkIdeal a ≤ Ideal.span {g}) (hJ' : J'.stalkIdeal a = Submodule.colon (J.stalkIdeal a) ↑(Ideal.span {g})) : D'.ordAlongIdeal J' a = D'.ordAlongIdeal J a

Along a prime divisor D' with stalk (f), f ∤ g, the order of the colon J : (g) equals the order of J (for J_a ⊆ (g)): ord_{D'} (J : g) = ord_{D'} J.