The ideal sheaf of the strict transform of a hypersurface

For a smooth hypersurface H ⊇ Y, the birational transform π_*^{-1}(I_H, 1) = I_F^{-1} π⁻¹(I_H) is the ideal sheaf of the strict transform H' (isIdealSheafOf_strictTransform): this is Bierstone–Milman's f' = y_exc^{-d} f ∘ σ with d = 1 [BM97, §3, "The strict transform"]. Both are ideal sheaves with the stalks of a closed submanifold, so it suffices to compare stalks. Over the centre, in the pair chart of Hironaka.Manifold.BlowUp.Transform.StrictCharts (H = {z_{σ k₀} = 0}) and a blow-up chart of index i, π⁻¹(I_H) is generated by z_{σ k₀} ∘ π = u_i u_{k₀} (or by u_i when k₀ = i), so the colon by u_i is (u_{k₀}), the ideal of H' = {u_{k₀} = 0} in that chart, or the unit ideal where H' is absent (k₀ = i, or u_{k₀} a unit at the point); the stalk is a domain. Off the exceptional divisor I_F is the unit ideal, π⁻¹(I_H) is generated by h ∘ π for the coordinate h of an adapted chart of H, and h ∘ π is the coordinate of the transported chart adapted to H'. The comparison of the orders along the centre needs I_H ⊆ I_Y at the points of Y (stalkIdeal_idealSheaf_le_of_subset: germs vanishing on H vanish on Y ⊆ H).

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_le_of_subset {𝕜 : 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 : ℕ} {H : Set M} (hY : IsClosedSubmanifold ψ Y c) (hH : IsClosedSubmanifold ψ H 1) (hYH : Y ⊆ H) {a : M} (ha : a ∈ Y) : hH.idealSheaf.stalkIdeal a ≤ hY.idealSheaf.stalkIdeal a

For Y ⊆ H, the ideal of H is contained in the ideal of Y at the points of Y (germs vanishing on H vanish on Y).

theorem Manifold.range_singleIdx_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {e : OpenPartialHomeomorph N E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ N) {p : N} (hp : p ∈ e.source) (k : Fin n) : (Set.range fun (j : Fin 1) => coord E ψ e he hp ((singleEmb k) j)) = {coord E ψ e he hp k}

The range of the single coordinate of a hypersurface chart.

theorem Manifold.isIdealSheafOf_strictTransform {𝕜 : 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 : ℕ} {H : Set M} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hH : IsClosedSubmanifold ψ H 1) (hYH : Y ⊆ H) : IsIdealSheafOf ψ (strictTransformSet π Y H) 1 (MarkedIdealSheaf.birationalTransform hY h { I := hH.idealSheaf, m := 1 }).I

The ideal sheaf of the strict transform of a smooth hypersurface H ⊇ Y is the birational transform of (I_H, 1) (f' = y_exc^{-d} f ∘ σ with d = 1, [BM97, §3, "The strict transform"]).