The monomial split, II: orders at the generic points of the components

At the generic point η of an irreducible component D of a member E^i of a normal-crossings family, the local ring 𝒪_{X,η} has maximal ideal (E^i)_η = (z_c), generated by the one parameter of the member (the reduced ideal of D at η is both the maximal ideal and, by the minimal-prime dictionary of Hironaka/Resolution/Algebraic/Snc/DictionaryGenericPoints.lean, the stalk of E^i); no other member passes through η, since two distinct parameters cannot both generate 𝔪_η. Hence at η the stalk of a monomial 𝒪_X(−∑_D a_D D) is (z_c)^{a_D}, of order a_D, and the order of (z_c)^a · J is a + ord J, by the multiplicativity of the order on the regular local ring 𝒪_{X,η} containing ℚ. The membership half of [Kol07, Definition–Lemma 110], that I ⊆ (z_c)^{ord_D I} at every point of D, is the propagation of [Kol07, Definition 47] from the generic point: ordAlong_stalkIdeal_eq_ord_stalkIdeal for the integral component subscheme together with the local lemma le_pow_of_le_ordAlong_span_singleton (m ≤ ord_{(p)} I ⟹ I ⊆ (p)^m for a prime element p).

• Snc.stalkIdeal_monomial_genericPoint: the stalk of a monomial at a generic point.
• Snc.ord_monomial_genericPoint: the order of a monomial at a generic point.

The local algebra used here is in Hironaka/Scheme/Snc/ParameterAlgebra.lean, Hironaka/Resolution/Algebraic/Snc/DictionaryGenericPoints.lean, Hironaka/Resolution/Algebraic/Snc/DictionaryRegular.lean and Hironaka/Resolution/Algebraic/Snc/ComponentStalks.lean.

The component at its generic point

theorem Hironaka.BMO.Snc.stalkIdeal_monomial_genericPoint {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) [TopologicalSpace.NoetherianSpace ↥X] {i : E.ι} {η : ↥X} (hη : η ∈ (E.component i).support.genericPoints) (a : ↥X → ℕ) : (E.monomial a).stalkIdeal η = (E.component i).stalkIdeal η ^ a η

At the generic point of a component of E^i the stalk of a monomial is the power of (E^i)_η at the component's exponent.

Orders at the generic point

theorem Hironaka.BMO.Snc.ord_monomial_genericPoint {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) [CharZero k] [TopologicalSpace.NoetherianSpace ↥X] {i : E.ι} {η : ↥X} (hη : η ∈ (E.component i).support.genericPoints) (a : ↥X → ℕ) : (E.monomial a).ord η = ↑(a η)

The order of a monomial at the generic point of a component is the component's exponent (the reading of 𝒪_X(−∑_D a_D D) in [Kol07, Definition–Lemma 110]).