Density of the strict transform off the exceptional divisor at a regular point

Along a finite succession of blow-ups with smooth centres, at a point of the strict transform Y_i of a closed subspace whose quotient stalk is regular, the points of Y_i off the exceptional family E_i accumulate (mem_closure_cosupport_strictTransformSubspaceSeq_diff_support_of_isRegular). This is not stated in the sources; it is what turns clause (3) of [Wlo09, Theorem 2.0.2] into its proper form, where no exceptional divisor through a point carries a coordinate of the final strict transform (Hironaka/Resolution/Analytic/Wlo09/ProperSncOfEmbeddedDesing.lean), and it gives the density of the preimage of the regular locus under the resolution of an analytic space.

The strict transform is taken stalkwise as the saturation ⋃_k (σ^*𝓘 : 𝓘_D^k) of the total transform by the exceptional ideal [BM97, Proposition 3.13]; since these saturations have local generators (saturationStalk_hasLocalGenerators), the definition strictTransformSubspace takes this branch at every point (stalkIdeal_strictTransformSubspace). The lemmas:

• a regular quotient stalk is a coordinate ideal on an adapted chart and the full vanishing ideal of the smooth germ (exists_adaptedChart_of_isRegularLocalRing_quotient with vanishingStalk_cosupport_eq_stalkIdeal_of_eq_span_coord), and regularity of the quotient stalk is open along the cosupport (eventually_isRegularLocalRing_quotient_of_isRegular);
• a saturation by the exceptional ideal never contains the exceptional ideal unless it is the unit ideal (stalkIdeal_strictTransformSubspace_eq_top_of_exceptional_le);
• off the centre, regularity of the quotient stalk transports along the blowing-down (isRegularLocalRing_quotient_strictTransformSubspace_iff_of_notMem), which is an open map there (IsBlowUp.image_mem_nhds_of_notMem);
• the theorem, by induction on the stage; the case of a point on the new exceptional divisor is mem_closure_cosupport_diff_exceptional_of_isRegular at one blow-up.

The argument is uniform in the field 𝕜 and uses no Nullstellensatz.

theorem Hironaka.Manifold.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.strictTransformSubspace hY h I).stalkIdeal a' = Manifold.saturationStalk hY h I a'

The stalks of the strict transform are the saturations, unconditionally: the saturation stalks have local generators (saturationStalk_hasLocalGenerators), so the definition strictTransformSubspace takes its saturation branch at every point (stalkIdeal_strictTransformSubspace_of_hasLocalGenerators).

theorem Hironaka.Manifold.stalkIdeal_strictTransformSubspace_eq_top_of_exceptional_le {𝕜 : 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') (hle : (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal a' ≤ (Manifold.strictTransformSubspace hY h I).stalkIdeal a') : (Manifold.strictTransformSubspace hY h I).stalkIdeal a' = ⊤

A saturation by the exceptional ideal never contains the exceptional ideal unless it is the unit ideal: if 𝓘_D ≤ Ỹ_{a'} then Ỹ_{a'} = ⊤. The chain k ↦ (T : 𝓘_D^k) is stationary from some N in the Noetherian stalk (exists_colon_pow_stationary_at), so the saturation is (T : 𝓘_D^N); 𝓘_D ≤ (T : 𝓘_D^N) gives 𝓘_D^{N+1} ≤ T, hence 1 ∈ (T : 𝓘_D^{N+1}) = (T : 𝓘_D^N).

theorem Hironaka.Manifold.mem_closure_cosupport_diff_exceptional_of_isRegular {𝕜 : 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') (ha' : a' ∈ (Manifold.strictTransformSubspace hY h I).support) (hreg : IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E M').presheaf.stalk a') ⧸ (Manifold.strictTransformSubspace hY h I).stalkIdeal a')) : a' ∈ closure ((Manifold.strictTransformSubspace hY h I).support \ (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).support)

At a point of the strict transform under one blow-up whose quotient stalk is regular, the points of the strict transform off the exceptional divisor accumulate: the stalk is a coordinate ideal on an adapted chart and the full vanishing ideal of the cosupport there, the exceptional equation is not in it (stalkIdeal_strictTransformSubspace_eq_top_of_exceptional_le), so it does not vanish identically on the cosupport near the point.

theorem Hironaka.Manifold.isRegularLocalRing_quotient_strictTransformSubspace_iff_of_notMem {𝕜 : 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') (ha' : π a' ∉ Y) : IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E M').presheaf.stalk a') ⧸ (Manifold.strictTransformSubspace hY h I).stalkIdeal a') ↔ IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E M).presheaf.stalk (π a')) ⧸ I.stalkIdeal (π a'))

Off the centre, regularity of the quotient stalk transports along the blowing-down: the germ map is bijective there (IsBlowUp.germMap_bijective_of_notMem) and the stalk of the strict transform is the image of the stalk of I.

theorem Manifold.IsBlowUp.image_mem_nhds_of_notMem {𝕜 : 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} (h : IsBlowUp ψ Y c π) {a' : M'} (ha' : π a' ∉ Y) {N : Set M'} (hN : N ∈ nhds a') : π '' N ∈ nhds (π a')

Off the centre the blowing-down is an open map: the image of a neighbourhood of a point off the exceptional divisor is a neighbourhood of its image (the field isLocalDiffeomorphOn_compl, a local homeomorphism there).

theorem Hironaka.Manifold.eventually_isRegularLocalRing_quotient_of_isRegular {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] (J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M')) {a : M'} (hreg : IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E M').presheaf.stalk a) ⧸ J.stalkIdeal a)) : ∀ᶠ (y : ↑↧M') in nhds a, y ∈ J.support → IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E M').presheaf.stalk y) ⧸ J.stalkIdeal y)

Regularity of the quotient stalk is open along the cosupport: on the source of the adapted chart the stalks of J are the coordinate span (exists_adaptedChart_of_isRegularLocalRing_quotient), a coordinate span is proper iff its coordinates vanish (span_coord_ne_top_iff), and a proper coordinate span has a regular quotient (isRegularLocalRing_quotient_span_coord).

theorem Hironaka.Manifold.mem_closure_cosupport_strictTransformSubspaceSeq_diff_support_of_isRegular {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (i : Fin (S.length + 1)) (z : (S.stage i).carrier) (hz : z ∈ Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq J i)) (hreg : IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E (S.stage i).carrier).presheaf.stalk z) ⧸ Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq J i) z)) : z ∈ closure (Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq J i) \ (S.totalTransformSeq i).support)

Density of the strict transform off the exceptional divisor at a regular point, at every stage i of a finite succession: at a point z of the strict transform Y_i whose quotient stalk is regular, the points of Y_i off the exceptional family E_i accumulate at z. Base i = 0: E_0 = ∅ (totalTransformSeq_zero). Step: if z is off the new divisor (the first case), push down along the local isomorphism and apply the induction hypothesis at π z; if z is on the new divisor (the second case), mem_closure_cosupport_diff_exceptional_of_isRegular gives a regular point of Y_{i+1} off the new divisor arbitrarily near z, and the first case applies to it. Uniform in 𝕜; no Nullstellensatz.