The functor from analytic manifolds to analytic spaces is fully faithful

A K-morphism F : Sp(M) ⟶ Sp(N) between the analytic spaces of two manifolds is induced by a unique analytic map, namely its underlying map toSpaceFun ψ F : M → N (toSpace_fullyFaithful). This is not stated in the sources; it is what makes the local coordinations of [Hir64, Ch. 0, §1, p. 120], which are K-morphisms into (Kⁿ, 𝒜_{Kⁿ}), the same thing as charts. The proof:

• Evaluation is preserved by the stalk maps (eval_stalkMap): for a germ σ at F y with value c, σ - c is a non-unit; the stalk map is a local K-homomorphism sending constants to constants, so F^*σ - c is a non-unit, i.e. F^*σ has value c. Hence a pulled-back section has the composed values, (F^*s)(y) = s(F y) (sheafHom_apply): the sheaf map of a K-morphism of sheaves of functions is precomposition with the underlying map.
• The underlying map is analytic (contMDiff_baseFun): in a chart χ at F x with coordinates ψ', the coordinate functions ψ'_i ∘ χ (chartSection) pull back to analytic functions on F⁻¹(χ.source) whose values are ψ'_i (χ (F y)), so χ ∘ F is analytic near x.
• Two local K-homomorphisms out of a stalk 𝒪_{N,b} agreeing on the coordinate germs of a chart agree (ringHom_ext_of_coord'): Hadamard's lemma (exists_eq_sum_coord_mul') gives the 𝔪-adic approximation of every germ by polynomials in the coordinates, and Krull's intersection theorem in the Noetherian target finishes.
• A K-morphism is determined by its underlying map (hom_ext_baseFun): the stalk maps at y of two morphisms with the same base map are local K-homomorphisms 𝒪_{N, F y} → 𝒪_{M, y} into a Noetherian local ring which agree on the coordinate germs, because the pulled-back coordinate sections have the same values; hence they agree, and a morphism of sheaves is determined by its stalk maps.

Then toSpaceHom ψ : AnalyticMap M N → (Sp(M) ⟶ Sp(N)) is injective (toSpaceHom_injective) and surjective (exists_toSpaceHom_eq, the analytic map being ⟨toSpaceFun F, contMDiff_toSpaceFun F⟩). The extensionality on points is used to show that a comparison morphism is an isomorphism chart by chart (Hironaka.AnalyticSpace.Manifold.StratumIso) and for morphisms into a non-singular space (Hironaka.AnalyticSpace.HomExtNonSingular); the stalk lemma ringHom_ext_of_coord' is used for the uniqueness of lifts through a blow-up chart (Hironaka.AnalyticSpace.MonoidalUnique) and in the gluing of local resolutions (Hironaka.Resolution.Analytic.Kol07Thm45.PieceLemma39Model, Hironaka.Resolution.Analytic.Kol07Thm45.PieceLemma39Shear).

noncomputable def AnalyticSpace.KLocallyRingedSpace.baseFun {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 : ofManifold K E M ⟶ ofManifold K E' N) : M → N

The underlying map M → N of a K-morphism Sp(M) ⟶ Sp(N), with the manifolds' types.

Equations

• AnalyticSpace.KLocallyRingedSpace.baseFun F x = (CategoryTheory.ConcreteCategory.hom (↑F).base) x

theorem AnalyticSpace.KLocallyRingedSpace.baseFun_apply {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 : ofManifold K E M ⟶ ofManifold K E' N) (x : M) : baseFun F x = (CategoryTheory.ConcreteCategory.hom (↑F).base) x

theorem AnalyticSpace.KLocallyRingedSpace.continuous_baseFun {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 : ofManifold K E M ⟶ ofManifold K E' N) : Continuous (baseFun F)

theorem AnalyticSpace.KLocallyRingedSpace.eval_stalkMap {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 : ofManifold K E M ⟶ ofManifold K E' N) (y : M) (σ : ↑((Manifold.structureSheaf K E' N).presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑F).base) y))) : (Manifold.eval K E M y) ((CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑F) y)) σ) = (Manifold.eval K E' N ((CategoryTheory.ConcreteCategory.hom (↑F).base) y)) σ

The stalk map of a K-morphism preserves the value of a germ: σ - σ(F y) is a non-unit, so is its image, which is F^*σ - σ(F y).

theorem AnalyticSpace.KLocallyRingedSpace.sheafHom_apply {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 : ofManifold K E M ⟶ ofManifold K E' N) (U : TopologicalSpace.Opens N) (s : ↑((Manifold.structureSheaf K E' N).presheaf.obj (Opposite.op U))) (y : M) (hy : (CategoryTheory.ConcreteCategory.hom (↑F).base) y ∈ U) : ↑((CommRingCat.Hom.hom ((↑F).c.app (Opposite.op U))) s) ⟨y, hy⟩ = ↑s ⟨(CategoryTheory.ConcreteCategory.hom (↑F).base) y, hy⟩

A pulled-back section has the composed values, (F^*s)(y) = s(F y).

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_baseFun {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] {n : ℕ} [IsManifold (modelWithCornersSelf K E') ⊤ N] (ψ' : E' ≃L[K] Fin n → K) (F : ofManifold K E M ⟶ ofManifold K E' N) : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ (baseFun F)

The underlying map of a K-morphism between the spaces of two manifolds is analytic: in a chart χ at F x, the coordinate functions of χ pull back to analytic functions whose values are the coordinates of χ ∘ F.

theorem AnalyticSpace.KLocallyRingedSpace.ringHom_ext_of_coord' {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (ψ : E ≃L[K] Fin n → K) {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf K E) ⊤ M) {a : M} (ha : a ∈ φ.source) (α β : ↑((Manifold.structureSheaf K E M).presheaf.stalk a) →+* R) (hα : IsLocalHom α) (hβ : IsLocalHom β) (hc : ∀ (c : K), α ((Manifold.const K E M a) c) = β ((Manifold.const K E M a) c)) (hz : ∀ (i : Fin n), α (Manifold.coord E ψ φ hφ ha i) = β (Manifold.coord E ψ φ hφ ha i)) : α = β

Two local ring homomorphisms from 𝒪_{M,a} into a Noetherian local ring that agree on the constants and on the coordinate germs of a chart at a agree: Hadamard's lemma gives the 𝔪-adic approximation by polynomials in the coordinates, and Krull's intersection theorem finishes (the form of ringHom_ext_of_coord for the stalk of a manifold).

theorem AnalyticSpace.KLocallyRingedSpace.hom_ext_baseFun {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] {n : ℕ} [IsManifold (modelWithCornersSelf K E) ⊤ M] [IsManifold (modelWithCornersSelf K E') ⊤ N] (ψ : E ≃L[K] Fin n → K) {n' : ℕ} (ψ' : E' ≃L[K] Fin n' → K) (F G : ofManifold K E M ⟶ ofManifold K E' N) (h : baseFun F = baseFun G) : F = G

A K-morphism between the spaces of two manifolds is determined by its underlying map: its stalk maps are local K-homomorphisms into Noetherian local rings agreeing on the coordinate germs (the pulled-back coordinate sections have the same values), and a morphism of sheaves is determined by its stalk maps. ψ' supplies the coordinates on the target's model space E': the coordinate germs ψ'_i ∘ χ of a chart χ at F x generate the maximal ideal of 𝒪_{N, F x}, and the two stalk maps agree on them because the pulled-back coordinate sections have the same values along the common underlying map; ψ gives the Noetherianity of the stalks of the source through its charts.

noncomputable def AnalyticSpace.toSpaceFun {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M N : AnalyticManifold K E} (F : toSpace ψ M ⟶ toSpace ψ N) : M.carrier → N.carrier

The underlying map M → N of a morphism Sp(M) ⟶ Sp(N), with the manifolds' types (the base map of the morphism of locally ringed spaces).

Equations

• AnalyticSpace.toSpaceFun ψ F x = (CategoryTheory.ConcreteCategory.hom (↑F).base) x

theorem AnalyticSpace.toSpaceFun_toSpaceHom {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M N : AnalyticManifold K E} (f : AnalyticMap M N) : toSpaceFun ψ (toSpaceHom ψ f) = ⇑f

theorem AnalyticSpace.contMDiff_toSpaceFun {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M N : AnalyticManifold K E} (F : toSpace ψ M ⟶ toSpace ψ N) : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E) ⊤ (toSpaceFun ψ F)

The underlying map of a morphism Sp(M) ⟶ Sp(N) is analytic.

theorem AnalyticSpace.hom_ext_toSpaceFun {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M N : AnalyticManifold K E} (F G : toSpace ψ M ⟶ toSpace ψ N) (h : toSpaceFun ψ F = toSpaceFun ψ G) : F = G

A morphism Sp(M) ⟶ Sp(N) is determined by its underlying map.

theorem AnalyticSpace.toSpaceHom_injective {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M N : AnalyticManifold K E} : Function.Injective (toSpaceHom ψ)

Sp is faithful.

theorem AnalyticSpace.exists_toSpaceHom_eq {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M N : AnalyticManifold K E} (F : toSpace ψ M ⟶ toSpace ψ N) : ∃ (f : AnalyticMap M N), toSpaceHom ψ f = F

Sp is full: every morphism Sp(M) ⟶ Sp(N) is Sp(f) for the analytic map f underlying it.

theorem AnalyticSpace.toSpace_fullyFaithful {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} (ψ : E ≃L[K] Fin n → K) {M N : AnalyticManifold K E} : Function.Bijective (toSpaceHom ψ)

Sp is fully faithful: analytic maps M → N correspond bijectively to morphisms Sp(M) ⟶ Sp(N).