Charts of a manifold as isomorphisms with open subsets of Kⁿ

A chart φ of an analytic manifold M modelled on E ≃ Kⁿ identifies its domain with an open subset of Kⁿ as K-local-ringed spaces. The pieces:

• two mutually inverse analytic maps induce a K-isomorphism of the spaces of the manifolds (ofManifoldIso, by the functoriality of ofManifoldHom);
• the chart φ, followed by the coordinates ψ : E ≃L[K] Kⁿ (lifted to Kn K n), is an analytic bijection φ.source ≃ G onto the open G = ψ(φ.target) ⊆ Kⁿ with analytic inverse (chartToOpens, chartFromOpens), hence Sp(φ.source) ≅ Sp(G) (chartKIso);
• Sp(G) ≅ (G, 𝒜_G) (ofManifold_restrictOpen_iso for the manifold Kⁿ), and (G, 𝒜_G) is the local analytic K-space with no equations (localModelZeroIso: the quotient by the zero ideal sheaf), which is the open subspace ⊤ of itself (restrictOpenTopIso).

Together (chartLocalModelIso): Sp(M) | φ.source ≅ (localModel K n G ![]) | ⊤, which is Hironaka's clause (i) in the definition of an analytic space [Hir64, Ch. 0, §1, pp. 119–120] for the space of a manifold; it is the locallyModel field of toSpace (Hironaka.AnalyticSpace.Manifold.Defs).

theorem AnalyticSpace.KLocallyRingedSpace.ofManifoldHom_congr {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace K E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] {f g : M → N} (h : f = g) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) : ofManifoldHom f hf = ofManifoldHom g ⋯

ofManifoldHom depends on the map only.

noncomputable def AnalyticSpace.KLocallyRingedSpace.ofManifoldIso {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace K E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] (f : M → N) (g : N → M) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) (hg : ContMDiff (modelWithCornersSelf K E') (modelWithCornersSelf K E) ⊤ g) (hgf : ∀ (x : M), g (f x) = x) (hfg : ∀ (y : N), f (g y) = y) : (ofManifold K E M).KIso (ofManifold K E' N)

Two mutually inverse analytic maps induce a K-isomorphism Sp(M) ≅ Sp(N) (the functoriality of ofManifoldHom).

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.ofManifoldIso_hom {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace K E'] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] (f : M → N) (g : N → M) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) (hg : ContMDiff (modelWithCornersSelf K E') (modelWithCornersSelf K E) ⊤ g) (hgf : ∀ (x : M), g (f x) = x) (hfg : ∀ (y : N), f (g y) = y) : (ofManifoldIso f g hf hg hgf hfg).hom = ofManifoldHom f hf

def AnalyticSpace.KLocallyRingedSpace.chartSourceOpens {E : Type u_1} [NormedAddCommGroup E] {M : Type u} [TopologicalSpace M] (φ : OpenPartialHomeomorph M E) : TopologicalSpace.Opens M

The source of a chart, as an open of M.

Equations

• AnalyticSpace.KLocallyRingedSpace.chartSourceOpens φ = { carrier := φ.source, is_open' := ⋯ }

def AnalyticSpace.KLocallyRingedSpace.chartOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) (φ : OpenPartialHomeomorph M E) : TopologicalSpace.Opens (Kn K n)

The open G = ψ(φ.target) ⊆ Kⁿ of the chart φ in the coordinates ψ (lifted to Kn K n).

Equations

• AnalyticSpace.KLocallyRingedSpace.chartOpens ψ φ = { carrier := {y : AnalyticSpace.Kn K n | ψ.symm y.down ∈ φ.target}, is_open' := ⋯ }

theorem AnalyticSpace.KLocallyRingedSpace.mem_chartOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) (φ : OpenPartialHomeomorph M E) {y : Kn K n} : y ∈ chartOpens ψ φ ↔ ψ.symm y.down ∈ φ.target

def AnalyticSpace.KLocallyRingedSpace.chartToOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) (φ : OpenPartialHomeomorph M E) (x : ↥(chartSourceOpens φ)) : ↥(chartOpens ψ φ)

The chart φ.source → G, x ↦ ψ (φ x).

Equations

• AnalyticSpace.KLocallyRingedSpace.chartToOpens ψ φ x = ⟨{ down := ψ (↑φ ↑x) }, ⋯⟩

def AnalyticSpace.KLocallyRingedSpace.chartFromOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) (φ : OpenPartialHomeomorph M E) (y : ↥(chartOpens ψ φ)) : ↥(chartSourceOpens φ)

The inverse chart G → φ.source, y ↦ φ⁻¹ (ψ⁻¹ y).

Equations

• AnalyticSpace.KLocallyRingedSpace.chartFromOpens ψ φ y = ⟨↑φ.symm (ψ.symm (↑y).down), ⋯⟩

theorem AnalyticSpace.KLocallyRingedSpace.chartFromOpens_chartToOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) (φ : OpenPartialHomeomorph M E) (x : ↥(chartSourceOpens φ)) : chartFromOpens ψ φ (chartToOpens ψ φ x) = x

theorem AnalyticSpace.KLocallyRingedSpace.chartToOpens_chartFromOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) (φ : OpenPartialHomeomorph M E) (y : ↥(chartOpens ψ φ)) : chartToOpens ψ φ (chartFromOpens ψ φ y) = y

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_ulift_coord {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K (Kn K n)) ⊤ fun (e : E) => { down := ψ e }

The coordinates ψ, lifted to Kn K n, are analytic.

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_coord_down {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) : ContMDiff (modelWithCornersSelf K (Kn K n)) (modelWithCornersSelf K E) ⊤ fun (y : Kn K n) => ψ.symm y.down

The inverse coordinates, from Kn K n, are analytic.

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_chartToOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M) : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K (Kn K n)) ⊤ (chartToOpens ψ φ)

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_chartFromOpens {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M) : ContMDiff (modelWithCornersSelf K (Kn K n)) (modelWithCornersSelf K E) ⊤ (chartFromOpens ψ φ)

noncomputable def AnalyticSpace.KLocallyRingedSpace.chartKIso {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M) : (ofManifold K E ↥(chartSourceOpens φ)).KIso (ofManifold K (Kn K n) ↥(chartOpens ψ φ))

A chart identifies its domain with an open subset of Kⁿ as K-local-ringed spaces: Sp(φ.source) ≅ Sp(G), G = ψ(φ.target).

Equations

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

def AnalyticSpace.noEquations (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) : Fin 0 → AnalyticFun K n G

The empty family of equations.

Equations

• AnalyticSpace.noEquations K n G i = i.elim0

theorem AnalyticSpace.stalkIdeal_modelIdeal_noEquations (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) : (modelIdeal K n G (noEquations K n G)).stalkIdeal x = ⊥

The ideal sheaf generated by no equations has zero stalks.

noncomputable def AnalyticSpace.localModelZeroIso (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) : (localModel K n G (noEquations K n G)).KIso (analyticSpaceOfOpen K n G)

The local analytic K-space with no equations is (G, 𝒜_G): the quotient of (G, 𝒜_G) by the zero ideal sheaf is (G, 𝒜_G) itself (quotientBotIso).

Equations

• AnalyticSpace.localModelZeroIso K n G = (AnalyticSpace.analyticSpaceOfOpen K n G).quotientBotIso (AnalyticSpace.modelIdeal K n G (AnalyticSpace.noEquations K n G)) ⋯

noncomputable def AnalyticSpace.chartLocalModelIso {K : Type} [RCLike K] {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (ψ : E ≃L[K] Fin n → K) {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M) : ((KLocallyRingedSpace.ofManifold K E M).restrictOpen (KLocallyRingedSpace.chartSourceOpens φ)).KIso ((localModel K n (KLocallyRingedSpace.chartOpens ψ φ) (noEquations K n (KLocallyRingedSpace.chartOpens ψ φ))).restrictOpen ⊤)

The open subspace of Sp(M) over a chart domain is a local analytic K-space, Hironaka's clause (i) [Hir64, Ch. 0, §1, p. 120] for the space of a manifold: with no equations, on the open G = ψ(φ.target) of Kⁿ, and W = ⊤.

Equations

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