Adapted coordinates as generators

On the source of an adapted chart (φ, σ) for Y, the adapted coordinates z_i := ψ_{σ i} ∘ φ — the sections chartSection E ψ φ hφ (σ i) of 𝒪_M over the chart domain — have Y as their common zero set and linearly independent differentials at every point of the domain: the differential of z_i is the coordinate functional π_{σ i} ∘ ψ composed with the derivative of the chart, which is onto (a chart of the maximal atlas has an analytic inverse, so its manifold derivative is invertible: Mathlib's OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, reached through mdifferentiable_of_mem_maximalAtlas), and the coordinate functionals π_{σ i} ∘ ψ are independent (linearIndependent_coordFunctional). So a closed submanifold is locally the common zero set of c sections with independent differentials (IsClosedSubmanifold.exists_generators'), a smooth subspace being "locally a coordinate subspace of a coordinate chart" [BM97, (3.8)(2)]; the converse (generators with independent differentials complete to an adapted chart) is the chart-extension theorem of Hironaka/Manifold/AdaptedChart.lean.

theorem Manifold.mdifferentiable_of_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) : OpenPartialHomeomorph.MDifferentiable (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) φ

A chart of the maximal atlas is a differentiable open partial homeomorphism in Mathlib's sense (OpenPartialHomeomorph.MDifferentiable, whose mfderiv is a continuous linear equivalence, mfderiv_surjective, …). Mathlib's mdifferentiable_of_mem_atlas asks for an IsManifold instance; this is the maximal-atlas form, from Mathlib's contMDiffOn_of_mem_maximalAtlas and contMDiffOn_symm_of_mem_maximalAtlas.

def Manifold.coordFunctional {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (j : Fin n) : E →L[𝕜] 𝕜

The coordinate functional π_j ∘ ψ.

Equations

• Manifold.coordFunctional ψ j = ContinuousLinearMap.proj j ∘SL ↑ψ

theorem Manifold.coordFunctional_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (j : Fin n) (v : E) : (coordFunctional ψ j) v = ψ v j

The coordinate functional π_j ∘ ψ evaluated at v (unfolding lemma).

theorem Manifold.linearIndependent_coordFunctional {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n c : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (σ : Fin c ↪ Fin n) : LinearIndependent 𝕜 fun (i : Fin c) => coordFunctional ψ (σ i)

The coordinate functionals π_{σ i} ∘ ψ, i : Fin c, are linearly independent.

theorem Manifold.IsAdaptedChart.hasIndependentDifferentialsAt {𝕜 : 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} {φ : OpenPartialHomeomorph M E} {c : ℕ} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ Y φ σ) {x : M} (hx : x ∈ φ.source) : HasIndependentDifferentialsAt E (fun (i : Fin c) (y : M) => ψ (↑φ y) (σ i)) x

The adapted coordinates ψ_{σ i} ∘ φ have independent differentials at every point of the chart domain.

theorem Manifold.IsClosedSubmanifold.exists_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 : ℕ} (hY : IsClosedSubmanifold ψ Y c) {a : M} (ha : 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}

A closed submanifold is locally the common zero set of c sections of 𝒪_M with independent differentials — the adapted coordinates of an adapted chart [BM97, (3.8)(2)].