winding number

Stream: Is there code for X?

[Patrick Kinnear]

I am mentoring an undergraduate student in a topology project, and she expressed some interest in Lean. I have been thinking of some topics that could have a related formalization aspect, and I wondered if there is existing work on winding number and related applications such as Borsuk-Ulam, an alternative proof of fundamental theorem of algebra, etc?

[Kevin Buzzard]

Whether or not there's existing work is not normally something I take into account when mentoring undergraduate projects -- if the student wants to prove theorem X and theorem X is already in mathlib then there's a high chance that the proof is incomprehensible to the student, so I tell them to write a well-documented comprehensible proof. But this isn't really an answer to your question, sorry

[Patrick Kinnear]

Thanks Kevin! I actually agree with the above but would still like to know whether there are existing approaches out there or not. The goal of the student project would not be (at least in the first instance) a contribution to mathlib.

[Jireh Loreaux]

@Patrick Kinnear unrelated, please tell me your avatar is what I think it is: an origami Yoda?!

[Patrick Kinnear]

Haha yes it is, I think I set this avatar when I was a teenager and don't know how to change it (and don't want to, since that little guy is gone now)

[Vincent Beffara]

I have a related answer :-) a few people are thinking about doing more complex analysis in Lean, but there is not much there yet. Things like continuous determinations of the argument and the logarithm on a simply connected domain for instance are on the roadmap, and should not be too far away from defining winding numbers in the plane. We also don't have meromorphic functions yet, and in particular the residue formula is not there either except in very particular cases. So there is a lot to be done in that direction!

[Vincent Beffara]

Actually defining winding numbers along C^1 paths in the complex plane, proving that they indeed are integer, this should already be quite doable.

[Patrick Kinnear]

Thanks Vincent!

[Antoine Chambert-Loir]

In spite of what its huge size might let everybody think, mathlib lacks a lot of basic stuff in many areas, and one discovers that when one tries something which is slightly off path of the main stream of results. So alternative proofs of the fundamental theorem of algebras, or of quadratic reciprocity, or of whatever results in analysis (Zygmund, Polya-Szegö's book) or in linear algebra, are certainly a good occasion of discovering (small) holes in the library, filling them while proving (new or not new) results.

[Anatole Dedecker]

@Patrick Kinnear Were you thinking of the analytic definition, or the purely topological one (via path lifting through a covering)? As Vincent said a few people are working/thinking about the analytic approach here, but I would also love to develop the topological approach. Note that there is almost nothing here (we have the definition docs#IsCoveringMap, but not much more), which is bad for us but maybe good for your student: if she is interested in contributing to mathlib, there should be a decent number of relatively low-hanging fruits in that direction, and even the path-lifting theorem (not the general lifting theorem) shouldn't be too hard IIRC (though it's probably a bit ambitious for a first project).

[Anatole Dedecker]

@Thomas Browning since you wrote the definition, do you have specific plans about developping the theory of covering spaces?

[Thomas Browning]

Anatole Dedecker said:

Thomas Browning since you wrote the definition, do you have specific plans about developping the theory of covering spaces?

@Jordan Brown and I are working on homotopy lifting. Uniqueness is done (ported from lean3), and we're starting on existence.

[Vincent Beffara]

Do we know that the exponential is a covering map of C^* ?

[Vincent Beffara]

In fact there is some discussion about what the appropriate setup is for contour integrals (as would be applied to e.g. state the residue theorem). Either restrict to C^1 paths, and then there is no issue of definition but the link with the homotopy part of the library is not so direct; or allow continuous paths (and nice topological things), but then one can only integrate functions that are locally derivatives. In the end we will likely need both.

[Anatole Dedecker]

I think currently nothing imports the definition of covering maps, so it probably doesn’t exist

[Junyan Xu]

The correct generality for contour integrals is probably this this? Mathlib has docs#StieltjesFunction (less general than bounded variation) but not any Stieltjes-flavored integration afaik. (Update: Apostol does use Riemann-Stieltjes to define contour integrals.)

[Vincent Beffara]

There is certainly a way to define contour integrals along rectifiable curves, but I do believe that integrating a holomorphic function along a docs#Path and being able to state that the integral is invariant under docs#Path.Homotopic is something that we should have.

[Junyan Xu]

I think you probably have to homotope the path to a rectifiable/smooth one and show the existence of homotopy through such paths if it's between two such paths, because I can't imagine how you could define integral along a non-rectifiable curve directly ...
For rectifiable curves, this seems to be a feasible way to convert to a Lebesgue integral that we already have.

[Vincent Beffara]

You can integrate a locally exact differential form along a continuous curve by choosing a fine enough subdivision. But this does put a restriction on the kind of functions that you can integrate this way (they have to locally be derivatives - but this is the case for holomorphic functions)

[Antoine Chambert-Loir]

Vincent Beffara said:

There is certainly a way to define contour integrals along rectifiable curves, but I do believe that integrating a holomorphic function along a docs#Path and being able to state that the integral is invariant under docs#Path.Homotopic is something that we should have.

I remember from my Complex Analysis courses (or Ruding's book, IIRC) that proving invariance by homotopy is rather delicate if you actually try to move the paths. Instead, it is worthwile to do invariance by homology, considering not only closed paths but formal linear combinations of them (let's call them “chains”).

[Junyan Xu]

The definition and homotopy (rel endpoints) invariance of integration of a locally exact form in a domain D along an arbitrary path p : I → D can actually be reduced to the homotopy lifting property for covering spaces. Take the space D × ℂ and equip it with the strongest topology such that for any primitive φ of the locally exact form on an open subset U ⊆ D, the map x ↦ (x, φ(x)) from U to D × ℂ is continuous, and we can show the projection from D × ℂ (with this topology) to D is a covering map. Given a path p : I → D we can then lift it to q : I → D × ℂ such that q(0) = (p(0), 0), and then the second coordinate of q(1) will be the integration of the locally exact form along p. We can lift a homotopy H : I × I → D to D × ℂ too, which yields homotopy invariance of q(1).

The space D × ℂ is an example of the etale space of a (pre)sheaf and the general construction is found in Exercise II.1.13 of GTM52. In the general construction the fiber over x : D is not ℂ but the stalk of the sheaf (of primitives) at x, but a germ at x is uniquely determined by its value at x in this case.

Etale spaces can also be used to prove the monodromy theorem, and in fact Conway does so in his GTM11, but the version he proved is weaker because it requires unrestricted continuation within a domain, while the Wikipedia version only assumes a continuation along each curve exists. Under the stronger assumption, Conway shows the Riemann surface of the analytic germ (the (path) connected component of the etale space (of the sheaf of analytic functions) containing the germ) is a covering space of the domain. In general, the etale space is not necessarily a covering space as continuation can hit a singularity anywhere, but the projection π : E → X is always a local homeomorphism.

To prove the monodromy theorem we have to show two things: (1) the lift of a path (or any continuous map from a connected, locally connected space Y to X) fixing an endpoint is unique; (2) if we can lift every path (for fixed y : Y) in a homotopy I × Y → X to E, then the map I × Y → E obtained by combining the lifted paths is continuous. For (1), given two lifts p1 and p2 we want to show {t :I | p1 t = p2 t} is nonempty (contains 0), closed (requires E to be Hausdorff), and open (this only requires that every point of E has a neighborhood U that is open and closed in π⁻¹(π(U)) such that π is injective on U, which is weaker than π being a covering map. I being locally connected is crucial here). For (2), we can follow the arguments here and show that every y : Y has a connected neighborhood V such that on I × V we may piecewise define a continuous lift using the U's around the image of I × {y} in E (we also need that π restricts to a homeomorphism on U here). By uniqueness of lifts V → E the map I × V → E is well-defined and continuous, and therefore for fixed y : V restricts to paths I → E that lifts the respective I → X, so again by uniqueness of lifts the original map I × Y → E agrees with this I × V → E on I × V and therefore is continuous at I × {y}, and since y is arbitrary it's continuous everywhere.

(There's apparently some more complicated argument to circumvent local connectedness.)

Another target of this approach would be the developing map from the universal cover (i.e. paths with fixed left endpoint up to homotopy rel endpoints) of a (G,X)-manifold to the model space X. This can be obtained by considering the (pre)sheaf of charts U ⊆ M → X and its etale space (which is a covering space), and homotopy invariance shows that the developing map is well-defined.

[Vincent Beffara]

This sounds further and further away from a doable first Lean project for a student :-) but indeed that would probably be the most mathlib-y approach. I have a proof-of-concept definition for integrals of a holomorphic function along continuous paths here https://github.com/vbeffara/RMT4/blob/main/RMT4/pintegral.lean with prerequisites about subdivisions here https://github.com/vbeffara/RMT4/blob/main/RMT4/Subdivision.lean but in retrospect what I am doing could likely be refactored in terms of coverings and path liftings, I will give it a thought.

[Junyan Xu]

Do we know that the exponential is a covering map of C^* ?

Maybe you can reduce to that the reals cover the circle, for which docs#Ico_eq_locus_Ioc_eq_iUnion_Ioo and docs#AddCircle.homeoIccQuot probably help. (A stronger thing to prove is that it's a Z-bundle.) We have docs#AddCircle.toCircle but it's not a homeo. I guess we can define winding number just using the reals over circle cover though.

[Junyan Xu]

I saw the other thread about the Riemann mapping theorem, and I think the last step would also be easy if we have enough about covering spaces. If we show that exp is a covering map from C to C\{0}, then a nonvanishing continuous function f on a simply connected domain can be lifted to obtain a continuous branch of log f, and it's holomorphic if f is, because exp is locally biholomorphic (because it has nonzero derivative, which can be implied by being a covering map (local injectivity is sufficient)). So we can bypass showing that primitives (in particular of dz/z) exist on a simply connected domain, although this can also be shown using the etale space approach above.

[Kevin Buzzard]

Now we have modular forms it would be interesting to see if we can formalise the short proof of Picard's theorem using the lambda function (a holomorphic covering map from the open unit disc to C - {0,1}).

[David Loeffler]

Kevin Buzzard said:

Now we have modular forms it would be interesting to see if we can formalise the short proof of Picard's theorem using the lambda function (a holomorphic covering map from the open unit disc to C - {0,1}).

I think this would be quite hard. How do you envisage showing that the lambda function is surjective onto $\mathbb{C} - \{0, 1\}$?

AFAIK, we don't know how to prove (yet) that the j-invariant is surjective (from the upper half-plane to $\mathbb{C}$). This is one of a bunch of things which follows easily from the valence formula, but formalising the standard proof of that (a contour integral around the boundary of the standard fundamental domain) is rather troublesome. It seems to me that proving surjectivity of the lambda-function should be at least as hard -- they are pretty much analogous, $j$ is the Hauptmodul for $\Gamma(1)$ while $\lambda$ is the Hauptmodul for $\Gamma(2)$.

[Kevin Buzzard]

I guess one could factor that out! One could prove "if there's an unramified map from the open disc to C-{0,1} then Picard is true" and then worry about the modular form argument later.

[David Loeffler]

I don't think it's really a "modular form argument" that's missing. What we're lacking is topological / complex-analytic: properties of contour integrals.

[David Loeffler]

Defining winding numbers of paths would definitely be a good start towards this. I'm very pleased to learn that work is under way to formalise the lifting property of coverings. @Thomas Browning please keep me posted on this!

[Vincent Beffara]

Junyan Xu said:

I saw the other thread about the Riemann mapping theorem, and I think the last step would also be easy if we have enough about covering spaces. If we show that exp is a covering map from C to C\{0}, then a nonvanishing continuous function f on a simply connected domain can be lifted to obtain a continuous branch of log f, and it's holomorphic if f is, because exp is locally biholomorphic (because it has nonzero derivative, which can be implied by being a covering map (local injectivity is sufficient)). So we can bypass showing that primitives (in particular of dz/z) exist on a simply connected domain, although this can also be shown using the etale space approach above.

Yes, if you can construct a log on the domain then you get a square root and the rest of the RMT proof works. But it seems like there would be a huge intersection between this and integrating dz/z

[Junyan Xu]

Yes, if you can construct a log on the domain then you get a square root and the rest of the RMT proof works. But it seems like there would be a huge intersection between this and integrating dz/z

I just want to that the (unique) existence of a lift for a map from a simply connected domain follows from general properties of covering spaces (lifting criterion), and it's not hard once we can lift paths uniquely. Constructing a log is about the covering map exp, while integrating dz/z is about the covering space D × ℂ → D I constructed earlier.
image.png

[Antoine Chambert-Loir]

In a course I taught 10 years ago, based on notes by Bost, I had given a proof of Picard's theorem that does not use the valence stuff, but it might use a bit of basic theory of Riemann surfaces. Surjectivity of j-function is done by showing that it tends to infinity when tau goes to infinity in the fundamental domain.
Link to notes : https://webusers.imj-prg.fr/~antoine.chambert-loir/enseignement/2011-12/tngd/tngd.pdf

[Junyan Xu]

the lambda function (a holomorphic covering map from the open unit disc to C - {0,1})

I'm not sure how we'd go about defining the lambda function; I know that we have Eisenstein series (not in mathlib yet) but not for arbitrary congruence subgroup (Γ(2) in this case) of SL(2,Z), I think. So it would be straightforward to get the j-invariant but not the lambda function. (What's the formula of lambda in terms of those Eisenstein series?)

However, there does exist a pretty elementary geometric construction of the lambda function (or rather, a holomorphic covering $\mathbb{H}\to\mathbb{C}\setminus\{0,1\}$ which is not shown to be equal to lambda), as explained in Li Zhong's complex analysis textbook (复分析导引, 李忠).
image.png

[Junyan Xu]

The idea is to start from half a fundamental domain D of the Γ(2)-action, which is an ideal triangle (something like $\{z \mid 0 < \text{Re}\ z < 1, |z| > 1 \}$ in the upper half plane, or the triangle bounded by three mutually tangent arcs tangent to the boundary in the unit disk). D is obviously homeomorphic to a disk, so using the Riemann mapping theorem (this part is not so elementary, I admit), we can find a biholomorphic map μ from D onto the upper half plane, and because the boundary of D is a simple closed curve, μ extends to a homeomorphism from the closure of D to the closed upper half plane (this certainly requires proof), with the boundary mapping into the real axis union ∞. By composing with an automorphism of the half plane, we may assume the three boundary points 0,1,∞ are mapped to 0,1,∞.

Using the Schwarz reflection principle, we may iteratively extend μ across the three sides of the ideal triangle, eventually filling up the whole disk / upper half plane. (Note that the sides don't include the endpoints 0,1,∞, so μ takes every real value except 0 and 1 on the sides.) μ together with one of its reflection are already enough to cover the whole C\{0,1}, but it will take more effort to show that the final result of the extensions is a covering map (for example, it's tricky to pin down the preimages of each of the three segments of the real line).

Instead of using the perfectly symmetric trivalent tree structure in the disk, for formalization purposes I expect it to be easier to break the symmetry and work in the upper half plane. We focus on the closed ideal triangle $\{z \mid 0 \le \text{Re}\ z \le 1 \}$ and show that after countably many steps of extension we exhaust all points in the domain. At the beginning (step 0) we have μ defined on the subregion of points on or above the semicircle with endpoints 0 and 1, and at step n there would be $2^n$ semicircles with rational numbers $0=r_0 < r_1 < r_2 < \dots < r_{2^n}=1$ as their endpoints, and μ would be extended to the subregion of points on or above the semicircles. At every step (except the first), for every $i=0,1,\dots,2^{n-1}$ we take the region bounded by the three semicircles through $r_{2i},\ r_{2i+1}$ and $r_{2i+2}$ (on which μ is already defined) and reflect it across the two lower semicircles, partitioning both intervals $[r_{2i}, r_{2i+1}]$ and $[r_{2i+1}, r_{2i+2}]$ into two and obtaining a total of four new semicircles. It turns out the sequence $r_i$ of $2^n+1$ rational numbers is exactly the Stern--Brocot sequence and the diameter of the semicircle through $r_i$ and $r_{i+1}$ is equal to $1/q_i q_{i+1}$, where $q_i$ is the denominator of $r_i$. Since the denominators of new rational numbers inserted must eventually go to infinity, the sizes of the semicircles at step n goes to 0 as n goes to infinity, which shows that we can extend μ to the whole ideal triangle $\{z \mid 0 \le \text{Re}\ z \le 1 \}$. After that, one more reflection + translation is enough to extend μ to the whole upper half plane.

(I didn't know that the Stern--Brocot sequence can be generated this way through conformal reflection across circles, but it's just a simple computation: if you have three real numbers p,q and r, then the reflection through the circle with pq as diameter takes r to ((p+q)r-2pq)/(2r-p-q)=(p(r-q)+q(r-p))/((r-p)+(r-q)), and when p=a/b, q=(a+c)/(b+d), r=c/d and bc-ad=1 we have (p(r-q)+q(r-p))/((r-p)+(r-q))=(2a+c)/(2b+d), which is sufficient to inductively show the sequence $r_i$ agrees with Stern--Brocot.)

[Junyan Xu]

Instead of extending in a step-by-step manner, we can also show that two copies of the ideal triangle form a fundamental domain of the Γ(2)-action and see out how its four boundary segments are identified in pairs by the group action, and use the group action to extend μ immediately to the whole upper half plane. Here's how a Lean proof could go: let $D_4$ denote the ideal triangle with one reflected copy attached to every side. By Schwarz reflection μ is defined on $D_4$, holomorphic on the interior, with image equal to C\{0,1}. Since two copies of the triangle already form a fundamental domain, $D_4\to\mathbb{H}/\Gamma(2)$ is surjective and we can show it's a quotient map. The points in $D_4$ identified by the Γ(2)-action have the same image under μ, so μ factors through a continuous function $\mu': \mathbb{H}/\Gamma(2)\to\mathbb{C}\setminus\{0,1\}$, which we show to be a homeomorphism. The quotient map $\mathbb{H}\to\mathbb{H}/\Gamma(2)$ is a covering map because the Γ(2)-action is docs#ProperlyDiscontinuousSMul, so composing with μ' we get a covering map $\mathbb{H}\to\mathbb{C}\setminus\{0,1\}$, which is also holomorphic, because it's holomorphic in the interior of $D_4$, which intersects every Γ(2)-orbit in $\mathbb{H}$ (note the three sides of an ideal triangle are all in the interior), and Γ(2) acts biholomorphically.

Given that we have the Riemann mapping theorem for the domain D (which is star-shaped in the unit disk so it's easy to show primitives exist on it, and lifting $\mathbb{C}\to\mathbb{C}\setminus\{0,1\}$ should also be easier because $\mathbb{C}$ is star-shaped, so we may not need homotopy lifting in full generality but it's definitely nice to have it), the hardest missing ingredient seems to be the extension of this Riemann map to the boundary (see this answer which gives Conway's book as reference).

[Junyan Xu]

Regarding valence formula for modular functions, there was a talk by @Manuel Eberl half a year ago at the Cambridge seminar, and I have screenshots of some of the slides that I'm willing to share with people working on it, but it would be even better if he could share the full slides. (This blog post says he has some joint forthcoming work, but I don't find it published anywhere.)

[Vincent Beffara]

There is an elementary proof of Picard's theorem in the book of Tauvel in chapter 13, based on a quantitative version of the open mapping theorem for holomorphic functions and a few prerequisites on spaces of holomorphic functions that are almost in Mathlib.

[Wenda Li]

Junyan Xu said:

Regarding valence formula for modular functions, there was a talk by Manuel Eberl half a year ago at the Cambridge seminar, and I have screenshots of some of the slides that I'm willing to share with people working on it, but it would be even better if he could share the full slides. (This blog post says he has some joint forthcoming work, but I don't find it published anywhere.)

Manuel's slides at Certified and Symbolic-Numeric Computation this year could be relevant. As for the formalising work, we finished four chapters of Aposol's textbook -- the paper is still in preparation though :-)

[Junyan Xu]

Thanks! Yeah the relevant slides (from page 24 on) look identical. Looking forward to your paper!

[Junyan Xu]

based on a quantitative version of the open mapping theorem for holomorphic functions

That seems to be called Landau's theorem on Wikipedia, but Wikipedia's proof of little Picard using it is very confusing. I found this book chapter which is much better and probably similar to the proof in Tauvel.

[Junyan Xu]

Actually, since the valence formula is basically computing the degree of the line bundle of k-differential forms on a compact Riemann surface (or a finite quotient of it with orbifold points), the mathlib-y way is probably proving it in that generality ...

Only the other hand, little Picard also has a strengthening/quantitative version called the Schottky's theorem.

[Junyan Xu]

@Thomas Browning @Jordan Brown FYI I've formalized the continuity part of homotopy lifting at this gist. My motivation is to produce a general enough version to prove the monodromy theorem, and my work probably overlaps with yours, but I hope it also fills in some missing pieces.

[Vincent Beffara]

In the meantime I wrote some API for interval subdivisions, http://vbeffara.perso.math.cnrs.fr/RMT4/RMT4/Subdivision.html#Subdivision.exists_adapted is similar to your lebesgue_number_lemma_unitInterval and in http://vbeffara.perso.math.cnrs.fr/RMT4/RMT4/pintegral.html there is a partial version of existence in the case of integrating holomorphic functions along continuous curves - and indeed http://vbeffara.perso.math.cnrs.fr/RMT4/RMT4/pintegral.html#LocalPrimitiveOn looks very much like a trivialization of the covering you mentioned in that case.

[Vincent Beffara]

(Existence is much easier to build in that case because IIUC it amounts to telescopic sums instead of general gluing of continuous functions ...)

[Vincent Beffara]

Here https://github.com/vbeffara/RMT4/blob/main/RMT4/Covering.lean is some code defining the topology on D \times \C and proving that the fibers are discrete, from local existence of primitives. I think there is not much missing to show that the projection is a covering.

Is there a name for "a bunch of maps for each open set of an open covering, such that if they agree anywhere on the intersection of two open sets they agree everywhere on the intersection"?

[Junyan Xu]

Not sure what to call it. I've just been able to show that a free, properly discontinuous action induces a covering map, and as a consequence the real line covers the circle. It should be relatively easy to show the projection is a covering using docs#IsOpenMap.to_quotientMap combined with my QuotientMap.trivialization_of_mulAction. However, there doesn't seem to be a type synonym to put the discrete topology on \C ...

[Vincent Beffara]

We can always do this

def discrete (α : Type) : Type := α

instance {α : Type} : TopologicalSpace (discrete α) := ⊥

instance {α : Type} : DiscreteTopology (discrete α) := ⟨rfl⟩

and use discrete \C but this loses all the rest of the nice features of the complex numbers... and with abbrev instead I believe we get two competing instances of TopologicalSpace?

[Johan Commelin]

Sorry, I haven't followed in detail. But why do you need the discrete topology? Are you mapping into it? Because there is an API for locally constant functions, which are of course the same thing as continuous functions into a discrete space.

[Vincent Beffara]

With abbrev:

import Mathlib

abbrev discrete (α : Type) : Type := α

instance {α : Type} : TopologicalSpace (discrete α) := ⊥

instance {α : Type} : DiscreteTopology (discrete α) := ⟨rfl⟩

def φ : ℂ → discrete ℂ := λ z => z

def ψ : discrete ℂ → ℂ := λ z => z

example : Continuous φ := by continuity

example : Continuous ψ := by continuity

which looks really really bad (but that was expected)

[Vincent Beffara]

A trivialization of a covering is a local homeomorphism with a product with a discrete space, which we possibly need to mention at some point; and in the context above, that discrete space is just \C but with discrete topology

[Vincent Beffara]

docs#IsEvenlyCovered wants I to have discrete topology

[Anatole Dedecker]

I’ve been wanting a Discrete type alias for some time, with some API it shouldn’t be too bad

[Yaël Dillies]

I've been helping write aliases for the order theoretic topologies, so I know what the API should look like.

[Junyan Xu]

I did letI : TopologicalSpace G := ⊥; have : DiscreteTopology G := ⟨rfl⟩ to endow the discrete topologyin the above gist, but when G already has a topology I don't know what happens. Maybe you can disable certain instances to avoid conflicts, but I think I should provide a version of QuotientMap.trivialization_of_mulAction with IsCoveringMap as conclusion so I don't need to include DiscreteTopology among the assumptions ...

[Vincent Beffara]

Ah but if you replace one instance by another, you make many (but not all) other instances incompatible with the new one ... if you replace the topology, then continuity of the product might fail (well not if you put the discrete topology of course but you get the point).

[Vincent Beffara]

A big part of the covering structure just wrote itself, only open_source and the continuity of toFun and invFun are missing. Which makes sense because those are the bits that depend on the weird topology on the space, so the correct proof will involve e few more API lemmas.

[Anatole Dedecker]

I think it would make sense to change the definition of docs#IsEvenlyCovered to:

def IsEvenlyCovered (x : X) (I : Type*) :=
  ∃ t : Trivialization (Discrete I) f, x ∈ t.baseSet

[Vincent Beffara]

Hm, that requires some thinking. In the case of covering spaces I is already discrete anyway, so the Discrete is redundant and might add some friction in the API. But we can experiment while Mathlib.Topology.Covering is a leaf.

[Anatole Dedecker]

We could always add some characterizations assuming [DiscreteTopology I] but I get your point

[Vincent Beffara]

Also, with your change and the current definition of covering maps, there are too many coverings IIUC: Prod.fst seems to always fit. So we would need to put the discreteness condition back in IsCoveringMap. (I didn't think this through so it may well be complete nonsense ...)

[Anatole Dedecker]

I don't think so.fst : ℂ × ℂ → ℂ would still not be a covering because it doesn't locally trivialize to ℂ × (Discrete ℂ) right?

[Anatole Dedecker]

Oh wait I didn't think this through either

[Junyan Xu]

I think you're right, docs#Trivialization .toFun would be ℂ × ℂ → ℂ × (Discrete ℂ) which isn't continuous.

[Anatole Dedecker]

Yes I've checked and I'm confident in my claim now, because the current definition of IsCoveringMap with this new IsEvenlyCovered would still imply that the fibers are discrete

[Vincent Beffara]

OK then. :man_facepalming: