Consequences of the chart-extension theorem: adapted charts and order one

The chart-extension theorem exists_chart_extending of Hironaka/Manifold/AdaptedChart.lean (analytic functions vanishing at a with independent differentials are coordinates of a chart centred at a) has the following consequences for adapted charts and for sections of order one:

• the chart it produces is an adapted chart for the common zero set of the z_i on its source (exists_adaptedChart_zeroSet', through isAdaptedChart_zeroSet');
• a section h of 𝒪_M has order one at a iff h(a) = 0 and dh(a) ≠ 0 (ord_eq_one_iff_fderiv_ne_zero'): the chart form of Hironaka/Manifold/Chart/Order.lean (some ∂_i h(a) ≠ 0) is translated through the chain rule mfderiv_eq_fderiv_comp_chart and the invertibility of the chart's derivative — dh(a) vanishes iff all its values on the basis ψ⁻¹(e_i) vanish;
• the order-one form (Kollár's construction of hypersurfaces of maximal contact, [Kol07, Theorem 80 (2)] and its proof: a local section of order one at x has a smooth zero divisor near x): a section of order one at a is a coordinate of a chart centred at a, and its zero set is on that chart's source a closed smooth hypersurface with that chart as adapted chart (exists_adapted_chart_of_ord_eq_one'; IsClosedSubmanifoldOn through IsAdaptedChart.isClosedSubmanifoldOn').

The third point is the analytic implicit function theorem in the form the maximal-contact construction uses (Hironaka/Manifold/Chart/MaximalContact.lean); the sources take it for granted ("by the implicit function theorem, z = 0 defines a regular submanifold" [BM97, §1]; [Hir64, p. 121]).

theorem Manifold.exists_adaptedChart_zeroSet' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {c : ℕ} (z : Fin c → M → 𝕜) (a : M) (hz : ∀ (i : Fin c), ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ (z i) a) (hz0 : ∀ (i : Fin c), z i a = 0) (hind : HasIndependentDifferentialsAt E z a) : ∃ (e : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n), e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M ∧ a ∈ e.source ∧ ↑e a = 0 ∧ IsAdaptedChart ψ (e.source ∩ {x : M | ∀ (i : Fin c), z i x = 0}) e σ ∧ ∀ x ∈ e.source, ∀ (i : Fin c), z i x = ψ (↑e x) (σ i)

The chart of exists_chart_extending is an adapted chart for the common zero set of the z_i on its source.

theorem Manifold.eval_coordDerivStalk_germ {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {U : TopologicalSpace.Opens M} (haU : a ∈ U) (h : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) (i : Fin n) : (eval 𝕜 E M a) ((coordDerivStalk E ψ φ hφ ha i) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a haU)) h)) = (fderiv 𝕜 (extendSection 𝕜 E h ∘ ↑φ.symm) (↑φ a)) (ψ.symm (Pi.single i 1))

The value at a of ∂_i of the germ of a section is the derivative of the section read in the chart, in the direction ψ⁻¹(e_i) (coordDeriv_apply).

theorem Manifold.ord_eq_one_iff_fderiv_ne_zero' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [FiniteDimensional 𝕜 E] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {U : TopologicalSpace.Opens M} {a : M} (ha : a ∈ U) (h : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a ha)) h) = 1 ↔ extendSection 𝕜 E h a = 0 ∧ mderivFun E (extendSection 𝕜 E h) a ≠ 0

A section h of 𝒪_M has order one at a iff h(a) = 0 and dh(a) ≠ 0 (the criterion Kollár uses in the proof of [Kol07, Theorem 80]).

theorem Manifold.exists_adapted_chart_of_ord_eq_one' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {U : TopologicalSpace.Opens M} {a : M} (ha : a ∈ U) (h : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) (hord : IsLocalRing.ordElem ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a ha)) h) = 1) : ∃ (e : OpenPartialHomeomorph M E) (σ : Fin 1 ↪ Fin n), e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M ∧ a ∈ e.source ∧ e.source ⊆ ↑U ∧ ↑e a = 0 ∧ (∀ x ∈ e.source, extendSection 𝕜 E h x = ψ (↑e x) (σ 0)) ∧ IsAdaptedChart ψ (e.source ∩ {x : M | extendSection 𝕜 E h x = 0}) e σ ∧ IsClosedSubmanifoldOn ψ e.source (e.source ∩ {x : M | extendSection 𝕜 E h x = 0}) 1

The order-one form of the chart-extension theorem ([Kol07, Theorem 80 (2)] and its proof): a section h of 𝒪_M with ord_a h = 1 is the σ 0-th coordinate of a chart e centred at a with source inside the domain of h, and H = (h = 0) is, on the source of e, a closed smooth hypersurface with e as adapted chart and a closed submanifold of codimension one of that source.