Project idea: proper group actions

Stream: LFTCM 2024

[Anatole Dedecker]

Here's a thread for discussing the proper group actions project.

[Florestan]

I'm in !

[Etienne Marion]

Me too

[Vincent Guirardel]

Mee too

[Luigi Massacci]

Me too

[Anatole Dedecker]

I'm setting up a repository and refreshing my mind about what we have and what needs to be done, we can talk about it after the talks.

[Anatole Dedecker]

I was scared that we wouldn't have enough things to do, but I just realized we don't know that the composition of proper maps is proper :sweat_smile:

[Anatole Dedecker]

Here's the repository for the project: https://github.com/ADedecker/ProperAction

[Vincent Guirardel]

J'ai reussi a rentrer la composition des applications propres, mais en utilisant la composition des applications continues qu'on a reprouvé. Je ne sais pas comment utiliser ContinuousMap.comp a partir de f et g et des preuves que f et g sont continues.

[Anatole Dedecker]

You have to use docs#Continuous.comp, not docs#ContinuousMap.comp, I can explain more tomorrow (usually we keep the conversations in English on Zulip, don’t know wether that’s too relevant here though)

[Vincent Guirardel]

Thanks very much.

[Anatole Dedecker]

docs#isProperMap_iff_ultrafilter_of_t2

[Florestan]

I pushed a nearly complete proof of t2Space_of_ProperSMul, in the file Basic_florestan . Surprisingly (or not), the most tedious part for me was to show the "obvious fact" that the preimage of the diagonal in (X/G)^2 is equal to the image of the defining map G x X -> X x X. In fact, the only sorry left is one of the inclusions of this fact.

[Anatole Dedecker]

Nice! Yes I can see why that could be a bit tedious, but it’s a good exercise!

[Florestan]

I think I'm gonna skip the coq session, do you want to meet somewhere ?

[Anatole Dedecker]

I would like to do the Coq session. Do you want to work on something in autonomy, or do you need me for anything ? I can also do some back and forth if you need some help.

[Florestan]

No, don't worry, I will work in autonomy !

[Florestan]

We are in the big meeting room in the library

[Etienne Marion]

I did the PR for proper maps: https://github.com/leanprover-community/mathlib4/pull/11754
I was not sure whether I had to indicate that it depends on yours because I do not use outside lemmas so I didn't indicate it.

[Etienne Marion]

I added my results to your PR on proper actions. There are errors because it relies on my PR.

[Anatole Dedecker]

Sorry I was spending some time helping the Cantor people. Indeed #11754 should come before #11746, so the first one doesn’t have to depend on the second. You can go on branch FEVA_ProperAction and do git merge em/ProperMap, I’ll tell you tomorrow how to indicate the dependence on GitHub.

[Etienne Marion]

OK did that, but there seems to be a problem with imports anymay.

[Anatole Dedecker]

We’ll see tomorrow

[Etienne Marion]

Did you bring back the keys yesterday ?

[Vincent Guirardel]

Etienne Marion said:

Did you bring back the keys yesterday ?

yes

[Vincent Guirardel]

I don't manage tu push my file: "you have divergent branches..."

[Vincent Guirardel]

OK, I managed (with help)

[Anatole Dedecker]

Where did you push? I can't see it.

[Anatole Dedecker]

Small tip: when someone (including a bot like "reviewerdog") makes a suggestion, and you're reasonably confident that it shouldn't break anything, you can click "commit suggestion" to do it in GitHub. But we can talk about all of this right after the talk.

[Anatole Dedecker]

Also: the errors in GitHub might be a bit scary, but they should tell you what to do to fix them.

[Etienne Marion]

Well I don't find them really clear right now :(

[Anatole Dedecker]

Okay let's talk about it right after the end of the questions then.

[Etienne Marion]

Looks like there are troubles with imports of files we did not use.

[Florestan]

I pushed a partial proof of properMap_of_naiveProper_T2_FirstCountablewhich says that if $X$ and $Y$ are T2 and first countable,
then the naive definition
of proper map is equivalent to the good definition

[Florestan]

I have 2 sorrys:

[Florestan]

lemma isCompact_seq_lim {y:Y} {seq : ℕ → Y}
    (hconv: Tendsto seq atTop (𝓝 y)):
    IsCompact (Set.range seq ∪ {y})

which says that a convergent sequence and its limit is compact, which I guess should be somewhere

[Florestan]

and a kind of factorization lemme

lemma map_factor {A B C:Type*} {U : Set A} {f : A → B} {s : C → B}
    (h: ∀ c : C, s c ∈ f '' U):
    ∃ s' : C → A, ( s = f ∘ s' ∧ ∀ c : C, s' c ∈ U)

[Florestan]

which looks obvious, but couldn't do

[Florestan]

comments, ideas or simplications welcome !

[Anatole Dedecker]

Nice! I will have a closer look at this (and the rest of the PR) a bit later (maybe this evening, otherwise tomorrow).
Regarding the first sorry, I think I went looking for this a while ago but never found it. I'll double check, but if it is indeed missing that would be a good thing to add.
For the second one let's talk in the thread you opened about it (https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Map.20factorization/near/430395859 for other readers)

[Anatole Dedecker]

Ah, we do have the first sorry: docs#Filter.Tendsto.isCompact_insert_range. It looks like it's been there for some time, so I probably missed it when I last searched for it. Note that it is a consequence of the much more general docs#Filter.Tendsto.isCompact_insert_range_of_cocompact, so the same lemma applies for sequences and continuous functions vanishing at infinity!

[Anatole Dedecker]

Etienne's PR just got merged :tada: Of course this created some conflict between master and #11746, as indicated at the bottom of the PR. This is good git practice so I'll let one of you fix it by running git fetch, git merge origin/master, and then fix the conflicts in VSCode.

[Etienne Marion]

Done! Just to be sure: the issue was that some modifications of #11746 were done on ProperMap which was modified by my PR so it did not know which modification was supposed to be merged to master? I don't really understand what fetch does, it seems to pull the current master branch.

[Florestan]

Great, thank you Anatole, and congrats Etienne !

[Etienne Marion]

Thank you!

[Etienne Marion]

I proved map_factor:

lemma map_factor {A B C:Type*} {U : Set A} {f : A → B} {s : C → B}
    (h: ∀ c : C, s c ∈ f '' U):
    ∃ s' : C → A, ( s = f ∘ s' ∧ ∀ c : C, s' c ∈ U) := by
  choose s' hs' using h
  refine ⟨s', ?_, fun c ↦ (hs' c).1⟩
  ext c
  rw [← (hs' c).2]
  rfl

choose creates automatically a function and adds the right hypothesis so no need to use set.

[Florestan]

Yes, thank you, in the end I just used directly choose

Etienne Marion said:

I proved map_factor:

[Etienne Marion]

Yes makes sense

[Anatole Dedecker]

Ah, I was going to suggest something like docs#Function.invFun, for some reason I didn’t think about using choose directly :man_facepalming:
But yes, the reason we don’t have a lemma for it is it’s just easier to use choose directly in the middle of the proof (it’s quite flexible, especially if you use choose!).

[Anatole Dedecker]

Etienne Marion said:

Done! Just to be sure: the issue was that some modifications of #11746 were done on ProperMap which was modified by my PR so it did not know which modification was supposed to be merged to master?

Yes.

I don't really understand what fetch does, it seems to pull the current master branch.

git fetch tells git to lookup the changes that happened on the global (online) repo, without making any change to your local copy of Mathlib. Then, git merge origin/master tells git to merge, into the current branch, the branch master from the global repo (hence the need to fetch, but no need to pull).

[Anatole Dedecker]

(Disclaimer: I am not at all a git wizard, just a regular user)

[Etienne Marion]

Ok thanks!

[Anatole Dedecker]

@Florestan I had a look at the proof of properMap_of_naiveProper_T2_FirstCountable, and I think you're making your life a little harder than necessary (mathematically). My suggestion (motivated by the fact that I know that both this and docs#isProperMap_iff_isCompact_preimage are special cases of a result about compactly generated spaces) would be to first prove a lemma saying that, in a T2 first countable space, a set is closed if and only if its intersection with any compact subset is closed (using docs#Filter.Tendsto.isCompact_insert_range).
Then you can use the very-underrated docs#Set.image_inter_preimage to prove easily that your map is closed: take a closed subset $C$ in the domain, you want to show $f(C)$ is closed, hence you have to show that $f(C) \cap K$ is closed for any compact $K$. But $f(C) \cap K = f(C \cap f^{-1}(K))$ is compact, hence closed by separation.

Does that make sense? In any case do not delete your current proof, I will make some comments on it so that you can learn some tricks!

[Anatole Dedecker]

As I think I told you during the week, the reason we don't have compactly generated spaces yet is because we wanted to think before choosing one of the three definitions of https://en.wikipedia.org/wiki/Compactly_generated_space, which are all equivalent in this case because of separation. I'm more and more leaning towards moving forward with definition 1, but in the mean time it would be nice to make sure that the proofs can be easily generalized to this setup.

[Anatole Dedecker]

Also, note that in my suggested proof above, I make no assumption about the domain! No separation (actually, Lean already complains that this is not used in your proof), but also no first countability!

[Anatole Dedecker]

I just opened a discussion about the annoying linter failure on the PR at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20tag.20on.20StieltjesFunction.2Emeasure_singleton/near/430482334

[Etienne Marion]

Anatole Dedecker said:

I just opened a discussion about the annoying linter failure on the PR at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20tag.20on.20StieltjesFunction.2Emeasure_singleton/near/430482334

About that, why can’t we just increase the limit of time as suggested in the failure?

[Anatole Dedecker]

The thing is the issue does not appear at build time, it appears at linting time, which makes it a bit harder to control (to me at least, I'm sure there is a way to do that). To be more specific, one of these steps is to check that, even when all of mathlib is imported, the left hand side of a simp lemma cannot be reduced by simp without this exact lemma (otherwise it means the lemma would never trigger since the LHS would have already been simplified). In our case, Lean fails to make sense of the LHS in reasonable time when all of Mathlib is imported, thus causing a linter failure.

I don't know how the linter works, but I guess there would be no reason for the "increase limit for this lemma" option to be passed on to the linter.

[Anatole Dedecker]

Although now that I think about it it has to be, otherwise lemmas which need a raised limit would never pass the linting step :face_palm: Let me try it.

[Anatole Dedecker]

Well it didn't work, apparently the linter still used the same limit as before. :shrug:

[Riccardo Brasca]

You can remove the simp tag from that lemma (adding a comment). It is used only three times.

[Anatole Dedecker]

I asked about it in the public thread linked above (most people do not follow this stream), if no one answers I'll do that.

[Florestan]

Anatole Dedecker said:

Florestan I had a look at the proof of properMap_of_naiveProper_T2_FirstCountable, and I think you're making your life a little harder than necessary (mathematically). My suggestion (motivated by the fact that I know that both this and docs#isProperMap_iff_isCompact_preimage are special cases of a result about compactly generated spaces) would be to first prove a lemma saying that, in a T2 first countable space, a set is closed if and only if its intersection with any compact subset is closed (using docs#Filter.Tendsto.isCompact_insert_range).
Then you can use the very-underrated docs#Set.image_inter_preimage to prove easily that your map is closed: take a closed subset $C$ in the domain, you want to show $f(C)$ is closed, hence you have to show that $f(C) \cap K$ is closed for any compact $K$. But $f(C) \cap K = f(C \cap f^{-1}(K))$ is compact, hence closed by separation.

Does that make sense? In any case do not delete your current proof, I will make some comments on it so that you can learn some tricks!

I see, I will try at some point to implement your suggestion. And thanks a lot for all your comments !

[Etienne Marion]

Hey! I got back to the PR today, thanks a lot Anatole for your detailed comments, and also for that amazing shortcut using congrm! I added the proof you suggested using the idea of compactly generated space, although it does not really belong to this file.

[Etienne Marion]

I added some documentation and proved the equivalence between properly discontinuous and proper when X is T2 and X × X is compactly generated. However this cannot really be added now because compactly generated spaces are not defined yet if I understood correctly (and maybe the chosen definition won't be the same as the one I used). @Anatole Dedecker do you think we should wait for this to be added to Mathlib or change assumptions so that we can ask for reviewing?

[Anatole Dedecker]

Hey! Sorry for the delay, I was at CIRM again this week for another conference, and that took all of my energy again :sweat_smile: Thanks for all your work Étienne! Regarding things about compactly generated spaces, I think we can add them just for the sake of deducing the sequential and locally compact special cases, with a comment saying that when we have defined compactly generated spaces we should move to that definition and remove the special cases (since the gap will be bridged by typeclass inference).

[Anatole Dedecker]

More concretly, I would:

• replace the current docs#isProperMap_iff_isCompact_preimage by the primed version that we have
• add a comment saying this should be the only result needed, but because we don't have a way to state it nicely we just use it as an intermediate results to get the two usual consequences
• move the two "compact generation" criterions to this file, and use them to add lemmas WeaklyLocallyCompactSpace.isProperMap_iff_isCompact_preimage and SequentialSpace.isProperMap_iff_isCompact_preimage for the two use cases.

Does that make sense ?

[Etienne Marion]

Yes I think I get it, thanks! Hope you enjoyed the conference

[Anatole Dedecker]

Yes it was really nice, thanks!

[Etienne Marion]

I moved the stuff and I also reworked docs#isProperMap_iff_tendsto_cocompact as it was based on docs#isProperMap_iff_isCompact_preimage. I added the comment just before the statement, I am not sure if it should be added to the implementation notes in the header.

[Anatole Dedecker]

I think it would make sense to have it in the implementation notes as well

[Etienne Marion]

Ok

[Etienne Marion]

I have a question: each time I switch from master to our branch, I have to restart lean because it is not the same version (which is fine), but I also have to use lake exe cache get! because "the imports are out of date and must be rebuilt", which is a bit annoying. And I have to do the same when I switch back to master. Is there a way to avoid this (apart from merging master into our branch)?

[Anatole Dedecker]

No there is no real way around lake exe cache get. Note however that if no changes has been made since you last got the cache, and if you don’t use get!, it will not download anything and just unpack the cache that is already on your computer

[Etienne Marion]

Oh ok thanks! I was wondering what the difference was between get and ˋget!`,
I thought it was just about the number of file downloaded.

[Anatole Dedecker]

get! is meant to be used if something is wrong and get doesn’t fix it, so you just want to download everything from scratch. Otherwise you should rely on the fact that get is quite smart in downloading only the file which have changed since the last cache, and other optimizations I’m probably not aware of

[Etienne Marion]

Do you think we can remove the WIP label and add awaiting-review?

[Anatole Dedecker]

Sure! I had a very quick look and apart from a few potential cleanups in the proofs (and some merge conflict) I think it looks more than ready to be reviewed (in fact I think I should have told you so a week ago already, since you cleaned up everything).

[Etienne Marion]

The pull request finally got merged :tada: :tada: :tada: