The local models of analytic K-spaces: embeddings and coordinations

The local analytic K-spaces localModel K n G f = (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}), 𝓘 = (f₁, …, f_k), of [Hir64, Ch. 0, §1] sit in (Kⁿ, 𝒜_{Kⁿ}), and an analytic K-space has a local Kⁿ-coordination at every point (exists_localCoordination).

• AnalyticFun.eval g p, the value at a point of G of a regular analytic K-function on G.
• localModel.ι : localModel K n G f ⟶ affine K n, the embedding into (Kⁿ, 𝒜_{Kⁿ}), onto the locally closed set S(𝓘) (closed in the open G): the quotient's canonical morphism followed by the open immersion (G, 𝒜_G) ⟶ (Kⁿ, 𝒜_{Kⁿ}).
• coordSection K n i, the i-th coordinate function z_i on Kⁿ as a global analytic function.
• LocalCoordination X x: a local Kⁿ-coordination (U, h) at x [Hir64, Ch. 0, §1, p. 120] is an open neighbourhood U of x with a K-morphism h : X|U → (Kⁿ, 𝒜_{Kⁿ}) inducing a K-isomorphism of X|U onto a local analytic K-space in (Kⁿ, 𝒜_{Kⁿ}); here h is factored as a K-isomorphism onto an open subspace W of a local model L, the open immersion L|W ⟶ L, and the embedding localModel.ι of L onto the locally closed set S(𝓘) ⊆ G ⊆ Kⁿ.

The embedding localModel.ι is injective on points (injective_base_localModel_ι, injective_toFun_localModel_ι) with surjective stalk maps (surjective_stalkMap_localModel_ι: those of the quotient's canonical morphism are, and the open immersion is an isomorphism on stalks), hence a monomorphism of K-spaces (eq_of_comp_localModel_ι_eq, by Mathlib's SheafedSpace.mono_of_base_injective_of_stalk_epi). The support of localModel K n G f is the common zero set of the f_i (mem_cosupport_modelIdeal_iff), and an open subspace of a local model is again a local model (localModel_restrictOpen_iso).

def AnalyticSpace.AnalyticFun.eval {K : Type} [RCLike K] {n : ℕ} {G : TopologicalSpace.Opens (Kn K n)} (g : AnalyticFun K n G) (p : ↥G) : K

The value at a point of G of a regular analytic K-function on G.

Equations

• g.eval p = ↑g p

noncomputable def AnalyticSpace.localModel.ι (K : Type) [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : localModel K n G f ⟶ affine K n

The embedding of the local model into (Kⁿ, 𝒜_{Kⁿ}), onto the set S(𝓘), closed in the open G and so locally closed in Kⁿ: the quotient's canonical morphism followed by the open immersion (G, 𝒜_G) ⟶ (Kⁿ, 𝒜_{Kⁿ}) (Hironaka's "local analytic K-space in (Kⁿ, 𝒜_{Kⁿ})").

Equations

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

def AnalyticSpace.coordSection (K : Type) [RCLike K] (n : ℕ) (i : Fin n) : ↑((affine K n).presheaf.obj (Opposite.op ⊤))

The i-th coordinate function z_i on Kⁿ as a global analytic function.

Equations

• AnalyticSpace.coordSection K n i = ⟨fun (p : ↥⊤) => (↑p).down i, ⋯⟩

theorem AnalyticSpace.surjective_stalkMap_comp {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toTopCat) (hf : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x))) (hg : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap g ((CategoryTheory.ConcreteCategory.hom f.base) x)))) : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (CategoryTheory.CategoryStruct.comp f g) x))

The stalk map of a composite is surjective when both stalk maps are.

theorem AnalyticSpace.injective_base_localModel_ι {K : Type} [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (↑(localModel.ι K n G f)).base)

The closed embedding of a local model into (Kⁿ, 𝒜_{Kⁿ}) is injective on points.

theorem AnalyticSpace.surjective_stalkMap_localModel_ι {K : Type} [RCLike K] (n : ℕ) (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(localModel.ι K n G f)) z))

The stalk maps of the closed embedding of a local model into (Kⁿ, 𝒜_{Kⁿ}) are surjective.

theorem AnalyticSpace.KLocallyRingedSpace.injective_toFun_localModel_ι {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : Function.Injective (Hom.toFun (localModel.ι K n G f))

The closed embedding ι : L ⟶ (Kⁿ, 𝒜_{Kⁿ}) of a local model is injective on points.

theorem AnalyticSpace.KLocallyRingedSpace.eq_of_comp_localModel_ι_eq {K : Type} [RCLike K] {A : KLocallyRingedSpace K} {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (a b : A ⟶ localModel K n G f) (h : CategoryTheory.CategoryStruct.comp a (localModel.ι K n G f) = CategoryTheory.CategoryStruct.comp b (localModel.ι K n G f)) : a = b

The closed embedding of a local model is a monomorphism of K-spaces: a ≫ ι = b ≫ ι forces a = b (injective on points, surjective on stalks).

structure AnalyticSpace.LocalCoordination {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : Type u

A local Kⁿ-coordination (U, h) of X at x [Hir64, Ch. 0, §1, p. 120]: an open neighbourhood U of x and a K-morphism h : X|U ⟶ (Kⁿ, 𝒜_{Kⁿ}) which induces a K-isomorphism of X|U onto a local analytic K-space in (Kⁿ, 𝒜_{Kⁿ}) — h factors as the K-isomorphism iso onto an open subspace W of the local model L = V(f) ⊆ G, followed by the open immersion L|W ⟶ L and the embedding localModel.ι : L ⟶ (Kⁿ, 𝒜_{Kⁿ}), whose image S(𝓘) is closed in the open G (h_eq).

• U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace

  The open neighbourhood.

• mem : x ∈ self.U
• n : ℕ

  The dimension of the ambient Kⁿ.

• h : X.restrictOpen self.U ⟶ affine K self.n

  The coordination h : X|U ⟶ (Kⁿ, 𝒜_{Kⁿ}).

• k : ℕ
• G : TopologicalSpace.Opens (Kn K self.n)
• f : Fin self.k → AnalyticFun K self.n self.G
• W : TopologicalSpace.Opens ↑↑(localModel K self.n self.G self.f).toPresheafedSpace
• iso : (X.restrictOpen self.U).KIso ((localModel K self.n self.G self.f).restrictOpen self.W)

  The induced K-isomorphism onto the local analytic K-space.

• h_eq : self.h = CategoryTheory.CategoryStruct.comp self.iso.hom (CategoryTheory.CategoryStruct.comp ((localModel K self.n self.G self.f).ofRestrict self.W) (localModel.ι K self.n self.G self.f))