The completion map of the analytic stalk is injective

Bierstone–Milman's first condition on the local rings of their category of spaces [BM97, (0.1)(1)]: "the natural homomorphism 𝒪_{X,a} → 𝒪̂_{X,a} into the completion is injective"; and Krull's intersection theorem in the geometric form Kollár uses [Kol07, Definition 55]: "if Ẑ_x = Ŵ_x then Z ∩ U = W ∩ U" on a neighbourhood U of x.

• ⋂_k 𝔪_a^k = 0 in the analytic stalk 𝒪_{M,a} (iInf_maximalIdeal_pow_eq_bot): a germ in every 𝔪_a^k has Taylor series in every (X)^k (IsTaylorHom.mem_maximalIdeal_pow_iff), hence of infinite order, hence zero, hence the germ is zero (IsTaylorHom.injective'); so the stalk is 𝔪_a-adically Hausdorff (isHausdorff_stalk) and the completion map is injective (injective_algebraMap_adicCompletion, Mathlib's AdicCompletion.of_injective).
• Ideals of a Noetherian local ring with the same extension to the completion are equal (Ideal.eq_of_map_adicCompletion_eq: Krull, in the form I R̂ ∩ R = I), and two locally finitely generated ideal sheaves with equal stalks at a have equal stalks near a (IdealSheaf.exists_opens_forall_stalkIdeal_eq): the generators of one near a are combinations of the generators of the other at a, hence, as sections, on a neighbourhood (TopCat.Presheaf.germ_eq). The propagation is stated for ideal sheaves over any sheaf of commutative rings; the geometric form for the analytic stalk (exists_opens_forall_stalkIdeal_eq_of_map_adicCompletion_eq) carries Kollár's Noetherian hypothesis explicitly (the Noetherian instance for the analytic stalk is Hironaka/Manifold/Germ/StalkNoetherian.lean).

These results compare ideal sheaves through their completions; they are used in the maximal-contact arguments (Hironaka/Manifold/MaximalContact/).

Krull's intersection theorem in a chart

theorem Manifold.IsTaylorHom.iInf_maximalIdeal_pow_eq_bot {𝕜 : 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) {T : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜} (hT : IsTaylorHom E ψ φ a T) : ⨅ (k : ℕ), IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k = ⊥

In a chart: ⋂_k 𝔪_a^k = 0 — a germ in every 𝔪_a^k has Taylor series in every (X)^k, hence zero Taylor series, hence is zero (the Taylor homomorphism is injective).

Krull's intersection theorem for the stalk

theorem Manifold.iInf_maximalIdeal_pow_eq_bot {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (a : M) : ⨅ (k : ℕ), IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ^ k = ⊥

Krull's intersection theorem for the analytic stalk, ⋂_k 𝔪_a^k = 0, through the Taylor homomorphism of the chart at a ([BM97, (0.1)(1)]; [Kol07, Definition 55]).

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

The analytic stalk is 𝔪_a-adically Hausdorff.

theorem Manifold.injective_algebraMap_adicCompletion {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (a : M) : Function.Injective ⇑(algebraMap (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)))

Bierstone–Milman's condition (0.1)(1) [BM97, (0.1)]: the completion map 𝒪_{M,a} → 𝒪̂_{M,a} is injective.

Krull's theorem for ideals of a Noetherian local ring

theorem Ideal.eq_of_map_adicCompletion_eq {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {I J : Ideal R} (h : map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) I = map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) J) : I = J

Krull's intersection theorem I = ⋂_s (I + 𝔪^s) [Kol07, Definition 55] in the form I R̂ ∩ R = I: ideals of a Noetherian local ring with the same extension to the completion are equal.

Equal stalks propagate to a neighbourhood

theorem Manifold.IdealSheaf.eventually_stalkIdeal_le {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {I J : IdealSheaf 𝒪} {a : ↑X} (h : J.stalkIdeal a ≤ I.stalkIdeal a) : ∀ᶠ (b : ↑X) in nhds a, J.stalkIdeal b ≤ I.stalkIdeal b

One inclusion: if the stalk of J at a lies in that of I, the generators of J near a are combinations of the generators of I at a, hence on a neighbourhood, so J_b ⊆ I_b for b near a.

theorem Manifold.IdealSheaf.eventuallyEq_stalkIdeal_of_eq {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {I J : IdealSheaf 𝒪} {a : ↑X} (h : I.stalkIdeal a = J.stalkIdeal a) : ∀ᶠ (b : ↑X) in nhds a, I.stalkIdeal b = J.stalkIdeal b

Two locally finitely generated ideal sheaves with equal stalks at a have equal stalks near a (filter form).

theorem Manifold.IdealSheaf.exists_opens_forall_stalkIdeal_eq {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {I J : IdealSheaf 𝒪} {a : ↑X} (h : I.stalkIdeal a = J.stalkIdeal a) : ∃ (U : TopologicalSpace.Opens ↑X), a ∈ U ∧ ∀ b ∈ U, I.stalkIdeal b = J.stalkIdeal b

Two locally finitely generated ideal sheaves with equal stalks at a agree on an open neighbourhood of a.

The geometric form of Krull's theorem

theorem Manifold.exists_opens_forall_stalkIdeal_eq_of_map_adicCompletion_eq {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (I J : IdealSheaf (structureSheaf 𝕜 E M)) (a : M) [IsNoetherianRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)] (h : Ideal.map (algebraMap (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a))) (I.stalkIdeal a) = Ideal.map (algebraMap (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (AdicCompletion (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ↑((structureSheaf 𝕜 E M).presheaf.stalk a))) (J.stalkIdeal a)) : ∃ (U : TopologicalSpace.Opens M), a ∈ U ∧ ∀ b ∈ U, I.stalkIdeal b = J.stalkIdeal b

Kollár's geometric form of Krull's intersection theorem [Kol07, Definition 55], "if Ẑ_x = Ŵ_x then Z ∩ U = W ∩ U": two locally finitely generated ideal sheaves with equal completions at a agree on a neighbourhood of a, for 𝒪_{M,a} Noetherian — Kollár's hypothesis, carried explicitly (the instance for the analytic stalk is proved in Hironaka/Manifold/Germ/StalkNoetherian.lean).