The holomorphic structure sheaf #
The holomorphic structure sheaf of a complex manifold assigns to an open set U the ring
of complex analytic maps U → ℂ. Its sections are Mathlib's ContMDiffMap at regularity
ω, so their pointwise ring and complex vector space structures are reused directly.
The same restriction maps give a sheaf of complex vector spaces, suitable for cohomology.
On a complex curve, these sections are precisely the manifold-differentiable functions.
On a compact connected complex manifold, the constant-section map is an algebra
isomorphism ℂ ≃ₐ[ℂ] H⁰(X, 𝒪). The inverse is evaluation at any point, independently of
which point is chosen. In particular, the space of global sections has dimension one.
The function coercions and algebra instance use the bundled analytic-map representation.
Pointwise computation is provided by section evaluation lemmas.
The sheaf of modules has exactly the same underlying presheaf of functions.
Evaluation of germs gives a surjective ring homomorphism from each stalk to ℂ.
Holomorphic maps induce morphisms to the pushed-forward structure sheaf by precomposition,
and pull back holomorphic germs (stalkPrecomp), functorially and preserving their values.
The sheaf construction follows smoothSheafCommRing in
Mathlib/Geometry/Manifold/Sheaf/Smooth.lean by Heather Macbeth and Adam Topaz, using
StructureGroupoid.LocalInvariantProp.sheaf at analytic rather than smooth regularity.
The stalk evaluation and precomposition constructions follow smoothSheafCommRing.evalHom
and ContMDiff.smoothSheafCommRingHom in the same file.
The global-sections computation uses Mathlib's
MDifferentiable.exists_eq_const_of_compactSpace (the maximum principle).
For the classical structure sheaf and its global sections, see Otto Forster,
Lectures on Riemann Surfaces, §§1, 6.
noncomputable def
TauCeti.holomorphicStructureSheaf
{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]
:
The holomorphic structure sheaf of a complex manifold, as a sheaf of commutative rings.
Its sections on U are the complex analytic maps U → ℂ.
Instances For
theorem
TauCeti.holomorphicStructureSheaf.obj_eq
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
:
(holomorphicStructureSheaf I X).obj.obj U = ↧(ContMDiffMap I (modelWithCornersSelf ℂ ℂ) ↥(Opposite.unop U) ℂ ⊤)
Sections of the structure sheaf are bundled complex analytic functions.
noncomputable def
TauCeti.holomorphicStructureSheaf.toFun
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
:
↑((holomorphicStructureSheaf I X).obj.obj U) → ↥(Opposite.unop U) → ℂ
The function underlying a section of the structure sheaf.
Instances For
@[instance_reducible]
noncomputable instance
TauCeti.holomorphicStructureSheaf.instCoeFunCarrierObjOppositeOpensCarrierOfCommRingCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnopComplex
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
:
CoeFun ↑((holomorphicStructureSheaf I X).obj.obj U) fun (x : ↑((holomorphicStructureSheaf I X).obj.obj U)) =>
↥(Opposite.unop U) → ℂ
@[instance_reducible]
noncomputable instance
TauCeti.holomorphicStructureSheaf.instAlgebraComplexCarrierObjOppositeOpensCarrierOfCommRingCatObjFunctorIsSheafGrothendieckTopology
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
:
Algebra ℂ ↑((holomorphicStructureSheaf I X).obj.obj U)
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.zero_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.one_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.add_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f g : ↑((holomorphicStructureSheaf I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.mul_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f g : ↑((holomorphicStructureSheaf I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.pow_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f : ↑((holomorphicStructureSheaf I X).obj.obj U))
(n : ℕ)
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.neg_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f : ↑((holomorphicStructureSheaf I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.sub_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f g : ↑((holomorphicStructureSheaf I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.smul_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(c : ℂ)
(f : ↑((holomorphicStructureSheaf I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
theorem
TauCeti.holomorphicStructureSheaf.ext
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
{f g : ↑((holomorphicStructureSheaf I X).obj.obj U)}
(h : ∀ (x : ↥(Opposite.unop U)), toFun I X U f x = toFun I X U g x)
:
Sections of the structure sheaf are equal if they agree at every point.
theorem
TauCeti.holomorphicStructureSheaf.ext_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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
{f g : ↑((holomorphicStructureSheaf I X).obj.obj U)}
:
theorem
TauCeti.holomorphicStructureSheaf.contMDiff
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f : ↑((holomorphicStructureSheaf I X).obj.obj U))
:
A section of the structure sheaf is complex analytic on its domain.
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.map_apply
{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]
{U V : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(h : U ⟶ V)
(f : ↑((holomorphicStructureSheaf I X).obj.obj U))
(x : ↥(Opposite.unop V))
:
toFun I X V ((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf I X).obj.map h)) f) x = toFun I X U f (TopologicalSpace.Opens.inclusion ⋯ x)
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.algebraMap_apply
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
(c : ℂ)
(x : ↥(Opposite.unop U))
:
theorem
TauCeti.holomorphicStructureSheaf.mdifferentiable
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f : ↑((holomorphicStructureSheaf I X).obj.obj U))
:
MDiff (toFun I X U f)
A section of the structure sheaf is holomorphic on its domain.
noncomputable def
TauCeti.holomorphicStructureSheaf.ofContMDiff
{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]
{U : TopologicalSpace.Opens X}
(f : ↥U → ℂ)
(hf : ContMDiff I (modelWithCornersSelf ℂ ℂ) ⊤ f)
:
↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U))
Complex analytic functions give sections of the structure sheaf for any complex model.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.ofContMDiff_apply
{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]
{U : TopologicalSpace.Opens X}
(f : ↥U → ℂ)
(hf : ContMDiff I (modelWithCornersSelf ℂ ℂ) ⊤ f)
(x : ↥U)
:
noncomputable def
TauCeti.holomorphicStructureSheaf.ofMDifferentiable
{X : Type}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) 1 X]
{U : TopologicalSpace.Opens X}
(f : ↥U → ℂ)
(hf : MDiff f)
:
↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X).obj.obj (Opposite.op U))
Holomorphic functions on a complex curve give sections of its structure sheaf.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.ofMDifferentiable_apply
{X : Type}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) 1 X]
{U : TopologicalSpace.Opens X}
(f : ↥U → ℂ)
(hf : MDiff f)
(x : ↥U)
:
noncomputable def
TauCeti.holomorphicStructureSheaf.evalHom
{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)
:
Evaluation of germs at their base point, as a morphism of commutative rings.
Instances For
noncomputable def
TauCeti.holomorphicStructureSheaf.eval
{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)
:
The ring homomorphism evaluating a holomorphic germ at its base point.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.germ_evalHom
{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]
(U : TopologicalSpace.Opens X)
(x : X)
(hx : x ∈ U)
:
CategoryTheory.CategoryStruct.comp ((holomorphicStructureSheaf I X).presheaf.germ U x hx) (evalHom I X x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CommRingCat.ofHom (ContMDiffMap.evalRingHom ⟨x, hx⟩))
Evaluation after the germ map is evaluation on the original section.
theorem
TauCeti.holomorphicStructureSheaf.germ_evalHom_assoc
{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]
(U : TopologicalSpace.Opens X)
(x : X)
(hx : x ∈ U)
{Z : CommRingCat}
(h : ↧ℂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((holomorphicStructureSheaf I X).presheaf.germ U x hx)
(CategoryTheory.CategoryStruct.comp (evalHom I X x) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (ContMDiffMap.evalRingHom ⟨x, hx⟩)) h)
Evaluation after the germ map is evaluation on the original section.
theorem
TauCeti.holomorphicStructureSheaf.evalHom_germ
{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]
(U : TopologicalSpace.Opens X)
(x : X)
(hx : x ∈ U)
(f : ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (evalHom I X x))
((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf I X).presheaf.germ U x hx)) f) = toFun I X (Opposite.op U) f ⟨x, hx⟩
Evaluation of a germ, in the categorical form of the stalk evaluation map.
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.eval_germ
{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]
(U : TopologicalSpace.Opens X)
(x : X)
(hx : x ∈ U)
(f : ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U)))
:
(eval I X x) ((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf I X).presheaf.germ U x hx)) f) = toFun I X (Opposite.op U) f ⟨x, hx⟩
Evaluating the germ of a section returns its value at the base point.
theorem
TauCeti.holomorphicStructureSheaf.eval_surjective
{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)
:
Function.Surjective ⇑(eval I X x)
Every complex number is the value of a constant holomorphic germ.
instance
TauCeti.holomorphicStructureSheaf.instNontrivialCarrierStalkCommRingCatPresheaf
{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)
:
Nontrivial ↑((holomorphicStructureSheaf I X).presheaf.stalk x)
noncomputable def
TauCeti.holomorphicStructureSheaf.precomp
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
(U : (TopologicalSpace.Opens Y)ᵒᵖ)
:
↑((holomorphicStructureSheaf J Y).obj.obj U) →+* ↑((holomorphicStructureSheaf I X).obj.obj
(Opposite.op
((TopologicalSpace.Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).obj (Opposite.unop U))))
Precomposition by a complex analytic map, on the rings of holomorphic sections.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.precomp_apply
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
(U : (TopologicalSpace.Opens Y)ᵒᵖ)
(g : ↑((holomorphicStructureSheaf J Y).obj.obj U))
(x : ↥((TopologicalSpace.Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).obj (Opposite.unop U)))
:
toFun I X
(Opposite.op
((TopologicalSpace.Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).obj (Opposite.unop U)))
((precomp I X f hf U) g) x = toFun J Y U g ⟨f ↑x, ⋯⟩
noncomputable def
TauCeti.holomorphicStructureSheaf.homOfContMDiff
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
:
holomorphicStructureSheaf J Y ⟶ (TopCat.Sheaf.pushforward CommRingCat (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).obj
(holomorphicStructureSheaf I X)
A complex analytic map induces a morphism 𝒪_Y ⟶ f_*𝒪_X by precomposition.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.homOfContMDiff_app
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
(U : (TopologicalSpace.Opens Y)ᵒᵖ)
:
noncomputable def
TauCeti.holomorphicStructureSheaf.homOfMDifferentiable
{X Y : Type}
[TopologicalSpace X]
[TopologicalSpace Y]
[ChartedSpace ℂ X]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) 1 X]
[IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y]
(f : X → Y)
(hf : MDiff f)
:
holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) Y ⟶ (TopCat.Sheaf.pushforward CommRingCat (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).obj
(holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) X)
A holomorphic map between complex curves induces a morphism of structure sheaves.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.homOfMDifferentiable_app
{X Y : Type}
[TopologicalSpace X]
[TopologicalSpace Y]
[ChartedSpace ℂ X]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) 1 X]
[IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y]
(f : X → Y)
(hf : MDiff f)
(U : (TopologicalSpace.Opens Y)ᵒᵖ)
:
(homOfMDifferentiable f hf).hom.app U = CommRingCat.ofHom (precomp (modelWithCornersSelf ℂ ℂ) X f ⋯ U)
noncomputable def
TauCeti.holomorphicStructureSheaf.stalkPrecomp
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
(x : X)
:
↑((holomorphicStructureSheaf J Y).presheaf.stalk (f x)) →+* ↑((holomorphicStructureSheaf I X).presheaf.stalk x)
A complex analytic map f pulls holomorphic germs at f x back to holomorphic germs at x,
by precomposition: the stalk map of homOfContMDiff.
Instances For
theorem
TauCeti.holomorphicStructureSheaf.stalkPrecomp_germ
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
(x : X)
(U : TopologicalSpace.Opens Y)
(hx : f x ∈ U)
(g : ↑((holomorphicStructureSheaf J Y).obj.obj (Opposite.op U)))
:
(stalkPrecomp I X f hf x)
((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf J Y).presheaf.germ U (f x) hx)) g) = (CategoryTheory.ConcreteCategory.hom
((holomorphicStructureSheaf I X).presheaf.germ
((TopologicalSpace.Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ })).obj U) x hx))
((precomp I X f hf (Opposite.op U)) g)
The pullback of the germ of a section is the germ of the precomposed section.
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.eval_stalkPrecomp
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
(x : X)
(s : ↑((holomorphicStructureSheaf J Y).presheaf.stalk (f x)))
:
Pulling a germ back along f preserves its value: the value at x of the pullback is the
value at f x of the germ.
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.stalkPrecomp_id
{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)
:
Pulling germs back along the identity does nothing.
theorem
TauCeti.holomorphicStructureSheaf.stalkPrecomp_comp
{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]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace ℂ E']
{H' : Type u_4}
[TopologicalSpace H']
{J : ModelWithCorners ℂ E' H'}
{Y : Type}
[TopologicalSpace Y]
[ChartedSpace H' Y]
{E'' : Type u_5}
[NormedAddCommGroup E'']
[NormedSpace ℂ E'']
{H'' : Type u_6}
[TopologicalSpace H'']
{K : ModelWithCorners ℂ E'' H''}
{Z : Type}
[TopologicalSpace Z]
[ChartedSpace H'' Z]
(g : Y → Z)
(hg : ContMDiff J K ⊤ g)
(f : X → Y)
(hf : ContMDiff I J ⊤ f)
(x : X)
(s : ↑((holomorphicStructureSheaf K Z).presheaf.stalk (g (f x))))
:
Pulling germs back along g ∘ f is pulling back along g and then along f.
noncomputable def
TauCeti.holomorphicStructureSheafModules
{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]
:
TopCat.Sheaf (ModuleCat ℂ) ↧X
The holomorphic structure sheaf viewed as a sheaf of complex vector spaces.
Instances For
theorem
TauCeti.holomorphicStructureSheafModules.obj_eq
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
:
Sections of the module sheaf are the same complex vector spaces as the ring sections.
@[instance_reducible]
noncomputable instance
TauCeti.holomorphicStructureSheafModules.instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
:
CoeFun ↑((holomorphicStructureSheafModules I X).obj.obj U)
fun (x : ↑((holomorphicStructureSheafModules I X).obj.obj U)) => ↥(Opposite.unop U) → ℂ
noncomputable def
TauCeti.holomorphicStructureSheafModules.sectionsLinearEquiv
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
:
↑((holomorphicStructureSheafModules I X).obj.obj U) ≃ₗ[ℂ] ↑((holomorphicStructureSheaf I X).obj.obj U)
Ring sections and module sections have the same complex vector space structure.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.sectionsLinearEquiv_apply
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
(f : ↑((holomorphicStructureSheafModules I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.sectionsLinearEquiv_symm_apply
{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]
(U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ)
(f : ↑((holomorphicStructureSheaf I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
theorem
TauCeti.holomorphicStructureSheafModules.contMDiff
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f : ↑((holomorphicStructureSheafModules I X).obj.obj U))
:
A section of the module sheaf is complex analytic on its domain.
theorem
TauCeti.holomorphicStructureSheafModules.mdifferentiable
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f : ↑((holomorphicStructureSheafModules I X).obj.obj U))
:
A section of the module sheaf is holomorphic on its domain.
noncomputable def
TauCeti.holomorphicStructureSheafModules.ofContMDiff
{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]
{U : TopologicalSpace.Opens X}
(f : ↥U → ℂ)
(hf : ContMDiff I (modelWithCornersSelf ℂ ℂ) ⊤ f)
:
↑((holomorphicStructureSheafModules I X).obj.obj (Opposite.op U))
Complex analytic functions give sections of the module sheaf for any complex model.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.ofContMDiff_apply
{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]
{U : TopologicalSpace.Opens X}
(f : ↥U → ℂ)
(hf : ContMDiff I (modelWithCornersSelf ℂ ℂ) ⊤ f)
(x : ↥U)
:
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.zero_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.add_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f g : ↑((holomorphicStructureSheafModules I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U (f + g) x = instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U f x + instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U g x
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.neg_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f : ↑((holomorphicStructureSheafModules I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.sub_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(f g : ↑((holomorphicStructureSheafModules I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U (f - g) x = instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U f x - instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U g x
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.smul_apply
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(c : ℂ)
(f : ↑((holomorphicStructureSheafModules I X).obj.obj U))
(x : ↥(Opposite.unop U))
:
theorem
TauCeti.holomorphicStructureSheafModules.ext
{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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
{f g : ↑((holomorphicStructureSheafModules I X).obj.obj U)}
(h :
∀ (x : ↥(Opposite.unop U)),
instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U f x = instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U g x)
:
Sections of the module sheaf are equal if they agree at every point.
theorem
TauCeti.holomorphicStructureSheafModules.ext_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]
{U : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
{f g : ↑((holomorphicStructureSheafModules I X).obj.obj U)}
:
f = g ↔ ∀ (x : ↥(Opposite.unop U)),
instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U f x = instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U g x
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.map_apply
{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]
{U V : (TopologicalSpace.Opens ↑↧X)ᵒᵖ}
(h : U ⟶ V)
(f : ↑((holomorphicStructureSheafModules I X).obj.obj U))
(x : ↥(Opposite.unop V))
:
instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X V ((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheafModules I X).obj.map h)) f) x = instCoeFunCarrierComplexObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyForallSubtypeMemUnop._aux_1
I X U f (TopologicalSpace.Opens.inclusion ⋯ x)
theorem
TauCeti.holomorphicStructureSheafModules.forget_eq
{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]
:
Forgetting the ring or module structure gives the same presheaf of functions.
theorem
TauCeti.holomorphicStructureSheaf.algebraMap_bijective
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
:
Function.Bijective ⇑(algebraMap ℂ ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op ⊤)))
On a nonempty compact connected complex manifold, every global holomorphic section is a unique constant section.
noncomputable def
TauCeti.holomorphicStructureSheaf.globalSectionsEquiv
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
:
Constants identify the global sections of the holomorphic structure sheaf with ℂ.
Instances For
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.globalSectionsEquiv_apply
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
(c : ℂ)
:
(globalSectionsEquiv I X) c = (algebraMap ℂ ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op ⊤))) c
theorem
TauCeti.holomorphicStructureSheaf.globalSectionsEquiv_symm_apply
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
(f : ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op ⊤)))
(x : ↥⊤)
:
Evaluation at any point is the inverse of the constant-section isomorphism.
instance
TauCeti.holomorphicStructureSheaf.instFiniteDimensionalComplexCarrierObjOppositeOpensCarrierOfCommRingCatObjFunctorIsSheafGrothendieckTopologyOpTop
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
:
FiniteDimensional ℂ ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op ⊤))
@[simp]
theorem
TauCeti.holomorphicStructureSheaf.finrank_globalSections
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
:
The space of global holomorphic sections on a nonempty compact connected complex
manifold is one-dimensional over ℂ.
instance
TauCeti.holomorphicStructureSheafModules.instFiniteDimensionalComplexCarrierObjOppositeOpensCarrierOfModuleCatObjFunctorIsSheafGrothendieckTopologyOpTop
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
:
FiniteDimensional ℂ ↑((holomorphicStructureSheafModules I X).obj.obj (Opposite.op ⊤))
@[simp]
theorem
TauCeti.holomorphicStructureSheafModules.finrank_globalSections
{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]
[I.Boundaryless]
[IsManifold I 1 X]
[CompactSpace X]
[PreconnectedSpace X]
[Nonempty X]
:
The module sheaf's global sections on a nonempty compact connected complex manifold form a one-dimensional complex vector space.