Maximal-ideal separatedness of holomorphic stalks

Let X be a complex analytic manifold modelled without boundary on a complex normed space E. This file proves that the stalk (holomorphicStructureSheaf 𝓘(ℂ, E) X).presheaf.stalk x is separated (IsHausdorff) with respect to its maximal ideal: a holomorphic germ lying in every power of the maximal ideal is zero.

The argument requires neither finite-dimensionality of E nor Noetherianity of the stalk (so Krull's intersection theorem is not needed). If a germ s lies in 𝔪_x ^ n, restricting any local representative of s read in a holomorphic chart e to any complex line z ↦ e x + z • v through e x produces a one-variable holomorphic function vanishing to order at least n at 0. Lying in 𝔪_x ^ n for every n therefore forces infinite analytic order at 0 along every complex line, hence vanishing near e x by one-variable analytic continuation along radial discs (AnalyticAt.eventuallyEq_zero_iff_forall_eventuallyEq_zero_comp_add_smul). (For complex curves E = ℂ, TauCeti.Geometry.Manifold.Complex.StructureSheaf.Order obtains separatedness from local coordinate division instead.)

Main results

• OpenPartialHomeomorph.iInf_pow_ker_eval_eq_bot: at the center x of any chart e ∈ maximalAtlas 𝓘(ℂ, E) ω X, the intersection of all powers of RingHom.ker (eval 𝓘(ℂ, E) X x) is ⊥.
• OpenPartialHomeomorph.isHausdorff_maximalIdeal_stalk: the stalk at x is IsHausdorff with respect to its maximal ideal.
• TauCeti.holomorphicStructureSheaf.instIsHausdorffMaximalIdealStalkOfOmega: IsHausdorff instance on stalks of any complex analytic manifold [IsManifold 𝓘(ℂ, E) ω X], with no finite-dimensionality assumption on E.
• TauCeti.holomorphicStructureSheaf.instIsHausdorffMaximalIdealStalk: IsHausdorff instance on stalks of any finite-dimensional complex manifold [FiniteDimensional ℂ E] [IsManifold 𝓘(ℂ, E) 1 X].

References

• J.-P. Demailly, Complex Analytic and Differential Geometry, Chapter II, §3.
• R. C. Gunning and H. Rossi, Analytic Functions of Several Complex Variables, Chapter II.

theorem OpenPartialHomeomorph.iInf_pow_ker_eval_eq_bot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ E) ⊤ X) {x : X} (hx : x ∈ e.source) : ⨅ (n : ℕ), RingHom.ker (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf ℂ E) X x) ^ n = ⊥

At the center of a complex analytic chart, the powers of the evaluation kernel have trivial intersection.

theorem OpenPartialHomeomorph.isHausdorff_maximalIdeal_stalk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] (e : OpenPartialHomeomorph X E) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ E) ⊤ X) {x : X} (hx : x ∈ e.source) : IsHausdorff (IsLocalRing.maximalIdeal ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x)) ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x)

At the center of a complex analytic chart, the holomorphic stalk is Hausdorff with respect to its maximal ideal.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.iInf_pow_ker_eval_eq_bot_of_omega {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf ℂ E) ⊤ X] (x : X) : ⨅ (n : ℕ), RingHom.ker (eval (modelWithCornersSelf ℂ E) X x) ^ n = ⊥

On a complex analytic manifold (without assuming finite-dimensionality), the powers of the evaluation kernel on any holomorphic stalk have trivial intersection.

theorem TauCeti.holomorphicStructureSheaf.iInf_pow_maximalIdeal_stalk_eq_bot_of_omega {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf ℂ E) ⊤ X] (x : X) : ⨅ (n : ℕ), IsLocalRing.maximalIdeal ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x) ^ n = ⊥

On a complex analytic manifold (without assuming finite-dimensionality), the powers of the maximal ideal of any holomorphic stalk have trivial intersection.

instance TauCeti.holomorphicStructureSheaf.instIsHausdorffMaximalIdealStalkOfOmega {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf ℂ E) ⊤ X] (x : X) : IsHausdorff (IsLocalRing.maximalIdeal ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x)) ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x)

On a complex analytic manifold (without assuming finite-dimensionality), every holomorphic stalk is Hausdorff with respect to its maximal ideal.

theorem TauCeti.holomorphicStructureSheaf.iInf_pow_maximalIdeal_stalk_eq_bot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf ℂ E) 1 X] (x : X) : ⨅ (n : ℕ), IsLocalRing.maximalIdeal ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x) ^ n = ⊥

On a finite-dimensional complex manifold, the powers of the maximal ideal of any holomorphic stalk have trivial intersection.

instance TauCeti.holomorphicStructureSheaf.instIsHausdorffMaximalIdealStalk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {X : Type} [TopologicalSpace X] [ChartedSpace E X] [IsManifold (modelWithCornersSelf ℂ E) 1 X] (x : X) : IsHausdorff (IsLocalRing.maximalIdeal ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x)) ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ E) X).presheaf.stalk x)

On a finite-dimensional complex manifold, every holomorphic stalk is Hausdorff with respect to its maximal ideal.