A local coordinate generates the ideal of vanishing holomorphic germs

On a complex curve, a chart centered at a point gives a holomorphic germ vanishing at that point. Every holomorphic germ vanishing there is divisible by this coordinate germ. Thus the kernel of stalk evaluation is the principal ideal generated by any centered chart. This is the local defining equation for the ideal sheaf of a point, and the local algebra used in twisting a divisor sheaf by a point.

The division is holomorphic even at the center: Mathlib's dslope extends the difference quotient analytically there. The statements apply to charts of the maximal differentiable atlas and need neither compactness nor connectedness of the curve.

References

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

noncomputable def OpenPartialHomeomorph.holomorphicCoordinateSection {X : Type} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (e : OpenPartialHomeomorph X ℂ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (z : ℂ) : ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X).obj.obj (Opposite.op { carrier := e.source, is_open' := ⋯ }))

The chart coordinate translated by z, as a holomorphic section on the chart source.

@[simp]

theorem OpenPartialHomeomorph.holomorphicCoordinateSection_apply {X : Type} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (e : OpenPartialHomeomorph X ℂ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (z : ℂ) (y : ↥{ carrier := e.source, is_open' := ⋯ }) : TauCeti.holomorphicStructureSheaf.toFun (modelWithCornersSelf ℂ ℂ) X (Opposite.op { carrier := e.source, is_open' := ⋯ }) (e.holomorphicCoordinateSection he z) y = ↑e ↑y - z

The translated coordinate section evaluates at y to e y - z.

noncomputable def OpenPartialHomeomorph.holomorphicCoordinateGerm {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) : ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X).presheaf.stalk x)

The germ at x of a centered chart coordinate.

theorem OpenPartialHomeomorph.holomorphicCoordinateGerm_def {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) : e.holomorphicCoordinateGerm he x hx = (CategoryTheory.ConcreteCategory.hom ((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X).presheaf.germ { carrier := e.source, is_open' := ⋯ } x hx)) (e.holomorphicCoordinateSection he (↑e x))

The centered coordinate germ is the germ of the translated coordinate section.

@[simp]

theorem OpenPartialHomeomorph.eval_holomorphicCoordinateGerm {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) : (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf ℂ ℂ) X x) (e.holomorphicCoordinateGerm he x hx) = 0

The germ of a centered chart coordinate evaluates to zero at its center.

@[simp]

theorem OpenPartialHomeomorph.holomorphicCoordinateGerm_ne_zero {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) : e.holomorphicCoordinateGerm he x hx ≠ 0

A centered coordinate has a nonzero germ: a chart cannot be constant on a neighborhood of its center.

theorem OpenPartialHomeomorph.analyticAt_holomorphicSection_extend_comp_symm {X : Type} [TopologicalSpace X] [ChartedSpace ℂ X] (e : OpenPartialHomeomorph X ℂ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (x : X) (hx : x ∈ e.source) (U : TopologicalSpace.Opens X) (hxU : x ∈ U) (s : ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X).obj.obj (Opposite.op U))) : AnalyticAt ℂ ((Function.extend Subtype.val (TauCeti.holomorphicStructureSheaf.toFun (modelWithCornersSelf ℂ ℂ) X (Opposite.op U) s) fun (x : ↑↧X) => 0) ∘ ↑e.symm) (↑e x)

A holomorphic section, extended by zero outside its domain and written in a local chart, is analytic at every point of its domain in the chart source.

@[simp]

theorem OpenPartialHomeomorph.holomorphicCoordinateGerm_dvd_iff_eval_eq_zero {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)) : e.holomorphicCoordinateGerm he x hx ∣ f ↔ (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf ℂ ℂ) X x) f = 0

A holomorphic germ is divisible by a centered chart coordinate exactly when it vanishes at the center. The quotient is holomorphic also at the coordinate's zero.

theorem OpenPartialHomeomorph.ker_eval_eq_span_holomorphicCoordinateGerm {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) : RingHom.ker (TauCeti.holomorphicStructureSheaf.eval (modelWithCornersSelf ℂ ℂ) X x) = Ideal.span {e.holomorphicCoordinateGerm he x hx}

The ideal of holomorphic germs vanishing at x is generated by any centered local chart coordinate. This identifies the local ideal of a point without a choice of preferred chart.