Closed analytic submanifolds: coordinates and the induced manifold structure

For a closed analytic submanifold Y of codimension c (IsClosedSubmanifold ψ Y c, with its adapted charts IsAdaptedChart ψ Y φ σ, on whose source Y = {z_σ = 0} for the coordinates z = ψ ∘ φ), this module provides the coordinate bookkeeping and the manifold structure on Y. The adapted charts are the shape in which the chart-extension theorem (Hironaka/Manifold/AdaptedChart.lean) produces charts (z_i = π_{σ i} ∘ ψ ∘ φ).

• IsClosedSubmanifoldOn ψ U Y c, Y a closed submanifold of the open subset U, phrased in M;
• HasIndependentDifferentialsAt E z a: the differentials d(z_i)(a) are linearly independent (as functionals on the tangent space, through mderivFun);
• the induced structure of a manifold on Y: the chart IsAdaptedChart.chartOn of Y induced by an adapted chart (the complementary coordinates, Fin (n - c) many, through the coordinate splitting embedCompl, projCompl), the charted space IsClosedSubmanifold.chartedSpace (a chosen adapted chart at each point), the stalk IsClosedSubmanifold.stalk hY a of 𝒪_Y, and the specification IsRestrictStalk of the restriction of germs 𝒪_{M,a} →+* 𝒪_{Y,a} (through stalkToGerm, as germs of functions on Y).

The field lives in Type, the manifold in Type u. The manifold structure on Y, the restriction of germs and the ideal sheaf of Y are developed in Hironaka/Manifold/Submanifold/.

noncomputable def Manifold.complEquiv {n c : ℕ} (σ : Fin c ↪ Fin n) : { j : Fin n // j ∉ Set.range ⇑σ } ≃ Fin (n - c)

The coordinates not in the range of σ, indexed by Fin (n - c).

Equations

• Manifold.complEquiv σ = Fintype.equivFinOfCardEq ⋯

noncomputable def Manifold.embedCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (w : Fin (n - c) → 𝕜) : Fin n → 𝕜

𝕜^{n-c} embedded as the coordinate subspace {y | ∀ i, y (σ i) = 0}.

Equations

• Manifold.embedCompl σ w j = if h : j ∈ Set.range ⇑σ then 0 else w ((Manifold.complEquiv σ) ⟨j, h⟩)

noncomputable def Manifold.projCompl {𝕜 : Type} {n c : ℕ} (σ : Fin c ↪ Fin n) (y : Fin n → 𝕜) : Fin (n - c) → 𝕜

The coordinates outside the range of σ.

Equations

• Manifold.projCompl σ y k = y ↑((Manifold.complEquiv σ).symm k)

theorem Manifold.embedCompl_apply_range {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (w : Fin (n - c) → 𝕜) (i : Fin c) : embedCompl σ w (σ i) = 0

The embedded vector vanishes on the range of σ.

theorem Manifold.projCompl_embedCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (w : Fin (n - c) → 𝕜) : projCompl σ (embedCompl σ w) = w

Projecting the embedding of w gives back w.

theorem Manifold.embedCompl_projCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {y : Fin n → 𝕜} (hy : ∀ (i : Fin c), y (σ i) = 0) : embedCompl σ (projCompl σ y) = y

Embedding the projection of y gives back y when y vanishes on the range of σ.

theorem Manifold.continuous_embedCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : Continuous (embedCompl σ)

The embedding embedCompl σ is continuous.

theorem Manifold.continuous_projCompl {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : Continuous (projCompl σ)

The projection projCompl σ is continuous.

def Manifold.IsClosedSubmanifoldOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (U Y : Set M) (c : ℕ) : Prop

Y is a closed submanifold of the open subset U: Y ∩ U is closed in U and every point of Y ∩ U lies in the source of an adapted chart whose source is inside U.

Equations

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

noncomputable def Manifold.mderivFun {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (z : M → 𝕜) (a : M) : TangentSpace (modelWithCornersSelf 𝕜 E) a →L[𝕜] 𝕜

The manifold derivative of a function M → 𝕜 at a, as a functional on the tangent space (the codomain TangentSpace 𝓘(𝕜) (z a) is 𝕜 by definition; this form makes a family of derivatives non-dependent).

Equations

• Manifold.mderivFun E z a = mfderiv% z a

def Manifold.HasIndependentDifferentialsAt {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {c : ℕ} (z : Fin c → M → 𝕜) (a : M) : Prop

The differentials of z_1, …, z_c at a are linearly independent.

Equations

• Manifold.HasIndependentDifferentialsAt E z a = LinearIndependent 𝕜 fun (i : Fin c) => Manifold.mderivFun E (z i) a

noncomputable def Manifold.IsAdaptedChart.symmAux {𝕜 : 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 φ σ) {a : M} (ha : a ∈ Y) (w : Fin (n - c) → 𝕜) : ↑Y

The inverse of the induced chart (junk value a off the target).

Equations

• h.symmAux ha w = if hw : ψ.symm (Manifold.embedCompl σ w) ∈ φ.target then ⟨↑φ.symm (ψ.symm (Manifold.embedCompl σ w)), ⋯⟩ else ⟨a, ha⟩

theorem Manifold.IsAdaptedChart.coe_symmAux {𝕜 : 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 φ σ) {a : M} (ha : a ∈ Y) {w : Fin (n - c) → 𝕜} (hw : ψ.symm (embedCompl σ w) ∈ φ.target) : ↑(h.symmAux ha w) = ↑φ.symm (ψ.symm (embedCompl σ w))

The inverse of the induced chart on the target.

theorem Manifold.IsAdaptedChart.mem_target_of_mem_source {𝕜 : 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 : ↑Y} (hx : ↑x ∈ φ.source) : ψ.symm (embedCompl σ (projCompl σ (ψ (↑φ ↑x)))) ∈ φ.target

The induced chart maps its source into its target.

noncomputable def Manifold.IsAdaptedChart.chartOn {𝕜 : 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 φ σ) {a : M} (ha : a ∈ Y) : OpenPartialHomeomorph (↑Y) (Fin (n - c) → 𝕜)

The chart of Y induced by an adapted chart: the complementary coordinates.

Equations

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

theorem Manifold.IsAdaptedChart.chartOn_apply {𝕜 : 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 φ σ) {a : M} (ha : a ∈ Y) (x : ↑Y) : ↑(h.chartOn ha) x = projCompl σ (ψ (↑φ ↑x))

The induced chart of Y is the adapted chart followed by the projection onto the coordinates outside σ (rfl).

theorem Manifold.IsAdaptedChart.chartOn_symm_apply {𝕜 : 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 φ σ) {a : M} (ha : a ∈ Y) (w : Fin (n - c) → 𝕜) : ↑(h.chartOn ha).symm w = h.symmAux ha w

The inverse of the induced chart is symmAux, the inverse adapted chart on the coordinate subspace {z_σ = 0}, with the junk value a off the target (rfl).

theorem Manifold.IsAdaptedChart.chartOn_source {𝕜 : 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 φ σ) {a : M} (ha : a ∈ Y) : (h.chartOn ha).source = {x : ↑Y | ↑x ∈ φ.source}

The source of the induced chart is the trace of the adapted chart's source on Y (rfl).

theorem Manifold.IsAdaptedChart.chartOn_target {𝕜 : 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 φ σ) {a : M} (ha : a ∈ Y) : (h.chartOn ha).target = {w : Fin (n - c) → 𝕜 | ψ.symm (embedCompl σ w) ∈ φ.target}

The target of the induced chart is the set of w ∈ 𝕜^{n-c} whose embedding into {z_σ = 0} lies in the adapted chart's target (rfl).

noncomputable def Manifold.IsClosedSubmanifold.adaptedChartAt {𝕜 : 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) (x : ↑Y) : OpenPartialHomeomorph M E

A chosen adapted chart at each point of a closed submanifold.

Equations

• hY.adaptedChartAt x = ⋯.choose

noncomputable def Manifold.IsClosedSubmanifold.adaptedIdx {𝕜 : 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) (x : ↑Y) : Fin c ↪ Fin n

The index set of the chosen adapted chart.

Equations

• hY.adaptedIdx x = ⋯.choose

theorem Manifold.IsClosedSubmanifold.mem_source_adaptedChartAt {𝕜 : 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) (x : ↑Y) : ↑x ∈ (hY.adaptedChartAt x).source

The chosen adapted chart contains its point.

theorem Manifold.IsClosedSubmanifold.isAdaptedChart_adaptedChartAt {𝕜 : 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) (x : ↑Y) : IsAdaptedChart ψ Y (hY.adaptedChartAt x) (hY.adaptedIdx x)

The chosen chart is adapted.

@[instance_reducible]

noncomputable def Manifold.IsClosedSubmanifold.chartedSpace {𝕜 : 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) : ChartedSpace (Fin (n - c) → 𝕜) ↑Y

The charted space structure of a closed submanifold, modelled on 𝕜^{n-c}.

Equations

• hY.chartedSpace = { atlas := Set.range fun (x : ↑Y) => ⋯.chartOn ⋯, chartAt := fun (x : ↑Y) => ⋯.chartOn ⋯, mem_chart_source := ⋯, chart_mem_atlas := ⋯ }

@[reducible, inline]

abbrev Manifold.IsClosedSubmanifold.stalk {𝕜 : 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 : ↑Y) : Type u

The stalk of 𝒪_Y at a, for the induced charted structure.

Equations

• hY.stalk a = ↑((Manifold.structureSheaf 𝕜 (Fin (n - c) → 𝕜) ↑Y).presheaf.stalk a)

def Manifold.IsClosedSubmanifold.IsRestrictStalk {𝕜 : 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 : ↑Y) (r : ↑((structureSheaf 𝕜 E M).presheaf.stalk ↑a) →+* hY.stalk a) : Prop

The specification of the restriction of germs to Y: a ring homomorphism r : 𝒪_{M,a} →+* 𝒪_{Y,a} is the restriction when it sends the germ of every section f of 𝒪_M to the germ of f|_Y (read as germs of functions on Y through stalkToGerm).

Equations

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