The pointwise pass over a member

Step 2.1 of the proof of [Kol07, Theorem 103] applies [Kol07, Lemma 102] to each member Eʲ of the boundary: the centres of the output over Eʲ are push-forwards of centres of the inductive run on the strict transform of Eʲ, whose data are the restrictions of the outer data ([Kol07, Lemma 62]). For the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) this means that the classification of such a centre at a point g q' follows from the inductive classification at q'. This module holds the pointwise statement centerClassifiedAt_of_comap_member: for a closed immersion g : Y ⟶ X whose kernel is the member Eʲ⁰ of E, and a family F on Y whose members are the restrictions of the other members of E, every chain-coordinate system at g q' in which the current ideal K has the K-shape or the I-shape restricts to one at q'. The coordinate k₀ of Eʲ⁰ generates the kernel of the stalk map (ker_stalkMap_of_isClosedImmersion); the others restrict to a regular system of parameters (isRegularSystemOfParameters_comp_succAbove); the members of F through q' are the members of E through g q' other than Eʲ⁰ (a member restricting Eʲ⁰ itself would have the zero stalk, against the snc of F); the exponent of k₀ in the top monomial is 0 (the restricted ideal is nonzero); and the shape restricts — either no level below r kills k₀ (map_span_mul_chainKIdeal_of_forall, map_span_mul_chainIdeal_of_forall), or a first level l₀ does (exists_min_level; map_span_mul_chainKIdeal_of_lt, map_span_mul_chainIdeal_of_lt, the truncated un-isolated form). The inductive classification, read at the restricted system (truncated in the second case, chainCoordsFree_castLE), gives a stratum of the restricted centre, which lifts with k₀ adjoined (stratumIn_comap_of_stratumIn, terminalIn_comap_of_terminalIn, terminalIn_comap_of_eq_span, stratumIn_comap_of_stratumIn_castLE) to the stalk of the pushed-forward centre (stalkIdeal_map_of_isClosedImmersion). The chain coordinates are those of [Kol07, Definition 24]. This argument is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Raw.

theorem Hironaka.Resolution.exists_min_level {r : ℕ} (v : Fin (r + 1) → ℕ) (h : ¬∀ (i : Fin (r + 1)), ↑i < r → v i = 0) : ∃ (l₀ : ℕ) (hl : l₀ < r), v ⟨l₀, ⋯⟩ ≠ 0 ∧ ∀ (i : Fin (r + 1)), ↑i < l₀ → v i = 0

The first level at which the exponent of a given coordinate is positive.

theorem Hironaka.Resolution.chainCoordsFree_castLE {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {p : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk p)} {c : { j : E.ι // p ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (h : ChainCoordsFree E p z c σ a) {l : ℕ} (hl : l + 1 ≤ r + 1) : ChainCoordsFree E p z c (fun (i : Fin (l + 1)) => σ (Fin.castLE hl i)) fun (i : Fin (l + 1)) => a (Fin.castLE hl i)

Chain coordinates truncated to the first l + 1 levels are chain coordinates.

theorem Hironaka.Resolution.centerClassifiedAt_of_comap_member {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (E : X.DivisorFamily) (F : Y.DivisorFamily) (e : F.ι → E.ι) (he : Function.Injective e) (hcomp : ∀ (a : F.ι), F.component a = (E.component (e a)).comap g) (j₀ : E.ι) (hker : AlgebraicGeometry.Scheme.Hom.ker g = E.component j₀) (hF : F.IsSnc) (hmiss : ∀ b ∉ Set.range e, b = j₀) {K : X.IdealSheafData} {Z' : Y.IdealSheafData} {q' : ↥Y} [IsRegularLocalRing ↑(X.presheaf.stalk (g q'))] [IsRegularLocalRing ↑(Y.presheaf.stalk q')] (hK0 : (K.comap g).stalkIdeal q' ≠ ⊥) (h : CenterClassifiedAt F (K.comap g) Z' q') : CenterClassifiedAt E K (Z'.map g) (g q')

The pointwise pass over a member ([Kol07, Lemma 102] and [Kol07, Lemma 62]): for a closed immersion g : Y ⟶ X whose kernel is the member Eʲ⁰ of E, and a family F on Y whose members are the restrictions of the other members of E, the classification of a centre Z' on Y at q' for the restricted ideal gives the classification of its push-forward at g q' for the ideal on X: the outer chain coordinates restrict to Y (killing the coordinate of Eʲ⁰), the outer shape restricts to the inner shape, and the inner stratum lifts with the killed coordinate adjoined.