Finite vanishing order of holomorphic germs

The powers of the ideal of holomorphic germs vanishing at a point of a complex curve have zero intersection. Consequently every nonzero germ lies in a unique last power of that ideal. This supplies finite, intrinsic local multiplicities for divisor sheaves: the multiplicity is measured without choosing a preferred coordinate.

The analytic input is finite vanishing order in a local chart. A germ divisible by the n-th power of the centered coordinate has analytic order at least n; a nonzero analytic germ cannot satisfy this for every n. No compactness or connectedness is required.

References

• Otto Forster, Lectures on Riemann Surfaces, §§1, 6 and 16.

The proof uses Mathlib's natCast_le_analyticOrderAt and the coordinate-division theorem OpenPartialHomeomorph.ker_eval_eq_span_holomorphicCoordinateGerm.

theorem OpenPartialHomeomorph.exists_not_dvd_holomorphicCoordinateGerm_pow {X : Type} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (e : OpenPartialHomeomorph X ℂ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (x : X) (hx : x ∈ e.source) {f : ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X).presheaf.stalk x)} (hf : f ≠ 0) : ∃ (n : ℕ), ¬e.holomorphicCoordinateGerm he x hx ^ n ∣ f

A nonzero holomorphic germ is not divisible by arbitrarily high powers of a centered chart coordinate.

@[simp]

theorem OpenPartialHomeomorph.holomorphicCoordinateGerm_pow_mem_pow_ker_eval_iff {X : Type} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (e : OpenPartialHomeomorph X ℂ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (x : X) (hx : x ∈ e.source) (n j : ℕ) : e.holomorphicCoordinateGerm he x hx ^ n ∈ RingHom.ker (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf ℂ ℂ) X x) ^ j ↔ j ≤ n

The n-th power of a centered coordinate vanishes to exactly order n, measured by powers of the evaluation kernel. In particular every finite multiplicity occurs.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.iInf_pow_ker_eval_eq_bot {X : Type} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (x : X) : ⨅ (n : ℕ), RingHom.ker (eval (modelWithCornersSelf ℂ ℂ) X x) ^ n = ⊥

The vanishing ideal of holomorphic germs on a complex curve is separated: a germ in every power of that ideal is zero.

theorem TauCeti.holomorphicStructureSheaf.existsUnique_mem_pow_ker_eval_notMem_succ {X : Type} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (x : X) {f : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X).presheaf.stalk x)} (hf : f ≠ 0) : ∃! n : ℕ, f ∈ RingHom.ker (eval (modelWithCornersSelf ℂ ℂ) X x) ^ n ∧ f ∉ RingHom.ker (eval (modelWithCornersSelf ℂ ℂ) X x) ^ (n + 1)

A nonzero holomorphic germ has a unique finite vanishing multiplicity, characterized intrinsically by consecutive powers of the evaluation kernel.