API for divisors in complex analysis

Stream: mathlib4

[Stefan Kebekus]

I would like to add an API for divisors, a standard tool in complex analysis to keep track of pole/vanishing orders of meromorphic objects, typically functions or differential forms. In principle that is very easy: the textbook definition for a divisor on a domain U is a function to ℤ whose support is locally finite in U. In lean, I guess this translates to:

structure Divisor (U : Set ℂ)
  where
  toFun : ℂ → ℤ
  supportInU : toFun.support ⊆ U
  supportDiscreteWithinU : toFun =ᶠ[Filter.codiscreteWithin U] 0

instance (U : Set ℂ) : CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ)
  where
  coe := Divisor.toFun

attribute [coe] Divisor.toFun

I think that I should give the set of divisors the structure of a partially ordered group, so users can work with standard tactics on expressions involving divisors. I am, however, fairly new to lean and struggling to set up the necessary structures/classes/types/instances correctly. Any help is greatly appreciated.

@Johan Commelin @Markus Himmel @Yaël Dillies You probably know the answer to my question right away ... perhaps you could point me to code that I can copy, or help me with a little template that I can use as a starting point? Thanks!

[Yaël Dillies]

There are indeed plenty of examples in mathlib. If you look at docs#DFunLike and docs#SetLike and uncollapse "Instances", you will be given a list of similar constructions

[Yaël Dillies]

Hopefully that's enough to get you started. Feel free to come back with more specific questions once you have them :smile:

[Stefan Kebekus]

@Yaël Dillies Thanks for your very quick answer, I will look at this ... and probably come back to you soon.

[Michael Stoll]

@Stefan Kebekus Do you know about docs#Finsupp ?

[Stefan Kebekus]

@Michael Stoll No, I did not know that. That seems like code I can easily copy, thank you!

... und schöne Grüße nach Bayreuth.

[Michael Stoll]

import Mathlib

variable {U : Set ℂ}

#synth AddCommGroup (U →₀ ℤ) -- Finsupp.instAddCommGroup

It comes with an abelian group instance :smile:
(But note that here U is promoted to a subtype of ℂ.)

Grüße nach Freiburg!

[Michael Stoll]

(I realize that you want discrete, not finite, though. So you will indeed have to copy and adapt the code.)

[Stefan Kebekus]

Yes, I will need to adapt. But maybe this is now doable...

[Stefan Kebekus]

The API for divisors is now available as PR 22357. Thanks to everyone for your generous help.

@Michael Stoll If you have the time for a review…

[Jz Pan]

Maybe more generally you should define locally of finite support function as a generalization to Finsupp?

[Stefan Kebekus]

The API for divisors is now available in mathlib. Thank you for all your help! As soon as PR #22292 (characterize level sets of the order for analytic/meromorphic functions) is reviewed and merged, I can define the divisor of a meromorphic function.

[Johan Commelin]

I was discussing algebraic cycles with @Raphael Douglas Giles the other day. And it turns out that if X is a scheme, then an algebraic cycle on X is exactly the same as your Divisor X (except that X is not a topological field).

So I'm coming around to the idea that maybe we should drop that field condition from your definition. Of course it would be weird to call it Divisor when X is a higher dimensional scheme, because we're now also talking about algebraic cycles in higher degrees (aka codimension).

After all, an algebraic cycle (non-homogeneous, because we'll add the grading by subgroups later) is a formal sum of integral closed subschemes, but we might as well take a formal sum of the generic points.
And the sum has to be locally finite, but that's exactly the condition that you also have.
And a sum of generic points is locally finite if and only if the sum of integral closed subschemes is locally finite.

[Jz Pan]

This reminds me of Fulton's Intersection Theory

2025-03-15 153149.png

[Stefan Kebekus]

@Johan Commelin I think you are right, the proposed definition for "cycle" will work on analytic spaces and analytic schemes, modulo the question of whether "locally finite" or "discrete" is the correct definition [would have to think]. I guess the same (or something very close) will also work in more general settings [ind-schemes, algebraic spaces, stacks, Riemann-Zariski-Spaces, Berkovich analytic spaces, p-Adic nonarchimedian, …]. But we have no definition for a super-type that comprises all these spaces.

[Stefan Kebekus]

Dear all, in private communication with Comellin, we considered the following way out: We rename "DivisorOn U" and make ourselves honest by calling it what it really is: "Function.discretesuppWithin U ℤ", defined for arbitrary topological spaces. The method "MeromorphicOn.divisor f U" will then simply return an object of type "Function.discretesuppWithin U ℤ", which is no big deal.

[Stefan Kebekus]

If people here agree to this suggestion, I would be glad to implement that. To avoid chaos, I would however wait until PR 22819 is merged.

[Stefan Kebekus]

@Jz Pan Thanks for pointing that out! Note, however, that the setting is more involved in the complex analytic case we consider here. The topological space underlying a complex space is more involved and definitively not Noetherian. This brings up the "local finiteness" condition that is so much easier in algebraic geometry.

[Stefan Kebekus]

@Johan Commelin I started implementing this suggestion, but I got a little stuck. Could you please have a look at the file Mathlib/Analysis/Meromorphic/Divisor/Basic.lean in branch origin/kebekus/divisor.2?

Never mind the file name and the out-of-date docstrings … there are a few lines that do not compile, and I cannot fix that because I have no clue what your optimized code is doing.

Thanks!

[Johan Commelin]

@Stefan Kebekus I took the liberty of pushing a tiny patch directly to that branch.

[Johan Commelin]

To fix the final error, I changed OrderedAddCommGroup to LinearOrderedAddCommGroup. Because the latter is a Lattice, while the former is not...

[Johan Commelin]

I don't know if this still matches your intentions.

[Stefan Kebekus]

Thanks for the quick & helpful response! That was exactly what I needed.

[Raphael Douglas Giles]

I'm wondering, for the application of this stuff to algebraic cycles on schemes, should we change the condition that the support is discrete to say that the support is locally finite (and then in your case where k is a T1 space using your theorem to translate into your current definition)? I think in the case of schemes these definitions shouldn't be equivalent, but maybe I'm missing something

[Stefan Kebekus]

@Raphael Douglas Giles Message arrived. I will need a while to think.

[Stefan Kebekus]

I have now implemented Johan's and Raphael's suggestions -- there is a new type class Function.locallyFinsuppWithin and two files, Mathlib/Analysis/Analytic/Divisor.lean and Mathlib/Analysis/Meromorphic/Divisor.lean that define divisors for analytic functions in one variable and for meromorphic functions, respectively. The code now uses the new method WithTop.untop₀ that was discussed earlier in a different thread.

The result is available as PR #23296.

@Johan Commelin If you can find some time to look at the PR…

[Johan Commelin]

@Stefan Kebekus Thanks! Do you think it's easy to do the renaming in a separate PR? That should be a quick merge. And then the diff of this PR will be much smaller.

[Stefan Kebekus]

@Johan Commelin Thanks for the prompt reply. I am unsure what precisely "renaming" refers to.

• Renaming of the file? -- Probably yes.
• Renaming of the type class? -- Probably no, for two reasons. First: the type class is used in the *Divisor.lean files. Second: Following Raphael's suggestion, we also change the API from "disceteWithin" to the new "locallyFinsuppWithin". This is reflected by changes in the construction of the divisor.
  I am unsure if that answers your questions. Does it?

[Johan Commelin]

Just the file rename should already help make the diff of the current PR more legible.
In fact, I'm surprised that git doesn't recognize this as a rename...

[Stefan Kebekus]

Ok. I will see what I can do and come back to you.

[Johan Commelin]

Merci!

[Stefan Kebekus]

@Johan Commelin Voliá. Here is a new PR #23302.

[Johan Commelin]

@Stefan Kebekus Thanks! That diff is much easier to review.

[Johan Commelin]

3 small comments, but basically ready to merge.

[Stefan Kebekus]

Small comments are addressed.

[Stefan Kebekus]

@Johan Commelin Files are moved to their final location in PR #23328.