The pointwise pass along a hypersurface of maximal contact

Step 2.2 of the proof of [Kol07, Theorem 103] applies [Kol07, Lemma 102] to the triple (X_r, I_r, H_r + F_r) with the hypersurface of maximal contact H_r as first member. For the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) the centres of that run must be classified for the outer data (I_r, F_r), the boundary without H_r. Its first blow-up Z₋₁ is the union of the components of H_r inside V(I_r); at a point q of it the stalk of I_r lies in that of H_r (H_r ≤ I_r is the maximal contact at the mark 1, and H_r ⊆ V(I_r) along Z₋₁), so a K-shape of I_r is impossible — its top generator is a unit times a monomial in chain coordinates, outside (h) — and an I-shape has Z_q = (f₀) = (h), the absorption, the chain of length one (centerClassifiedAt_of_stalkIdeal_le_of_isSncAt_append). At a later centre — the push-forward of a centre of the inductive run on H_r — the pass is the variant for a chain hypersurface of the pass over a member (centerClassifiedAt_of_comap_member, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Pass): in outer chain coordinates the equation h of H_r lies in I_r and outside (z_C) + 𝔪² (so the top exponent b is 0); the flag is re-based to make h a chain coordinate (exists_update_chainKIdeal_eq, exists_update_chainIdeal_eq, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Rebase); the coordinates and the shape descend to H_r along the stalk map (exists_restricted_chain_coords, map_chainKIdeal_succAbove_of_trivial, map_chainIdeal_succAbove_of_trivial); the inner classification is read there; the stratum lifts (stratumIn_comap_of_stratumIn_succAbove, terminalIn_comap_of_terminalIn_succAbove, the absorption through comap_span_range_succAbove_eq) and transfers back to the original flag (stratumIn_of_stratumIn_update_chainKIdeal, stratumIn_of_stratumIn_update_chainIdeal, terminalIn_of_terminalIn_update, span_range_update_eq_of_mem_chainIdeal). This is centerClassifiedAt_of_comap_chain. The bookkeeping: IsSncAt transports along an injection of families with equal members (isSncAt_of_injective), and the embedding of the total transforms of a sub-family has its complement characterised both ways (exists_embeds_totalTransformSeq'). The chain coordinates are those of [Kol07, Definition 24]. This argument is not in the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step22.

theorem Hironaka.Resolution.isSncAt_of_injective {X : AlgebraicGeometry.Scheme} {E F : X.DivisorFamily} (e : F.ι → E.ι) (he : Function.Injective e) (hcomp : ∀ (a : F.ι), E.component (e a) = F.component a) {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} (h : E.IsSncAt x z) : F.IsSncAt x z

IsSncAt transports along an injection of families with equal members.

theorem Hironaka.Resolution.exists_embeds_totalTransformSeq' {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {E₁ E₂ : X.DivisorFamily} (e₀ : E₁.ι → E₂.ι) : Function.Injective e₀ → (∀ (a : E₁.ι), E₂.component (e₀ a) = E₁.component a) → ∀ (i : Fin (S.length + 1)), ∃ (e : (S.totalTransformSeq E₁ i).ι → (S.totalTransformSeq E₂ i).ι), Function.Injective e ∧ (∀ (b : (S.totalTransformSeq E₁ i).ι), (S.totalTransformSeq E₂ i).component (e b) = (S.totalTransformSeq E₁ i).component b) ∧ (∀ b ∉ Set.range e, ∃ a ∉ Set.range e₀, b = S.originalIdx E₂ i a) ∧ ∀ a ∉ Set.range e₀, S.originalIdx E₂ i a ∉ Set.range e

exists_embeds_totalTransformSeq with the complement characterised both ways: the members of the total transform of E₂ outside the range are exactly the transforms of the members of E₂ outside the range of e₀.

theorem Hironaka.Resolution.notMem_span_singleton_of_notMem_sup_sq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {C : Set (Fin n)} {x : R} (hx2 : x ∉ Ideal.span (z '' C) ⊔ IsLocalRing.maximalIdeal R ^ 2) (hxm : x ∈ IsLocalRing.maximalIdeal R) {k : Fin n} (hk : k ∈ C) : z k ∉ Ideal.span {x}

A coordinate of a regular system lies outside the prime of an element off (z_C) + 𝔪².

theorem Hironaka.Resolution.span_singleton_eq_of_mem_of_notMem_sq {R : Type u_1} [CommRing R] [IsLocalRing R] {x f : R} (hxm : x ∈ IsLocalRing.maximalIdeal R) (hf : f ∈ Ideal.span {x}) (hf2 : f ∉ IsLocalRing.maximalIdeal R ^ 2) : Ideal.span {f} = Ideal.span {x}

An element of (x) outside 𝔪² generates (x) (for x ∈ 𝔪).

theorem Hironaka.Resolution.monomialOf_notMem_of_forall_notMem {R : Type u_1} [CommRing R] {n : ℕ} {z : Fin n → R} {P : Ideal R} (hP : P.IsPrime) {C : Set (Fin n)} {b : Fin n → ℕ} (hb : ∀ (κ : Fin n), b κ ≠ 0 → κ ∈ C) (hC : ∀ k ∈ C, z k ∉ P) : monomialOf z b ∉ P

A monomial in coordinates outside a prime lies outside the prime.

theorem Hironaka.Resolution.comap_span_range_succAbove_eq {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {n : ℕ} {z : Fin (n + 1) → R} {k₀ : Fin (n + 1)} {φ : R →+* S} (hφ : Function.Surjective ⇑φ) (hker : RingHom.ker φ = Ideal.span {z k₀}) {r : ℕ} {σ : Fin (r + 2) → Fin (n + 1)} {t : Fin (r + 2)} (hk₀ : σ t = k₀) {σ' : Fin (r + 1) → Fin n} (hσ : ∀ (i : Fin (r + 1)), k₀.succAbove (σ' i) = σ (t.succAbove i)) : Ideal.comap φ (Ideal.span (Set.range ((fun (i : Fin n) => φ (z (k₀.succAbove i))) ∘ σ'))) = Ideal.span (Set.range (z ∘ σ))

The absorption lifts along the descent to a chain hypersurface: the preimage of the span of the shortened chain is the span of the full chain.

theorem Hironaka.Resolution.centerClassifiedAt_of_stalkIdeal_le_of_isSncAt_append {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {H K Z : 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) (hZ : Z.stalkIdeal q = H.stalkIdeal q) (hKH : K.stalkIdeal q ≤ H.stalkIdeal q) : CenterClassifiedAt E K Z q

The classification of Z₋₁ in Step 2.2. At a point q of the hypersurface H of maximal contact where the current ideal lies in the ideal of H, no K-shape exists, and an I-shape has the absorption Z_q = (f₀), the chain of length one; here Z has the stalk of H.

theorem Hironaka.Resolution.exists_restricted_chain_coords {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) (hsurj : Function.Surjective e) {q' : ↥Y} [IsRegularLocalRing ↑(X.presheaf.stalk (g q'))] {n : ℕ} {z : Fin (n + 1) → ↑(X.presheaf.stalk (g q'))} {c : { j : E.ι // g q' ∈ (E.component j).support } → Fin (n + 1)} (hcinj : Function.Injective c) (hcmem : ∀ (j : { j : E.ι // g q' ∈ (E.component j).support }), (E.component ↑j).stalkIdeal (g q') = Ideal.span {z (c j)}) {r : ℕ} {σ : Fin (r + 1) → Fin (n + 1)} (hσinj : Function.Injective σ) (hσc : ∀ (i : Fin (r + 1)) (j : { j : E.ι // g q' ∈ (E.component j).support }), σ i ≠ c j) (t : Fin (r + 1)) {x : ↑(X.presheaf.stalk (g q'))} (hupd : IsLocalRing.IsRegularSystemOfParameters (Function.update z (σ t) x)) (hker : RingHom.ker (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap g q')) = Ideal.span {x}) : ∃ (c' : { a : F.ι // q' ∈ (F.component a).support } → Fin n) (σ' : Fin r → Fin n), (∀ (i : Fin r), (σ t).succAbove (σ' i) = σ (t.succAbove i)) ∧ (∀ κ ∈ Set.range c', (σ t).succAbove κ ∈ Set.range c) ∧ (∀ (κ : Fin n), (σ t).succAbove κ ∈ Set.range c → κ ∈ Set.range c') ∧ (IsLocalRing.IsRegularSystemOfParameters fun (i : Fin n) => (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap g q')) (Function.update z (σ t) x ((σ t).succAbove i))) ∧ Function.Injective c' ∧ (∀ (a : { a : F.ι // q' ∈ (F.component a).support }), (F.component ↑a).stalkIdeal q' = Ideal.span {(CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap g q')) (Function.update z (σ t) x ((σ t).succAbove (c' a)))}) ∧ Function.Injective σ' ∧ ∀ (i : Fin r) (a : { a : F.ι // q' ∈ (F.component a).support }), σ' i ≠ c' a

The restricted chain coordinates along a chain hypersurface: after the re-basing x = z₁ (σ t), the coordinates of the members and the chain shortened at t restrict along the stalk map.

theorem Hironaka.Resolution.centerClassifiedAt_of_comap_chain {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) (hsurj : Function.Surjective e) {H : X.IdealSheafData} (hker : AlgebraicGeometry.Scheme.Hom.ker g = H) {K : X.IdealSheafData} {Z' : Y.IdealSheafData} {q' : ↥Y} [IsRegularLocalRing ↑(X.presheaf.stalk (g q'))] {m : ℕ} {w : Fin m → ↑(X.presheaf.stalk (g q'))} (hsnc : (E.append H).IsSncAt (g q') w) (hHK : H.stalkIdeal (g q') ≤ K.stalkIdeal (g q')) (hKq : K.stalkIdeal (g 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 along the hypersurface of maximal contact (the variant of centerClassifiedAt_of_comap_member for a chain hypersurface). For a closed immersion g with kernel H, H snc with the family E at g q', and the equation of H in the current ideal K (maximal contact at the mark 1), the classification of a centre Z' on Y at q' for the restricted ideal and the family F = E|_Y (every member restricts) gives the classification of its push-forward at g q': in every chain-coordinate system the top monomial is 1, the flag is re-based so that the equation of H is a chain coordinate, the coordinates and the shape restrict along the descent, and the inner stratum lifts and transfers back.