A closed submanifold as a bundled analytic manifold; restriction of analytic maps

The restriction of a blow-up sequence of X to a closed subscheme S ⊆ X is a blow-up sequence starting with S [Kol07, Definition 30.2]. A finite succession (FiniteSuccession) starts with a bundled AnalyticManifold 𝕜 E, so a closed submanifold S ⊆ M of codimension s (IsClosedSubmanifold ψ S s) has to be bundled with its induced structure: the charts are the complementary coordinates of the adapted charts (IsAdaptedChart.chartOn), modelled on 𝕜^{n-s} (IsClosedSubmanifold.chartedSpace, IsClosedSubmanifold.isManifold'), and the space is Hausdorff and second countable as a subspace of M. That a smooth closed subspace of a manifold is a manifold, locally a coordinate subspace, is [BM97, (3.8)(2)]. This module provides

• IsClosedSubmanifold.toAnalyticManifold hS : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜);
• IsClosedSubmanifold.contMDiff_codRestrict: an analytic map into M with values in S is analytic into S for the induced charts (in the induced chart at the image point it is projCompl σ ∘ ψ ∘ φ ∘ f, a composition of analytic maps; contMDiffAt_iff_target);
• IsClosedSubmanifold.restrictMap: the restriction S' → S of an analytic map f : M' → M with f(S') ⊆ S between closed submanifolds of the same codimension s in manifolds modelled on E, as a bundled analytic map between the bundled submanifolds (the inclusion S' → M' is analytic, IsClosedSubmanifold.contMDiff_val); the restricted blow-downs π_i|_{S_{i+1}} : S_{i+1} → S_i of a restricted blow-up sequence are its instances;
• IsClosedSubmanifold.congr_chart: the notion of closed submanifold does not depend on the linear chart ψ : E ≃ 𝕜ⁿ (a succession carries one chosen chart per step, FiniteSuccession.chartAt): an adapted chart for ψ becomes one for ψ' after the linear change ψ'⁻¹ ∘ ψ of E, with the same coordinate functions.

The bundle

noncomputable def Manifold.IsClosedSubmanifold.toAnalyticManifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {s : ℕ} [T2Space M] [SecondCountableTopology M] (hS : IsClosedSubmanifold ψ S s) : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)

A closed submanifold S ⊆ M of codimension s as a bundled analytic manifold modelled on 𝕜^{n-s}, with the induced charts (IsClosedSubmanifold.chartedSpace, IsClosedSubmanifold.isManifold'); Hausdorff and second countable as a subspace of M. It is the manifold with which the restriction of a blow-up sequence to S starts [Kol07, Definition 30.2].

Equations

• hS.toAnalyticManifold = { carrier := ↑S, top := instTopologicalSpaceSubtype, charted := hS.chartedSpace, manifold := ⋯, t2 := ⋯, secondCountable := ⋯ }

def Manifold.IsClosedSubmanifold.preimageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {s : ℕ} [T2Space M] [SecondCountableTopology M] (hS : IsClosedSubmanifold ψ S s) (Y : Set M) : Set hS.toAnalyticManifold.carrier

A subset Y ⊆ M read inside the bundled submanifold S: the preimage of Y under the inclusion S → M (Kollár's restricted centre Z_i ∩ S_i, a subset of S_i [Kol07, Definition 30.2]).

Equations

• hS.preimageVal Y = {p : hS.toAnalyticManifold.carrier | ↑p ∈ Y}

theorem Manifold.IsClosedSubmanifold.mem_preimageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {s : ℕ} [T2Space M] [SecondCountableTopology M] (hS : IsClosedSubmanifold ψ S s) (Y : Set M) (p : hS.toAnalyticManifold.carrier) : p ∈ hS.preimageVal Y ↔ ↑p ∈ Y

Restriction of analytic maps to closed submanifolds

theorem Manifold.IsClosedSubmanifold.contMDiff_codRestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {s : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {N : Type u} [TopologicalSpace N] [ChartedSpace F N] (hS : IsClosedSubmanifold ψ S s) {f : N → M} (hf : ContMDiff (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 E) ⊤ f) (hfS : ∀ (x : N), f x ∈ S) : ContMDiff (modelWithCornersSelf 𝕜 F) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ (Set.codRestrict f S hfS)

An analytic map into M with values in the closed submanifold S is analytic into S for the induced charts: in the induced chart at the image point it reads projCompl σ ∘ ψ ∘ φ ∘ f.

def Manifold.IsClosedSubmanifold.restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {S' : Set M'} [T2Space M] [SecondCountableTopology M] [T2Space M'] [SecondCountableTopology M'] (hS' : IsClosedSubmanifold ψ S' s) (hS : IsClosedSubmanifold ψ S s) (f : M' → M) (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) (hfS : ∀ x ∈ S', f x ∈ S) : AnalyticMap hS'.toAnalyticManifold hS.toAnalyticManifold

The restriction of an analytic map f : M' → M with f(S') ⊆ S to closed submanifolds of the same codimension, as a bundled analytic map between the bundled submanifolds. The blow-downs π_i^S : S_{i+1} → S_i of a restricted blow-up sequence [Kol07, Definition 30.2] are of this form.

Equations

• hS'.restrictMap hS f hf hfS = ⟨Set.codRestrict (f ∘ Subtype.val) S ⋯, ⋯⟩

theorem Manifold.IsClosedSubmanifold.restrictMap_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S : Set M} {s : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {S' : Set M'} [T2Space M] [SecondCountableTopology M] [T2Space M'] [SecondCountableTopology M'] (hS' : IsClosedSubmanifold ψ S' s) (hS : IsClosedSubmanifold ψ S s) (f : M' → M) (hf : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ f) (hfS : ∀ x ∈ S', f x ∈ S) (p : hS'.toAnalyticManifold.carrier) : ↑((hS'.restrictMap hS f hf hfS) p) = f ↑p

The restricted map is the restriction: its values in M are those of f (rfl).

Independence of the chart ψ

theorem Manifold.IsAdaptedChart.exists_congr_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c n' : ℕ} (ψ' : E ≃L[𝕜] Fin n' → 𝕜) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ Y φ σ) : ∃ (φ' : OpenPartialHomeomorph M E) (σ' : Fin c ↪ Fin n'), φ'.source = φ.source ∧ IsAdaptedChart ψ' Y φ' σ' ∧ ∀ x ∈ φ.source, ∀ (i : Fin c), ψ' (↑φ' x) (σ' i) = ψ (↑φ x) (σ i)

An adapted chart for ψ becomes an adapted chart for ψ' (the same source, the same coordinate functions) after the linear change of E carrying ψ to ψ'.

theorem Manifold.IsClosedSubmanifold.congr_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c n' : ℕ} (ψ' : E ≃L[𝕜] Fin n' → 𝕜) (hY : IsClosedSubmanifold ψ Y c) : IsClosedSubmanifold ψ' Y c

The notion "closed submanifold of codimension c" does not depend on the linear chart ψ : E ≃ 𝕜ⁿ (a succession carries one chosen chart per step). Not in the sources; a routine change of charts.