Lifting chain-relative data across a hypersurface

The induction step of the statement CP1 of the embedded desingularization (the local form of the ideal at the absorbing stage, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) descends one level of the maximal-contact chain: the run one dimension down, on the hypersurface H = V(h), knows the local form of the restricted ideal J|_H along Γ̃ ⊆ H, and the ideal J on the ambient contains h (maximal contact persists for the round's ideal). At the ring level this is the step R/(h) → R: given a regular system of parameters w of R' = R/(h) realising the boundary members through the point, chain coordinates w ∘ σ' and exponent data on R' with Γ.map φ = (w ∘ σ') and J.map φ = M⁰ · chainIdeal (w ∘ σ') M, one lifts w to R (units times the members' own generators on the members' coordinates, arbitrary preimages elsewhere), prepends h, and reads Γ = (h) + (lifts) and J = (h) + M⁰ · chainIdeal (lifts) M = chainIdeal (h, lifts) (M⁰, M) (chainIdeal_succ): the top monomial of the level becomes the level-1 factor of the chain, and the new top monomial is 1. The lifted family is a regular system of parameters of R because it generates 𝔪_R modulo ker φ = (h) and has dim R' + 1 = dim R members (AlgebraicGeometry.natCast_sub_card_eq_ringKrullDim_of_ker). The coordinates are those of [Kol07, Definition 24]. The lift is used by Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainLift.

theorem Hironaka.Resolution.monomialOf_cons_zero {R : Type u} [CommRing R] {n : ℕ} (x : R) (l : Fin n → R) (b : Fin n → ℕ) : monomialOf (Fin.cons x l) (Fin.cons 0 b) = monomialOf l b

A monomial in Fin.cons x l with exponent vector Fin.cons 0 b is the monomial in l.

theorem Hironaka.Resolution.monomialOf_map {R : Type u} [CommRing R] {S : Type v} [CommRing S] (φ : R →+* S) {n : ℕ} (l : Fin n → R) (b : Fin n → ℕ) : φ (monomialOf l b) = monomialOf (⇑φ ∘ l) b

Monomials are compatible with ring homomorphisms.

theorem Hironaka.Resolution.comap_map_eq_of_ker_le {R : Type u} [CommRing R] {S : Type v} [CommRing S] (φ : R →+* S) (hφ : Function.Surjective ⇑φ) {K : Ideal R} (hK : RingHom.ker φ ≤ K) : Ideal.comap φ (Ideal.map φ K) = K

An ideal containing the kernel of a surjection is the preimage of its image.

theorem Hironaka.Resolution.exists_chain_lift {R : Type u} [CommRing R] {R' : Type u} [IsRegularLocalRing R] [CommRing R'] [IsRegularLocalRing R'] (φ : R →+* R') (hφ : Function.Surjective ⇑φ) {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.IsRegularSystemOfParameters z) {j₀ : Fin n} (hker : RingHom.ker φ = Ideal.span {z j₀}) {ι : Type v} (e : ι → R) {n' : ℕ} (w : Fin n' → R') (hw : IsLocalRing.IsRegularSystemOfParameters w) (c' : ι → Fin n') (hc' : Function.Injective c') (hce : ∀ (j : ι), Ideal.span {w (c' j)} = Ideal.span {φ (e j)}) {r : ℕ} (σ' : Fin (r + 1) → Fin n') (hσ' : Function.Injective σ') (hσc : ∀ (i : Fin (r + 1)) (j : ι), σ' i ≠ c' j) (a' : Fin (r + 1) → Fin n' → ℕ) (ha' : ∀ (i : Fin (r + 1)) (k : Fin n'), a' i k ≠ 0 → k ∈ Set.range c') (b' : Fin n' → ℕ) (hb' : ∀ (k : Fin n'), b' k ≠ 0 → k ∈ Set.range c') (J Γ : Ideal R) (hJh : z j₀ ∈ J) (hΓh : z j₀ ∈ Γ) (hΓ : Ideal.map φ Γ = Ideal.span (Set.range (w ∘ σ'))) (hJ : Ideal.map φ J = Ideal.span {monomialOf w b'} * chainIdeal (w ∘ σ') fun (i : Fin (r + 1)) => monomialOf w (a' i)) : ∃ (zz : Fin (n' + 1) → R) (c : ι → Fin (n' + 1)) (σ : Fin (r + 2) → Fin (n' + 1)) (a : Fin (r + 2) → Fin (n' + 1) → ℕ), IsLocalRing.IsRegularSystemOfParameters zz ∧ Function.Injective c ∧ (∀ (j : ι), Ideal.span {e j} = Ideal.span {zz (c j)}) ∧ Function.Injective σ ∧ (∀ (i : Fin (r + 2)) (j : ι), σ i ≠ c j) ∧ (∀ (i : Fin (r + 2)) (k : Fin (n' + 1)), a i k ≠ 0 → k ∈ Set.range c) ∧ Γ = Ideal.span (Set.range (zz ∘ σ)) ∧ J = chainIdeal (zz ∘ σ) fun (i : Fin (r + 2)) => monomialOf zz (a i)

The ring core of the induction step of CP1: chain-relative data on R' = R/(h) lift to R with the chain (h, lifts), the level's top monomial becoming the first chain factor and the new top monomial 1.