Path lifting

Stream: maths

[Vincent Beffara]

Here https://github.com/vbeffara/RMT4/blob/main/RMT4/Lift.lean is the proof of the existence of lifts of continuous paths through coverings, namely:

variable {E X : Type*} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {γ : C(I, X)} {A : E}

theorem lift (hf : IsCoveringMap f) (hγ : γ 0 = f A) : ∃ Γ : C(I, E), Γ 0 = A ∧ f ∘ Γ = γ

I would like to PR it, but in fact I am wondering whether it is at the right level of generality. Indeed, some intermediate lemmas (but not all) don't use the fact that neighborhoods can be chosen uniformly along the fibers, and the discreteness of the fibers appears nowhere at all. What to do?

[Vincent Beffara]

(I misclicked, this probably belongs in #maths but I can't move it now.)

[Anatole Dedecker]

Didn’t @Thomas Browning say he was working on that too?

[Vincent Beffara]

Oops, I didn't catch that :man_facepalming:

[Patrick Massot]

I am pretty worried by that C(I, X). Why aren't you working with function defined on $\R$?

[Vincent Beffara]

Mostly to make life more difficult because of all the coercions, in retrospect. (And to use ConnectedSpace on it but that is minor.) What worries you about it?

[Patrick Massot]

I'm worried it will be difficult to use, because of all the coercions.

[Anatole Dedecker]

On the other hand we have docs#Path which you could use here (and in that case you indeed end up having a function only defined on I)

[Adam Topaz]

My thoughts on this, FWIW, is that the interval is an important enough object that we should develop as much API around I as possible anyway, so it's probably okay to use I in such statements.

[Anatole Dedecker]

I agree with Adam here, we won’t get far if we have to avoid the interval all the time.

[Thomas Browning]

Anatole Dedecker said:

Didn’t Thomas Browning say he was working on that too?

@Jordan Brown and I were working towards this on branch#jlc_branch at the same level of generality. We already have uniqueness, but if you've got existence finished, I think you might as well PR it.

[Antoine Chambert-Loir]

If you want a supergeneral path lifting theorem, Bourbaki's Topologie Générale has one, but for coverings, one crucial point is you have uniqueness of such a lifting, and this is that result that is to formalize here. (Anyway, I would recommend the treatment there. The result is then extended to cubes and ultimately to all simply connected spaces, in the sense that all of their coverings are trivial, and from the case of intervals, the case of convex subsets of R^n (or of a real topological vector space) follows.

[Antoine Chambert-Loir]

“Supergeneral” means: $I$ is a real interval, $X$ is a non-empty Hausdorff topological space, $f \colon X \to I$ is a continuous map which is open, proper, and whose fibers are totally discontinuous. Then $f$ admits a continuous section. (Topologie Générale, chap. III, §2, n°10, th. 3.)
Interesting applications are: lifting of roots of a continuous family of polynomials, or lifting of a map $I \to X/G$, when $G$ is a discrete group acting properly on $X$.

[Flo (Florent Schaffhauser)]

$f : I \rightarrow X$?

[Vincent Beffara]

The proof of that one is much more involved though, and if I understand it right it is not strictly more general because of the compactness assumptions (e.g. in my initial motivation which is integrating holomorphic functions along continuous paths, the fibers are the complex plane equipped with the discrete topology).

[Vincent Beffara]

Flo (Florent Schaffhauser) said:

$f : I \rightarrow X$?

No, there is a trick in the proof of the Corollaire of Théorème 3, it is indeed f : X -> I (the way to get path lifting from the statement is not obvious).

[Antoine Chambert-Loir]

Vincent Beffara said:

The proof of that one is much more involved though, and if I understand it right it is not strictly more general because of the compactness assumptions (e.g. in my initial motivation which is integrating holomorphic functions along continuous paths, the fibers are the complex plane equipped with the discrete topology).

Indeed, coverings are continuous and open maps, but those with infinite fibers are not proper.

[Junyan Xu]

Patrick Massot said:

I am pretty worried by that C(I, X). Why aren't you working with function defined on $\R$?

docs#Path, docs#ContinuousMap.Homotopy etc. are all defined in terms of the unit interval I, so the current statement is well connected to the homotopy API and I wouldn't worry about it. docs#Set.IccExtend is the way to extend to a path to a function on $\R$ and has extensive API as well.

but for coverings, one crucial point is you have uniqueness of such a lifting

Actually uniqueness also holds under a more general condition (basically: every point upstairs has a neighborhood that is clopen in the preimage of its image, and on which the map is injective).

Didn’t @Thomas Browning say he was working on that too?
Oops, I didn't catch that :man_facepalming:

I saw that they were working on homotopy lifting and later I shared my work with them but did not get a response. I found a mathlib3 branch but not a mathlib4 one. Glad that they finally shared the mathlib4 branch! I like the generality of working with connectedComponent and will probably adapt my more general version of uniqueness to work with that too. And I'll try the approach of defining the lift step by step using a finite partition of the interval and see if it leads to a shorter proof. Maybe I could even work in the generality of IsCoveringMapOn.

[Junyan Xu]

The next step would be proving the lifting criterion; the fundamental group condition is trivial for a map from a simply connected space, so you can get a branch of the square root on a simply connected domain as required for the proof of RMT. Given that the quotient map ℝ → ℝ/ℤ and n-fold cover ℝ/ℤ → ℝ/ℤ have been shown to be covering maps in my PR #7596 (I should probably make them FiberBundles ...), we may utilize the homeomorphism between ℂ \ {0} and ℝ/ℤ × ℝ to show exp and the nth power map are covering maps on ℂ \ {0}. We'd need to show that the product of a covering map with id (or another covering map) is also a covering map, and that composition with homeomorphisms preserves covering maps (there is already docs#Trivialization.compHomeomorph but not a version that changes the base, apparently). In addition to RMT, exp being a covering map would also allow defining the winding number.

#7596 also adds some reasonably convenient constructors for IsCoveringMap, which should be useful for showing the etale space associated to a locally exact form is a covering space. I looked into Bunch.lean and Covering.lean in @Vincent Beffara's repo and it seems the proof that it's a covering space is sorry-free. I think for mathlib we'd probably take a more principled approach though, which is to define etale spaces of presheaves, prove general properties of them, and then specialize to our situation (sheaf of functions such that any two functions agree on an open set, with a group action on the sections that is free and transitive on the stalks). I've started working on this with PR #7655 adding lemmas for local homeomorphisms.

[Vincent Beffara]

Yes this Bunch to covering is sorry free but it does feel like a special case of something more general. I wanted to run towards this contour integral definition ... and the usage of it in Covering.lean is really wrong because I am just picking one local primitive above each point rather than using all of them (the outcome is the same up to homeomorphism anyway, so better not to use choice).

[Vincent Beffara]

I wanted to use partitions initially (and then glue pieces together using the Path API) but in the end just using connexity was easier, at least for path lifting.

[Vincent Beffara]

Is it true in general that if p is a covering then f \mapsto p \circ f is a covering on C(I, X)?

[Antoine Chambert-Loir]

(For uniqueness of lifting along a map $f \colon X \to Y$, the natural hypothesis is that the map $f$ is separated: the diagonal map $X \to X \times_Y X$ is a closed immersion.)

[Junyan Xu]

we may utilize the homeomorphism between ℂ \ {0} and ℝ/ℤ × ℝ to show exp and the nth power map are covering maps on ℂ \ {0}

Actually, it's probably much easier to show the properly discontinuous condition ... which is trivial when the group that acts is finite, and for the case of exp, a translation by a large enough integer certainly separates two compact sets.

Antoine Chambert-Loir said:

(For uniqueness of lifting along a map $f \colon X \to Y$, the natural hypothesis is that the map $f$ is separated: the diagonal map $X \to X \times_Y X$ is a closed immersion.)

Thanks! By stacks#0CY0 it's equivalent to that every two points of Y with the same image in X has disjoint neighborhoods in Y, which is more succinct and more general than what I had. (Actually f doesn't have to be continuous.) You still need local injectivity though, otherwise there are examples like the projection from R^2 to R, or the horizontal projection from the letter Y to the letter I.

Vincent Beffara said:

Is it true in general that if p is a covering then f \mapsto p \circ f is a covering on C(I, X)?

Not sure what the motivation is, but looks like a fun question!

[Vincent Beffara]

The motivation would be to get homotopy lifting for paths on X as path lifting on C(I, X).

[Junyan Xu]

My proof of IsCoveringMap.lift_path is 33 lines using what I already have. For homotopy lifting, the usual proof is to lift each horizontal path and show they combine to form a continuous map on I × I using IsLocallyHomeomorph.continuous_lift. I've also changed my gist to use SeparatedMap as suggested by @Antoine Chambert-Loir.

[Vincent Beffara]

OK I had in mind to show the covering property of f \mapsto p \circ f using continuous_lift or something similar, overall it would amount to roughly the same thing.

Besides using compactness and Lebesgue number vs connexity, we are doing roughly the same. Definitely there should be somewhere in the API a lemma to glue partial paths like we have to do, without the pain of going through frontier_Iic_subset, closure_le_eq, closure_lt_subset_le and so on, but more along the lines of docs#Continuous.if_le for ContinuousOn. That would certainly be useful in other parts of mathlib as well. Essentially docs#Path.trans but without going back to the unit interval.

[Patrick Massot]

There should be things in the sphere eversion project.

[Junyan Xu]

Definitely there should be somewhere in the API a lemma to glue partial paths like we have to do, without the pain of going through frontier_Iic_subset, closure_le_eq, closure_lt_subset_le and so on, but more along the lines of docs#Continuous.if_le for ContinuousOn.

Yeah, a ContinuousOn version of Continuous.if_le would be convenient. Maybe we can furthermore extract something for extending step by step, maybe specific to the unit interval, but let's sure it also applies in the product situation as in IsLocallyHomeomorph.exists_lift_nhds.

BTW the only lemma I used for homotopy lifting about SeparatedMap is separatedMap_iff_nhds, and the rest are just me formalizing stacks#0CY0 :)

[Antoine Chambert-Loir]

Junyan Xu said:

we may utilize the homeomorphism between ℂ \ {0} and ℝ/ℤ × ℝ to show exp and the nth power map are covering maps on ℂ \ {0}

Actually, it's probably much easier to show the properly discontinuous condition ... which is trivial when the group that acts is finite, and for the case of exp, a translation by a large enough integer certainly separates two compact sets.

Antoine Chambert-Loir said:

(For uniqueness of lifting along a map $f \colon X \to Y$, the natural hypothesis is that the map $ f$ is separated: the diagonal map $ X \to X \times_Y X $ is a closed immersion.)

Thanks! By stacks#0CY0 it's equivalent to that every two points of Y with the same image in X has disjoint neighborhoods in Y, which is more succinct and more general than what I had. (Actually f doesn't have to be continuous.) You still need local injectivity though, otherwise there are examples like the projection from R^2 to R, or the horizontal projection from the letter Y to the letter I.

Vincent Beffara said:

Is it true in general that if p is a covering then f \mapsto p \circ f is a covering on C(I, X)?

Not sure what the motivation is, but looks like a fun question!

Bourbaki's Topologie algebrique is full of stuff like that. Probably with I replaced with any locally compact space (compactly generated topology should suffice).

[Antoine Chambert-Loir]

Vincent Beffara said:

OK I had in mind to show the covering property of f \mapsto p \circ f using continuous_lift or something similar, overall it would amount to roughly the same thing.

Besides using compactness and Lebesgue number vs connexity, we are doing roughly the same. Definitely there should be somewhere in the API a lemma to glue partial paths like we have to do, without the pain of going through frontier_Iic_subset, closure_le_eq, closure_lt_subset_le and so on, but more along the lines of docs#Continuous.if_le for ContinuousOn. That would certainly be useful in other parts of mathlib as well. Essentially docs#Path.trans but without going back to the unit interval.

What is needed is glueing continuous functions for a locally closed covering. Then use closed intervals joined at their extremities.

[Anatole Dedecker]

Junyan Xu said:

The next step would be proving the lifting criterion; the fundamental group condition is trivial for a map from a simply connected space, so you can get a branch of the square root on a simply connected domain as required for the proof of RMT. Given that the quotient map ℝ → ℝ/ℤ and n-fold cover ℝ/ℤ → ℝ/ℤ have been shown to be covering maps in my PR #7596 (I should probably make them FiberBundles ...), we may utilize the homeomorphism between ℂ \ {0} and ℝ/ℤ × ℝ to show exp and the nth power map are covering maps on ℂ \ {0}. We'd need to show that the product of a covering map with id (or another covering map) is also a covering map, and that composition with homeomorphisms preserves covering maps (there is already docs#Trivialization.compHomeomorph but not a version that changes the base, apparently). In addition to RMT, exp being a covering map would also allow defining the winding number.

#7596 also adds some reasonably convenient constructors for IsCoveringMap, which should be useful for showing the etale space associated to a locally exact form is a covering space. I looked into Bunch.lean and Covering.lean in Vincent Beffara's repo and it seems the proof that it's a covering space is sorry-free. I think for mathlib we'd probably take a more principled approach though, which is to define etale spaces of presheaves, prove general properties of them, and then specialize to our situation (sheaf of functions such that any two functions agree on an open set, with a group action on the sections that is free and transitive on the stalks). I've started working on this with PR #7655 adding lemmas for local homeomorphisms.

I'm going to comment on #7596 soon :tm: but I just want to mention that at some point I (or someone else) will probably remove docs#ProperlyDiscontinuousSMul and replace it by docs#ProperSMul (with an extra DiscreteTopology)

[Junyan Xu]

You may want to consult https://mathoverflow.net/questions/360706/when-a-free-action-gives-rise-to-a-g-principal-bundle when you got to do that ...

The homotopy lifting property is now proved here but there's still some glue missing to show that covering maps are injective on fundamental group.

[Junyan Xu]

Okay it's a bit more convoluted than I thought but I've now shown the injectivity. Mathlib doesn't yet have a def for the MonoidHom between fundamental groups induced by a continuous map, but there is the (universe non-polymorphic) docs#FundamentalGroupoid.fundamentalGroupoidFunctor. I think I'll extract the functor between groupoids from that and define the MonoidHom using docs#CategoryTheory.Functor.mapEnd, since I think it's indispensable to work with groups rather than groupoids to develop further theory.

liftPath can be used to define the winding number, and liftPath_apply_one_eq_of_homotopicRel shows it's independent of the homotopy class (rel endpoints) of the path.

I think I'll build on #7596 and develop some theory for Galois coverings next, and compute the fundamental group of circle. In the meantime, #7848 simplifies the definition of HomotopyRel.

[Junyan Xu]

The separated map PR #7911 is ready for review! A revelation is that locally injectivity is exactly the dual notion of separatedness (just replace all "closed" by "open"), so I built some API around Pullback to treat both unify the treatment of both.

I've now also created a project.

[Vincent Beffara]

Your project is not public :-(

[Notification Bot]

15 messages were moved from this topic to #mathlib4 > github projects by Johan Commelin.