Upper semicontinuity of the dimension

[Fre17, II 5.4]: for a pointed complex space (X, a) there is a neighbourhood U of a with dim_b X ≤ dim_a X for all b ∈ U — here for analytic K-spaces and the dimension AnalyticSpace.dimAt (Hironaka/AnalyticSpace/Dimension.lean): eventually_dimAt_le, dimAt_upperSemicontinuous.

The proof follows Freitag's, with two replacements named below. Reduce to a local model V(f) ⊆ G ⊆ Kⁿ through the local-model isomorphism of the definition (eventually_dimAt_le). At a point z of the model, the stalk is 𝒪_n/(f)_z through the Taylor isomorphism (ringKrullDim_stalk_localModel_eq); Noether normalization of (f)_z (exists_noetherNormalization_analytic) gives base coordinates e : Fin d ↪ Fin n and a linear change σ = substEquiv L with d = dim_z (Cohen–Seidenberg, ringKrullDim_quotient_eq_of_normMap) and, by module-finiteness, a monic relation σ (X_i^D + ∑_k c_k(X ∘ e) X_i^k) ∈ (f)_z for every coordinate (exists_monic_relation_of_finite). Each relation is a convergent series; it is realized as the section y ↦ g(y − z) of a polydisc (sectionOfConv, convAt_germ_sectionOfConv), which lies in (f) on an open W ∋ z (the spreading lemma exists_forall_germ_mem_span of Hironaka/AnalyticSpace/Propagation.lean, exists_opens_forall_convAt_germ_sectionOfConv_mem); at a nearby point z' its germ is the translated relation σ (shape a c'), a = (L (z' − z)) i, with re-expanded coefficients c' (Hironaka/Analytic/Rueckert/Reexpansion.lean, eventually_exists_shape_mem). So every coordinate satisfies a relation modulo (f)_{z'} ⊔ (σ X_{e j})_j that is monic with constant coefficients, and the parameter bound (Krull's height theorem, [Fre17, VII 5.6]) ringKrullDim_quotient_le_of_forall_exists_shape_mem gives dim_{z'} ≤ d = dim_z (eventually_ringKrullDim_stalk_localModel_le).

The two replacements: (i) Freitag translates a Weierstrass polynomial Q to the nearby centre and uses the module-finiteness of f_a^* : 𝒪_{Y,f(a)} → 𝒪_{X,a} with Cohen–Seidenberg's dim 𝒪_{Y,f(a)} ≥ dim 𝒪_{X,a}; here the translated monic relations give the bound directly through the generator count of Krull's height theorem, so no division at moving centres is needed. (ii) The spreading of g ∈ (f)_z to a neighbourhood is the sheaf-theoretic content of Freitag's "a polydisc which contains Y". Every other step is an item of [Fre17, II 5.4] or of the theory of convergent series (Conv, evalSeries, substEquiv; Hironaka/Analytic/). Used by Hironaka/AnalyticSpace/RegDensityLemmas.lean.

def AnalyticSpace.polydiscOpens {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) (ρ : Analytic.Radius n) : TopologicalSpace.Opens (Kn K n)

The open polydisc of radius ρ about q in Kⁿ.

Equations

• AnalyticSpace.polydiscOpens q ρ = { carrier := {y : AnalyticSpace.Kn K n | y.down - q.down ∈ Analytic.polydisc K ρ}, is_open' := ⋯ }

theorem AnalyticSpace.mem_polydiscOpens_self {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) (ρ : Analytic.Radius n) : q ∈ polydiscOpens q ρ

The centre lies in its polydisc.

theorem AnalyticSpace.contMDiffOn_evalSeries_sub {K : Type} [RCLike K] {n : ℕ} {T : MvPowerSeries (Fin n) K} {ρ : Analytic.Radius n} (hT : Analytic.ConvNorm (↑ρ) T ≠ ⊤) (q : Kn K n) : ContMDiffOn (modelWithCornersSelf K (Kn K n)) (modelWithCornersSelf K K) ⊤ (fun (y : Kn K n) => Analytic.evalSeries T (y.down - q.down)) ↑(polydiscOpens q ρ)

The function y ↦ T(y − q) of a convergent series T of radius ρ is analytic on the polydisc of radius ρ about q (analyticOnNhd_evalSeries of Hironaka/Analytic/ConvSeries/Rescale.lean).

noncomputable def AnalyticSpace.sectionOfConv {K : Type} [RCLike K] {n : ℕ} {T : MvPowerSeries (Fin n) K} {ρ : Analytic.Radius n} (hT : Analytic.ConvNorm (↑ρ) T ≠ ⊤) (q : Kn K n) : ↑((affine K n).presheaf.obj (Opposite.op (polydiscOpens q ρ)))

The section y ↦ T(y − q) of 𝒜_{Kⁿ} over the polydisc about q (the realization of a convergent series as an analytic function near q).

Equations

• AnalyticSpace.sectionOfConv hT q = Manifold.sectionOfContMDiffOn (fun (y : AnalyticSpace.Kn K n) => Analytic.evalSeries T (y.down - q.down)) (AnalyticSpace.polydiscOpens q ρ) ⋯

theorem AnalyticSpace.extendSection_sectionOfConv {K : Type} [RCLike K] {n : ℕ} {T : MvPowerSeries (Fin n) K} {ρ : Analytic.Radius n} (hT : Analytic.ConvNorm (↑ρ) T ≠ ⊤) (q : Kn K n) {y : Kn K n} (hy : y ∈ polydiscOpens q ρ) : Manifold.extendSection K (Kn K n) (sectionOfConv hT q) y = Analytic.evalSeries T (y.down - q.down)

The values of sectionOfConv.

theorem AnalyticSpace.convAt_germ_eq_of_eventuallyEq {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) {U : TopologicalSpace.Opens (Kn K n)} (hq : q ∈ U) (F : ↑((affine K n).presheaf.obj (Opposite.op U))) (T : ↥(Analytic.Conv K n)) (h : ∀ᶠ (y : Fin n → K) in nhds q.down, Manifold.extendSection K (Kn K n) F { down := y } = Analytic.evalSeries (↑T) (y - q.down)) : (taylorAffine K n q) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ U q hq)) F) = T

The Taylor series at q (identity chart; the specification IsTaylorHom of the Taylor homomorphism, Hironaka/Manifold/StructureSheaf.lean) of the germ of a section F is the convergent series T when F(y) = T(y − q) for y near q.

theorem AnalyticSpace.eventually_up_mem {K : Type} [RCLike K] {n : ℕ} (q : Kn K n) {U : TopologicalSpace.Opens (Kn K n)} (hq : q ∈ U) : ∀ᶠ (y : Fin n → K) in nhds q.down, { down := y } ∈ U

Points near q lie in an open neighbourhood of q, read in the coordinates Fin n → K.

theorem AnalyticSpace.convAt_germ_sectionOfConv {K : Type} [RCLike K] {n : ℕ} (T : ↥(Analytic.Conv K n)) {ρ : Analytic.Radius n} (hT : Analytic.ConvNorm ↑ρ ↑T ≠ ⊤) (q : Kn K n) : (taylorAffine K n q) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ (polydiscOpens q ρ) q ⋯)) (sectionOfConv hT q)) = T

The germ at q of sectionOfConv T is T under the Taylor isomorphism.

theorem AnalyticSpace.germ_mem_of_convAt_mem_map {K : Type} [RCLike K] {n : ℕ} {q : Kn K n} {U : TopologicalSpace.Opens (Kn K n)} (hq : q ∈ U) (F : ↑((affine K n).presheaf.obj (Opposite.op U))) {J : Ideal ↑((affine K n).presheaf.stalk q)} (h : (taylorAffine K n q) ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ U q hq)) F) ∈ Ideal.map (taylorAffine K n q) J) : (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ U q hq)) F ∈ J

Membership in an ideal of the stalk, read through the Taylor isomorphism taylorAffine.

noncomputable def AnalyticSpace.modelIdealAt {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) : Ideal ↥(Analytic.Conv K n)

The ideal (f)_z of a point of the local model, read in Conv K n.

Equations

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

theorem AnalyticSpace.modelIdealAt_ne_top {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) : modelIdealAt G f z ≠ ⊤

(f)_z is proper: the f_j vanish at the points of the model (span_germ_le_maximalIdeal of Hironaka/AnalyticSpace/Jacobian.lean).

theorem AnalyticSpace.continuous_localModel_pt {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) : Continuous fun (z' : ↑↑(localModel K n G f).toPresheafedSpace) => ↑↑z'

The underlying point of Kⁿ of a point of the local model depends continuously on it.

theorem AnalyticSpace.tendsto_localModel_sub {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) : Filter.Tendsto (fun (z' : ↑↑(localModel K n G f).toPresheafedSpace) => (↑↑z').down - (↑↑z).down) (nhds z) (nhds 0)

The displacement z' − z in the coordinates of Kⁿ tends to 0 as z' → z in the model.

theorem AnalyticSpace.eventually_localModel_pt_mem {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) {W : TopologicalSpace.Opens (Kn K n)} (hz : ↑↑z ∈ W) : ∀ᶠ (z' : ↑↑(localModel K n G f).toPresheafedSpace) in nhds z, ↑↑z' ∈ W

Points of the model near z lie in an open neighbourhood of z in Kⁿ.

theorem AnalyticSpace.exists_opens_forall_convAt_germ_sectionOfConv_mem {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) {g : ↥(Analytic.Conv K n)} (hg : g ∈ modelIdealAt G f z) {ρ : Analytic.Radius n} (hρ : Analytic.ConvNorm ↑ρ ↑g ≠ ⊤) : ∃ (W : TopologicalSpace.Opens (Kn K n)) (_ : ↑↑z ∈ W) (hWP : W ≤ polydiscOpens (↑↑z) ρ), ∀ (z' : ↑↑(localModel K n G f).toPresheafedSpace) (hz' : ↑↑z' ∈ W), (taylorAffine K n ↑↑z') ((CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ (polydiscOpens (↑↑z) ρ) ↑↑z' ⋯)) (sectionOfConv hρ ↑↑z)) ∈ modelIdealAt G f z'

Spreading ([Fre17, II 5.4], "a polydisc which contains Y"): an element g ∈ (f)_z (read in Conv K n) of radius ρ is the germ at z of the section y ↦ g(y − z) of the polydisc, and by exists_forall_germ_mem_span this section lies in (f) at every point of an open W ∋ z of the polydisc — so its germ at every nearby point z', read through the Taylor isomorphism at z', lies in (f)_{z'}.

theorem AnalyticSpace.eventually_exists_shape_mem {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) (L : (Fin n → K) ≃L[K] Fin n → K) {d : ℕ} (e : Fin d ↪ Fin n) (i : Fin n) {D : ℕ} (c : Fin D → ↥(Analytic.Conv K d)) (hc : (Analytic.substEquiv L) (Analytic.shapeSeries K i e 0 c) ∈ modelIdealAt G f z) : ∀ᶠ (z' : ↑↑(localModel K n G f).toPresheafedSpace) in nhds z, ∃ (a : K) (c' : Fin D → ↥(Analytic.Conv K d)), (Analytic.substEquiv L) (Analytic.shapeSeries K i e a c') ∈ modelIdealAt G f z'

Translation of a monic relation ([Fre17, II 5.4]: the Weierstrass polynomial Q(a₁, …, a_{n−1}, z_n − a_n) general in ℂ{z₁ − a₁, …}[z_n − a_n]): a monic relation σ (shape 0 c) ∈ (f)_z for the coordinate X i yields, at every point z' near z, a relation σ (shape a c') ∈ (f)_{z'} of the same shape — the germ at z' of the realized section is the translated series (exists_substEquiv_shapeSeries_translate), by the uniqueness of Taylor series (convAt_germ_eq_of_eventuallyEq).

theorem AnalyticSpace.eventually_ringKrullDim_stalk_localModel_le {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) : ∀ᶠ (z' : ↑↑(localModel K n G f).toPresheafedSpace) in nhds z, ringKrullDim ↑((localModel K n G f).presheaf.stalk z') ≤ ringKrullDim ↑((localModel K n G f).presheaf.stalk z)

[Fre17, II 5.4] on a local model, dim_{z'} ≤ dim_z for z' near z: Noether normalization at z gives d = dim 𝒪_{z} (ringKrullDim_quotient_eq_of_normMap, Cohen–Seidenberg) and monic relations for all coordinates (exists_monic_relation_of_finite); the relations persist at nearby points (eventually_exists_shape_mem, finitely many coordinates), where the parameter bound ringKrullDim_quotient_le_of_forall_exists_shape_mem (in place of Freitag's use of Cohen–Seidenberg for dim 𝒪_{Y,f(a)} ≥ dim 𝒪_{X,a}; Krull's height theorem, [Fre17, VII 5.6]) gives dim 𝒪_{z'} ≤ d. The bridge ringKrullDim_stalk_localModel_eq reads both stalks in Conv K n.

theorem AnalyticSpace.dimAt_eq_ringKrullDim_stalk_localModel {K : Type} [RCLike K] {X : AnalyticSpace K} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {n k : ℕ} {G : TopologicalSpace.Opens (Kn K n)} {f : Fin k → AnalyticFun K n G} {W : TopologicalSpace.Opens ↑↑(localModel K n G f).toPresheafedSpace} (e : (X.restrictOpen U).KIso ((localModel K n G f).restrictOpen W)) {y : ↑↑X.toPresheafedSpace} (hy : y ∈ U) : X.dimAt y = ringKrullDim ↑((localModel K n G f).presheaf.stalk ↑((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) ⟨y, hy⟩))

dimAt X y at any point of the chart X|U ≅ (localModel)|W is the Krull dimension of the stalk of the local model at the image point (the stalk transports of Hironaka/AnalyticSpace/RegularStalk.lean).

theorem AnalyticSpace.eventually_dimAt_le {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : ∀ᶠ (y : ↑↑X.toPresheafedSpace) in nhds x, X.dimAt y ≤ X.dimAt x

[Fre17, II 5.4]: dim_y X ≤ dim_x X for y near x — transport of the local-model statement along the local-model isomorphism of the definition, which is a homeomorphism of the open U ∋ x onto an open of the model.

theorem AnalyticSpace.dimAt_upperSemicontinuous {K : Type} [RCLike K] (X : AnalyticSpace K) : UpperSemicontinuous X.dimAt

The dimension is upper semicontinuous [Fre17, II 5.4]: x ↦ dim_x X.