The adapted chart at a point of a local model

The analytic half of Hironaka's "by means of jacobian criterion and the implicit function theorem" [Hir64, Ch. 0, §1, p. 121], set up: at a point z of the local model X = V(f₁, …, f_k) ⊆ G ⊆ Kⁿ whose ideal 𝓘_z = (f)_z is generated by c germs with independent differentials, those germs are represented by sections hs on an open U ⊆ G, the analytic inverse function theorem (exists_chart_extending, Hironaka/Manifold/AdaptedChart.lean) completes them to a chart e of the maximal atlas at z with hs i = (e ·)_{σ i} on e.source, and the propagation lemma exists_forall_germ_mem_span (Hironaka/AnalyticSpace/Propagation.lean) gives a neighbourhood W of z on which (f)_y = (hs)_y for every y. The data is packaged as ModelChartData; its consequences — on W, the support of X is the zero set {(e ·)_σ = 0} of the adapted coordinates, and the hs have independent differentials at every point of e.source — feed the K-isomorphism X|V ≅ (G', 𝒜_{G'}) of Hironaka/AnalyticSpace/ModelIso.lean.

• exists_chart_extending_affine — the chart statement on Kⁿ;
• ModelChartData, exists_modelChartData — the data at z from the hypotheses;
• ModelChartData.eval_eq_zero_iff, ModelChartData.hasIndependentDifferentialsAt.

theorem AnalyticSpace.exists_chart_extending_affine (K : Type) [RCLike K] (n : ℕ) {c : ℕ} (z : Fin c → Kn K n → K) (q : Kn K n) (hz : ∀ (i : Fin c), ContMDiffAt (modelWithCornersSelf K (Kn K n)) (modelWithCornersSelf K K) ⊤ (z i) q) (hz0 : ∀ (i : Fin c), z i q = 0) (hind : Manifold.HasIndependentDifferentialsAt (Kn K n) z q) : ∃ (e : OpenPartialHomeomorph (Kn K n) (Kn K n)) (σ : Fin c ↪ Fin n), e ∈ IsManifold.maximalAtlas (modelWithCornersSelf K (Kn K n)) ⊤ (Kn K n) ∧ q ∈ e.source ∧ ↑e q = 0 ∧ ∀ y ∈ e.source, ∀ (i : Fin c), z i y = (↑e y).down (σ i)

Analytic functions z₁, …, z_c on Kⁿ vanishing at q with independent differentials are the coordinates σ 1, …, σ c of a chart e of the maximal atlas at q with e q = 0 (exists_chart_extending on Kⁿ).

structure AnalyticSpace.ModelChartData {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) (c : ℕ) : Type u

The local data of Hironaka's implicit-function-theorem step [Hir64, Ch. 0, §1, p. 121] at a point z of the local model V(f) ⊆ G: sections hs on U ⊆ G generating the ideal (f) at every point of a neighbourhood W ∋ z, and a chart e of the maximal atlas on e.source ⊇ W whose coordinates σ i are the hs i.

• U : TopologicalSpace.Opens (Kn K n)

  The domain of the sections.

• hU : self.U ≤ G
• hs : Fin c → AnalyticFun K n self.U

  The sections representing the generators.

• e : OpenPartialHomeomorph (Kn K n) (Kn K n)

  The adapted chart.

• he : self.e ∈ IsManifold.maximalAtlas (modelWithCornersSelf K (Kn K n)) ⊤ (Kn K n)
• σ : Fin c ↪ Fin n

  The adapted coordinates.

• W : TopologicalSpace.Opens (Kn K n)

  The good neighbourhood of z.

• hzW : ↑↑z ∈ self.W
• hWU : self.W ≤ self.U
• hWe : ↑self.W ⊆ self.e.source
• hcoord (y : Kn K n) : y ∈ self.e.source → ∀ (i : Fin c), Manifold.extendSection K (Kn K n) (self.hs i) y = (↑self.e y).down (self.σ i)
• hideal (y : Kn K n) (hy : y ∈ self.W) : Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G y ⋯)) (f j)) = Ideal.span (Set.range fun (i : Fin c) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ self.U y ⋯)) (self.hs i))

theorem AnalyticSpace.germ_mem_maximalIdeal_of_mem_cosupport {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) (j : Fin k) : (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f j) ∈ IsLocalRing.maximalIdeal ↑((affine K n).presheaf.stalk ↑↑z)

A point of the support of the local model has all f j vanishing there, so the germs of the f j lie in the maximal ideal.

theorem AnalyticSpace.exists_modelChartData {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) {c : ℕ} (h : Fin c → ↑((affine K n).presheaf.stalk ↑↑z)) (hgen : Ideal.span (Set.range fun (i : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f i)) = Ideal.span (Set.range h)) (hind : LinearIndependent K fun (i : Fin c) => (dlin K n ↑↑z) (h i)) : Nonempty (ModelChartData G f z c)

From the hypotheses of the Jacobian criterion's geometric conclusion — 𝓘_z = (h) in 𝒜_{Kⁿ,z} with h of independent differentials — the chart data at z.

theorem AnalyticSpace.ModelChartData.eval_eq_zero_iff {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {y : Kn K n} (hy : y ∈ D.W) : (∀ (j : Fin k), (f j).eval ⟨y, ⋯⟩ = 0) ↔ ∀ (i : Fin c), (↑D.e y).down (D.σ i) = 0

On the good neighbourhood W, a point lies in the support of the local model (all f j vanish) iff the adapted coordinates (e ·)_{σ i} vanish: the support is the coordinate subspace of the chart.

theorem AnalyticSpace.ModelChartData.hasIndependentDifferentialsAt {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {k : ℕ} {f : Fin k → AnalyticFun K n G} {z : ↑↑(localModel K n G f).toPresheafedSpace} {c : ℕ} (D : ModelChartData G f z c) {y : Kn K n} (hy : y ∈ D.e.source) : Manifold.HasIndependentDifferentialsAt (Kn K n) (fun (i : Fin c) => Manifold.extendSection K (Kn K n) (D.hs i)) y

The adapted coordinates have independent differentials at every point of the chart domain (Hironaka/Manifold/Submanifold/Generators.lean), hence so do the sections hs, which agree with them on e.source.