Meromorphic functions

Stream: maths

[Adam Topaz]

@Heather Macbeth and I have been discussing the sheaf of meromorphic functions.

Here is an initial definition of the sheaf of rings of fractions.

import algebra.category.CommRing
import algebra.category.CommRing.filtered_colimits
import algebra.category.CommRing.limits

import category_theory.sites.sheaf
import category_theory.sites.sheafification
import topology.sheaves.sheaf_condition.sites
import ring_theory.localization
--import category_theory.filtered

open category_theory

universe u
variables {X : Type u} [topological_space X]
variables (P : Sheaf (opens.grothendieck_topology X) CommRing.{u})

open opposite topological_space

def is_regular_element {U : opens X} (s : P.val.obj (op U)) : Prop :=
∀ (V : opens X) (h : V ≤ U) (f : P.val.obj (op V)), P.val.map (hom_of_le h).op s * f = 0 → f = 0

def regular_element (U : opens X) : submonoid (P.val.obj (op U)) :=
{ carrier := { s | is_regular_element P s },
  one_mem' := begin
    intros V h f hf,
    simpa using hf
  end,
  mul_mem' := begin
    intros s t hs ht V h f hf,
    dsimp at hs ht,
    simp [mul_assoc] at hf,
    specialize hs V h _ hf,
    exact ht V h _ hs,
  end }

lemma map_is_regular_element {U V : opens X} (h : U ≤ V) (f : P.val.obj (op V)) :
  is_regular_element P f → is_regular_element P (P.val.map (hom_of_le h).op f) :=
begin
  intros hf W h g,
  rw [← comp_apply, ← P.val.map_comp, ← op_comp],
  intros h,
  apply hf _ _ _ h,
end

lemma comap_regular_element {U V : (opens X)ᵒᵖ} (h : U ⟶ V) :
  regular_element P U.unop ≤ (regular_element P V.unop).comap (P.val.map h).to_monoid_hom :=
begin
  intros f hf,
  have : V.unop ≤ U.unop := le_of_hom h.unop,
  change is_regular_element _ _,
  convert map_is_regular_element P this f hf,
  have : h = (hom_of_le this).op,
  { change h.unop.op = _,
    congr' 1 },
  rw this,
  refl,
end

noncomputable def total_fraction_presheaf : (opens X)ᵒᵖ ⥤ CommRing :=
{ obj := λ U, CommRing.of $ localization (regular_element P U.unop),
  map := λ U V h, begin
    apply is_localization.map _ (P.val.map h) (comap_regular_element _ _),
    change algebra (P.val.obj (op U.unop)) (localization _),
    apply_instance,
    change is_localization _ (localization _),
    apply_instance,
    change algebra (P.val.obj (op V.unop)) (localization _),
    apply_instance,
    change is_localization _ (localization _),
    apply_instance,
  end,
  map_id' := begin
    intros U,
    simp,
    change is_localization.map _ (ring_hom.id _) _ = ring_hom.id _,
    ext,
    simp,
  end,
  map_comp' := begin
    intros U V W f g,
    simp,
    change is_localization.map _ ((P.val.map g).comp (P.val.map f)) _ =
      (is_localization.map _ _ _).comp _,
    rw is_localization.map_comp_map,
    refl,
  end } .

-- Why is this needed???
instance (U : opens X) : is_filtered ((opens.grothendieck_topology X).cover U)ᵒᵖ :=
by apply_instance

noncomputable def total_fraction_sheaf : Sheaf (opens.grothendieck_topology X) CommRing :=
(presheaf_to_Sheaf _ _).obj (total_fraction_presheaf P)

-- Now if `P` is the sheaf of holomorphic functions, then `total_fraction_sheaf P` should be
-- the sheaf of meromorphic functions.

As you can see, there are some pain points in this code, around the following points:

1. I used Grothendieck topologies, because as far as I know we cannot easily sheafify presheaves of commutative rings using sheaves from the topology part of mathlib.
2. Mapping localizations is more difficult than it should be... I could add some algebra instances, sure, but it's still a bit annoying.
3. There are some annoying points coming up due to op, but I don't see any way to avoid them.
4. Why do I need to manually add the is_filtered instance toward the bottom?

[Adam Topaz]

It would be better to develop a general construction of localization of sheaves of commutative rings by a sub(pre)sheaf of monoids. If someone wants to try to even write down the type of such a construction, that would be great!

[Andrew Yang]

A probably not that related question: what is a better way to talk about a "sub(pre)sheaf of monoids"?
An mono into the image of the F : Sheaf X CommRing under some forgetful functor Sheaf X CommRing ⥤ Sheaf X Monoid?
I was thinking about this just this afternoon (though I was thinking about ideal sheaves) and I have yet obtained a satisfactory solution.

[Adam Topaz]

@Andrew Yang that question is definitely related! Note that to localize a ring, one must use docs#submonoid at some point

[Adam Topaz]

(at least in the way localization is currently done)

[Adam Topaz]

If you have a morphism of sheaves of monoids, you can localize at the images, I guess... But I don't know how workable that would be in practice

[Andrew Yang]

I thought so too. Since most of the substuff library talks about the bundled substuff, we would need to juggle with images all the time if we go for this approach.

[Adam Topaz]

For sheaves of ideals, you can model them as kernels of morphisms of sheaves of rings, for example.

[Kevin Buzzard]

You'll have a bad notion of equality that way

[Adam Topaz]

equality is evil anyway

[Kevin Buzzard]

Perhaps not for sheaves of ideals

[Adam Topaz]

ok, fair point..

[Yakov Pechersky]

Is there no way to use non_zero_divisors here?

[Yakov Pechersky]

For example, if I am reading the definition, correctly, you're working on { obj := λ U, CommRing.of $ fraction_ring (P.val.obj U), ...}? There are some API missing for your 2. point. Just to familiarize myself with this part of the library, is there a reason to not use CommRing.of_hom _ for your hom := construction?

[Adam Topaz]

@Yakov Pechersky take a look at the definition on the nlab,
http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/sheaf+of+meromorphic+functions

and also (in the algebraic context) the top of page 141 of Hartshorne.

[Adam Topaz]

I don't think using non_zero_divisors works in this level of generality.

[Adam Topaz]

As for CommRing.of_hom, it's not really needed here, as morphisms in the category CommRing are defeq to ring homs.

[Adam Topaz]

Oh wait, I see what you mean... maybe it does work to resolve 2, let me check.

[Adam Topaz]

No, unfortunately the same annoyances show up with CommRing.of_hom as well... lean is not able to deduce the algebra and is_localization instances for some reason.

[Yakov Pechersky]

Yeah it didn't help when I tried

[David Wärn]

A section of a sheaf of rings is regular if all its restrictions are non_zero_divisors. This is strictly stronger than just being a non_zero_divisor in P(U), so fraction_ring (P U) already inverts too many things

[Heather Macbeth]

Adam Topaz said:

As you can see, there are some pain points in this code, around the following points:

1. I used Grothendieck topologies, because as far as I know we cannot easily sheafify presheaves of commutative rings using sheaves from the topology part of mathlib.

I didn't realise we had both docs#category_theory.Sheaf and docs#Top.sheaf. Is it planned for the former to subsume the latter at some point?

[Adam Topaz]

Ping @Justus Springer @Andrew Yang

[Andrew Yang]

Quoting Justus from his PR linking the two notions:

@jcommelin I did briefly think about this and I'm not sure. It's a design decision I don't feel comfortable making at the moment. Removing the sheaf-on-space definition by making it a special case of the more general one certainly feels like the right thing to do. But on the other hand, I consider sheaves on spaces a pretty important special case and some users (e.g. me three weeks ago) may not want to think about sites and just do sheaves on spaces. So there probably should be a lot of API specialising every applicable concept around sheaves to the case of spaces anyway. So maybe it wouldn't even make that much of a difference in size. But conceptually, it would probably be the right thing do to in the long run.

Note that some things can already be deduplicated using the equivalence of categories: Right now there are two proofs that composing a sheaf with an isomorphism-reflecting limit-preserving functor again yields a sheaf. They work in slightly different settings, but you could definitely make one a special case of the other by going around the equivalence of categories. I might try to do that soon.

[Heather Macbeth]

Also -- how do I make a docs#category_theory.Sheaf? I think it's nearly possible to make the structure sheaf of a complex manifold as a docs#Top.sheaf -- docs#Top.local_predicate does this, the only problem is that it makes a sheaf of types rather than a sheaf of rings.

[Adam Topaz]

We have the equivalence between the two notions as an equivalence of categories.

[Heather Macbeth]

I see. Would some sheaf person be up for modifying docs#Top.local_predicate to make sheaves of rings?

[Adam Topaz]

The type vs. commring is an issue.

[Adam Topaz]

We could refactor local_predicate to take in a sufficiently nice concrete category instead of Type*.

[Adam Topaz]

Or we could build up enough of the API so that using Sheaf (opens.grothendieck_topology X) A isn't so scary.

[Adam Topaz]

@Andrew Yang what do you think?

[Heather Macbeth]

Adam Topaz said:

We have the equivalence between the two notions as an equivalence of categories.

If I understand correctly, an equivalence of categories wouldn't give a bijection of the objects, let alone a bijection respecting definitional equality ... so this sounds like it would get awkward.

[Adam Topaz]

I think the functors for this equivalence are defeq to the identity on the level of presheaves, but I'm not 100% sure (I think Justus is the person who built that equivalence?)

[Heather Macbeth]

Oh, that's nice then!

[Andrew Yang]

For a presheaf Cᵒᵖ ⥤ D, we know that it is a sheaf on the space iff it is a sheaf wrt the grothendieck topology, and the two categories are defined as merely a subtype of the category of presheaves, so it should not be a pain to move from one to another.

[Heather Macbeth]

Adam Topaz said:

We could refactor local_predicate to take in a sufficiently nice concrete category instead of Type*.

This sounds great ...

[Andrew Yang]

I'm not sure how one would generalize local_predicate to concrete categories.
We would need to know that the set of the functions satisfying P locally is an object in the category, and the condition would vary for different categories?

[Andrew Yang]

Note that we have docs#category_theory.presheaf.is_sheaf_iff_is_sheaf_forget, so we should still be able to use the local predicate stuff for good enough concrete categories.

[Heather Macbeth]

Andrew Yang said:

I'm not sure how one would generalize local_predicate to concrete categories.
We would need to know that the set of the functions satisfying P locally is an object in the category, and the condition would vary for different categories?

Could you do it for categories which have been constructed using docs#category_theory.bundled or docs#category_theory.bundled_hom.category ?

[Andrew Yang]

We would still need to prove things like https://github.com/leanprover-community/mathlib/blob/dc3cbb7d7d31191be71a6a52015e03a7578ff961/src/algebraic_geometry/structure_sheaf.lean#L147-L210
for each local predicates we want to use, and the condition crucially depends on the P used.

[Heather Macbeth]

Even if there's no way to abstract it to sheaves of "certain kinds of categories", it might be nice to provide a local-predicate construction for sheaves of rings, since that one's used a lot.

[Antoine Chambert-Loir]

David Wärn said:

A section of a sheaf of rings is regular if all its restrictions are non_zero_divisors. This is strictly stronger than just being a non_zero_divisor in P(U), so fraction_ring (P U) already inverts too many things

For those of you who want to look at old stuff, this problem is the source of a mistake in Grothendieck's EGA (it is written that the obvious presheaf is a sheaf, but it's not a presheaf!). It has been adressed in a nice paper of Steven Kleiman, Some misconceptions about K_X, L'enseignement mathématique, DOI:10.5169/seals-50379

[Yakov Pechersky]

Antoine, I added a refence to your blog post about this, by Kevin's pointer to it! https://github.com/leanprover-community/mathlib/blob/master/src/field_theory/ratfunc.lean#L58

[Yakov Pechersky]

It was my motivation to generalize ratfunc.lift_on to arbitary [comm_ring K} without requiring [is_domain K]

[Justus Springer]

I think there is still a lot of stuff in the sheaf theory library that should be generalised from sheaves of types to sheaves valued in more general "nice enough" category. In fact, working with sheaves in lean made me realise what exactly "nice enough" means in this context: It needs to be a concrete category whose forgetful functor reflects isomorphisms and preserves limits and filtered colimits. The first two properties ensures that a presheaf is a sheaf if and only if the underlying presheaf of types is a sheaf, while preserving colimits ensures that taking stalks commutes with the forgetful functor. All the typical "algebraic" categories, like Group or CommRing satisfy this property (and this is already in mathlib). The stacks project calls these categories "types of algebraic structures" in stacks#007L. So I believe if sheafification and the stuff about local prediactes should be generalised, it is this class of categories one should look at, not only CommRing.

[Adam Topaz]

Those are exactly the conditions I had set up for sheafification over a general site.

[Adam Topaz]

E.g. docs#category_theory.grothendieck_topology.sheafify_is_sheaf

[Justus Springer]

Oh wow, I didn't know this already exists in mathlib for sites.

[Adam Topaz]

Actually since we have the adjunction docs#category_theory.sheafification_adjunction and the equivalence between the site-theoretic definition of sheaves and the topological one, as an equivalence of categories, it would be easy to obtain the sheafification adjunction for topological spaces as well by composing... that's some sort of sheafification in general for topological spaces, although if you need more control over the stalks that would require additional work.

[Justus Springer]

Yeah, it seems it's about time that sheaves on sites and sheaves on spaces are unified. Maybe I should have tried to do that when I built the equivalence. The longer the theories move independently the harder it will be to clean it up and unify them. In a sense it doesn't matter that much because we'll still want all the API for the special case of sheaves on spaces, but it's the right thing to do conceptually.

[Andrew Yang]

I also think that we should make the sites one the official definition (while keeping all the other sheaves on topology stuff). I would suppose that the transition won't be that painful, since we are just replacing a Prop valued thing into another that we know is equivalent.
This gives us sheaves in categories without products (which I do not know how useful it is), but more importantly this makes it easier to access the sites stuff (sheafification, pullback-pushforward, abelian-ness, etc).

[Adam Topaz]

(Thanks for the reminder that I should eventually mathlibify the fact that abelian sheaves are an abelian category ;))
mathlibify is the left adjoint to the forgetful functor from mathlib to lte, of course.

[Junyan Xu]

If we just want the sheaf for schemes and not general ringed spaces, then according to the misconceptions paper, we can define sections of the presheaf using the "wrong" definition on open affines, then sheafify and extend to all opens, using Andrew's work at https://leanprover-community.github.io/mathlib_docs/category_theory/sites/dense_subsite.html.

[Adam Topaz]

Sure, but we should have a construction that will also let us construct meromorphic functions in the holomorphic setting (and other settings as well), not just in the algebraic context.

[David Loeffler]

I'd like to gather some opinions about how best to implement meromorphic functions (from an open subset of ℂ to ℂ).

We can certainly define a function to be MeromorphicAt z if ∃ (n : ℕ), AnalyticAt ℂ (fun x ↦ (x - z) ^ n * f x) z. But I am worried that this would capture some rather silly functions: e.g. with this definition the function "f(x) = 1 if x = 0 and else 0" is meromorphic at 0, which seems undesirable.

We could try requiring that $f(z)$ should be defined as 0 if f has a pole, but this plays badly with arithmetic on functions: with this definition, $f(x) = 1/x$ and $g(x) = 1$ are both meromorphic, but $f(x) + g(x)$ is not. We can rescue addition by instead requiring that, even at a pole, f z must equal the constant term of the Laurent expansion of f at z, but it doesn't seem to be possible to fix multiplication the same way.

I think there's no way of fixing this without dropping the idea that meromorphic functions be a subset of ℂ → ℂ: we need to carry around more data.

I wondered about encoding meromorphic functions as functions ℂ → ℂ((X)), where ℂ((X)) is the space of Laurent series in a formal variable X, satisfying the compatibility condition that for all z, the Laurent series f z ∈ ℂ((X)) has to be a Laurent expansion for the function "x ↦ constant term of f (x)" around z. Then addition and multiplication are well-defined, and we have a uniquely determined evaluate at a point map given by taking constant terms of Laurent series (which is even a map of ℂ-vector spaces); but we have to live with the fact that in general eval f z * eval g z ≠ eval (f * g) z.

I'd be interested in any feedback as to whether this is a good approach.

[Johan Commelin]

In your 2nd paragraph, you meant (x - z) ^ n instead of x ^ n, right?

[Johan Commelin]

It doesn't change your point, of course.

[David Loeffler]

yes, that was a typo, sorry!

[Vincent Beffara]

I like the question, and thought about it recently, and besides what you are describing I had two alternative definitions:

• the meromorphic functions on a connected open set are the field of fractions of holomorphic functions on that set, which is nicely defined. but there is the issue of evaluation at a point because we need to say that $x/x$ at $x=0$ is $1$ and Lean would think it is $0$
• meromorphic functions on U are the holomorphic functions from U to the Riemann sphere that are not identically infinite.

[Flo (Florent Schaffhauser)]

How about defining a meromorphic function on an open subset U of C as a function that:

1. Is defined on U minus a closed discrete set P.
2. Is analytic/holomorphic on U \ P.
3. Has a Laurent series expansion on a small punctured disk (contained in U\P) around each point p of P.

With that definition, it should be provable in a rather elementary way that if we extend by \infty at points of P, then a meromorphic function “on U” is a holomorphic map U \to CP^1 and vice-versa.

(sent from a cell phone, sorry)

[Johan Commelin]

I think the either: we consider maps to $\mathbb{P}^1$, or the values at poles must be $0$. The benefit of the second convention is that it will be a lot easier to reason with all the finite values, since they will be ordinary complex numbers.

[Flo (Florent Schaffhauser)]

I’m afraid that setting the value at a pole to be 0 might introduce complications later on :oh_no:

[Vincent Beffara]

Yes, up to the question of whether we want to impose poles at P or not (I would be inclined not to, because then the sum and product of meromorphic functions is nicely meromorphic, you don't need to take care of cancellations)

[Flo (Florent Schaffhauser)]

But surely we do not want exp(1/z) to be considered meromorphic, right?

[Johan Commelin]

@Flo (Florent Schaffhauser) It has to have some value, unless you want to work with functions defined on subtypes. But that creates its own set of headaches.

[Vincent Beffara]

Right, I mean at every point at P we have either a pole or a continuous extension

[Johan Commelin]

But what is "a pole"?

[Johan Commelin]

What is the type of a meromorphic function?

[Flo (Florent Schaffhauser)]

@Johan Commelin In that case, can the value be an \infty symbol? We would just have to take C \cup {\infty} as target.

[Flo (Florent Schaffhauser)]

Johan Commelin said:

What is the type of a meromorphic function?

Triples (U, P, f: U\P \to C) satisfying the conditions above.

[Vincent Beffara]

I think the easiest would be \C \to \C with IsMeromophicOn U as a predicate that states \exists P, discrete P and whatever

[Riccardo Brasca]

Is working with the riemann sphere too much work?

[Flo (Florent Schaffhauser)]

Vincent Beffara said:

I think the easiest would be \C \to \C with IsMeromophicOn U as a predicate that states \exists P, discrete P and whatever

Yes, \exists P is also fine, I think. Probably makes things easier to check that the sum and product of meromorphic functions are meromorphic.

[Vincent Beffara]

Riccardo Brasca said:

Is working with the riemann sphere too much work?

That would depend on whether we have the Riemann sphere (with nice API) :wink:

[Riccardo Brasca]

Yes of course. But it seems the mathematically correct approach, but maybe we are very far from complex manifolds...

[Flo (Florent Schaffhauser)]

Johan Commelin said:

But what is "a pole"?

I think we can simply say that a function defined on an open set minus a point has a pole at that point if it admits a Laurent series expansion in a punctured disk around that point.

[Riccardo Brasca]

Like this a constant function has poles everywhere

[Riccardo Brasca]

of course we can add "a laurent series such that...", but this seems already a little complicated

[Flo (Florent Schaffhauser)]

Sure, poles of order 0 :wink:

[Flo (Florent Schaffhauser)]

No, you’re right, we have to add something 👍🏻

[Flo (Florent Schaffhauser)]

We define the Laurent series expansion, it gives us an “order” at the point, and we call the point a pole if the order is negative.

[Flo (Florent Schaffhauser)]

The key notion is the Laurent series expansion, not that of a pole.

[Riccardo Brasca]

Laurent series expansion of what?

[Geoffrey Irving]

I’ve formalized complex manifolds and the Riemann sphere as part of the Mandelbrot work, whence a metamorphic function is just a holomorphic function from C to S.

[Geoffrey Irving]

I am halfway through the Lean 4 port, and then I can upstream those pieces first if people are interested.

[Riccardo Brasca]

Geoffrey Irving said:

I’ve formalized complex manifolds and the Riemann sphere as part of the Mandelbrot work, when a metamorphic function is just a holomorphic function from C to S.

This is exactly what I proposed

[Flo (Florent Schaffhauser)]

Riccardo Brasca said:

Laurent series expansion of what?

Of a function f: U \ P \to C

[Geoffrey Irving]

@Riccardo Brasca Apologies, I missed that when scrolling.

[Riccardo Brasca]

It has the drawback that a function f : ℂ → ℂ cannot be meromorphic, but we can maybe live with that

[Riccardo Brasca]

@Geoffrey Irving no worries, I am very happy to know that is doable and even happier to know that it is already done!

[Geoffrey Irving]

Such a function always has a unique lift, at least.

[Riccardo Brasca]

Exactly, I think a coercion will do the job

[Geoffrey Irving]

https://github.com/girving/ray/blob/main/src/riemann_sphere.lean

[Flo (Florent Schaffhauser)]

Riccardo Brasca said:

It has the drawback that a function f : ℂ → ℂ cannot be meromorphic, but we can maybe live with that

Sorry, why?

[Riccardo Brasca]

I was talking about the approach with the Riemann sphere. Because it takes values in ℂ and not in the Riemann sphere

[Geoffrey Irving]

The holomorphic def in https://github.com/girving/ray/blob/main/src/complex_manifold.lean includes all of these, so you can be generic if desired.

[Riccardo Brasca]

(of course there is a "canonical" meromorphic function associated to f)

[Geoffrey Irving]

I should spell it out:

1. Holomorphic C to S functions are meromorphic at any finite value
2. Holomorphic S to S functions are meromorphic including at infinity (they are rational)

[Flo (Florent Schaffhauser)]

Flo (Florent Schaffhauser) said:

Vincent Beffara said:

I think the easiest would be \C \to \C with IsMeromophicOn U as a predicate that states \exists P, discrete P and whatever

Yes, \exists P is also fine, I think. Probably makes things easier to check that the sum and product of meromorphic functions are meromorphic.

But still I would be a bit reluctant to define a meromorphic function as a function defined on all of C.

[Geoffrey Irving]

From experience, working over manifolds and charted spaces does have a fairly significant pain cost, of course.

[Riccardo Brasca]

I agree this seems problematic, since we have to choose a garbage value. One possibility can be a predicate on functions ℂ → Option ℂ

[Geoffrey Irving]

Alexandroff C. :)

[Geoffrey Irving]

My Riemann sphere is just Option C if you unpack definitions.

[Riccardo Brasca]

Yes, of course. The point of the API is to hide that or not

[Riccardo Brasca]

Anyway, we can keep on discussing several approaches forever, each one will have benefits and drawbacks... maybe the best thing is to choose one and go for it (after a not too long discussion...)

[Flo (Florent Schaffhauser)]

To be clear, I like the option of defining meromorphic functions “on U” as CP^1-valued holomorphic functions on U, especially if the Riemann sphere is already defined.

[Flo (Florent Schaffhauser)]

But we may have to go back to the other approach sooner or later, to define functions that have an essential singularity at a point.

There, you just replace the Laurent series expansion by an expansion as a series indexed from -\infty to +\infty.

[Flo (Florent Schaffhauser)]

And you get for instance exp(1/z) as an example, etc.

[Flo (Florent Schaffhauser)]

Riccardo Brasca said:

Anyway, we can keep on discussing several approaches forever, each one will have benefits and drawbacks... maybe the best thing is to choose one and go for it (after a not too long discussion...)

Yes, I’ve reached my point, I will shut up now :wink:

[Flo (Florent Schaffhauser)]

Flo (Florent Schaffhauser) said:

But still I would be a bit reluctant to define a meromorphic function as a function defined on all of C.

Also because at some point we will have to define the sheaf of meromorphic functions on a complex analytic manifold.

[David Loeffler]

The "Riemann sphere" approach seems to be getting some traction; but do we really want the constant function $\infty$ to be a meromorphic function? I'm quite keen on having meromorphic functions having a natural ring structure (and even a field structure if $U$ is connected) and that seems to be something that's hard to get with the Riemann-sphere definition – the ring operations are not even defined unless you restrict to functions such that $f^{-1}(\infty)$ is discrete, and even then, defining addition and multiplication is awkward to do.

[Flo (Florent Schaffhauser)]

Yes, you’re right, the function f: U \to \CP^1 should be holomorphic and not equal to the constant function $\infty$.

[Riccardo Brasca]

Good point

[Flo (Florent Schaffhauser)]

Also about the definition of sum and product being awkward with that approach, yes.

[David Loeffler]

Riccardo Brasca said:

Anyway, we can keep on discussing several approaches forever, each one will have benefits and drawbacks... maybe the best thing is to choose one and go for it (after a not too long discussion...)

Here's a first stab at my "function taking values in Laurent series" approach:

import Mathlib
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)
noncomputable section

/-! IGNORE THIS -- make a FormalMultlinearSeries out of a one-variable
power series -/
def PowerSeries.formalMultilinearSeries
    (f : PowerSeries ℂ) : FormalMultilinearSeries ℂ ℂ ℂ :=
fun n ↦ (PowerSeries.coeff ℂ n f) •
  (ContinuousMultilinearMap.mkPiAlgebra ℂ (Fin n) ℂ)

/-! A `LaurentFamily` is a family of formal Laurent series indexed by `ℂ`. -/
structure LaurentFamily where (laurentSeriesAt : ℂ → LaurentSeries ℂ)

def LaurentFamily.constTermAt (f : LaurentFamily) (z : ℂ) :=
(f.laurentSeriesAt z).coeff 0

def LaurentFamily.orderAt (f : LaurentFamily) (z : ℂ) :=
(f.laurentSeriesAt z).order

def MeromorphicAt (f : LaurentFamily) (z : ℂ) : Prop :=
  HasFPowerSeriesAt
  (fun x ↦ (x - z) ^ (f.orderAt z) * f.constTermAt x)
  (f.laurentSeriesAt z).powerSeriesPart.formalMultilinearSeries z

[Sebastien Gouezel]

For what it's worth, I would use the naive definition from your first post (i.e., f is meromorphic on U if there exists a discrete set such that f is holomorphic on U - P, and (z -p)^n f extends continuously at p in P for some n), without caring about the specific value at p. Because I think the zeta function and the Gamma functions we already have are meromorphic, and I am very happy to be able to use them as functions from $\mathbb{C}$ to $\mathbb{C}$.

[Geoffrey Irving]

^ And anything with that definition easily lifts to something C to S which is equal except on the discrete countable set, so we can provide the conversion function (I’ve already proven the needed lemmas in the files shared above). Specifically, you can write the function which produces the S value at a point, and the lift is just all of these S values.

[David Loeffler]

Sebastien Gouezel said:

For what it's worth, I would use the naive definition from your first post (i.e., f is meromorphic on U if there exists a discrete set such that f is holomorphic on U - P, and (z -p)^n f extends continuously at p in P for some n), without caring about the specific value at p. Because I think the zeta function and the Gamma functions we already have are meromorphic, and I am very happy to be able to use them as functions from $\mathbb{C}$ to $\mathbb{C}$.

That's actually a pretty convincing argument! I tried to flesh out my Laurent-series definition a little, but it seems to be more painful to work with than I anticipated.

[Heather Macbeth]

@David Loeffler I was actually planning to define meromorphic functions using sheaf theory (docs#TopCat.Presheaf.totalQuotientPresheaf in particular) -- my current PR #7332 is on the way to this.

[Heather Macbeth]

This would be a definition in arbitrary dimension rather than just for ℂ, so maybe we should have both definitions and they should be proved equivalent on ℂ?

[Heather Macbeth]

Geoffrey Irving said:

I’ve formalized complex manifolds and the Riemann sphere as part of the Mandelbrot work

@Geoffrey Irving I think I missed this earlier comment of yours. What do you mean by having formalized complex manifolds? (The definition has been in mathlib for many years.)

[Geoffrey Irving]

Where is it? I mean writing down the analytic groupoid and things like HolomorphicAt (a manifold version of AnalyticAt). It’s not hard on top of the existing manifold machinery, to be clear: https://github.com/girving/ray/blob/main/src/complex_manifold.lean

[Geoffrey Irving]

I could have just used smooth manifolds, but I believe they are only equivalent in finite dimensions. Admittedly that’s all I need, but I thought I might as well write down the single file with the analytic groupoid.

[Heather Macbeth]

Oh, I see. We should really decide whether our development of complex manifolds is going to take place in the ℂ-smooth setting or the ℂ-analytic setting, given that they are mathematically equivalent. I have been working so far in the ℂ-smooth setting, e.g. docs#MDifferentiable.exists_eq_const_of_compactSpace

[Heather Macbeth]

I suppose I would say that you formalized analytic manifolds :)

[Geoffrey Irving]

I’m happy to adjust, but regardless of what we use for the manifold type classes I think having the equivalent of AnalyticAt is valuable. The relationship of pointwise vs. global for differentiable vs. analytic is quite different.

And yeah, if we do think having analytic manifolds as a separate type class is useful, happy to change the name. We can also define suitable finite dimensionality type classes, and make the type classes cleanly interconvert.

[Heather Macbeth]

I'm also very happy to have the ability to talk about real analytic manifolds!

[Geoffrey Irving]

Should we also correct the name here? :)

https://en.m.wikipedia.org/wiki/Complex_manifold

I suppose they explicitly limit only to finite dimensions.

[Heather Macbeth]

Sorry, I don't follow?

[Geoffrey Irving]

That’s why I called it ComplexManifold.

(But I do agree that AnalyticManifold is better.)

[Heather Macbeth]

I don't understand, sorry -- are you saying that you think there is a difference between the Wikipedia definition and the mathlib SmoothManifoldWithCorners \C?

[Yaël Dillies]

(I think Geoffrey is arguing that ComplexManifold corresponds to Wikipedia's complex manifolds and that if you want to change one name you should also change the other)

[Geoffrey Irving]

But I’m not actually arguing that, just making a bad joke. I think we should have AnalyticManifold in Mathlib given that it will cover arbitrary fields and infinite dimensions.

[Junyan Xu]

The analytic groupoid was recently merged into mathlib! I see that a review was requested from @Heather Macbeth but she didn't leave one, maybe she didn't notice ...

[Junyan Xu]

Sebastien Gouezel said:

For what it's worth, I would use the naive definition from your first post (i.e., f is meromorphic on U if there exists a discrete set such that f is holomorphic on U - P, and (z -p)^n f extends continuously at p in P for some n), without caring about the specific value at p.

I agree with this too, and I think it's important that we allow a discrete set of regular points where the value could differ from what it should be, so that we don't need to change the value at 0 when adding up 1+1/z and -1/z, for example. I think the situation is similar to docs#MeasureTheory.AEEqFun, but instead of docs#MeasureTheory.Measure.ae we use the filter of co-discrete sets; in higher dimensions you'd work with the filter of complements of sets that are locally a hypersurface (the zero set of a nonzero holomorphic function). The identity principle docs#AnalyticOn.eqOn_of_preconnected_of_frequently_eq (and in higher dimension docs#AnalyticOn.eqOn_of_preconnected_of_eventuallyEq) should facilitate working with functions up to equivalence under the filter (it's crucial that hypersurfaces have real codimension 2 so they don't disconnect a domain). Worth noting in higher dimensions meromorphic functions (which are locally quotients of ) don't necessarily correspond to maps to the Riemann sphere (for example z1/z2 is undefined at (0,0)), so that approach doesn't work. The sheaf approach still works and we should prove the equivalence.

[Alex Kontorovich]

For what it's worth, my preferred way to discuss poles (I don't know if this is the best for formalization) is the following. First I prove Riemann's removable singularity theorem (if a function is holomorphic in U-{p} and bounded there, then it can be extended to a holomorphic function on U). Then: f has a pole at p if: it's holomorphic on U-{p}, and 1/fhas a removable singularity at p with value 0. Thoughts on this approach? (Very down to earth... so probably not "mathlib"y...)

[Kevin Buzzard]

The issue is how to add 1-1/z and 1/z, because whether you used infinity or a junk value for the value at 0 the sum of two of these values won't be 1.

In the classical algebraic geometry theory of varieties one uses the concept of a rational map, which when I had to lecture this stuff myself I defined via equivalence classes of non-infinite-valued functions defined on dense open subsets and I remember at the time thinking how awful it would be to formalise. The concept of a sheaf of meromorphic functions is a thing and it has tripped up mathematicians in the past; the exposition in Hartshorne contains errors IIRC. But this way avoids infinity completely, functions are all defined on an unspecified dense open and you show afterwards that there's at most one finite correct answer for the value at any point

[Flo (Florent Schaffhauser)]

Kevin Buzzard said:

The issue is how to add 1-1/z and 1/z, because whether you used infinity or a junk value for the value at 0 the sum of two of these values won't be 1.

Indeed. But in principle, if along with the two functions f1 and f2 we had their set of poles P1 and P2 and the Laurent series at each pole, we could determine the set of poles of f1 + f2 along with the Laurent series at each of these poles (a subset of P1 \cup P2).

[Flo (Florent Schaffhauser)]

This would give a definition of the sum of two meromorphic functions and then one has to check that the sum of two holomorphic functions seen as meromorphic ones coincide with their sum as holomorphic functions (seen, again, as a meromorphic one).

[Kevin Buzzard]

Right, you're saying "I desperately want to cling to the idea of a canonical representative" but if you do this then things like proving associativity of addition will be a case split nightmare. I'm saying it's easier to work with the entire equivalence classes, where things are only defined up to some error set, like they do with Lp spaces and functions being ae equivalent.

[Kevin Buzzard]

Examples where we cling to a canonical representative do exist in mathlib however. The rationals are defined as coprime pairs (n,d) with d>0 and finsupp also carries around the explicit finite support of the function. But this is for computability reasons which I don't think apply here.

[Kevin Buzzard]

If you define the rationals as equivalence classes then proving the basic API that they're a field is much much easier. It's just that addition of [1/2] and [1/2] will be [4/4] which upsets people who want to #eval everything (indeed quotients in general upset the #eval crowd precisely because there is no canonical representative which they can point to without having to continually run an algorithm to tame representatives). This is not an issue here because there's no need to make the theory computable.

[Flo (Florent Schaffhauser)]

Point taken!

[Johan Commelin]

Kevin Buzzard said:

The issue is how to add 1-1/z and 1/z, because whether you used infinity or a junk value for the value at 0 the sum of two of these values won't be 1.

I think the issue is already to decide what value 1-1/z would take at z = 0. If it takes the value 1 (because after all, 1 - 1/0 = 1 - 0 = 1 in Lean), then there is no problem at all with adding 1 - 1/z and 1/z.

[Johan Commelin]

If we give up on canonical representatives, then evaluating a meromorphic function at a point will become quite a bit more complicated. But maybe that is in fact still the way to minimize the global amount of pain when working with meromorphic functions.

[Sebastien Gouezel]

Why do you want to have a canonical representative, instead of many representatives? In measure theory, we have the space 𝓛^p (the space of all functions whose norm is p-integrable), and the space L^p (the space of equivalence classes up to measures zero of such functions, which becomes a Banach space with a nice norm and so on). Most of the time, you work with regular functions in 𝓛^p (although you know that, morally, they are only defined almost everywhere), and when you need to do functional analysis you switch to the equivalence classes L^p. And it works very well!

[Johan Commelin]

One approach that we might take, in order to figure out the "correct" definition in Lean is to apply some top-down strategizing. As @Sebastien Gouezel pointed out, we already have examples of functions that should satisfy the MeromorphicAt predicate. So that more or less means that we'll work with functions $\mathbb{C} \to \mathbb{C}$ and a predicate on those.
Now if we write down a bunch of basic API lemmas that we want to be true, all proven by sorry, then we can try to start organizing them in a way shows which of them should be "axioms" (aka part of the definition of the predicate), and which one we can slickly derive from those more basic ones.

[Johan Commelin]

Yeah, so we could have a AEMeromorphicWithin predicate. (I don't know if AE is really the right prefix...)

[David Loeffler]

Johan Commelin said:

Yeah, so we could have a AEMeromorphicWithin predicate. (I don't know if AE is really the right prefix...)

How is AEMeromorphic supposed to be different from Meromorphic?

[Johan Commelin]

e.g. with this definition the function "f(x) = 1 if x = 0 and else 0" is meromorphic at 0, which seems undesirable.

This function would be AEMeromorphic, but I would hesitate to call it meromorphic.

[Junyan Xu]

Johan Commelin said:

I think the issue is already to decide what value 1-1/z would take at z = 0. If it takes the value 1 (because after all, 1 - 1/0 = 1 - 0 = 1 in Lean), then there is no problem at all with adding 1 - 1/z and 1/z.

Johan Commelin said:

e.g. with this definition the function "f(x) = 1 if x = 0 and else 0" is meromorphic at 0, which seems undesirable.

This function would be AEMeromorphic, but I would hesitate to call it meromorphic.

If you want Meromorphic to allow only the correct value at regular points, then multiplicativity Meromorphic f → Meromorphic g → Meromorphic (f * g) and Meromorphic f → Meromorphic f⁻¹ are unachievable. Additivity is achievable (in dimension one) by allowing only the constant term of the Laurent expansion as the value at a pole (a convention which 1/z and 1-1/z conform to, but Gamma doesn't: compare docs#Complex.Gamma_zero with image.png), but that seems to be too stringent a restriction without enough benefit (won't fix multiplicativity).

[David Loeffler]

@Johan Commelin Are you proposing that we make a definition AEMeromorphic but not Meromorphic? Or are you proposing to have both, and set things up so that each ae-eq class of AEMeromorphic functions has a unique Meromorphic representative (where ae = away from a discrete set)? The latter seems to bring us back to the problem we had at the start.

[Kevin Buzzard]

Johan Commelin said:

Kevin Buzzard said:

The issue is how to add 1-1/z and 1/z, because whether you used infinity or a junk value for the value at 0 the sum of two of these values won't be 1.

I think the issue is already to decide what value 1-1/z would take at z = 0. If it takes the value 1 (because after all, 1 - 1/0 = 1 - 0 = 1 in Lean), then there is no problem at all with adding 1 - 1/z and 1/z.

Well let me write the first one as $(z-1)/z$ and then the problem is back.

[Johan Commelin]

David Loeffler said:

Johan Commelin Are you proposing that we make a definition AEMeromorphic but not Meromorphic? Or are you proposing to have both, and set things up so that each ae-eq class of AEMeromorphic functions has a unique Meromorphic representative (where ae = away from a discrete set)? The latter seems to bring us back to the problem we had at the start.

I think I'm leaning towards:

• AEMeromorphic (and AEMeromorphicWithin U) are predicates on functions $\mathbb{C} \to \mathbb{C}$.
• Meromorphic U is a new type (so data, not a prop) that comes with a way to evaluate terms at regular points. It also comes with an instance of CommRing.

I don't have a strong opinion on how Meromorphic U would be defined. It could be via a quotient using AEMeromorphicWithin U, or it could be a hands-on structure, or it could be using functions to the Riemann sphere.

[Junyan Xu]

It seems AEMeromorphicWithin U is also a CommRing, with an ideal of a.e. zero functions that you can quotient out to get the field Meromorphic U (if U is connected).

And I just realized that the co-discrete subsets don't actually form a filter, because the union of two discrete subsets may not be discrete, for example S={1,1/2,1/3,...} and {0}. The correct filter in all dimensions should use the sets locally contained in zero sets of (locally) holomorphic functions, and the union of two zero sets is a zero set because you can take the product of the two holomorphic functions and the intersection of the neighborhoods on which they are defined. In one dimension, a simpler description of this filter is that it consists of complements of sets S such that every point p has a neighborhood whose intersection with S is either empty or {p}.

If you don't use filters, you may get away with discrete subsets, because if there are infinitely many poles in around a point p then the function is pathologic around p and can't be meromorphic there.

[David Loeffler]

The complements of discrete closed subsets are a filter (in any non-discrete $T_3$ space).

[David Loeffler]

Junyan Xu said:

It seems AEMeromorphicWithin U is also a CommRing, with an ideal of a.e. zero functions that you can quotient out to get the field Meromorphic U (if U is connected).

This is of course true (and is quite close to how $L^p$ spaces already work in mathlib), but defining it this way you lose the ability to evaluate elements of Meromorphic U anywhere.

[Yaël Dillies]

With my naming police hat on: Please please don't make AESomeAdjective a structure when SomeAdjective is a predicate, or the other way around.

[Johan Commelin]

Meromorphic U wouldn't be a predicate, it would be bundled functions.

[Johan Commelin]

Or is that what you are objecting against?

[Johan Commelin]

So you want MeromorphicFunction U? If I'm allowed to be a bit naughty... Meromorphism U?

[Yaël Dillies]

Yes, that's exactly what I'm objecting about. Because then people will expect AEMeromorphic to be bundled functions, but it would be a predicate. I had MeromorphicFun in mind, but Meromorphism sounds even better.

[Kevin Buzzard]

I am torn here between the beauty of the word "meromorphism" and the fact that we should stick to the language in the human literature, however noncanonical :-)

[Junyan Xu]

Meromorph, in analogy to docs#Homeomorph :)

[Yaël Dillies]

Ah! I've always wanted to rename Homeomorph to Homeo.

[David Loeffler]

As for naming: I'm not keen on AEMeromorphic for the predicate on functions ("AE" is too strongly suggestive of measure theory). I'd suggest Quasimeromorphic or something.

For the bundled version I'd vote for MeromorphicMap, rather then Meromorphism (by analogy with ContinuousMap).

[Yaël Dillies]

But there wasn't any other option for ContinuousMap, right? Continuism?

[Richard Copley]

Topologism?

[Richard Copley]

Topomorphism is taken

[Geoffrey Irving]

AEMeromorphic is also bad because the true function is meromorphic everywhere. I would expect e^(1/z) to be considered almost everywhere meromorphic. The same issue applies to QuasiMeromorphic.

[Junyan Xu]

Yeah I think there's no need to add AE to the name.
This reference looks nice:
image.png

[Heather Macbeth]

I don't think it's worth doing a bare-hands definition in several variables -- better to go straight to manifolds and the sheaf-y stuff.

[Antoine Chambert-Loir]

Junyan Xu said:

Yeah I think there's no need to add AE to the name.
This reference looks nice:
image.png

That's not a good definition because it is not a priori local.
Same for meromorphic functions as fraction field of the homomorphic ones.
(Also, they would fail for non paracompact manifolds).

[Junyan Xu]

What's non-local about this definition? The definition of thin subsets is also local: image.png

Same for meromorphic functions as fraction field of the homomorphic ones.

Of course there are many manifolds (e.g. the Riemann sphere) with many meromorphic functions but no nonconstant holomorphic functions. The plan is certainly to take the sheafification of the presheaf of FractionRings. (This doesn't work in general in the algebraic setting as pointed out in the misconceptions paper, but in our setting a holomorphic function on an open set is a nonzerodivisor iff it's identically zero on none of the connected components, so nonzerodivisors restrict to nonzerodivisors and we indeed get a presheaf of FractionRings.)

I also don't see why the definitions won't work for paracompact manifolds, but let me mention the interesting fact that a connected Hausdorff complex 1-manifold is automatically second-countable/paracompact, a theorem due to Tibor Radó. This is not true in higher dimensions, and for real analytic 1-manifolds, as the long line admits real analytic structures. (I learned this because I became curious whether the uniformization theorem requires second countability.)

[Antoine Chambert-Loir]

Whatever the definition of thin, the fact that the definition requests a global thin set makes it nonlocal. A variant would ask, for every point, the existence of a neighborhood, a thin set there, etc.

If you have this, to get a global thin set requires to take some union of the locally given thin sets, which you can't say anything about unless the space is paracompact, because then you can refine the open covering to a locally finite one, etc.

[David Loeffler]

Junyan Xu said:

Yeah I think there's no need to add AE to the name.
This reference looks nice:
image.png

@Junyan Xu IMHO, the problem with that definition is that it is not a predicate on functions $G \to \mathbb{C}$.

[Flo (Florent Schaffhauser)]

@David Loeffler Indeed, it is isn’t. But shouldn’t the definition of a meromorphic function on $G$ reflect the fact that in general it is not a function on $G$?

[David Loeffler]

Isn't that begging the question a bit? The whole point of this thread was to decide which, among the many possible formalisations of the notion of "meromorphic", we should implement in mathlib.

[Flo (Florent Schaffhauser)]

Yes, I know, I just haven’t given up yet :wink:

[David Loeffler]

I thought we had decided to formalise two different notions in parallel – a "bundled" notion and a "predicate on functions" version – and AEMeromorphic was supposed to be the predicate version.

I don't greatly care what it's called, and I agree with the remark that AEMeromorphic is probably a bad name; but I am very keen to have a definition which makes it meaningful to say e.g. "the Gamma function is [quasi/ae/weakly/etc]-meromorphic".

[Flo (Florent Schaffhauser)]

Yes, you’re right, this seems to be the consensus, and I don’t have an issue with that :relieved:

[Johan Commelin]

/poll How should we call functions that are meromorphic outside a "small" locus

• QuasiMeromorphic
• WeaklyMeromorphic
• PreMeromorphic

[Sebastien Gouezel]

I don't understand the question. Consider the function f equal to 1/z on the unit disk, except at 0 where it is equal to 37, and which is arbitrarily bad outside the unique disk. Would you use your predicate as PremerormorphicOn f (ball 0 1) here? And if the function is equal to 0 at 0, would you like to promote it to MeromorphicOn f (ball 0 1), or would the latter be kept for functions taking values in the Riemann sphere (and equal to infinity at the pole)?

[Wen Yang]

I think that one day someone will define something like a meromorphic function on a space without complex structure using a certain property of a meromorphic function. That will be more appropriate to be called a quasi-meromorphic function.

[Flo (Florent Schaffhauser)]

Sebastien Gouezel said:

I don't understand the question. Consider the function f equal to 1/z on the unit disk, except at 0 where it is equal to 37, and which is arbitrarily bad outside the unique disk. Would you use your predicate as PremerormorphicOn f (ball 0 1) here?

Yes, that is also unclear to me. And if one wants to define a meromorphic function on ball 0 1, will it be necessary to also give its values outside the open unit ball?

And if the function is equal to 0 at 0, would you like to promote it to MeromorphicOn f (ball 0 1), or would the latter be kept for functions taking values in the Riemann sphere (and equal to infinity at the pole)?

I would say: only in the second case is the function promoted to MeromorphicOn f (ball 0 1). But maybe I am not understanding what the consensus is this far.

[Junyan Xu]

David Loeffler said:

Junyan Xu IMHO, the problem with that definition is that it is not a predicate on functions $G \to \mathbb{C}$.

I think it is if you existentially quantify over the thin set M? The definition says that $f$ is a holomorphic function on $G\setminus M$, but we can instead say that $f : G \to \mathbb{C}$ is holomorphic on $G \setminus M$ and we don't care about its value outside of $M$.

[Johan Commelin]

In my opinion, Meromorphic{X} should be reserved for equivalence classes of "premeromorphic{X} functions". In particular, it will not be a predicate on honest functions. So

the function f equal to 1/z on the unit disk, except at 0 where it is equal to 37, and which is arbitrarily bad outside the unique disk

will be PreMeromorphicOn f (ball 0 1), and if it is in fact 0 [edit: 1/z] outside the disc (but still equal to 37 at 0) then it will be PreMeromorphic f.

[David Loeffler]

Johan Commelin said:

In my opinion, Meromorphic{X} should be reserved for equivalence classes of "premeromorphic{X} functions". In particular, it will not be a predicate on honest functions. So

the function f equal to 1/z on the unit disk, except at 0 where it is equal to 37, and which is arbitrarily bad outside the unique disk

will be PreMeromorphicOn f (ball 0 1)

Agreed.

and if it is in fact `0` outside the disc (but still equal to `37` at `0`) then it will be `PreMeromorphic f`.

I don't think you meant that :smile:

[Johan Commelin]

Yes, you are right, I didn't mean that. Of course I meant 1/z outside the disc. :see_no_evil: :oops:

[Junyan Xu]

IMO Meromorphic/MeromorphicOn should be a predicate, and the bundled/equivalence class version could be called (as suggested before) MeromorphicMap or Meromorph.

[Johan Commelin]

Fair enough. But I would even think that we might have only a predicate PreMeromorphic{X} and a bundled Meromorph{icMap}. I'm not sure what the predicate Meromorphic{X} would be... (I can come up with definitions, but they don't seem to have a useful API.)

[Junyan Xu]

Note that my Meromorphic is your PreMeromorphic (see my vote above). We could maybe define some MaximallyMeromorphic that is the Meromorphic that you have in mind (i.e. equals to $\hat{f}$ on $G\setminus P$ in the textbook definition), but yes it's probably not very useful. If you already allow $\infty$ be replaced by an arbitrary value, why not allow a thin set of finite values to be arbitrary as well?

[Wen Yang]

Geoffrey Irving 发言道：

I’ve formalized complex manifolds and the Riemann sphere as part of the Mandelbrot work

Where is it in mathlib4? I am going to formalize hyperbolic surfaces, so I need the Riemann sphere.​

[Geoffrey Irving]

^ It’s in a separate repo that I’ve just finished porting to Lean 4. Will share in a couple days, and then I can start porting whatever pieces people want. AnalyticManifold and the RiemannSphere might be a good place to start.

[Geoffrey Irving]

^ And here's the thread about the Lean 4-ported repo: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Mandelbrot.20-.20Lean.204.20version/near/396156117