Hironaka's weak transform has the colon stalks

The weak transform of I by the blowing-up π with centre Y divides π⁻¹(I) by the ν-th power of I_F, ν the generic order of I along the connected component of Y through the point [Hir64, Ch. 0, §5, p. 142]. The definition (IdealSheaf.weakTransformOf, the unbundled reading of AnalyticManifold.IdealSheaf.weakTransform) uses the pointwise exponent a' ↦ (genericOrdAlong I_Y I (π a')).toNat; the existence theorem of Hironaka.Manifold.BlowUp.Transform.Colon applies because this exponent is at most the order of I along Y at π a' (genericOrdAlong_le: the infimum over the component through π a' is bounded by the value at π a') and is locally constant on the exceptional divisor: near a point of Y, the points of Y lie in a connected chart ball, hence in the same connected component of Y (IsClosedSubmanifold.eventually_connectedComponentIn_eq, from IsAdaptedChart.exists_preconnected_mem_nhds), and the generic order only depends on the component (genericOrdAlong_eq_of_mem_connectedComponentIn). The definition carries no hypothesis I ≠ 0 (Hironaka's standing assumption, under which the generic order is finite): where the order is ⊤ the exponent is 0 and the weak transform is the total transform there.

The result, isDivExceptional_weakTransformOf, is transferred to the weak transform of the vocabulary of the main theorems in Hironaka.Manifold.BlowUp.Transform.Bundled.

theorem Manifold.IdealSheaf.genericOrdAlong_eq_of_mem_connectedComponentIn {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) {a b : ↑X} (h : b ∈ connectedComponentIn D.support a) : D.genericOrdAlong J b = D.genericOrdAlong J a

The generic order along the component through a depends only on the component.

theorem Manifold.IdealSheaf.genericOrdAlong_le {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} (D J : IdealSheaf 𝒪) {a : ↑X} (ha : a ∈ D.support) : D.genericOrdAlong J a ≤ D.ordAlongIdeal J a

The generic order along the component through a ∈ D is at most the order along D at a.

theorem Manifold.IsClosedSubmanifold.eventually_connectedComponentIn_eq {𝕜 : 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 : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : M} (ha : a ∈ Y) : ∀ᶠ (b : M) in nhds a, b ∈ Y → connectedComponentIn Y b = connectedComponentIn Y a

A closed submanifold is locally connected: near a point a of Y, the points of Y lie in the connected component of Y through a.

theorem Manifold.isDivExceptional_weakTransformOf {𝕜 : 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} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) : (IdealSheaf.pullback π ⋯ I).IsDivExceptional (IdealSheaf.pullback π ⋯ hY.idealSheaf) (fun (a' : ↑↧M') => (hY.idealSheaf.genericOrdAlong I (π a')).toNat) (IdealSheaf.weakTransformOf hY h I)

The weak transform has the colon stalks (π⁻¹(I)_{a'} : I_{F,a'}^{ν}), ν the generic order of I along the component of Y through π a' [Hir64, Ch. 0, §5, p. 142].