The germ ring as a factorial Noetherian regular local ring

The stalk 𝒪_{M,a} of an analytic manifold is a Noetherian regular local ring of Krull dimension n (Hironaka/Manifold/Germ/StalkNoetherian.lean, bundled here as isNoetherianRing_isRegularLocalRing_stalk) and a unique factorization domain (uniqueFactorizationMonoid_stalk): the classical factoriality of the ring Conv 𝕜 n of convergent power series (Hironaka/Analytic/Rueckert/UFD.lean, from Rückert's basis theorem and Gauss's lemma) transported through the Taylor isomorphism 𝒪_{M,a} ≃+* Conv 𝕜 n. Two corollaries on principal ideals: the Krull dimension of the quotient of 𝒪_{M,a} by a proper principal ideal (f) is at least n − 1 (Mathlib's dim R ≤ dim R/(x) + 1 for x in the maximal ideal of a Noetherian local ring), and exactly n − 1 when f ≠ 0 (Krull's principal ideal theorem in the domain 𝒪_{M,a}: a nonzero f ∈ 𝔪_a is a nonzerodivisor in the Jacobson radical). These are the ring-theoretic facts about hypersurface germs used for analytic spaces (Hironaka/Space/) and in the order computations of the resolution algorithm.

theorem Manifold.uniqueFactorizationMonoid_stalk_of_chart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : UniqueFactorizationMonoid ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

In a chart of the maximal atlas at a, the stalk 𝒪_{M,a} is a unique factorization domain: the factoriality of the ring of convergent power series (uniqueFactorizationMonoid_conv) through the Taylor isomorphism taylorEquivConv.

theorem Manifold.isNoetherianRing_isRegularLocalRing_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) : IsNoetherianRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ∧ IsRegularLocalRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ∧ ringKrullDim ↑((structureSheaf 𝕜 E M).presheaf.stalk a) = ↑(Module.finrank 𝕜 E)

𝒪_{M,a} is a Noetherian regular local ring of Krull dimension n, bundled.

theorem Manifold.uniqueFactorizationMonoid_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) : UniqueFactorizationMonoid ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The stalks of an analytic manifold are unique factorization domains.

theorem Manifold.le_ringKrullDim_quotient_span_singleton_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) {f : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)} (hf : f ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : ↑(Module.finrank 𝕜 E) ≤ ringKrullDim (↑((structureSheaf 𝕜 E M).presheaf.stalk a) ⧸ Ideal.span {f}) + 1

For f ∈ 𝔪_a, n ≤ dim 𝒪_{M,a} / (f) + 1: Mathlib's dim R ≤ dim R/(x) + 1 for x in the maximal ideal of a Noetherian local ring.

theorem Manifold.ringKrullDim_quotient_span_singleton_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) {f : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)} (hf : f ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (hf0 : f ≠ 0) : ringKrullDim (↑((structureSheaf 𝕜 E M).presheaf.stalk a) ⧸ Ideal.span {f}) + 1 = ↑(Module.finrank 𝕜 E)

The sharp form, Krull's principal ideal theorem in the domain 𝒪_{M,a}: for 0 ≠ f ∈ 𝔪_a, dim 𝒪_{M,a} / (f) + 1 = n — a nonzero element of the maximal ideal of the domain 𝒪_{M,a} is a nonzerodivisor in the Jacobson radical.