Local rings of holomorphic germs

A germ of a holomorphic function is invertible exactly when its value at the base point is nonzero. Consequently the stalks of the holomorphic structure sheaf are local rings, their maximal ideals consist of the germs vanishing at the base point, and their residue fields are canonically ℂ via evaluation. These are the local algebra needed for local equations of divisors and their invertible sheaves on complex curves.

The results hold for any complex model with corners; compactness, connectedness, and a manifold regularity assumption are unnecessary.

The unit criterion adapts Heather Macbeth's smoothSheafCommRing.isUnit_stalk_iff in Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean to the analytic structure sheaf.

References

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

@[simp]

theorem TauCeti.holomorphicStructureSheaf.isUnit_stalk_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) (X : Type) [TopologicalSpace X] [ChartedSpace H X] {x : X} (f : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)) : IsUnit f ↔ (eval I X x) f ≠ 0

A holomorphic germ is a unit exactly when its value at the base point is nonzero.

theorem TauCeti.holomorphicStructureSheaf.nonunits_stalk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) (X : Type) [TopologicalSpace X] [ChartedSpace H X] (x : X) : nonunits ↑((holomorphicStructureSheaf I X).presheaf.stalk x) = ↑(RingHom.ker (eval I X x))

The nonunits of a holomorphic stalk are exactly the kernel of evaluation.

instance TauCeti.holomorphicStructureSheaf.instIsLocalRingStalk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) (X : Type) [TopologicalSpace X] [ChartedSpace H X] (x : X) : IsLocalRing ↑((holomorphicStructureSheaf I X).presheaf.stalk x)

Stalks of the holomorphic structure sheaf are local rings.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.maximalIdeal_stalk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) (X : Type) [TopologicalSpace X] [ChartedSpace H X] (x : X) : IsLocalRing.maximalIdeal ↑((holomorphicStructureSheaf I X).presheaf.stalk x) = RingHom.ker (eval I X x)

The maximal ideal of a holomorphic stalk consists of the germs vanishing at its base point.

noncomputable def TauCeti.holomorphicStructureSheaf.residueFieldEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) (X : Type) [TopologicalSpace X] [ChartedSpace H X] (x : X) : IsLocalRing.ResidueField ↑((holomorphicStructureSheaf I X).presheaf.stalk x) ≃+* ℂ

Evaluation identifies the residue field of a holomorphic stalk with ℂ.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.residueFieldEquiv_residue {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) (X : Type) [TopologicalSpace X] [ChartedSpace H X] (x : X) (f : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)) : (residueFieldEquiv I X x) ((IsLocalRing.residue ↑((holomorphicStructureSheaf I X).presheaf.stalk x)) f) = (eval I X x) f

The residue-field comparison sends the residue of a germ to its value at the base point.