Elementary tools for the descent step of CP1

The descent of the chain form along the pushforward of a run on a smooth hypersurface H ↪ X (the induction step of the statement CP1 of the embedded desingularization, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainPushforward) rests on four elementary facts, each about closed immersions or supports and none about the chain form itself:

• along a closed immersion g, the reduced ideal of the closure of an image point pulls back to the reduced ideal of the closure of the point (comap_vanishingIdeal_closure_of_isClosedImmersion), and the member data of cp1For_concat (a generic point of V(J) off the boundary at which J is the component's ideal) descend to the restriction J|_Y when V(J) ⊆ g(Y) (exists_level_data_comap);
• the strict transform along the pushforward of a run pulls back, along the stage embedding, to the strict transform of the restriction (strictTransformSeq_pushforward_comap), and a centre of the pushforward contains the strict transform of c ⊇ H iff the corresponding centre contains that of c|_H (centerContains_pushforward_iff_of_ker_le) — the transport of Hironaka.Resolution.Algebraic.Kol07.Thm36.IndexTransport (strictTransformSeq_pushforward, centerContains_pushforward_iff) with c = (c|_H) extended by zero (map_comap_of_ker_le);
• the chain form ignores members missing the point: for a sub-family selecting every member through p the two chain forms agree (chainRelativeAt_subfamily_iff); and a divisor disjoint from V(J) keeps its strict transforms disjoint from the supports of the marked transforms of (J, 1) along any blow-up sequence, both lying over the originals (disjoint_support_markedTransformSeq_strictTransformSeq).

The pushforward of a blow-up sequence along a closed immersion is that of [Kol07, Definition 30] (30.2–30.3); the marked transform is that of [Kol07, Definition 60].

S2c (ii): supports lie over the originals

theorem Hironaka.Resolution.disjoint_support_markedTransformSeq_strictTransformSeq_mk {X : AlgebraicGeometry.Scheme} (hN : AlgebraicGeometry.IsLocallyNoetherian X) (S : X.BlowUpSequence) (J D : X.IdealSheafData) (hD : Disjoint ↑J.support ↑D.support) (j : ℕ) (hj : j < S.length + 1) : Disjoint ↑(S.markedTransformSeq J 1 ⟨j, hj⟩).support ↑(S.strictTransformSeq D ⟨j, hj⟩).support

S2c (ii) in the ⟨j, hj⟩ form of the indices: along any blow-up sequence the support of the marked transform of (J, 1) lies over V(J) (the marked transform contains the pull-back) and the support of the strict transform of D lies over V(D) (coe_support_strictTransform), so disjointness of V(J) and V(D) propagates to every stage.

theorem Hironaka.Resolution.disjoint_support_markedTransformSeq_strictTransformSeq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J D : X.IdealSheafData) (hD : Disjoint ↑J.support ↑D.support) (i : Fin (S.length + 1)) : Disjoint ↑(S.markedTransformSeq J 1 i).support ↑(S.strictTransformSeq D i).support

A divisor disjoint from V(J) stays disjoint from the support of the marked transform of (J, 1) along any blow-up sequence, at every stage.

S2b: the pushforward's strict transforms and centres

theorem Hironaka.Resolution.strictTransformSeq_pushforward_comap {X Y : AlgebraicGeometry.Scheme} (L : Y.BlowUpSequence) (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] {c : X.IdealSheafData} (hc : AlgebraicGeometry.Scheme.Hom.ker g ≤ c) (i : Fin (L.length + 1)) : ((L.pushforward g).strictTransformSeq c (L.pushforwardStageIdx g i)).comap (L.pushforwardStageHom g i) = L.strictTransformSeq (c.comap g) i

For c ⊇ ker g, the strict transform of c along the pushforward pulls back along the stage embedding to the strict transform of c|_Y (strictTransformSeq_pushforward).

theorem Hironaka.Resolution.centerContains_pushforward_iff_of_ker_le {X Y : AlgebraicGeometry.Scheme} (L : Y.BlowUpSequence) (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] {c : X.IdealSheafData} (hc : AlgebraicGeometry.Scheme.Hom.ker g ≤ c) (l : ℕ) : CenterContains (L.pushforward g) c l ↔ CenterContains L (c.comap g) l

For c ⊇ ker g, a centre of the pushforward contains the strict transform of c iff the corresponding centre of L contains the strict transform of c|_Y (centerContains_pushforward_iff).

S2a: the member data descend along a closed immersion

theorem Hironaka.Resolution.comap_vanishingIdeal_closure_of_isClosedImmersion {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (η' : ↥Y) : (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {g η'})).comap g = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})

Along a closed immersion g the reduced ideal of the closure of g η' pulls back to the reduced ideal of the closure of η' — the pullback is reduced (its subscheme is isomorphic to V(closure {g η'}), which lies in the image, exists_iso_subscheme_comap_of_ker_le) with support the preimage of the closure, which is the closure of η' for a closed embedding.

theorem Hironaka.Resolution.exists_level_data_comap {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] {J : X.IdealSheafData} (hJ : AlgebraicGeometry.Scheme.Hom.ker g ≤ J) (E : X.DivisorFamily) {η : ↥X} (hη : η ∈ J.support.genericPoints) (hηE : ∀ (j : E.ι), η ∉ (E.component j).support) (hIc : J.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) : ∃ (η' : ↥Y), g η' = η ∧ η' ∈ (J.comap g).support.genericPoints ∧ (∀ (j : (E.comap g).ι), η' ∉ ((E.comap g).component j).support) ∧ (J.comap g).stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η'

The member data of cp1For_concat — a generic point η of V(J) off every member of E at which J is the ideal of the component — descend along a closed immersion g with ker g ⊆ J: η = g η' for a generic point η' of V(J|_Y) off every member of E|_Y, at which J|_Y is the ideal of the component.

S2c (i): the chain form ignores members missing the point

theorem Hironaka.Resolution.chainRelativeAt_subfamily_iff {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} (q : E.ι → Prop) {I Γ : X.IdealSheafData} {p : ↥X} (hq : ∀ (j : E.ι), p ∈ (E.component j).support → q j) : ChainRelativeAt (E.subfamily q) I Γ p ↔ ChainRelativeAt E I Γ p

For a sub-family of E selecting every member through p, the chain form along Γ at p for the sub-family and for E agree — the members through p correspond (the coordinates c are re-indexed along the correspondence; stalks are unchanged).