Structure sheaf of a complex manifold

Stream: maths

[Heather Macbeth]

I just opened #19094, building the sheaf of functions on a manifold satisfying a docs#structure_groupoid.local_invariant_prop, for example the sheaf of holomorphic functions on a complex manifold.

Now is the time to make a decision we have put off for a while: with complex manifolds, should we work with "differentiable", "ℂ-smooth" or analytic functions? The point: these are mathematically equivalent conditions.

• Analytic is the strongest, but we don't have any differential geometry machinery (e.g. the associated structure groupoid) built up there.
• Smooth has the most currently-available differential geometry machinery.
• Differentiable is the category in which Yury has developed the complex analysis library

For now I wrote the PR for "differentiable", but I don't mind switching if we can come to an agreement.

cc @Sebastien Gouezel @Yury G. Kudryashov @Patrick Massot

[Patrick Massot]

Proving stuff should be easier with the a priori weaker differentiable assumption, right?

[Jireh Loreaux]

I would imagine so, as long as we have the results to "upgrade" differentiable to one of the variants when necessary. And I think we have at least the analytic one already.

[Johan Commelin]

Patrick Massot said:

Proving stuff should be easier with the a priori weaker differentiable assumption, right?

But it also means that your assumptions will usually be weaker. So probably it will be good to have some amount of API.

[Heather Macbeth]

We (@Johan Commelin @Oliver Nash @Adam Topaz @Moritz Doll) have been talking about this in Banff, and one point is that since the underlying manifolds basically have to be $C^\infty$ (being the only category in which we currently have enough machinery), it is philosophically more consistent to consider $C^\infty$ functions too.

[Heather Macbeth]

(It's easy enough to make a constructor for a $C^\infty$ thing from a differentiable thing.)

[Patrick Massot]

Ok, you should try it then.

[Yury G. Kudryashov]

Why can't we reuse infinitely smooth manifolds with complex as the base field?

[Yury G. Kudryashov]

With a constructor from differentiable and an implication about analytic

[Heather Macbeth]

Indeed, this is what I meant by the second option I listed, the ℂ-smooth option. And I think it's my favourite option (even though it's not how I did it currently).

[Sebastien Gouezel]

Using smooth is also my favorite option. In this way, the tangent bundle to a complex manifold is also a complex manifold, without having to do any additional work.

[Yury G. Kudryashov]

My opinion in more details:

1. For now, reusing smooth manifolds code seems like the best option.
2. If we ever decide to add real analytic manifolds, then we can switch to that typeclass (or add an instance saying that a smooth complex manifold is a complex analytic manifold; this will create a cycle but I hope we'll use Lean 4 by then).

[Heather Macbeth]

OK, thanks! Let's stick with ℂ-smooth at least in the medium term; someday someone will build (real- and complex-)analytic manifolds and we can revisit.