Division by a power of a coordinate, on a chart and in a stalk

The quotient u^{-m} F of an analytic function F by the m-th power of a coordinate u = x_k is a well-defined analytic function on the whole chart when F is divisible by x_k^m near every point of the hyperplane {x_k = 0}: it is the m-fold iterate of the canonical coordinate quotient coordQuot of Hironaka.Manifold.BlowUp.Lift (F/x_k off the hyperplane, ∂_k F on it), and x_k^m · (u^{-m} F) = F (coordQuot_iterate_spec). The divisibility hypothesis is read off a stalk: a germ lying in the m-th power of the ideal generated by a coordinate germ of a chart is, near the point, the product of the m-th power of the coordinate function with an analytic function (exists_eq_pow_mul_of_mem_span_pow_coord). Two facts about ideals close the file: in a domain, the colon of the ideal spanned by the a^m g_j by a^m is the ideal spanned by the g_j (Ideal.colon_span_range_pow_mul: the quotient is independent of the generators), and multiplying generators by a unit does not change the ideal (Ideal.span_range_unit_mul).

These are the tools for dividing the total transform of an ideal by a power of the exceptional divisor, as in Hironaka's weak transform [Hir64, Ch. 0, §5, p. 142] and Kollár's chart formula for the birational transform [Kol07, Definition 60, (60.3)]; they are used in Hironaka.Manifold.BlowUp.Transform.Colon.

Iterated coordinate division on an open set

theorem Manifold.coordQuot_eq_of_eq_mul {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) {F Q : (Fin n → 𝕜) → 𝕜} {U : Set (Fin n → 𝕜)} (hU : IsOpen U) (hQ : AnalyticOnNhd 𝕜 Q U) (h : ∀ y ∈ U, F y = y k * Q y) {y : Fin n → 𝕜} (hy : y ∈ U) : coordQuot k F y = Q y

If F = x_k · Q on an open set with Q analytic, the canonical quotient of F by x_k is Q there.

theorem Manifold.analyticAt_apply_coord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) (w : Fin n → 𝕜) : AnalyticAt 𝕜 (fun (v : Fin n → 𝕜) => v k) w

The coordinate function x_k is analytic.

theorem Manifold.coordQuot_iterate_spec {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {N : Set (Fin n → 𝕜)} (hN : IsOpen N) (k : Fin n) (m : ℕ) (F : (Fin n → 𝕜) → 𝕜) : AnalyticOnNhd 𝕜 F N → (∀ v ∈ N, v k = 0 → ∃ (N' : Set (Fin n → 𝕜)), IsOpen N' ∧ v ∈ N' ∧ ∃ (G : (Fin n → 𝕜) → 𝕜), AnalyticOnNhd 𝕜 G N' ∧ ∀ w ∈ N', F w = w k ^ m * G w) → AnalyticOnNhd 𝕜 ((coordQuot k)^[m] F) N ∧ ∀ v ∈ N, v k ^ m * (coordQuot k)^[m] F v = F v

If F is analytic on the open set N and, near every point of N on the hyperplane {x_k = 0}, F is x_k^m times an analytic function, then the m-fold canonical quotient x_k^{-m} F is analytic on N and x_k^m · (x_k^{-m} F) = F on N.

From a stalk to a chart

theorem Manifold.exists_eq_pow_mul_of_mem_span_pow_coord {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Φ : OpenPartialHomeomorph M E} (hΦ : Φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {b : M} (hb : b ∈ Φ.source) (k : Fin n) (m : ℕ) {W : TopologicalSpace.Opens M} (hbW : b ∈ W) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op W))) (hs : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ W b hbW)) f ∈ Ideal.span {coord E ψ Φ hΦ hb k ^ m}) : ∃ (N' : Set (Fin n → 𝕜)), IsOpen N' ∧ ψ (↑Φ b) ∈ N' ∧ ∃ (G : (Fin n → 𝕜) → 𝕜), AnalyticOnNhd 𝕜 G N' ∧ ∀ w ∈ N', extendSection 𝕜 E f (↑Φ.symm (ψ.symm w)) = w k ^ m * G w

Reading a stalk statement on a chart: if the germ at b of a section f lies in the m-th power of the ideal generated by the coordinate germ x_k of a chart Φ at b, then near ψ (Φ b) the function f ∘ Φ⁻¹ ∘ ψ⁻¹ is x_k^m times an analytic function.

Two facts about ideals

theorem Ideal.colon_span_range_pow_mul {R : Type u_2} [CommRing R] [IsDomain R] {a : R} (ha : a ≠ 0) (m : ℕ) {ι : Type u_3} [Finite ι] (g : ι → R) : Submodule.colon (span (Set.range fun (j : ι) => a ^ m * g j)) {a ^ m} = span (Set.range g)

In a domain, the colon of the ideal spanned by the a^m · g_j by a^m is the ideal spanned by the g_j: the quotient is independent of the generators.

theorem Ideal.span_range_unit_mul {R : Type u_2} [CommRing R] {v : R} (hv : IsUnit v) {ι : Type u_3} (g : ι → R) : span (Set.range fun (j : ι) => v * g j) = span (Set.range g)

Multiplying generators by a unit does not change the ideal they span.