Local monomialization of a real-analytic function, in Mathlib's terms

The local monomialization of a real-analytic function [Ati70, Resolution Theorem], with the Jacobian clause of [BM97, Theorem 1.10], stated with Mathlib's definitions alone (exists_proper_analytic_monomialization): for f real-analytic on an open set U ⊆ ℝⁿ and not identically zero near any point, a proper real-analytic map π : M → U from an analytic manifold, an analytic isomorphism over {f ≠ 0}, such that in the chart of M at every point both f ∘ π and the Jacobian determinant of π are units times monomials.

The proof applies the principalization theorem with the Jacobian clause [BM97, Theorem 1.10] (exists_extensionCompatibleFamily_isNormalCrossingsDivisor_jacobianIdeal_mul_pullback in the namespace AnalyticManifold) to the principal ideal sheaf (f) on the manifold U (IdealSheaf.principal of the section analyticSection hf):

• (f) is nonzero at every point, since f is not identically zero near any point (isNonzeroEverywhere_principal_analyticSection), and its support is the zero set of f (compl_support_principal_analyticSection), so the resolution σ : M̃ → U is proper and an analytic isomorphism over {f ≠ 0};
• the pull-back σ*(f) is generated at every point by the germ of f ∘ σ, the Jacobian ideal by the germ of the Jacobian determinant of σ in any pair of charts (exists_stalk_jacobianStalk_eq_span_of_charts), and their product is a normal-crossings divisor; both generators divide its monomial generator, so near every point q, in one chart c q of the maximal atlas, f ∘ σ and the Jacobian determinant of σ in the chart c q are units times monomials (IdealSheaf.IsNormalCrossingsDivisor.exists_chart_forall_le_span);
• the manifold M is ULift M̃ (in any universe) with the charts c q as its preferred charts (Manifold.rechartedSpace), so that both monomial forms hold in the chart of M at every point; ULift.down : M → M̃ is an analytic isomorphism (Manifold.rechartedDiffeomorph), and π = σ ∘ ULift.down.

def Hironaka.Resolution.Standard.analyticSection {n : ℕ} {U : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : AnalyticOnNhd ℝ f ↑U) : ↑((Manifold.structureSheaf ℝ (EuclideanSpace ℝ (Fin n)) ((AnalyticManifold.of ℝ (EuclideanSpace ℝ (Fin n))).restrict U).carrier).presheaf.obj (Opposite.op ⊤))

An analytic function f on the open set U ⊆ ℝⁿ as a global section of the sheaf of analytic functions on the manifold U.

Equations

• Hironaka.Resolution.Standard.analyticSection hf = ⟨fun (x : ↥(Opposite.unop (Opposite.op ⊤))) => f ↑↑x, ⋯⟩

theorem Hironaka.Resolution.Standard.analyticSection_apply {n : ℕ} {U : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : AnalyticOnNhd ℝ f ↑U) (x : ↥⊤) : ↑(analyticSection hf) x = f ↑↑x

The section analyticSection hf is f restricted to U.

theorem Hironaka.Resolution.Standard.compl_support_principal_analyticSection {n : ℕ} {U : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : AnalyticOnNhd ℝ f ↑U) : (Manifold.IdealSheaf.support (Manifold.IdealSheaf.principal (analyticSection hf)))ᶜ = {x : ((AnalyticManifold.of ℝ (EuclideanSpace ℝ (Fin n))).restrict U).carrier | f ↑x ≠ 0}

The support of the ideal sheaf (f) on U is the zero set of f.

theorem Hironaka.Resolution.Standard.isNonzeroEverywhere_principal_analyticSection {n : ℕ} {U : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : AnalyticOnNhd ℝ f ↑U) (hf₀ : ∀ x ∈ U, ∃ᶠ (y : EuclideanSpace ℝ (Fin n)) in nhds x, f y ≠ 0) : Manifold.IdealSheaf.IsNonzeroEverywhere (Manifold.IdealSheaf.principal (analyticSection hf))

The ideal sheaf (f) on U is nonzero at every point when f is not identically zero near any point of U.

theorem exists_proper_analytic_monomialization {n : ℕ} (U : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))) {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : AnalyticOnNhd ℝ f ↑U) (hf₀ : ∀ x ∈ U, ∃ᶠ (y : EuclideanSpace ℝ (Fin n)) in nhds x, f y ≠ 0) : ∃ (M : Type u) (x : TopologicalSpace M) (x_1 : ChartedSpace (EuclideanSpace ℝ (Fin n)) M) (π : M → ↥U), IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M ∧ T2Space M ∧ SecondCountableTopology M ∧ ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ π ∧ IsProperMap π ∧ IsLocalDiffeomorphOn (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ π (π ⁻¹' {x : ↥U | f ↑x ≠ 0}) ∧ Set.BijOn π (π ⁻¹' {x : ↥U | f ↑x ≠ 0}) {x : ↥U | f ↑x ≠ 0} ∧ ∀ (p : M), IsMonomialAt n (fun (q : M) => f ↑(π q)) p ∧ IsMonomialAt n (fun (q : M) => (fderiv ℝ (Subtype.val ∘ π ∘ ↑(extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) p).symm) (↑(extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) p) q)).det) p

Local monomialization of a real-analytic function [Ati70, Resolution Theorem, p. 147]. Let f be real-analytic on an open set U ⊆ ℝⁿ, and not identically zero near any point of U. There is a proper real-analytic map π : M → U from an n-dimensional real-analytic manifold M, an analytic isomorphism over the points where f does not vanish, such that near every point p of M, in the coordinates y of the chart of M at p, both f ∘ π and the Jacobian determinant of π are monomials in y times analytic functions that do not vanish at p (IsMonomialAt).

This is the form of resolution of singularities that analysis uses: the change of variables x = π(y) turns an integral of a function of f(x) over U into a sum of integrals of functions of monomials against monomial densities. Atiyah uses it to divide distributions, Bernstein and Gelfand, independently, for the meromorphic continuation of $\int |P|^\lambda \varphi$, and Watanabe for the asymptotics of Bayesian learning [Wat09, Theorem 2.3]. The theorem follows from Bierstone and Milman's principalization with the Jacobian clause [BM97, Theorem 1.10], applied to the ideal sheaf generated by f.

Relation to the source.

• Strengthening. Atiyah states the theorem near a point: for f analytic and not identically zero near 0 ∈ ℝⁿ, his map is over some open neighbourhood of 0. Here π is over the whole of U, for f not identically zero near any point of U, which is his hypothesis on a connected U. The monomial form of the Jacobian determinant is not in his theorem: it is Bierstone and Milman's clause [BM97, the sentence after Theorem 1.10]. His coordinates are centred at the point and the chart coordinates here need not be, which is no weaker: a coordinate that does not vanish at the point contributes a unit.
• Gap. Atiyah's standing convention that manifolds are connected [Ati70, footnote 2] is not asserted for M.

Source statement: [Ati70, Resolution Theorem, p. 147]