Adapted charts from generators

A closed subset Y of an analytic manifold M which is, near each of its points, the common zero set of c analytic functions with linearly independent differentials is a closed submanifold of codimension c (isClosedSubmanifold_of_generators; the converse of the description of a closed submanifold by an adapted chart, IsClosedSubmanifold). This is the implicit function theorem as the sources use it: "by the implicit function theorem, z = 0 defines a regular submanifold" [BM97, §1], a smooth space is "locally a coordinate subspace of a coordinate chart" [BM97, (3.8)(2)], and a local section of order 1 has a smooth zero divisor [Kol07, Theorem 80, proof].

The proof completes the generators z_1, …, z_c to a chart at a (exists_chart_extending); no analysis is reproved, the analytic inverse function theorem being Mathlib's ContDiffAt.toOpenPartialHomeomorph at n = ω:

• exists_dual_basis_extension_rclike (linear algebra): linearly independent continuous functionals ℓ_i on a finite-dimensional E sit at positions σ i of a family lam of n = dim E functionals with v ↦ (lam_j v)_j bijective;
• coordExtension, exists_coordExtension: the map Ψ x = ψ⁻¹ (g_i x at σ i, lam_j (x − y) elsewhere), analytic at y with invertible derivative when the dg_i(y) are independent;
• exists_openPartialHomeomorph_mem_contDiffGroupoid: an analytic map with invertible derivative at y restricts to an OpenPartialHomeomorph E E in the analytic groupoid contDiffGroupoid ω 𝓘(𝕜, E) with y in its source;
• trans_mem_maximalAtlas: a chart of the maximal atlas composed with an element of the groupoid is a chart of the maximal atlas; so is its composite with an analytic open partial homeomorphism of E with analytic inverse, and every restriction of that composite to an open set (trans_mem_maximalAtlas_of_analytic', trans_restrOpen_mem_maximalAtlas_of_analytic');
• mfderiv_eq_fderiv_comp_chart, hasIndependentDifferentialsAt_iff_chart: independence of the manifold derivatives is independence of the differentials read in any chart;
• exists_chart_extending: analytic z_i vanishing at a with independent differentials are the coordinates σ i of a chart e of the maximal atlas at a with e a = 0;
• isClosedSubmanifold_of_generators: the statement above, from exists_chart_extending at each a ∈ Y, the chart restricted to the neighbourhood carrying the generators.

The chart-extension theorem is how the zero sets of analytic functions with independent differentials — hypersurfaces of maximal contact, centres — are recognised as closed submanifolds in the Hironaka library (Hironaka/Manifold/Chart/).

Linear algebra: extending independent functionals to a dual basis

theorem Manifold.exists_dual_basis_extension_rclike {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] (hE : Module.finrank 𝕜 E = n) {ι : Type u_2} (ℓ : ι → E →L[𝕜] 𝕜) (hℓ : LinearIndependent 𝕜 ℓ) : ∃ (lam : Fin n → E →L[𝕜] 𝕜) (σ : ι → Fin n), Function.Injective σ ∧ (∀ (i : ι), lam (σ i) = ℓ i) ∧ Function.Bijective ⇑(ContinuousLinearMap.pi lam)

Linearly independent continuous functionals ℓ_i on a finite-dimensional E of dimension n sit at positions σ i in a family lam of n functionals with v ↦ (lam_j v)_j bijective: a basis of the dual extending them (Basis.extend). Not in the sources; linear algebra for exists_coordExtension.

The coordinate extension

noncomputable def Manifold.coordExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin c → Fin n) (g : Fin c → E → 𝕜) (lam : Fin n → E →L[𝕜] 𝕜) (y x : E) : E

The coordinate extension of g_1, …, g_c at y along σ: the map x ↦ ψ⁻¹ (w x) with w x (σ i) = g i x and w x j = lam j (x − y) for j outside the range of σ (Function.extend).

Equations

• Manifold.coordExtension ψ σ g lam y x = ψ.symm (Function.extend σ (fun (i : Fin c) => g i x) fun (j : Fin n) => (lam j) (x - y))

theorem Manifold.coordExtension_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {σ : Fin c → Fin n} (hσ : Function.Injective σ) (lam : Fin n → E →L[𝕜] 𝕜) {y : E} (g : Fin c → E → 𝕜) (x : E) (i : Fin c) : ψ (coordExtension ψ σ g lam y x) (σ i) = g i x

The σ i-th coordinate of the extension is g i.

theorem Manifold.coordExtension_apply_of_not_mem_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {σ : Fin c → Fin n} (lam : Fin n → E →L[𝕜] 𝕜) {y : E} (g : Fin c → E → 𝕜) (x : E) {j : Fin n} (hj : ¬∃ (i : Fin c), σ i = j) : ψ (coordExtension ψ σ g lam y x) j = (lam j) (x - y)

The coordinates outside the range of σ are the affine forms lam j (x − y).

theorem Manifold.coordExtension_self {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {σ : Fin c → Fin n} (hσ : Function.Injective σ) {g : Fin c → E → 𝕜} (lam : Fin n → E →L[𝕜] 𝕜) {y : E} (hg0 : ∀ (i : Fin c), g i y = 0) : coordExtension ψ σ g lam y y = 0

The extension is centred: Ψ y = 0 when the g i vanish at y.

theorem Manifold.contDiffAt_coordExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {σ : Fin c → Fin n} (hσ : Function.Injective σ) {g : Fin c → E → 𝕜} (lam : Fin n → E →L[𝕜] 𝕜) {y : E} (hg : ∀ (i : Fin c), ContDiffAt 𝕜 ⊤ (g i) y) : ContDiffAt 𝕜 ⊤ (coordExtension ψ σ g lam y) y

The extension is analytic at y when the g i are.

theorem Manifold.hasFDerivAt_coordExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {σ : Fin c → Fin n} (hσ : Function.Injective σ) {g : Fin c → E → 𝕜} (lam : Fin n → E →L[𝕜] 𝕜) {y : E} (hg : ∀ (i : Fin c), DifferentiableAt 𝕜 (g i) y) : HasFDerivAt (coordExtension ψ σ g lam y) (↑ψ.symm ∘SL ContinuousLinearMap.pi (Function.extend σ (fun (i : Fin c) => fderiv 𝕜 (g i) y) lam)) y

The derivative of the extension at y is ψ⁻¹ composed with the family of functionals dg_i(y) at σ i and lam j elsewhere.

theorem Manifold.exists_coordExtension {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {g : Fin c → E → 𝕜} {y : E} (hg : ∀ (i : Fin c), ContDiffAt 𝕜 ⊤ (g i) y) (hind : LinearIndependent 𝕜 fun (i : Fin c) => fderiv 𝕜 (g i) y) : ∃ (σ : Fin c ↪ Fin n) (Ψ : E → E) (L : E ≃L[𝕜] E), ContDiffAt 𝕜 ⊤ Ψ y ∧ HasFDerivAt Ψ (↑L) y ∧ (∀ (x : E) (i : Fin c), ψ (Ψ x) (σ i) = g i x) ∧ ((∀ (i : Fin c), g i y = 0) → Ψ y = 0)

Analytic functions g_1, …, g_c at y with linearly independent differentials extend to a coordinate system at y: an injection σ : Fin c ↪ Fin n and Ψ : E → E, analytic at y with invertible derivative, whose σ i-th coordinate is g i; Ψ y = 0 when the g i vanish at y. The linear-algebra step of completing z = 0 to a coordinate system.

The analytic inverse function theorem, chart-valued

theorem Manifold.exists_openPartialHomeomorph_mem_contDiffGroupoid {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {Ψ : E → E} {y : E} (hΨ : ContDiffAt 𝕜 ⊤ Ψ y) (L : E ≃L[𝕜] E) (hL : HasFDerivAt Ψ (↑L) y) {s : Set E} (hs : IsOpen s) (hy : y ∈ s) : ∃ (e : OpenPartialHomeomorph E E), y ∈ e.source ∧ e.source ⊆ s ∧ Set.EqOn (↑e) Ψ e.source ∧ e ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E)

The analytic inverse function theorem in chart-valued form (Mathlib's ContDiffAt.toOpenPartialHomeomorph at n = ω and ContDiffAt.to_localInverse): a map Ψ : E → E analytic at y with invertible derivative restricts, inside any open s ∋ y, to an open partial homeomorphism e with y ∈ e.source, e = Ψ on its source, lying in the analytic groupoid contDiffGroupoid ω 𝓘(𝕜, E) (analytic with analytic inverse).

Composing a chart with an element of the analytic groupoid

theorem Manifold.trans_mem_maximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {e : OpenPartialHomeomorph E E} (he : e ∈ contDiffGroupoid ⊤ (modelWithCornersSelf 𝕜 E)) : χ.trans e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M

A chart χ of the maximal analytic atlas composed with an element e of the analytic groupoid of the model space is again a chart of the maximal atlas (mem_maximalAtlas_iff: the transition maps with the atlas are e.symm ≫ₕ (χ.symm ≫ₕ e') and (e'.symm ≫ₕ χ) ≫ₕ e).

theorem Manifold.trans_mem_maximalAtlas_of_analytic' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {e₀ : OpenPartialHomeomorph E E} (h : AnalyticOnNhd 𝕜 (↑e₀) e₀.source) (h' : AnalyticOnNhd 𝕜 (↑e₀.symm) e₀.target) : e.trans e₀ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M

The composite of a chart of the maximal atlas with an analytic open partial homeomorphism of E with analytic inverse is a chart of the maximal atlas (trans_mem_maximalAtlas with mem_contDiffGroupoid_omega_of_analytic').

theorem Manifold.trans_restrOpen_mem_maximalAtlas_of_analytic' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {e : OpenPartialHomeomorph M E} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {e₀ : OpenPartialHomeomorph E E} (h : AnalyticOnNhd 𝕜 (↑e₀) e₀.source) (h' : AnalyticOnNhd 𝕜 (↑e₀.symm) e₀.target) (s : Set M) (hs : IsOpen s) : (e.trans e₀).restrOpen s hs ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M

So is each restriction of that composite to an open set (Mathlib's restr_mem_maximalAtlas).

Differentials read in a chart

theorem Manifold.mfderiv_eq_fderiv_comp_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ χ.source) {f : M → 𝕜} (hf : MDiffAt f a) : mfderiv% f a = fderiv 𝕜 (f ∘ ↑χ.symm) (↑χ a) ∘SL mfderiv% ↑χ a

The chain rule: the manifold derivative of f : M → 𝕜 at a is the derivative of f ∘ χ⁻¹ at χ a, read through the chart's derivative.

theorem Manifold.hasIndependentDifferentialsAt_iff_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {χ : OpenPartialHomeomorph M E} (hχ : χ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ χ.source) {c : ℕ} {z : Fin c → M → 𝕜} (hz : ∀ (i : Fin c), MDiffAt (z i) a) : HasIndependentDifferentialsAt E z a ↔ LinearIndependent 𝕜 fun (i : Fin c) => fderiv 𝕜 (z i ∘ ↑χ.symm) (↑χ a)

Independence of the differentials (HasIndependentDifferentialsAt, in terms of mfderiv) is independence of the differentials of the functions read in any chart χ at a: mfderiv is fderiv in the chart composed with the chart's derivative, an isomorphism of the tangent spaces.

The adapted chart

theorem Manifold.exists_chart_extending {𝕜 : 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 ∧ ∀ x ∈ e.source, ∀ (i : Fin c), z i x = ψ (↑e x) (σ i)

Completion of generators to a chart — the implicit function theorem as used in [BM97, §1] ("by the implicit function theorem, z = 0 defines a regular submanifold"), [Kol07, Theorem 80, proof] and [Hir64, p. 121]: analytic functions z_1, …, z_c at a vanishing at a with linearly independent differentials are the coordinates σ 1, …, σ c of a chart e of the maximal analytic atlas at a with e a = 0, i.e. z i = π_{σ i} ∘ ψ ∘ e on the source of e. Proof: read the z i in the chart χ = chartAt E a (hasIndependentDifferentialsAt_iff_chart), extend their differentials to a dual basis and the functions to a coordinate map Ψ at χ a (exists_coordExtension), invert it analytically (exists_openPartialHomeomorph_mem_contDiffGroupoid) and compose (trans_mem_maximalAtlas).

Closed submanifolds from generators

theorem Manifold.isClosedSubmanifold_of_generators {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {Y : Set M} {c : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hY : IsClosed Y) (h : ∀ a ∈ Y, ∃ (U : TopologicalSpace.Opens M) (_ : a ∈ U) (z : Fin c → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))), (∀ x ∈ Y ∩ ↑U, HasIndependentDifferentialsAt E (fun (i : Fin c) => extendSection 𝕜 E (z i)) x) ∧ Y ∩ ↑U = {x : M | x ∈ U ∧ ∀ (i : Fin c), extendSection 𝕜 E (z i) x = 0}) : IsClosedSubmanifold ψ Y c

A closed set Y such that every a ∈ Y has an open neighbourhood U and sections z_1, …, z_c ∈ 𝒪_M(U) with linearly independent differentials at every point of Y ∩ U and Y ∩ U = {z_1 = … = z_c = 0} is a closed submanifold of codimension c ([BM97, (3.8)(2)]; the converse of the description by adapted charts). Proof: at a ∈ Y, exists_chart_extending completes the z i — analytic at a, vanishing at a, independent — to a chart e at a whose coordinates σ i are the z i; the restriction of e to U is adapted to Y, because on U the zero set of the z i is Y.