K-local-ringed spaces

Hironaka's analytic K-spaces, K = ℝ or ℂ, are K-local-ringed spaces: local-ringed spaces with a structural morphism to Spec K, forming the category ℜ/K of which the analytic K-spaces are the full subcategory An/K [Hir64, Ch. 0, §1, pp. 119–121]. This file defines them and the constructions the rest of the theory rests on: the open subspace X | U, and the K-local-ringed space (M, 𝒪_M) of an analytic manifold together with the K-morphism of an analytic map.

The K-structure

The K-structure is data: a ring homomorphism K →+* Γ(X, 𝒪_X). By the adjunction between global sections and Spec on locally ringed spaces this is the same as a morphism X → Spec K, and it keeps K : Type while the carrier lives in an arbitrary universe. Morphisms of locally ringed spaces need not respect it: over ℂ the map f(z) ↦ conj (f (conj z)) is a ring automorphism of the convergent power series ring ℂ{z} that is not ℂ-linear, and over ℝ a nonzero ℚ-derivation d of ℝ gives the ring homomorphism r ↦ r + d(r) ε into ℝ[ε]/(ε²), different from the canonical one. The morphisms of K-local-ringed spaces are therefore the K-morphisms: morphisms of locally ringed spaces that commute with the structural homomorphisms on global sections. Every restriction map and every stalk map of a K-morphism is then K-linear (Hom.algebraMap_res, Hom.algebraMap_stalk).

Main definitions

• KLocallyRingedSpace K: a LocallyRingedSpace with algebraMap : K →+* Γ(X, 𝒪_X), with its category (the K-morphisms), KIso (the K-isomorphisms) and Hom.toFun (the underlying continuous map); Hom.ofFac: a factorization of a K-morphism through a K-morphism is a K-morphism.
• KLocallyRingedSpace.restrictOpen X U: the open subspace X | U, the restriction of the locally ringed space along the open embedding of U with the restricted K-structure, and the open immersion ofRestrict : X | U ⟶ X as a K-morphism.
• KLocallyRingedSpace.ofManifold K E M: the locally ringed space (M, 𝒪_M) of an analytic manifold M modelled on E, 𝒪_M the sheaf of analytic functions, with the constants as K-structure. For M = Kⁿ this is Hironaka's (Kⁿ, 𝒜_{Kⁿ}) (AnalyticSpace.affine), and 𝒜_G for an open G ⊆ Kⁿ is its restriction restrictOpen, as Hironaka defines it.
• ofManifoldHom f hf : ofManifold K E M ⟶ ofManifold K E' N, the K-morphism induced by an analytic map f : M → N, the analytic analogue of Mathlib's ChartedSpace.locallyRingedSpaceMap for smooth manifolds: the base map is f; the sheaf map 𝒪_N ⟶ f_* 𝒪_M is precomposition with f, an analytic function g on U ⊆ N going to g ∘ f on f⁻¹(U) (ofManifoldSheafHom); the stalk maps 𝒪_{N, f x} → 𝒪_{M, x} are local, because the value at x of g ∘ f is the value at f x of g (stalkMap_ofManifoldHomAux_evalHom) and a germ is a unit exactly when its value is nonzero; the K-structure is respected, a constant pulling back to the same constant. The model spaces E, E' of source and target may differ: a chart φ : U → E is an analytic map into the manifold E, and an open subset of Kⁿ is a manifold modelled on Kⁿ. This is the morphism part of the functor Sp from analytic manifolds to the analytic K-spaces of [Hir64, Ch. 0, §1, pp. 119–120] (AnalyticSpace.toSpaceHom).

structure AnalyticSpace.KLocallyRingedSpace (K : Type) [RCLike K] extends AlgebraicGeometry.LocallyRingedSpace : Type (u + 1)

A K-local-ringed space [Hir64, Ch. 0, §1, p. 119]: a locally ringed space X together with its structural homomorphism algebraMap : K →+* Γ(X, 𝒪_X), the ring-homomorphism form of a morphism X → Spec K.

• carrier : TopCat
• presheaf : TopCat.Presheaf CommRingCat ↑self.toPresheafedSpace
• IsSheaf : self.presheaf.IsSheaf
• isLocalRing (x : ↑↑self.toPresheafedSpace) : IsLocalRing ↑(self.presheaf.stalk x)
• algebraMap : K →+* ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op self.toLocallyRingedSpace))

  The K-structure: the constants K → Γ(X, 𝒪_X).

@[instance_reducible]

instance AnalyticSpace.KLocallyRingedSpace.instCoeSortType {K : Type} [RCLike K] : CoeSort (KLocallyRingedSpace K) (Type u)

Equations

• AnalyticSpace.KLocallyRingedSpace.instCoeSortType = { coe := fun (X : AnalyticSpace.KLocallyRingedSpace K) => ↑↑X.toPresheafedSpace }

@[reducible, inline]

abbrev AnalyticSpace.KLocallyRingedSpace.Hom {K : Type} [RCLike K] (X Y : KLocallyRingedSpace K) : Type u

The K-morphisms [Hir64, Ch. 0, §1, p. 121]: the morphisms of locally ringed spaces that commute with the structural homomorphisms on global sections.

Equations

• X.Hom Y = { f : X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace // (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Γ.map f.op)).comp Y.algebraMap = X.algebraMap }

@[instance_reducible]

instance AnalyticSpace.KLocallyRingedSpace.instCategory {K : Type} [RCLike K] : CategoryTheory.Category.{u, u + 1} (KLocallyRingedSpace K)

The category ℜ/K of K-local-ringed spaces [Hir64, Ch. 0, §1, p. 121].

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.Hom.ext {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} {f g : X ⟶ Y} (h : ↑f = ↑g) : f = g

A K-morphism is determined by its underlying morphism of locally ringed spaces; the K-condition is a proposition.

def AnalyticSpace.KLocallyRingedSpace.Hom.toFun {K : Type} [RCLike K] {X Y : KLocallyRingedSpace K} (f : X ⟶ Y) : ↑↑X.toPresheafedSpace → ↑↑Y.toPresheafedSpace

The underlying continuous map of a K-morphism.

Equations

• AnalyticSpace.KLocallyRingedSpace.Hom.toFun f x = (CategoryTheory.ConcreteCategory.hom (↑f).base) x

@[reducible, inline]

abbrev AnalyticSpace.KLocallyRingedSpace.KIso {K : Type} [RCLike K] (X Y : KLocallyRingedSpace K) : Type u

K-isomorphisms: the isomorphisms of the category ℜ/K (Hironaka's "K-isomorphic").

Equations

• X.KIso Y = (X ≅ Y)

def AnalyticSpace.KLocallyRingedSpace.Hom.ofFac {K : Type} [RCLike K] {A B X : KLocallyRingedSpace K} (a : A ⟶ X) (b : B ⟶ X) (l : A.toLocallyRingedSpace ⟶ B.toLocallyRingedSpace) (hl : CategoryTheory.CategoryStruct.comp l ↑b = ↑a) : A ⟶ B

A factorization l of the K-morphism a through the K-morphism b is a K-morphism.

Equations

• AnalyticSpace.KLocallyRingedSpace.Hom.ofFac a b l hl = ⟨l, ⋯⟩

@[implicit_reducible]

def AnalyticSpace.KLocallyRingedSpace.restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : KLocallyRingedSpace K

The open subspace X | U [Hir64, Ch. 0, §1, p. 120]: the restriction of the locally ringed space along the open embedding of U, with the K-structure obtained by restricting the constants.

Equations

• X.restrictOpen U = { toLocallyRingedSpace := X.restrict ⋯, algebraMap := (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Γ.map (X.ofRestrict ⋯).op)).comp X.algebraMap }

def AnalyticSpace.KLocallyRingedSpace.ofRestrict {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : X.restrictOpen U ⟶ X

The open immersion X | U ⟶ X as a K-morphism.

Equations

• X.ofRestrict U = ⟨X.ofRestrict ⋯, ⋯⟩

instance AnalyticSpace.KLocallyRingedSpace.instIsOpenImmersionValHomLocallyRingedSpaceRestrictOpenEqRingHomCarrierObjOppositeCommRingCatΓOpCompHomMapOpAlgebraMapOfRestrict {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(X.ofRestrict U)

@[implicit_reducible]

noncomputable def AnalyticSpace.KLocallyRingedSpace.ofManifold (K : Type) [RCLike K] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace K E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] : KLocallyRingedSpace K

The locally ringed space (M, 𝒪_M) of an analytic manifold M modelled on E: 𝒪_M is the sheaf of analytic functions on M, whose stalks are local rings, and the constants give the K-structure. For M = Kⁿ this is Hironaka's (Kⁿ, 𝒜_{Kⁿ}), 𝒜_{Kⁿ} the sheaf of germs of analytic K-functions on Kⁿ, with the convergent power series rings K{z₁ - x₁, …, zₙ - xₙ} as stalks [Hir64, Ch. 0, §1].

Equations

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

The K-morphism of an analytic map

theorem AnalyticSpace.KLocallyRingedSpace.contMDiff_subtypeVal_comp_iff' {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 : WithTop ℕ∞} {U : TopologicalSpace.Opens N} (g : M → ↥U) : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') n (Subtype.val ∘ g) ↔ ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') n g

A map into an open subset U of a manifold is C^n iff it is C^n as a map into the manifold (Mathlib's ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff, for every n).

def AnalyticSpace.KLocallyRingedSpace.ofManifoldBase {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) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) : ↧M ⟶ ↧N

The continuous map underlying an analytic map, as a morphism of TopCat.

Equations

• AnalyticSpace.KLocallyRingedSpace.ofManifoldBase f hf = TopCat.ofHom { toFun := f, continuous_toFun := ⋯ }

noncomputable def AnalyticSpace.KLocallyRingedSpace.ofManifoldSheafHom {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) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) : (Manifold.structureSheaf K E' N).presheaf ⟶ (TopCat.Presheaf.pushforward CommRingCat (ofManifoldBase f hf)).obj (Manifold.structureSheaf K E M).presheaf

The sheaf map of an analytic map, 𝒪_N ⟶ f_* 𝒪_M: precomposition with f, an analytic function g on U ⊆ N going to g ∘ f on f⁻¹(U).

Equations

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

noncomputable def AnalyticSpace.KLocallyRingedSpace.ofManifoldHomAux {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) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) : (ofManifold K E M).toPresheafedSpace ⟶ (ofManifold K E' N).toPresheafedSpace

(Implementation.) The morphism of presheafed spaces underlying ofManifoldHom.

Equations

• AnalyticSpace.KLocallyRingedSpace.ofManifoldHomAux f hf = { base := AnalyticSpace.KLocallyRingedSpace.ofManifoldBase f hf, c := AnalyticSpace.KLocallyRingedSpace.ofManifoldSheafHom f hf }

theorem AnalyticSpace.KLocallyRingedSpace.stalkMap_ofManifoldHomAux_evalHom {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) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) (x : M) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ofManifoldHomAux f hf) x) (Manifold.contMDiffSheafCommRing.evalHom (modelWithCornersSelf K E) (modelWithCornersSelf K K) ⊤ M K x) = Manifold.contMDiffSheafCommRing.evalHom (modelWithCornersSelf K E') (modelWithCornersSelf K K) ⊤ N K (f x)

The stalk map of an analytic map followed by evaluation at x is evaluation at f x.

theorem AnalyticSpace.KLocallyRingedSpace.eval_stalkMap_ofManifoldHomAux {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) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) (x : M) (a : ↑((ofManifold K E' N).presheaf.stalk (f x))) : (Manifold.contMDiffSheafCommRing.eval (modelWithCornersSelf K E) (modelWithCornersSelf K K) ⊤ M K x) ((CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ofManifoldHomAux f hf) x)) a) = (Manifold.contMDiffSheafCommRing.eval (modelWithCornersSelf K E') (modelWithCornersSelf K K) ⊤ N K (f x)) a

The evaluation at x of the stalk map applied to a germ at f x is the evaluation of the germ at f x.

noncomputable def AnalyticSpace.KLocallyRingedSpace.ofManifoldHom {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) (hf : ContMDiff (modelWithCornersSelf K E) (modelWithCornersSelf K E') ⊤ f) : ofManifold K E M ⟶ ofManifold K E' N

The K-morphism induced by an analytic map f : M → N: base map f, sheaf map precomposition with f; the stalk maps are local since evaluation is preserved and a germ is a unit exactly when its value is nonzero; constants go to constants.

Equations

• AnalyticSpace.KLocallyRingedSpace.ofManifoldHom f hf = ⟨let __spread.0 := AnalyticSpace.KLocallyRingedSpace.ofManifoldHomAux f hf; { toHom := __spread.0, prop := ⋯ }, ⋯⟩