The controlled transform inside the saturation chain, and the exceptional set

Tools for identifying the final support of Włodarczyk's modified marked resolution with the strict transform of Y (the proof of [Wlo09, Theorem 7.4.1]), stated for any finite blow-up sequence of order ≥ 1 [Kol07, Definition 66]. The ideal-theoretic strict transform of a closed subspace along a blowing-up is described by its saturation, the colon of the total transform by the powers of the exceptional ideal [BM97, Proposition 3.13]; where a lemma needs the saturation to be finitely generated (proved for every RCLike field in BlowUp/Transform/SaturationFiniteType.lean), it takes that as an explicit hypothesis.

• The saturation is monotone in the ideal (saturationStalk_mono); the controlled transform of (I, m) lies in the saturation of I when I has order ≥ m along the centre (the colon description isDivExceptional_birationalTransform); and the saturation lies in the stalk of the strict transform in both branches of its definition.
• Hence, along a sequence of order ≥ 1, the marked chain at mark 1 lies in the saturation chain stage by stage (markedTransformSeq_le_strictTransformSubspaceSeq), and the cosupport of the final strict transform lies in the final support (cosupport_strictTransformSubspaceSeq_subset), unconditionally.
• The support of the family of exceptional divisors at stage i + 1 is the preimage of the support at stage i together with the exceptional divisor of the i-th blow-up (support_totalTransformSeq_succ, the recursion of [Hir64, Main Theorem II′(N), p. 156] read on supports), so a point off the final exceptional set lies over no centre at any stage; off the exceptional set the two chains agree (stalkIdeal_markedTransformSeq_eq_strictTransformSubspaceSeq_of_notMem_support).
• The density step: at a point of the support of J where J is locally the ideal of a coordinate subspace transversal to the members of a simple normal crossing family, the support off the family is dense (mem_closure_cosupport_diff_support_of_isSmoothTransversalIdealAt).
• The identity itself (cosupport_markedTransformSeq_eq_cosupport_strictTransformSubspaceSeq): for a sequence of order ≥ 1 whose exceptional families are simple normal crossing families, whose saturations are finitely generated and whose final controlled transform is at every support point locally the ideal of a coordinate subspace transversal to the exceptional divisors, the final support is the cosupport of the final strict transform.

These lemmas are applied to the embedded desingularization functor in Hironaka/Resolution/Analytic/Wlo09/StrictTransformClauses.lean.

theorem Hironaka.Manifold.saturationStalk_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) {I J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} (hIJ : I ≤ J) (a' : M') : Manifold.saturationStalk hY h I a' ≤ Manifold.saturationStalk hY h J a'

The saturation is monotone in the ideal sheaf.

theorem Hironaka.Manifold.birationalTransform_stalkIdeal_le_saturationStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {m : ℕ} (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal I a) (a' : M') : (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := I, m := m }).I.stalkIdeal a' ≤ Manifold.saturationStalk hY h I a'

The controlled transform of (I, m) lies in the saturation of I when I has order ≥ m along the centre: its stalk is the colon by the m-th power of the exceptional ideal (isDivExceptional_birationalTransform), one term of the saturation's supremum.

theorem Hironaka.Manifold.saturationStalk_le_stalkIdeal_strictTransformSubspace {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (a' : M') : Manifold.saturationStalk hY h I a' ≤ (Manifold.strictTransformSubspace hY h I).stalkIdeal a'

The saturation lies in the stalk of the strict transform strictTransformSubspace, in both branches of its definition (the stalks agree when the saturation has local generators; otherwise the strict transform is the unit ideal sheaf).

theorem Hironaka.Manifold.markedTransformSeq_le_strictTransformSubspaceSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J E₀ : M.IdealSheaf) (hge : S.IsOfOrderGe J 1 E₀) (i : Fin (S.length + 1)) : S.markedTransformSeq J 1 i ≤ S.strictTransformSubspaceSeq J i

Along a sequence of order ≥ 1 for (J, 1, E₀) [Kol07, Definition 66], the marked chain at mark 1 lies in the saturation chain (strictTransformSubspaceSeq) stage by stage: at each step the controlled transform lies in the saturation of the previous controlled transform (birationalTransform_stalkIdeal_le_saturationStalk, the order clause (4′) supplying the order ≥ 1 along the centre), which lies in the saturation of the previous strict transform (saturationStalk_mono, the induction hypothesis), which lies in the strict transform (saturationStalk_le_stalkIdeal_strictTransformSubspace).

theorem Hironaka.Manifold.cosupport_strictTransformSubspaceSeq_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J E₀ : M.IdealSheaf) (hge : S.IsOfOrderGe J 1 E₀) (i : Fin (S.length + 1)) : Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq J i) ⊆ Manifold.IdealSheaf.support (S.markedTransformSeq J 1 i)

One inclusion of the identity between the final support and the final strict transform, from the order hypothesis alone and with no finite-type input: the cosupport of the final strict transform lies in the final support supp(𝓘_r, 1) (a larger ideal sheaf has a smaller cosupport).

theorem Hironaka.Manifold.support_totalTransformSeq_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) (hcl : ∀ (j : (S.totalTransformSeq i.castSucc).ι), IsClosed ((S.totalTransformSeq i.castSucc).hyp j)) : (S.totalTransformSeq i.succ).support = ⇑(S.map i) ⁻¹' (S.totalTransformSeq i.castSucc).support ∪ S.exceptionalAt i

The support of the exceptional family at stage i + 1 is the preimage of the support at stage i together with the exceptional divisor of the i-th blow-up (the recursion E_{i+1} = red(π_i⁻¹(E_i) ∪ π_i⁻¹(Z_i)) of [Hir64, Main Theorem II′(N), p. 156] read on supports). The components at stage i are assumed closed (they are, for a sequence of order ≥ 1: isSnc_totalTransformSeq).

theorem Hironaka.Manifold.notMem_exceptionalAt_and_map_notMem_of_notMem_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) (hcl : ∀ (j : (S.totalTransformSeq i.castSucc).ι), IsClosed ((S.totalTransformSeq i.castSucc).hyp j)) {x : (S.stage i.succ).carrier} (hx : x ∉ (S.totalTransformSeq i.succ).support) : x ∉ S.exceptionalAt i ∧ (S.map i) x ∉ (S.totalTransformSeq i.castSucc).support

A point of stage i + 1 off the exceptional family lies off the i-th exceptional divisor and maps to a point off the exceptional family of stage i.

theorem Hironaka.Manifold.stalkIdeal_markedTransformSeq_eq_strictTransformSubspaceSeq_of_notMem_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J E₀ : M.IdealSheaf) (hge : S.IsOfOrderGe J 1 E₀) (hcl : ∀ (i : Fin (S.length + 1)) (j : (S.totalTransformSeq i).ι), IsClosed ((S.totalTransformSeq i).hyp j)) (hsat : ∀ (i : Fin S.length), Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (S.strictTransformSubspaceSeq J i.castSucc))) (i : Fin (S.length + 1)) (x : (S.stage i).carrier) (hx : x ∉ (S.totalTransformSeq i).support) : Manifold.IdealSheaf.stalkIdeal (S.markedTransformSeq J 1 i) x = Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq J i) x

Off the exceptional family the two chains agree, given that each saturation is finitely generated (the hypothesis under which the strict transform is the saturation, [BM97, Proposition 3.13]): at a point of stage i lying on no exceptional divisor, the stalk of the marked chain at mark 1 equals the stalk of the saturation chain. Both are the pullback of the previous stalks along the blow-up (birationalTransform_stalkIdeal_of_notMem, saturationStalk_of_notMem_cosupport), and the previous stalks agree by induction, the point lying over a point off the previous exceptional family (support_totalTransformSeq_succ).

theorem Hironaka.Manifold.span_coord_ne_top_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {c : ℕ} (σ : Fin c ↪ Fin n) : Ideal.span (Set.range fun (i : Fin c) => Manifold.coord E ψ φ hφ ha (σ i)) ≠ ⊤ ↔ ∀ (i : Fin c), ψ (↑φ a) (σ i) = 0

A coordinate ideal (z_σ) at a is proper iff every z_{σ i} vanishes at a (a coordinate not vanishing at a is a unit of the stalk, isUnit_coord_of_ne_zero; vanishing coordinates lie in the maximal ideal, coord_mem_maximalIdeal_of_eq_zero).

theorem Hironaka.Manifold.mem_closure_cosupport_diff_support_of_isSmoothTransversalIdealAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {x : M} (hxJ : x ∈ J.support) (hx : Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ F J x) : x ∈ closure (J.support \ F.support)

The density step: at a point x of the support of J where J is locally the ideal of a coordinate subspace transversal to the members of the simple normal crossing family F through x (the predicate IsSmoothTransversalIdealAt, the shape of the final controlled transform of the modified marked resolution), the support of J off the family is dense at x. In the chart, move x off every member through it along the members' own coordinates (which are not coordinates of the subspace) by an arbitrarily small nonzero amount; the members not through x form a closed set missing x (the family is locally finite with closed members).

theorem Hironaka.Manifold.cosupport_markedTransformSeq_eq_cosupport_strictTransformSubspaceSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J E₀ : M.IdealSheaf) (hge : S.IsOfOrderGe J 1 E₀) (hsnc : ∀ (i : Fin (S.length + 1)), Manifold.HypersurfaceFamily.IsSnc ψ (S.totalTransformSeq i)) (hsat : ∀ (i : Fin S.length), Manifold.IdealSheaf.HasLocalGenerators (Manifold.saturationStalk ⋯ ⋯ (S.strictTransformSubspaceSeq J i.castSucc))) (hc1 : ∀ x ∈ Manifold.IdealSheaf.support (S.markedTransformSeq J 1 (Fin.last S.length)), Manifold.HypersurfaceFamily.IsSmoothTransversalIdealAt ψ (S.totalTransformSeq (Fin.last S.length)) (S.markedTransformSeq J 1 (Fin.last S.length)) x) : Manifold.IdealSheaf.support (S.markedTransformSeq J 1 (Fin.last S.length)) = Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq J (Fin.last S.length))

The final support is the cosupport of the final strict transform, for any finite blow-up sequence of order ≥ 1 [Kol07, Definition 66] whose exceptional families are simple normal crossing families, whose saturations have local generators, and whose final controlled transform is at every support point locally the ideal of a coordinate subspace transversal to the exceptional divisors (the shape of the output of Włodarczyk's modified algorithm, the proof of [Wlo09, Theorem 7.4.1]). One inclusion is cosupport_strictTransformSubspaceSeq_subset; for the other, a support point is a limit of support points off the exceptional divisors (the density lemma), where the two chains agree (stalkIdeal_markedTransformSeq_eq_strictTransformSubspaceSeq_of_notMem_support), and the cosupport of the strict transform is closed.