CP1 descends along a pushed-forward run on a hypersurface of maximal contact

Step 2.2 of the proof of [Kol07, Theorem 103] runs the inductive order reduction on a smooth hypersurface of maximal contact H and pushes the run forward to X (Kol07, Definition 30, 30.3; the proof of [Kol07, Lemma 102]). This module proves the corresponding step of the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative; the predicate CP1For of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1For): CP1 for a run L on H, for the restricted data (J|_H, E|_H) at a point η' over η, gives CP1 for the push-forward of L, for (J, E) at η. Three facts combine. The first stage whose centre contains the strict transform of the component c̄ = V(closure {η}) ⊆ H is the same on both sides, because the member restricts to c̄|_H = I(closure {η'}) and the stop rule is preserved by the push-forward (centerContains_pushforward_iff_of_ker_le). Every point of the strict transform at that stage is the image of a point of the level's strict transform, since the stage embedding is a closed immersion with kernel the strict transform of H ⊇ c̄. The chain form of the level data at that point gives the chain form of the data on X at its image (chainRelativeAt_pushforward of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainPushforward). The hypersurfaces of maximal contact are those of [Kol07, Theorem 80]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22Core.

theorem Hironaka.Resolution.cp1For_pushforward {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) {E : X.DivisorFamily} (hE : E.IsSnc) (hEH : (E.append H).IsSnc) {J : X.IdealSheafData} (hHJ : H ≤ J) {η : ↥X} (hηH : η ∈ H.support) (L : H.subscheme.BlowUpSequence) (hS : (L.pushforward H.subschemeι).IsOrderGeSeq f J 1 E) {η' : ↥H.subscheme} (hη' : H.subschemeι η' = η) (h : CP1For L (J.comap H.subschemeι) (E.comap H.subschemeι) η') : CP1For (L.pushforward H.subschemeι) J E η

CP1 descends along a push-forward. For a smooth hypersurface H ⊆ X with H ⊆ V(J), H ∪ E snc, η ∈ H, and a run L on H whose push-forward is a smooth run of order ≥ 1 for (J, 1, E): CP1 for L with the restricted data (J|_H, E|_H) at the point η' over η gives CP1 for the push-forward with (J, E) at η. The first containing stages correspond, the points of the strict transform at that stage are images of points of the level's strict transform, and the chain form is transported pointwise.