Documentation

Hironaka.AnalyticSpace.RegularStalk

Regular stalks: a manifold point is simple #

Hironaka [Hir64, Ch. 0, Β§1, p. 121]: x is a simple point of X iff some open neighbourhood X|U of x is K-isomorphic to a local analytic K-space of the form (G, π’œ_{Kⁿ}|G), G an open subset of Kⁿ (by the Jacobian criterion and the implicit function theorem). This file proves the easy half: the stalk π’œ_{Kⁿ,q} is a regular local ring of dimension n (through RΓΌckert's basis theorem, isRegularLocalRing_stalk and ringKrullDim_stalk of Hironaka/Manifold/Germ/StalkNoetherian.lean, with finrank_ulift), and regularity and the dimension transport along the stalk isomorphisms of open immersions (restrictStalkIso) and of K-isomorphisms (IsRegularLocalRing.of_ringEquiv, ringKrullDim_eq_of_ringEquiv); so a point of an analytic K-space with a neighbourhood X|V β‰… (G', π’œ_{G'}), G' βŠ† K^d open, has a regular stalk of dimension d.

The converse rests on the Jacobian criterion and is proved elsewhere in this directory.

source
theorem AnalyticSpace.isRegularLocalRing_stalk_affine (K : Type) [RCLike K] (n : β„•) (q : Kn K n) :
IsRegularLocalRing ↑((affine K n).presheaf.stalk q)

The stalk π’œ_{Kⁿ,q} is a regular local ring.

source
theorem AnalyticSpace.ringKrullDim_stalk_affine (K : Type) [RCLike K] (n : β„•) (q : Kn K n) :
ringKrullDim ↑((affine K n).presheaf.stalk q) = ↑n

π’œ_{Kⁿ,q} has Krull dimension n.

source
theorem AnalyticSpace.isRegularLocalRing_stalk_analyticSpaceOfOpen (K : Type) [RCLike K] (n : β„•) (G : TopologicalSpace.Opens (Kn K n)) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) :
IsRegularLocalRing ↑((analyticSpaceOfOpen K n G).presheaf.stalk x)

The stalks of (G, π’œ_G) are regular local rings (restrictStalkIso).

source
theorem AnalyticSpace.ringKrullDim_stalk_analyticSpaceOfOpen (K : Type) [RCLike K] (n : β„•) (G : TopologicalSpace.Opens (Kn K n)) (x : ↑↑(analyticSpaceOfOpen K n G).toPresheafedSpace) :
ringKrullDim ↑((analyticSpaceOfOpen K n G).presheaf.stalk x) = ↑n

The stalks of (G, π’œ_G), G βŠ† Kⁿ open, have Krull dimension n.

source
theorem AnalyticSpace.KLocallyRingedSpace.isRegularLocalRing_stalk_of_restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) (h : IsRegularLocalRing ↑((X.restrictOpen U).presheaf.stalk x)) :
IsRegularLocalRing ↑(X.presheaf.stalk ↑x)

Regularity of a stalk passes from the open subspace X|U to X.

source
theorem AnalyticSpace.KLocallyRingedSpace.ringKrullDim_stalk_restrictOpen {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (x : ↑↑(X.restrictOpen U).toPresheafedSpace) :
ringKrullDim ↑((X.restrictOpen U).presheaf.stalk x) = ringKrullDim ↑(X.presheaf.stalk ↑x)

The Krull dimension of a stalk of the open subspace X|U is that of the stalk of X.

source
theorem AnalyticSpace.KLocallyRingedSpace.isRegularLocalRing_stalk_of_kIso {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) (h : IsRegularLocalRing ↑(B.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) a))) :
IsRegularLocalRing ↑(A.presheaf.stalk a)

Regularity of stalks transports along a K-isomorphism (its stalk maps are isomorphisms).

source
theorem AnalyticSpace.KLocallyRingedSpace.ringKrullDim_stalk_of_kIso {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (e : A.KIso B) (a : ↑↑A.toPresheafedSpace) :
ringKrullDim ↑(A.presheaf.stalk a) = ringKrullDim ↑(B.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom (↑e.hom).base) a))

The Krull dimension of stalks transports along a K-isomorphism.

source
theorem AnalyticSpace.isRegularLocalRing_stalk_of_kIso_analyticSpaceOfOpen {K : Type} [RCLike K] {X : AnalyticSpace K} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {x : ↑↑X.toPresheafedSpace} (hx : x ∈ V) {d : β„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (X.restrictOpen V).KIso (analyticSpaceOfOpen K d G')) :
IsRegularLocalRing ↑(X.presheaf.stalk x) ∧ ringKrullDim ↑(X.presheaf.stalk x) = ↑d

A point x with a neighbourhood X|V K-isomorphic to (G', π’œ_{G'}), G' βŠ† K^d open, is simple, with dim π’ͺ_{X,x} = d [Hir64, Ch. 0, Β§1, p. 121].