The flat descent datum at a point of the exceptional divisor: the completion identification

At a point a' of a blow-up chart Φ of index i over the centre, the chart ring R' = R[x_j/x_r] of R = 𝒪_{M,π(a')} maps to 𝒪_{M',a'} by the chart-ring map χ, and the flat descent datum of Algebra.HasFlatDescentDatum for χ is the completion 𝒪̂_{M',a'}. This is the input to the proof of [BM97, Proposition 3.13] by the flatness route (Hironaka.Manifold.BlowUp.Transform.StrictSubspaceProp313).

• Kollár's coordinates at a' (kollarCoords): the adapted coordinates of φ centred at π(a') and permuted by τ (τ r = σ i the divisor coordinate, the τ j, j < r, the other centre coordinates), with the centre coordinates x_j (j < r) shifted by u_{τ j}(a') · x_r (shiftCoords) so that the ratio coordinates x_j / x_r ↦ u_{τ j} − u_{τ j}(a') vanish at a': the chart ring of the shifted coordinates is R' and its chart origin is χ⁻¹(𝔪_{a'}) (IsLocalRing.comap_maximalIdeal_eq_chartOrigin). The pullback relations germMap π (x_j) = u_{σ i} · (u_{τ j} − u_{τ j}(a')), germMap π (x_r) = u_{σ i}, germMap π (x_j) = u_{τ j} − u_{τ j}(a') (j > r, transversal coordinates: IsBlowUpChart.germMap_coord_of_forall_ne) give χ by IsLocalRing.exists_chartRing_hom_of_mul_eq (exists_isChartRingHom). These are the coordinates of [Kol07, Definition 60, (60.2)], as used in the proof of [Kol07, Lemma 62].
• The completion identification (IsChartRingHom.hasFlatDescentDatum): the local map χ_loc : R'_{𝔪'} → 𝒪_{M',a'} induces a bijection of completions (R'_{𝔪'})^ → 𝒪̂_{M',a'} (IsLocalRing.completionMap_bijective_of_cohen), with the analytic constants 𝕜 → R → R' → R'_{𝔪'} as the coefficient field of (R'_{𝔪'})^ (a coefficient field since ev_{a'} ∘ χ_loc identifies R'_{𝔪'}/𝔪' ≅ 𝕜), the regular system of parameters y_m = x_{τ⁻¹ m} / x_r-or-x_{τ⁻¹ m} of R'_{𝔪'}, and the Taylor isomorphism 𝒪̂_{M',a'} ≅ 𝕜⟦X⟧ under which χ_loc(y_m) ↦ X_m (taylorHom_coord_sub). Hence R' → 𝒪̂_{M',a'} is flat (IsLocalRing.flat_comp_algebraMap_adicCompletion) and J 𝒪̂ ∩ 𝒪 = J. Completions of local rings enter Kollár's treatment in [Kol07, Definition 55].
• Proposition 3.13 at every point (saturationStalk_eq_span_strictTransformElems): over the centre through the datum and the pointwise theorem of Hironaka.Manifold.BlowUp.Transform.StrictSubspaceProp313, off the centre directly.

Pullbacks of constants and of transversal coordinates

theorem Manifold.germMap_const {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} (hπ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π) (p : M') (a : 𝕜) : (germMap π hπ p) ((const 𝕜 E M (π p)) a) = (const 𝕜 E M' p) a

The germ of a constant pulls back to the germ of the constant.

theorem Manifold.IsBlowUpChart.germMap_coord_of_forall_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hπ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) {m : Fin n} (hm : ∀ (k : Fin c), σ k ≠ m) : (germMap π hπ p) (coord E ψ φ hφ ⋯ m) = coord E ψ Φ ⋯ hp m

z_m ∘ π = u_m for a coordinate m transversal to the centre (the blow-up chart map is the identity off the block σ).

theorem Manifold.IsBlowUpChart.eval_coord_of_forall_ne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) {m : Fin n} (hm : ∀ (k : Fin c), σ k ≠ m) : (eval 𝕜 E M (π p)) (coord E ψ φ hφ ⋯ m) = (eval 𝕜 E M' p) (coord E ψ Φ ⋯ hp m)

The value at π p of a transversal coordinate is its value at p in the blow-up chart.

Kollár's coordinates at a point of the exceptional divisor

noncomputable def Manifold.kollarCoords {𝕜 : 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'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))

Kollár's coordinates at a': the centred adapted coordinates centredCoords (permuted by τ), with the centre coordinates x_j, j < r, shifted by u_{τ j}(a') · x_r (shiftCoords), so that the ratio coordinates x_j / x_r of the chart ring vanish at a'.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.kollarCoords_of_lt {𝕜 : 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'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) {j : Fin n} (hj : j < r) : kollarCoords hφ hΦ ha' r τ j = centredCoords hφ hΦ ha' τ j - (const 𝕜 E M (π a')) ((eval 𝕜 E M' a') (coord E ψ Φ ⋯ ha' (τ j))) * centredCoords hφ hΦ ha' τ r

theorem Manifold.kollarCoords_of_not_lt {𝕜 : 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'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) {j : Fin n} (hj : ¬j < r) : kollarCoords hφ hΦ ha' r τ j = centredCoords hφ hΦ ha' τ j

theorem Manifold.maximalIdeal_eq_span_centredCoords {𝕜 : 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'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (τ : Fin n ≃ Fin n) : IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) = Ideal.span (Set.range (centredCoords hφ hΦ ha' τ))

The centred coordinates generate 𝔪_{π(a')} (reindexed by τ).

theorem Manifold.maximalIdeal_eq_span_kollarCoords {𝕜 : 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'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) : IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) = Ideal.span (Set.range (kollarCoords hφ hΦ ha' r τ))

Kollár's coordinates at a' generate 𝔪_{π(a')}.

theorem Manifold.centredCoords_of_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'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) (haY : π a' ∈ Y) (hτr : τ r = σ i) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) {j : Fin n} (hj : j ≤ r) : centredCoords hφ hΦ ha' τ j = coord E ψ φ ⋯ ⋯ (τ j)

Over the centre the centre coordinates are already centred: x_j = z_{τ j} for j ≤ r.

theorem Manifold.germMap_kollarCoords_self {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) (haY : π a' ∈ Y) (hτr : τ r = σ i) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) (h : IsBlowUp ψ Y c π) : (germMap π ⋯ a') (kollarCoords hφ hΦ ha' r τ r) = coord E ψ Φ ⋯ ha' (σ i)

x_r ∘ π = u_{σ i}, the divisor coordinate.

theorem Manifold.germMap_kollarCoords_of_lt {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) (haY : π a' ∈ Y) (hτr : τ r = σ i) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) (h : IsBlowUp ψ Y c π) {j : Fin n} (hj : j < r) : (germMap π ⋯ a') (kollarCoords hφ hΦ ha' r τ j) = coord E ψ Φ ⋯ ha' (σ i) * (coord E ψ Φ ⋯ ha' (τ j) - (const 𝕜 E M' a') ((eval 𝕜 E M' a') (coord E ψ Φ ⋯ ha' (τ j))))

x_j ∘ π = u_{σ i} · (u_{τ j} − u_{τ j}(a')) for j < r: the shifted centre coordinates.

theorem Manifold.germMap_kollarCoords_of_gt {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) (hτr : τ r = σ i) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) (h : IsBlowUp ψ Y c π) {j : Fin n} (hj : r < j) : (germMap π ⋯ a') (kollarCoords hφ hΦ ha' r τ j) = coord E ψ Φ ⋯ ha' (τ j) - (const 𝕜 E M' a') ((eval 𝕜 E M' a') (coord E ψ Φ ⋯ ha' (τ j)))

x_j ∘ π = u_{τ j} − u_{τ j}(a') for j > r: the transversal coordinates.

theorem Manifold.exists_isChartRingHom {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (r : Fin n) (τ : Fin n ≃ Fin n) (haY : π a' ∈ Y) (hτr : τ r = σ i) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) (h : IsBlowUp ψ Y c π) : ∃ (χ : ↥(IsLocalRing.chartRing (kollarCoords hφ hΦ ha' r τ) r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')), IsChartRingHom h hΦ ha' (kollarCoords hφ hΦ ha' r τ) r τ χ

exists_chartRing_hom for Kollár's coordinates at a': the chart-ring map χ : R' → 𝒪_{M',a'} exists (IsLocalRing.exists_chartRing_hom_of_mul_eq on the pullback relations above).

The flat descent datum: the completion identification

theorem Manifold.isLocalHom_eval {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] (a : M') : IsLocalHom (eval 𝕜 E M' a)

Evaluation at a point is a local homomorphism (𝔪_a = ker ev_a).

theorem Manifold.IsChartRingHom.map_algebraMap_const {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) {x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))} {r : Fin n} {τ : Fin n ≃ Fin n} {χ : ↥(IsLocalRing.chartRing x r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')} (hχ : IsChartRingHom h hΦ ha' x r τ χ) (b : 𝕜) : χ ((algebraMap ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) ↥(IsLocalRing.chartRing x r)) ((const 𝕜 E M (π a')) b)) = (const 𝕜 E M' a') b

A chart-ring map carries the constants to the constants.

theorem Manifold.IsChartRingHom.comap_maximalIdeal_eq_chartOrigin {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) {x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))} {r : Fin n} {τ : Fin n ≃ Fin n} {χ : ↥(IsLocalRing.chartRing x r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')} (hχ : IsChartRingHom h hΦ ha' x r τ χ) (hx : IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) = Ideal.span (Set.range x)) : Ideal.comap χ (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M').presheaf.stalk a')) = IsLocalRing.chartOrigin x r

χ⁻¹(𝔪_{a'}) is the chart origin of x when x generates 𝔪_{π(a')}: the ratio coordinates x_j / x_r map to germs vanishing at a', the x_i to 𝔪_{π(a')} ∘ π ⊆ 𝔪_{a'}.

theorem Manifold.IsChartRingHom.taylorHom_chartYR {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) {x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))} {r : Fin n} {τ : Fin n ≃ Fin n} {χ : ↥(IsLocalRing.chartRing x r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')} (hχ : IsChartRingHom h hΦ ha' x r τ χ) (hgt : ∀ (j : Fin n), r < j → (germMap π ⋯ a') (x j) = coord E ψ Φ ⋯ ha' (τ j) - (const 𝕜 E M' a') ((eval 𝕜 E M' a') (coord E ψ Φ ⋯ ha' (τ j)))) (m : Fin n) : (taylorHom E ψ Φ ha' ⋯) (χ (IsLocalRing.chartYR x r (τ.symm m))) = MvPowerSeries.X m

The Taylor series at a' of χ(y_m), for the regular system of parameters y_m = x_{τ⁻¹ m}/x_r (τ⁻¹ m < r), x_r, x_{τ⁻¹ m} (τ⁻¹ m > r), is the variable X_m — given the transversal relations x_j ∘ π = u_{τ j} − u_{τ j}(a') for j > r.

theorem Manifold.IsChartRingHom.completionMap_bijective {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) {x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))} {r : Fin n} {τ : Fin n ≃ Fin n} {χ : ↥(IsLocalRing.chartRing x r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')} (hχ : IsChartRingHom h hΦ ha' x r τ χ) [(IsLocalRing.chartOrigin x r).IsPrime] (hx : IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) = Ideal.span (Set.range x)) (hgt : ∀ (j : Fin n), r < j → (germMap π ⋯ a') (x j) = coord E ψ Φ ⋯ ha' (τ j) - (const 𝕜 E M' a') ((eval 𝕜 E M' a') (coord E ψ Φ ⋯ ha' (τ j)))) : Function.Bijective ⇑(IsLocalRing.completionMap (IsLocalRing.chartLocalHom x r χ ⋯))

The completion identification (the flatness route to [BM97, Proposition 3.13]): the map of completions induced by the local homomorphism R'_{𝔪'} → 𝒪_{a'} of the chart-ring map χ is bijective — the Taylor expansions at a' of the chart coordinates χ(y_j) are the variables (IsChartRingHom.taylorHom_chartYR), so both completions are 𝕜⟦u_1, …, u_n⟧ on the same coefficient field (IsLocalRing.completionMap_bijective_of_cohen). Extracted from IsChartRingHom.hasFlatDescentDatum for order transport (IsLocalRing.ordFaithful_chartLocalHom).

theorem Manifold.IsChartRingHom.hasFlatDescentDatum {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) {x : Fin n → ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))} {r : Fin n} {τ : Fin n ≃ Fin n} {χ : ↥(IsLocalRing.chartRing x r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')} (hχ : IsChartRingHom h hΦ ha' x r τ χ) (hx : IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk (π a')) = Ideal.span (Set.range x)) (hgt : ∀ (j : Fin n), r < j → (germMap π ⋯ a') (x j) = coord E ψ Φ ⋯ ha' (τ j) - (const 𝕜 E M' a') ((eval 𝕜 E M' a') (coord E ψ Φ ⋯ ha' (τ j)))) : Algebra.HasFlatDescentDatum χ

The flat descent datum for a chart-ring map: for coordinates x generating 𝔪_{π(a')} whose ratio coordinates vanish at a' and with the transversal relations, the completion 𝒪̂_{M',a'} receives 𝒪_{M',a'} faithfully flatly (J 𝒪̂ ∩ 𝒪 = J) and R' → 𝒪̂_{M',a'} is flat — χ_loc : R'_{𝔪'} → 𝒪_{M',a'} induces an isomorphism of completions, both being 𝕜⟦X_1, …, X_n⟧ through Cohen structure (IsLocalRing.completionMap_bijective_of_cohen, with the analytic constants as coefficient field and the Taylor isomorphism on the analytic side).

Proposition 3.13 at every point

theorem Manifold.saturationStalk_eq_span_strictTransformElems {𝕜 : 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 : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (a' : M') : saturationStalk hY h I a' = Ideal.span (strictTransformElems hY h I a')

BM97 Proposition 3.13 ([BM97, Proposition 3.13], by the flatness route): at every point a' of the blowing-up, the saturation ⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) — the stalk of the strict transform, is the ideal generated by the strict transforms y^{-d}(f ∘ π) of the elements f of I_{π(a')}. Over the centre: an adapted chart and a blow-up chart at a', Kollár's coordinates at a', the chart-ring map and its flat descent datum, then the pointwise theorem of Hironaka.Manifold.BlowUp.Transform.StrictSubspaceProp313; off the centre directly.