Points of the blow-up of a centre with simple normal crossings

The point-level facts behind the nerve transition of Hironaka/Resolution/Algebraic/Monomial/Geometric/Kernel.lean, on a smooth k-scheme X with a centre Z carrying Kollár's snc data hZ for a finite family D of ideal sheaves (the hypothesis of Hironaka/Scheme/Snc/TotalTransformSnc.lean):

• exists_stalkIdeal_comap_eq_span_of_mem_support: at a point x' of the exceptional divisor over x, with Z_x = (z_c : c ∈ s), some z_c (c ∈ s) generates the exceptional ideal F_{x'} = π^*(Z_x). By the total-transform data of Hironaka/Scheme/Snc/TotalTransformData.lean, F_{x'} = (z'_j) and each π^* z_c generates an ideal of shape (z'_a z'_j), (z'_a), (z'_j) or (1); the shapes (z'_a), (1) are excluded since (π^* z_c) ⊆ F_{x'}, and if every c ∈ s had the shape (z'_a z'_j) then F_{x'} ⊆ 𝔪_{x'} F_{x'}, impossible by Nakayama for the regular parameter z'_j. This is the statement that x' lies in the chart of some z_c, as in the proof of [Hau14, Proposition 5.3].
• exists_chartOrigin_point, exists_chartOrigin_point_of_mem: the origin of the chart of a centre coordinate y_ρ, in the coordinates (60.2) of [Kol07, Definition 60], as a point of the blow-up over x at which π^* y_ρ generates the exceptional ideal and every other centre coordinate π^* y_i = (y_i / y_ρ) · y_ρ lies in 𝔪_{x'}².

Not in the sources as statements; they are the coordinate computations that Kollár's and Hauser's descriptions of the blow-up in charts take for granted.

Nakayama for the exceptional ideal

theorem Hironaka.Monomial.exists_stalkIdeal_comap_eq_span_of_mem_support {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {ι : Type u_1} [Finite ι] (D : ι → X.IdealSheafData) (Z : X.IdealSheafData) (hZ : ∀ x ∈ Z.support, ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x)) ∧ (∃ (c : { i : ι // x ∈ (D i).support } → Fin n), Function.Injective c ∧ ∀ (i : { i : ι // x ∈ (D i).support }), (D ↑i).stalkIdeal x = Ideal.span {z (c i)}) ∧ ∃ (s : Finset (Fin n)), Z.stalkIdeal x = Ideal.span (z '' ↑s)) (x' : ↥Z.blowUp) (hx' : x' ∈ (Z.comap Z.blowUpπ).support) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ x'))} {s : Finset (Fin n)} (hs : Z.stalkIdeal (Z.blowUpπ x') = Ideal.span (z '' ↑s)) (hD : ∀ c ∈ s, ∃ (i : ι), (D i).stalkIdeal (Z.blowUpπ x') = Ideal.span {z c}) : ∃ c ∈ s, (Z.comap Z.blowUpπ).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ x')) (z c)}

At a point x' of the exceptional divisor over x, with Z_x = (z_c : c ∈ s) and every z_c (c ∈ s) the coordinate of a member D_i of the family, some π^* z_c generates the exceptional ideal F_{x'}: x' lies in the chart of z_c (the proof of [Hau14, Proposition 5.3]).

The origin of a chart as a point of the blow-up

theorem Hironaka.Monomial.stalkIdeal_eq_span_image_eqRec {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {p q : ↥X} (h : q = p) {n : ℕ} (z : Fin n → ↑(X.presheaf.stalk p)) (s : Set (Fin n)) (hI : I.stalkIdeal p = Ideal.span (z '' s)) : I.stalkIdeal q = Ideal.span ((fun (i : Fin n) => ⋯ ▸ z i) '' s)

Transport of a stalk ideal's description along an equality of points.

theorem Hironaka.Monomial.germ_eqRec {X : AlgebraicGeometry.Scheme} {V : X.Opens} {p q : ↥X} (h : q = p) (hp : p ∈ V) (s : ↑(X.presheaf.obj (Opposite.op V))) : ⋯ ▸ (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V p hp)) s = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V q ⋯)) s

Transport of a germ along an equality of points.

theorem Hironaka.Monomial.exists_chartOrigin_point {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (Z : X.IdealSheafData) (x : ↥X) {n r : ℕ} (y : Fin n → ↑(X.presheaf.stalk x)) (hn : ↑n = ringKrullDim ↑(X.presheaf.stalk x)) (hy : IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) = Ideal.span (Set.range y)) (hZ : Z.stalkIdeal x = Ideal.span (y '' {i : Fin n | ↑i < r})) (ρ : Fin n) (hρ : ↑ρ + 1 = r) : ∃ (x' : ↥Z.blowUp) (hx' : Z.blowUpπ x' = x), (Z.comap Z.blowUpπ).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ x')) (⋯ ▸ y ρ)} ∧ ∀ (i : Fin n), ↑i < r → i ≠ ρ → (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ x')) (⋯ ▸ y i) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk x') ^ 2

The chart of [Kol07, Definition 60], formula (60.2): with a regular system of parameters y at x whose first r members generate Z_x, the origin of the chart of y_ρ (ρ = r - 1) is a point x' of the blow-up over x at which π^* y_ρ generates the exceptional ideal and every other π^* y_i (i < r) lies in 𝔪_{x'}², since π^* y_i = (y_i / y_ρ) · y_ρ with both factors in the maximal ideal of the chart ring's localisation at the origin.

theorem Hironaka.Monomial.exists_chartOrigin_point_of_mem {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (Z : X.IdealSheafData) (x : ↥X) {n : ℕ} (z : Fin n → ↑(X.presheaf.stalk x)) (hn : ↑n = ringKrullDim ↑(X.presheaf.stalk x)) (hz : IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) = Ideal.span (Set.range z)) {s : Finset (Fin n)} (hs : Z.stalkIdeal x = Ideal.span (z '' ↑s)) {kk : Fin n} (hk : kk ∈ s) : ∃ (x' : ↥Z.blowUp) (hx' : Z.blowUpπ x' = x), (Z.comap Z.blowUpπ).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ x')) (⋯ ▸ z kk)} ∧ ∀ c ∈ s, c ≠ kk → (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ x')) (⋯ ▸ z c) ∈ IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk x') ^ 2

The chart-origin point for an unordered set of centre coordinates: with snc coordinates z at x, Z_x = (z_c : c ∈ s) and k ∈ s, there is a point x' over x at which π^* z_k generates the exceptional ideal and π^* z_c ∈ 𝔪_{x'}² for every other c ∈ s (the origin of the chart of z_k, after reordering the coordinates).