Lifting the chain form across a smooth hypersurface

The scheme form of exists_chain_lift (Hironaka.Resolution.Algebraic.Wlo05.ChainRelativeLift), the induction step of the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): on X smooth over k, for a smooth hypersurface H (IsSmoothDivisor) with H ≤ J (the round's ideal contains H's: maximal contact persists for the nonmonomial part) and H ≤ Γ (Γ ⊆ H), the chain-relative form of J|_H along Γ|_H at a point w of H gives the chain-relative form of J along Γ at ι w on X, with top monomial 1. The stalk map of ι : H ↪ X is surjective with kernel H_p, the generator of H_p is completed to a regular system of parameters, the restricted family's stalks are the images of the members' stalks (stalkIdeal_comap), and the members through w on H are exactly the members through p on X (AlgebraicGeometry.mem_support_comap_iff_apply). The coordinates are those of [Kol07, Definition 24]; the hypersurfaces of maximal contact are those of [Kol07, Theorem 80], and the restriction of the ideal to a hypersurface through the centre is that of [Kol07, Lemma 62]. The lift is used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainPushforward.

theorem Hironaka.Resolution.monomialOf_zero {R : Type u_1} [CommRing R] {n : ℕ} (z : Fin n → R) : monomialOf z 0 = 1

The monomial with zero exponents is 1.

theorem Hironaka.Resolution.chainRelativeAt_of_closedImmersion {k : Type u} [Field k] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} (hE : E.IsSnc) {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) {J Γ : X.IdealSheafData} (hHJ : H ≤ J) (hHΓ : H ≤ Γ) (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (hg : AlgebraicGeometry.Scheme.Hom.ker g = H) (hY : ∀ (w : ↥Y), IsRegularLocalRing ↑(Y.presheaf.stalk w)) {w : ↥Y} (h : ChainRelativeAt (E.comap g) (J.comap g) (Γ.comap g) w) : ChainRelativeAt E J Γ (g w)

The closed-immersion form of the lift: the chain form lifts along ANY closed immersion g : Y ⟶ X with kernel the smooth hypersurface H (a hypersurface of maximal contact, [Kol07, Theorem 80 (2)], in the application); chainRelativeAt_of_hypersurface is the instance g := H.subschemeι, and the pushforward of a run along H ↪ X embeds its stages by closed immersions with kernel the strict transform of H (ker_pushforwardStageHom). The regularity hY of the source's stalks is derivable (g factors through Y ≅ H.subscheme) and is carried as a hypothesis for convenience: hH.1 for the hypersurface, the stage's smoothness over k for a stage of the pushforward's inner run.

theorem Hironaka.Resolution.chainRelativeAt_of_hypersurface {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} (hE : E.IsSnc) {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) {J Γ : X.IdealSheafData} (hHJ : H ≤ J) (hHΓ : H ≤ Γ) {w : ↥H.subscheme} (h : ChainRelativeAt (E.comap H.subschemeι) (J.comap H.subschemeι) (Γ.comap H.subschemeι) w) : ChainRelativeAt E J Γ (H.subschemeι w)

On X smooth over k, the chain-relative form of J|_H along Γ|_H at a point of the smooth hypersurface H lifts to the chain-relative form of J along Γ at that point of X, when H ≤ J and H ≤ Γ; the top monomial of the lift is 1 and the level's top monomial becomes the first chain factor.