Analytic manifolds and analytic maps

Hironaka's "non-singular analytic K-space" [Hir64, pp. 119–121] is an analytic manifold AnalyticManifold 𝕜 E: a bundled manifold without boundary modelled on a normed space E over 𝕜, with analytic (C^ω) chart changes, Hausdorff and second countable (Hironaka's spaces are Hausdorff and countable at infinity). Its carrier carries Mathlib's unbundled instances (ChartedSpace, IsManifold 𝓘(𝕜, E) ω, T2Space, SecondCountableTopology), and it coerces to the type of its points.

• Analytic maps AnalyticMap M N are Mathlib's bundled C^ω maps C^ω⟮𝓘(𝕜, E), M; 𝓘(𝕜, E), N⟯.
• AnalyticMap.IsIsoOver f U: f restricts to an analytic isomorphism f⁻¹(U) → U, condition (1) of Bierstone–Milman's blowing-up off its centre [BM88, Definition 4.1].
• An open subset U : Opens M is an analytic manifold M.restrict U (Mathlib's charted-space and IsManifold instances on Opens; Hausdorff and second countable as a subspace), with the analytic inclusion M.inclusion U.
• The disjoint union of a countable family of opens Gᵢ ⊆ Kⁿ is an analytic manifold sigmaOpens G modelled on Kⁿ (ChartedSpace.sigma, IsManifold.sigma).

The definitions are stated over any nontrivially normed field; the blowing-up, the monoidal transformations and the boundary predicates built on them are stated over 𝕜 ∈ {ℝ, ℂ} (RCLike, the fields of Hironaka's real and complex statements), and the main theorems instantiate 𝕜 = ℝ.

structure AnalyticManifold (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Type (max (u + 1) u_2)

A bundled analytic manifold over 𝕜 modelled on E: Hausdorff, second countable, without boundary, with analytic (C^ω) chart changes — for E finite-dimensional, Hironaka's non-singular analytic 𝕜-space [Hir64, pp. 119–121].

• carrier : Type u

  The underlying type of points.

• top : TopologicalSpace self.carrier
• charted : ChartedSpace E self.carrier
• manifold : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ self.carrier
• t2 : T2Space self.carrier
• secondCountable : SecondCountableTopology self.carrier

@[instance_reducible]

instance AnalyticManifold.instCoeSortType {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : CoeSort (AnalyticManifold 𝕜 E) (Type u)

Equations

• AnalyticManifold.instCoeSortType = { coe := AnalyticManifold.carrier }

@[reducible, inline]

abbrev AnalyticMap {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M N : AnalyticManifold 𝕜 E) : Type u

Analytic maps between analytic manifolds: Mathlib's bundled C^ω maps.

Equations

• AnalyticMap M N = ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤

def AnalyticMap.IsIsoOver {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M M' : AnalyticManifold 𝕜 E} (f : AnalyticMap M' M) (U : Set M.carrier) : Prop

f restricts to an analytic isomorphism f⁻¹(U) → U over the open set U: f is a local diffeomorphism on f⁻¹(U) and a bijection f⁻¹(U) → U — condition (1) of Bierstone–Milman's blowing-up [BM88, Definition 4.1], off the centre; the clause "σ is an isomorphism off the cosupport of I" of the principalization theorem.

Equations

• f.IsIsoOver U = (IsLocalDiffeomorphOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑f) (⇑f ⁻¹' U) ∧ Set.BijOn (⇑f) (⇑f ⁻¹' U) U)

noncomputable def AnalyticManifold.restrict {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) : AnalyticManifold 𝕜 E

The open subset U of M as an analytic manifold (Włodarczyk's neighbourhood U ⊃ Z of a compact set and the stages U_i over it, [Wlo09, Theorem 2.0.3 (1)]): Mathlib's charted-space and IsManifold instances on Opens; Hausdorff and second countable as a subspace of M.

Equations

• M.restrict U = { carrier := ↥U, top := instTopologicalSpaceSubtype, charted := U.instChartedSpace, manifold := ⋯, t2 := ⋯, secondCountable := ⋯ }

def AnalyticManifold.inclusion {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) (U : TopologicalSpace.Opens M.carrier) : AnalyticMap (M.restrict U) M

The inclusion U → M of an open subset as an analytic map (Mathlib's contMDiff_subtype_val).

Equations

• M.inclusion U = ⟨Subtype.val, ⋯⟩

noncomputable def AnalyticManifold.sigmaOpens {K : Type} [RCLike K] {n : ℕ} {ι : Type u} [Countable ι] (G : ι → TopologicalSpace.Opens (Fin n → K)) : AnalyticManifold K (Fin n → K)

The disjoint union A := ⊔ᵢ Gᵢ of a countable family of open subsets Gᵢ ⊆ Kⁿ as an analytic manifold modelled on Kⁿ (the ambient X' = ⊔ Uᵢ of the proof of [Kol07, Proposition 37]): the Σ-type with the charts of the summands (ChartedSpace.sigma, IsManifold.sigma), Hausdorff as a disjoint union of Hausdorff spaces and second countable for a countable index.

Equations

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