Holomorphic stalks are integral domains

On a finite-dimensional complex manifold without boundary, holomorphic sections over a preconnected open set have no zero divisors, by the analytic identity theorem in charts. Every point has a basis of connected open neighborhoods, so the same holds for the stalk of the holomorphic structure sheaf. Thus a holomorphic germ embeds in its fraction field, providing the local algebra for meromorphic functions and local analytic equations. The existing section and stalk comparisons transfer these properties to Mathlib's native complex-smooth structure sheaf as well.

Neither the manifold nor an arbitrary domain of sections is required to be connected: only the sectionwise statement needs preconnectedness of its domain. Compactness, separation and second countability are not needed. Zero-dimensional models are included.

References

• Lars Hörmander, An Introduction to Complex Analysis in Several Variables, §2.2.
• Otto Forster, Lectures on Riemann Surfaces, §§1, 6 and 16, for the curve case.
• The section argument uses ContMDiff.eq_of_eventuallyEq; the passage to stalks uses TopCat.Presheaf.stalk_noZeroDivisors_of_hasBasis.

instance TauCeti.holomorphicStructureSheaf.sectionsNoZeroDivisors {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {X : Type} [TopologicalSpace X] [ChartedSpace H X] [IsManifold I 1 X] (U : TopologicalSpace.Opens X) [PreconnectedSpace ↥U] : NoZeroDivisors ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U))

Holomorphic sections on a preconnected open set have no zero divisors.

instance TauCeti.holomorphicStructureSheaf.stalkIsDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {X : Type} [TopologicalSpace X] [ChartedSpace H X] [IsManifold I 1 X] (x : X) : IsDomain ↑((holomorphicStructureSheaf I X).presheaf.stalk x)

The stalk of holomorphic functions at any point of a finite-dimensional complex manifold without boundary is an integral domain.

instance TauCeti.holomorphicStructureSheaf.smoothSectionsNoZeroDivisors {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {X : Type} [TopologicalSpace X] [ChartedSpace H X] [IsManifold I 1 X] (U : TopologicalSpace.Opens X) [PreconnectedSpace ↥U] : NoZeroDivisors ↑((smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).obj.obj (Opposite.op U))

Complex-smooth sections on a preconnected open set have no zero divisors. This is the native smooth-sheaf version of sectionsNoZeroDivisors, over ℂ, not over ℝ.

instance TauCeti.holomorphicStructureSheaf.smoothStalkIsDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {X : Type} [TopologicalSpace X] [ChartedSpace H X] [IsManifold I 1 X] (x : X) : IsDomain ↑((smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).presheaf.stalk x)

A stalk of Mathlib's complex-smooth structure sheaf on a finite-dimensional complex manifold without boundary is an integral domain, via its comparison with holomorphic germs.