The descent of the chain form along a pushforward

The induction step of the statement CP1 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) on the scheme: Włodarczyk's proof descends to the hypersurface of maximal contact and runs the algorithm there; in Kollár's order the run on H is pushed forward to X ([Kol07, Definition 30, 30.3]; the proof of [Kol07, Lemma 102]). The chain form of the level data on H at a point of stage i of the run L on H gives the chain form of the data on X at the image point of the corresponding stage of L.pushforward ι: the stage embedding g = L.pushforwardStageHom ι i is a closed immersion with kernel the strict transform H_i (ker_pushforwardStageHom), H_i is a smooth hypersurface with H_i ≤ J_i (maximal contact persists along an order-≥ 1 run, IsOrderGeSeq.strictTransformSeq_le_and_isSmoothDivisor) and H_i ≤ c̃_i; the three pullbacks along g of the data on X_i are the data of L on H_i — the boundary through the restriction identity (totalTransformSeq_comap_pullbackStageHom_of_forall_lt), the marked transform through IsOrderGeSeq.markedTransformSeq_comap_pullbackStageHom, the strict transform through strictTransformSeq_pushforward_comap (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainDescentTools), the first two carried across pullback_pushforward by the heterogeneous-equality transports of Hironaka.Resolution.Algebraic.Kol07.GoingUp — and the lift of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainLift in its closed-immersion form lifts the level form. The hypersurfaces of maximal contact are those of [Kol07, Theorem 80]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Pushforward.

theorem Hironaka.Resolution.chainRelativeAt_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 c : X.IdealSheafData} (hHJ : H ≤ J) (hHc : H ≤ c) (L : H.subscheme.BlowUpSequence) (hS : (L.pushforward H.subschemeι).IsOrderGeSeq f J 1 E) (i : Fin (L.length + 1)) {p : ↥(L.stage i)} (h : ChainRelativeAt (L.totalTransformSeq (E.comap H.subschemeι) i) (L.markedTransformSeq (J.comap H.subschemeι) 1 i) (L.strictTransformSeq (c.comap H.subschemeι) i) p) : ChainRelativeAt ((L.pushforward H.subschemeι).totalTransformSeq E (L.pushforwardStageIdx H.subschemeι i)) ((L.pushforward H.subschemeι).markedTransformSeq J 1 (L.pushforwardStageIdx H.subschemeι i)) ((L.pushforward H.subschemeι).strictTransformSeq c (L.pushforwardStageIdx H.subschemeι i)) ((L.pushforwardStageHom H.subschemeι i) p)

The descent of the chain form along a pushforward: for H ⊆ X a smooth hypersurface with H ⊆ V(J), H ∪ E snc, c ⊇ H (a component inside H), and a run L on H whose pushforward to X is a smooth run of order ≥ 1 for (J, 1, E), the chain form of the level data on H at a point of stage i gives the chain form of the data on X at the image point of the corresponding stage ([Kol07, Definition 30, 30.3]; [Kol07, Theorem 80 (2)] for the hypersurface of maximal contact).