Holomorphic and complex-smooth structure sheaves

On a finite-dimensional boundaryless complex manifold, complex C^∞ functions are holomorphic and hence complex analytic. Thus the C^ω holomorphic structure sheaf agrees with Mathlib's C^∞ structure sheaf over ℂ, not the sheaf of real-smooth functions.

We identify sections and sheaves, preserve evaluation on stalks, and compare pullback by holomorphic maps. This allows the holomorphic sheaf to use Mathlib's existing native manifold locally ringed space and its morphisms, rather than a parallel construction. No compactness, Hausdorffness or second-countability assumption is needed.

The comparison uses the native holomorphic regularity theorem MDifferentiable.contMDiff. The locally ringed-space construction being compared is Heather Macbeth's ChartedSpace.locallyRingedSpace in Mathlib.

References

• Otto Forster, Lectures on Riemann Surfaces, §§1 and 6, for holomorphic functions and their local rings.

noncomputable def TauCeti.holomorphicStructureSheaf.smoothSectionsEquiv {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) : ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U)) ≃+* ↑((smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).obj.obj (Opposite.op U))

Holomorphic sections are exactly the complex-smooth sections, with the same values.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.smoothSectionsEquiv_apply {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) (s : ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U))) (x : ↥U) : ↑((smoothSectionsEquiv I X U) s) x = toFun I X (Opposite.op U) s x

The section comparison preserves values.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.smoothSectionsEquiv_symm_apply {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) (s : ↑((smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).obj.obj (Opposite.op U))) (x : ↥U) : toFun I X (Opposite.op U) ((smoothSectionsEquiv I X U).symm s) x = ↑s x

The inverse section comparison preserves values.

noncomputable def TauCeti.holomorphicStructureSheaf.smoothSheafIso {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] : holomorphicStructureSheaf I X ≅ (ChartedSpace.locallyRingedSpace I X).sheaf

The holomorphic structure sheaf is the complex-smooth structure sheaf used by Mathlib's native manifold locally ringed space.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.smoothSheafIso_hom_app {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) : (smoothSheafIso I X).hom.hom.app (Opposite.op U) = CommRingCat.ofHom (smoothSectionsEquiv I X U).toRingHom

On each open subset the sheaf comparison is the section comparison.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.smoothSheafIso_inv_app {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) : (smoothSheafIso I X).inv.hom.app (Opposite.op U) = CommRingCat.ofHom (smoothSectionsEquiv I X U).symm.toRingHom

On each open subset the inverse comparison is the inverse section comparison.

noncomputable def TauCeti.holomorphicStructureSheaf.smoothStalkIso {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) : (holomorphicStructureSheaf I X).presheaf.stalk x ≅ (smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).presheaf.stalk x

The induced isomorphism between holomorphic germs and complex-smooth germs.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.smoothStalkIso_hom_germ {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) (U : TopologicalSpace.Opens X) (hx : x ∈ U) (s : ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (smoothStalkIso I X x).hom) ((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf I X).presheaf.germ U x hx)) s) = (CategoryTheory.ConcreteCategory.hom ((smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).presheaf.germ U x hx)) ((smoothSectionsEquiv I X U) s)

The stalk comparison sends the germ of a section to the germ of its comparison.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.smoothStalkIso_inv_germ {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) (U : TopologicalSpace.Opens X) (hx : x ∈ U) (s : ↑((smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).obj.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (smoothStalkIso I X x).inv) ((CategoryTheory.ConcreteCategory.hom ((smoothSheafCommRing I (modelWithCornersSelf ℂ ℂ) X ℂ).presheaf.germ U x hx)) s) = (CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf I X).presheaf.germ U x hx)) ((smoothSectionsEquiv I X U).symm s)

The inverse stalk comparison takes the germ of a complex-smooth section to its holomorphic germ.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.eval_smoothStalkIso_hom {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) (s : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)) : (smoothSheafCommRing.eval I (modelWithCornersSelf ℂ ℂ) X ℂ x) ((CategoryTheory.ConcreteCategory.hom (smoothStalkIso I X x).hom) s) = (eval I X x) s

The stalk comparison preserves the value of a germ at its base point.

theorem TauCeti.holomorphicStructureSheaf.smoothSheafIso_hom_naturality {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] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℂ E'] [FiniteDimensional ℂ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℂ E' H'} [J.Boundaryless] {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] [IsManifold J 1 Y] (f : X → Y) (hf : ContMDiff I J ⊤ f) : CategoryTheory.CategoryStruct.comp (homOfContMDiff I X f hf) ((TopCat.Sheaf.pushforward CommRingCat (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).map (smoothSheafIso I X).hom) = CategoryTheory.CategoryStruct.comp (smoothSheafIso J Y).hom (ContMDiff.smoothSheafCommRingHom J Y f ⋯)

The sheaf comparison intertwines holomorphic pullback with Mathlib's complex-smooth pullback. Thus both give the same morphisms on the native manifold carrier.