CP3 at the stalk of a member, and the snc clause

Three stalk-level facts that the proof of the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) consumes in given chain coordinates, in Steps 2.1 and 2.2 of the proof of [Kol07, Theorem 103]:

• stalkIdeal_map_of_isClosedImmersion — the stalk of a pushed-forward ideal sheaf along a closed immersion g at g y is the preimage of the stalk at y under the stalk map (the kernel of the composite closed immersion, ker_stalkMap_of_isClosedImmersion; at a point off the support both sides are the unit ideal). It reads a centre's push-forward from a member back to the ambient scheme (the form of the centres in [Kol07, Lemma 62] and the proof of [Kol07, Lemma 102]).
• exists_chainCoordsFree_comap_member — the restriction of chain coordinates to a member: at a point of the member Eʲ, the images of the chain coordinates other than e_j = z_{c j} under the stalk map of the member are chain coordinates on Eʲ for the restricted family (E − Eʲ)|_{Eʲ} (the restriction of a simple normal crossing divisor of [Kol07, Definition 24]), the index maps re-indexed through succAbove. The restricted coordinates are a regular system of parameters of the stalk of the member (isRegularSystemOfParameters_comp_succAbove); the equations of the members restrict (stalkIdeal_comap_subschemeι_eq_span); the chain parameters and the supports of the exponents avoid the deleted coordinate.
• notMem_span_sup_sq_of_isSncAt_append — the snc clause of the re-basing of the flag (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Rebase): if E + H has simple normal crossings at q in coordinates w (as at the end of Step 2.1, [Kol07, 104, Step 2.1]) and z are chain coordinates for E at q, a local equation x of H lies outside (z_{c j} : j) + 𝔪². Indeed x is a unit multiple of the w-coordinate of H, each z_{c j} a unit multiple of another w-coordinate, and a coordinate of a regular system lies outside the span of the others plus 𝔪² (notMem_span_compl_sup_sq).

These identities are not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Pass and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Chain.

theorem Hironaka.Resolution.stalkIdeal_map_of_isClosedImmersion {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (Z : Y.IdealSheafData) (y : ↥Y) : (Z.map g).stalkIdeal (g y) = Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap g y)) (Z.stalkIdeal y)

The stalk of a pushed-forward ideal sheaf along a closed immersion is the preimage of the stalk.

theorem Hironaka.Resolution.exists_chainCoordsFree_comap_member {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (j : E.ι) {y : ↥(E.component j).subscheme} [IsRegularLocalRing ↑(X.presheaf.stalk ((E.component j).subschemeι y))] {n : ℕ} {z : Fin (n + 1) → ↑(X.presheaf.stalk ((E.component j).subschemeι y))} {c : { j' : E.ι // (E.component j).subschemeι y ∈ (E.component j').support } → Fin (n + 1)} {r : ℕ} {σ : Fin (r + 1) → Fin (n + 1)} {a : Fin (r + 1) → Fin (n + 1) → ℕ} (h : ChainCoordsFree E ((E.component j).subschemeι y) z c σ a) (hj : (E.component j).subschemeι y ∈ (E.component j).support) : ∃ (c' : { j' : ((E.erase j).comap (E.component j).subschemeι).ι // y ∈ (((E.erase j).comap (E.component j).subschemeι).component j').support } → Fin n) (σ' : Fin (r + 1) → Fin n), (∀ (j' : { j' : ((E.erase j).comap (E.component j).subschemeι).ι // y ∈ (((E.erase j).comap (E.component j).subschemeι).component j').support }), ∃ (hmem : (E.component j).subschemeι y ∈ (E.component ↑↑j').support), (c ⟨j, hj⟩).succAbove (c' j') = c ⟨↑↑j', hmem⟩) ∧ (∀ (i : Fin (r + 1)), (c ⟨j, hj⟩).succAbove (σ' i) = σ i) ∧ ChainCoordsFree ((E.erase j).comap (E.component j).subschemeι) y (fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (E.component j).subschemeι y)) (z ((c ⟨j, hj⟩).succAbove i))) c' σ' fun (i : Fin (r + 1)) => a i ∘ (c ⟨j, hj⟩).succAbove

The restriction of chain coordinates to a member ([Kol07, Definition 24]: the restriction of a simple normal crossing divisor to a member not containing the subvariety): at p ∈ Eʲ, the images of the coordinates other than e_j under the stalk map of the member are chain coordinates on Eʲ for the family (E − Eʲ)|_{Eʲ}, with the index maps determined by succAbove.

theorem Hironaka.Resolution.notMem_span_sup_sq_of_isSncAt_append {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {H : X.IdealSheafData} {q : ↥X} [IsRegularLocalRing ↑(X.presheaf.stalk q)] (hq : q ∈ H.support) {m : ℕ} {w : Fin m → ↑(X.presheaf.stalk q)} (hsnc : (E.append H).IsSncAt q w) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk q)} {c : { j : E.ι // q ∈ (E.component j).support } → Fin n} {r : ℕ} {σ : Fin (r + 1) → Fin n} {a : Fin (r + 1) → Fin n → ℕ} (hc : ChainCoordsFree E q z c σ a) {x : ↑(X.presheaf.stalk q)} (hx : H.stalkIdeal q = Ideal.span {x}) : x ∉ Ideal.span (z '' Set.range c) ⊔ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk q) ^ 2

The snc clause of the re-basing of the flag ([Kol07, 104, Step 2.1]: H + E has simple normal crossings after Step 2.1): if E.append H has snc at q and z are chain coordinates for E at q, then a local equation of H at q lies outside (z_{c j} : j) + 𝔪².