The pull-back of a monomial along a blow-up chart

If g = b ∏_k z_k^{e_k} in adapted coordinates for a simple normal crossings divisor E at π(a') and the centre Y has simple normal crossings with E, then in the induced coordinates of a blow-up chart at a' the pull-back g ∘ π is again a unit times a monomial supported on the coordinates of the total transform of E: the coordinate u_i of the exceptional divisor to the sum of the exponents of the coordinates in the centre's block, and each other coordinate to its own exponent (the computation Bierstone–Milman make for the strict transform in a blow-up chart, f'(w', z') = (z'_1)^{-d} f(w', z'_1, z'_1(⋯)) [BM97, §3, "The strict transform"]; Kollár's total transform of a divisor [Kol07, Definition 25]). In the stalk form of the Jacobian ledger (Hironaka/Resolution/Analytic/BM97/Ledger.lean) the unit b is absorbed and the monomial is read as the product of the powers of the vanishing stalks of the members: the stalk map germMap π carries ∏_{j ∈ s} (vanishing stalk of E^j at π p)^{e_j} to the product over the strict transforms of the same members at p, each with its exponent (a factor ⊤ where the strict transform misses p), times the vanishing stalk of the exceptional divisor π⁻¹ Y to the sum of the e_j over the members whose coordinate lies in the centre's block (germMap_prod_vanishingStalk_pow_totalTransform). The per-member identity (germMap_vanishingStalk_hyp) is the chart law for the coordinate germs (z_{σ i} ∘ π = u_{σ i}, z_{σ k} ∘ π = u_{σ i} u_{σ k} for k ≠ i, z_j ∘ π = u_j off the block: IsBlowUpChart.germMap_coord_self, germMap_coord_of_ne, germMap_coord_off) together with the description of the strict transforms in the blow-up chart (strictTransform_inter_source_self, strictTransform_inter_source_of_ne, strictTransform_inter_source_off) and the vanishing stalk of a coordinate hyperplane (IsClosedSubmanifold.vanishingStalk_eq_span_coord, vanishingStalk_eq_span_coord_of_forall_mem_iff); the product is assembled by Ideal.map of a finite product (Ideal.map_finset_prod). This is the transport of the old monomial in the step of the ledger (Hironaka/Resolution/Analytic/BM97/LedgerStep.lean).

theorem Manifold.HypersurfaceFamily.IsSncChartAt.vanishingStalk_hyp_eq_span {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {φ : OpenPartialHomeomorph M E} {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a cidx) (j : { j : F.ι // a ∈ F.hyp j }) : vanishingStalk (F.hyp ↑j) a = Ideal.span {coord E ψ φ ⋯ ⋯ (cidx j)}

In a simple normal crossings chart at a, the vanishing stalk of a component through a is spanned by the component's coordinate (mem_vanishingStalk_hyp_iff).

theorem Hironaka.Manifold.germMap_vanishingStalk_hyp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} {c : ℕ} {F : Manifold.HypersurfaceFamily M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {p : M'} {cidx : { j : F.ι // π p ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ (π p) cidx) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φ.source) (j : { j : F.ι // π p ∈ F.hyp j }) [Decidable (∃ (k : Fin c), σ k = cidx j)] : Ideal.map (Manifold.germMap π ⋯ p) (Manifold.vanishingStalk (F.hyp ↑j) (π p)) = (Manifold.vanishingStalk (π ⁻¹' Y) p ^ if ∃ (k : Fin c), σ k = cidx j then 1 else 0) * Manifold.vanishingStalk (Manifold.strictTransformSet π Y (F.hyp ↑j)) p

One member: the stalk map of the blow-up carries the vanishing stalk of a member through π p to the exceptional divisor's vanishing stalk (to the power 1 when the member's coordinate lies in the centre's block, 0 otherwise) times the vanishing stalk of its strict transform — the chart law for the coordinate germs, case by case on the member's coordinate: σ i (the strict transform misses the chart, strictTransform_inter_source_self), σ k with k ≠ i (z_{σ k} ∘ π = u_{σ i} u_{σ k}, the strict transform {u_{σ k} = 0}), off the block (z_j ∘ π = u_j). The vanishing stalk of the strict transform at p is read in the chart by vanishingStalk_eq_span_coord_of_forall_mem_iff, which needs no closed-submanifold hypothesis, so no simple normal crossings hypothesis on the centre enters.

theorem Hironaka.Manifold.germMap_prod_vanishingStalk_pow_totalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [hM : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {Y : Set M} {c : ℕ} {F : Manifold.HypersurfaceFamily M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {p : M'} {cidx : { j : F.ι // π p ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ (π p) cidx) {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φ.source) (s : Finset F.ι) (e : F.ι → ℕ) (hs : ∀ j ∈ s, π p ∈ F.hyp j) : Ideal.map (Manifold.germMap π ⋯ p) (∏ j ∈ s, Manifold.vanishingStalk (F.hyp j) (π p) ^ e j) = (∏ j ∈ s, Manifold.vanishingStalk ((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl j))) p ^ e j) * Manifold.vanishingStalk ((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inr PUnit.unit))) p ^ ∑ j ∈ s.attach, if ∃ (k : Fin c), σ k = cidx ⟨↑j, ⋯⟩ then e ↑j else 0

The pull-back of a monomial in the coordinates of a simple normal crossings divisor along a blow-up chart ([BM97, §3, "The strict transform"]; [Kol07, Definition 25]): the product of the per-member identities germMap_vanishingStalk_hyp, the exceptional exponents summed (Finset.prod_pow_eq_pow_sum).