/-
Copyright (c) 2026 Resolution. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Billy Snikkers (Resolution): drafted with Claude Opus 5.5
-/
module

public import Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
public import Mathlib.AlgebraicGeometry.Morphisms.Proper
public import Mathlib.AlgebraicGeometry.Morphisms.Smooth
public import Mathlib.AlgebraicGeometry.Restrict
public import Mathlib.Analysis.InnerProductSpace.PiL2
public import Mathlib.Analysis.Analytic.Basic
public import Mathlib.Analysis.Calculus.FDeriv.Basic
public import Mathlib.Geometry.Manifold.ContMDiff.Defs
public import Mathlib.Geometry.Manifold.Instances.Real
public import Mathlib.Geometry.Manifold.LocalDiffeomorph
public import Mathlib.Topology.Algebra.Module.Determinant
public import Mathlib.Topology.Maps.Proper.Basic

/-!
# Resolution of a variety and monomialization of an analytic function, in Mathlib's terms

Two theorems stated with Mathlib's definitions alone, together with three that Mathlib lacks,
defined from Mathlib's just before the theorem that uses them: effective Cartier ideal sheaves
(`AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier`) and blow-ups given by their
universal property (`AlgebraicGeometry.Scheme.Hom.IsBlowUpAlong`) for the first, and functions that
are monomials in a chart up to a unit (`IsMonomialAt`) for the second.

* **Resolution of a variety by a single blow-up** (`AlgebraicGeometry.exists_isBlowUpAlong_smooth`):
  an integral scheme `X`, separated and of finite type over a field `k` of characteristic zero, has
  a blow-up `π : X' → X` along an ideal sheaf supported exactly on the singular locus of `X`, the
  complement of its smooth locus, with `X'` smooth over `k`; `π` is proper and an isomorphism over
  the smooth locus. Smooth and proper are Mathlib's `Smooth` and `IsProper`, the smooth locus is
  `Scheme.Hom.smoothLocus`, ideal sheaves and their supports are Mathlib's `Scheme.IdealSheafData`
  and `Scheme.IdealSheafData.support`, and `π ∣_ V : π⁻¹(V) ⟶ V` is the restriction of `π` over an
  open `V`.
* **Local monomialization of a real-analytic function**
  (`exists_proper_analytic_monomialization`): for a real-analytic function `f` on an open set
  `U ⊆ ℝⁿ`, not identically zero near any point, there is a proper analytic map `π : M → U` from a
  real-analytic manifold, an analytic isomorphism over `{f ≠ 0}`, such that near every point of
  `M`, in the coordinates of the chart at that point, `f ∘ π` and the Jacobian determinant of `π`
  are units times monomials. An analytic manifold is a type with Mathlib's `ChartedSpace` structure
  modelled on `ℝⁿ` and analytic chart changes (`IsManifold (𝓡 n) ω`, `𝓡 n` Mathlib's model of
  `ℝⁿ`), and the coordinates of a point `q` in the chart at `p` are `extChartAt (𝓡 n) p q`.
-/

@[expose] public section

universe u

open AlgebraicGeometry CategoryTheory Filter Topology
open scoped Manifold ContDiff

/-! ### Resolution of a variety -/

namespace AlgebraicGeometry

/-- An ideal sheaf `J` on `X` is *effective Cartier*, the ideal sheaf of an effective Cartier
divisor, if near every point it is generated by a single non-zero-divisor: every point `x` has an
affine open neighbourhood `U` and a non-zero-divisor `g ∈ Γ(X, U)` with `J(U) = (g)`. Equivalently,
`J` is an invertible sheaf (locally free of rank one), the Stacks project's definition of an
effective Cartier divisor [Sta, Tag 01WR]; [Sta, Tag 01WS]. -/
def Scheme.IdealSheafData.IsEffectiveCartier {X : Scheme.{u}} (J : X.IdealSheafData) : Prop :=
  ∀ x : X, ∃ U : X.affineOpens, x ∈ U.1 ∧
    ∃ g ∈ nonZeroDivisors Γ(X, U), J.ideal U = Ideal.span {g}

/-- A morphism `π : B ⟶ X` is a *blow-up of `X` along the ideal sheaf `I`* if the inverse image of
the centre is an effective Cartier divisor (the inverse image `I.comap π` of `I` on `B` is effective
Cartier), and every morphism `f : Y ⟶ X` along which the inverse image of the centre is an
effective Cartier divisor (`I.comap f` is effective Cartier) factors as `f = g ≫ π` for a unique
`g : Y ⟶ B` [Sta, Tag 0806]. In other words `π` is final among the morphisms to `X` along which
the closed subscheme of `I` pulls back to an effective Cartier divisor, so it is unique up to unique
isomorphism over `X`.

Relation to the source.
* **Restatement.** The Stacks project defines the blow-up of `X` along `I` as the relative Proj of
  the Rees algebra $\bigoplus_n I^n$ and proves that it has this universal property
  [Sta, Tag 0806]; Hauser takes the universal property as the definition, for a variety and a
  closed subvariety [Hau14, Definition 4.4]. Here, as in the Stacks project, `X` is any scheme, the
  centre is any closed subscheme, given by its ideal sheaf `I`, and the test morphisms `f` come
  from all schemes `Y`. -/
def Scheme.Hom.IsBlowUpAlong {X B : Scheme.{u}} (π : B ⟶ X) (I : X.IdealSheafData) : Prop :=
  (I.comap π).IsEffectiveCartier ∧
    ∀ {Y : Scheme.{u}} (f : Y ⟶ X), (I.comap f).IsEffectiveCartier → ∃! g : Y ⟶ B, g ≫ π = f

/-- **Resolution of singularities** [Hir64, Main Theorem I, p. 132]. Every integral scheme `X`,
separated and of finite type over a field `k` of characteristic zero, is resolved by a single
blow-up: there is a blow-up `π : X' → X` along an ideal sheaf supported exactly on the singular
locus of `X`, with `X'` smooth over `k`. In particular `π` is proper and an isomorphism over the
smooth locus.

Relation to the source.
* **Translation.** Hironaka's "non-singular" (every local ring regular) is read as smooth over `k`,
  `Smooth (π ≫ f)`, and his singular locus as the complement of the smooth locus `f.smoothLocus`:
  for schemes locally of finite type over a field of characteristic zero the two notions agree
  [Sta, Tag 00TV].
* **Interpretation.** Hironaka's "say reduced and irreducible" is read as the hypothesis
  `IsIntegral X`. -/
theorem exists_isBlowUpAlong_smooth {k : Type u} [Field k] [CharZero k]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] [QuasiCompact f]
    [IsSeparated f] [IsIntegral X] :
    ∃ (X' : Scheme.{u}) (π : X' ⟶ X) (I : X.IdealSheafData),
      -- `π` is a blow-up of `X` along `I`
      π.IsBlowUpAlong I ∧
      -- the centre `I` is supported exactly on the singular locus of `X`
      (I.support : Set X) = (f.smoothLocus : Set X)ᶜ ∧
      -- `X'` is smooth over `k`
      Smooth (π ≫ f) ∧
      -- `π` is proper
      IsProper π ∧
      -- `π⁻¹(X_sm) → X_sm` is an isomorphism, `X_sm` the smooth locus of `X` over `k`
      IsIso (π ∣_ f.smoothLocus) :=
  sorry

end AlgebraicGeometry

/-! ### Local monomialization of a real-analytic function -/

/-- A real function `g` on an `n`-dimensional manifold `M` is *a monomial at `p`, up to a unit*,
if near `p`, in the coordinates `y` of the chart of `M` at `p`, `g = u · y^α` for an exponent
vector `α` and a real-analytic function `u` that does not vanish at `p`. -/
def IsMonomialAt (n : ℕ) {M : Type*} [TopologicalSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (g : M → ℝ) (p : M) : Prop :=
  ∃ (α : Fin n → ℕ) (u : M → ℝ), ContMDiffAt (𝓡 n) 𝓘(ℝ) ω u p ∧ u p ≠ 0 ∧
    ∀ᶠ q in 𝓝 p, g q = u q * ∏ i, extChartAt (𝓡 n) p q i ^ α i

/-- **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][Ati70] uses it to divide distributions, [Bernstein
and Gelfand][BG69], 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`. -/
theorem exists_proper_analytic_monomialization {n : ℕ}
    (U : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n)))
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : AnalyticOnNhd ℝ f U)
    (hf₀ : ∀ x ∈ U, ∃ᶠ y in 𝓝 x, f y ≠ 0) :
    ∃ (M : Type u) (_ : TopologicalSpace M) (_ : ChartedSpace (EuclideanSpace ℝ (Fin n)) M)
      (π : M → U),
      -- `M` is an `n`-dimensional real-analytic manifold, Hausdorff and second countable
      IsManifold (𝓡 n) ω M ∧ T2Space M ∧ SecondCountableTopology M ∧
      -- `π` is real-analytic and proper
      ContMDiff (𝓡 n) (𝓡 n) ω π ∧
      IsProperMap π ∧
      -- `π` is an analytic isomorphism over the points where `f` does not vanish
      IsLocalDiffeomorphOn (𝓡 n) (𝓡 n) ω π (π ⁻¹' {x | f x ≠ 0}) ∧
      Set.BijOn π (π ⁻¹' {x | f x ≠ 0}) {x | f x ≠ 0} ∧
      -- near every point `p`, in the coordinates of the chart at `p`, `f ∘ π` and the Jacobian
      -- determinant of `π` are monomials up to a unit
      ∀ p : M,
        IsMonomialAt n (fun q => f (π q)) p ∧
        IsMonomialAt n (fun q =>
          (fderiv ℝ ((↑) ∘ π ∘ (extChartAt (𝓡 n) p).symm) (extChartAt (𝓡 n) p q)).det) p :=
  sorry

end