Effros Theorem

Stream: mathlib4

[Lara Toledano]

I have formalized a yet to be published proof of the Effros Theorem by Jochen Wengenroth. Would this be a good candidate for the library? The proof is rather similar to van Mill's https://scispace.com/pdf/a-note-on-the-effros-theorem-476vrl1k23.pdf.

[Jireh Loreaux]

Is the informalized proof publicly available, e.g., on the arXiv?

[Lara Toledano]

Not yet. It is part of a much larger ongoing work. However Jochen Wengenroth would be happy to upload the relevant excerpt to the arXiv.

[Jireh Loreaux]

Okay, the main issue is that it would be poor etiquette / academically inappropriate to publish Jochen's own work. However, if you have Jochen's blessing to do so (preferably publically, so that this is common knowledge), then that's fine.

As for the question of "is this a result we would like in Mathlib?", the answer is "surely". Have you contributed to Mathlib before? I don't think I've seen you around. Note that Mathlib has some pretty high standards for contributions, so it may take a while to get something like this ready, depending on how long it is.

[Lara Toledano]

Jochen has asked me to formally verify his proof with the intent to publish the formalization as a collaboration if it is good enough. He himself is not familiar with proof assistants. I am very new to lean as I just started learning last month for this very project.

The code I wrote does compile, although I am sure it is still very far from the mathlib standards.
I am thrilled with lean as a language. I feel it is everything I had been longing for in my study of mathematics. I want to learn more and become an active member of this community. If the subject matter is in fact in the scope of mathlib, I hope I can find guidance here to improve on the work. I certainly am willing to invest the time.

As for the size of the work, I have written about 600 lines of code, but I am sure it is much longer than necessary. Many of the facts I proved feel like they should be in the library, therefore I assume they are and I just haven't found them because I didn't know where to look.

[Jireh Loreaux]

600 lines is much lower than I was expecting you to say. If you post it here we should be able to give you pointers.

[Lara Toledano]

Again, I am totally new. By "post it here", do you mean as a code snippet in this thread?

[Jireh Loreaux]

Sure, as a code snippet. You could create a PR, but it will be easier to provide quick feedback here on Zulip.

[Yaël Dillies]

I personally think a PR would be more suitable

[Lara Toledano]

Should I wait for Jochen to publically approve? How would that look like?

[Johan Commelin]

If Jochen has stated that his intent is to collaborate with you, then I think you can just go ahead an post the snippet. Either as PR, or as a message on this thread, or using Github Gist

[Lara Toledano]

Jochen Wengenroth published the excerpt to the arXiv, where he mentions me by name.
https://arxiv.org/abs/2512.00910

There, the main theorem is Theorem 4.1 (Effros), and the main helper is Theorem 3.4 (van Mill).

Here is my code. It seems too long for a code snippet, and copy paste to snippet changes white space for some reason. I put everything together in a single file.
EffrosTheorem.lean

The code compiles for lean version v4.26.0-rc2.

[Lara Toledano]

As I mentioned in the comments, I think I probably should replace the notation U • x by something like MulAction.ball x U.

On a more general note, I am curious to understand why the notation for the left coset in a group a • s is so simple, and not for the right coset MulOpposite.op a • s. One could have defined s • a as op a • s. Did the community decide against it, because the scalar multiplication becomes heterogeneous? What are the disadvantages of heterogeneous functions?

[Yaël Dillies]

Today is your lucky day:

import Mathlib

open scoped Pointwise RightActions

example (a : ℕ) (s : Set ℕ) : MulOpposite.op a • s = s <• a := rfl

[Lara Toledano]

new version:
EffrosTheorem.lean

Thanks again @Yaël Dillies for the info about RightActions. I refactored the work accordingly.

I also replaced the notation U • x for [MulAction G X] (U : Set G) (x : X) by a definition MulAction.ball x U, in analogy to UniformSpace.ball. However, since I use the equality ball x (U <• g) = ball (g • x) U, I still would like to have a notation where U appears before x, for example as U <•> x. The equality would then be written (U <• g) <•> x = U <•> (g • x). What would speak against such a definition? What would be a better notation than <•>?

[Yaël Dillies]

Do you know about open scoped Pointwise? Along with open scoped Right Actions, this will turn on the U <• x notation

[Lara Toledano]

Yaël Dillies said:

Do you know about open scoped Pointwise? Along with open scoped Right Actions, this will turn on the U <• x notation

I am confused. When I look at the definition of the <• notation, the expression U <• x does not appear to be defined in the context of [MulAction G X] (U : Set G) (x : X). I am not surprised by the diverse 'failed to synthesize' errors in the following code.

import Mathlib

variable [Group G] [MulAction G X] (g : G) (U : Set G) (x : X)

open scoped Pointwise
open scoped RightActions

#check g <• x --error
#check g •> x
#check U <• x --error
#check U •> x --error

[Yaël Dillies]

Oh sorry, I see! I thought you had (U : Set X) (x : G). You can get your thing by doing U • {x} instead, which is arguably not so bad?

[Lara Toledano]

Writing U • {x} does solve the issue of the order of the variables. It does however come with a downside: the instance problem sometimes gets stuck on the singleton. For example

import Mathlib

variable [Group G] [MulAction G X] (U : Set G) (x : X) (s : Set X)

open scoped Pointwise
open scoped RightActions

-- error: typeclass instance problem is stuck
example [Monoid G] [MulAction G X] (x : X) (g : G) (U : Set G) :
    (U <• g) • {x} = U • {g • x} := by sorry

At the moment I do not understand why the typeclass instance problem does or does not get stuck on a specific singleton. I wonder: is that a bug or a feature? Why not default to Singleton X (Set X)?

Here is a version of the file in which I replaced MulAction.ball x U by U • {x} and adjusted the proofs. There are 7 places where I needed to explicitly type the singleton.
EffrosTheorem.lean

[Ruben Van de Velde]

Could also be Finset

[Lara Toledano]

Well then I wonder: why not default to Singleton X (Finset X), since there is some coercion from Finset to Set?

[Yaël Dillies]

Because you don't want spurious uses of Finset where Set would suffice. In general, it is a hard problem for notation to know what its type should be. There are heuristics, and some of them are implemented but as you are experiencing here they are not necessarily satisfactory. Here I would advise biting the bullet and writing ({x} : Set X)

[Lara Toledano]

On another subject, does this snippet follow the naming conventions? How would you refactor it?

import Mathlib

lemma IsNowhereDense.mono [TopologicalSpace X] {s t : Set X} (hs : IsNowhereDense s) (ht : t ⊆ s) :
    IsNowhereDense t := by
  apply Set.eq_empty_of_subset_empty
  calc interior (closure t)
    _ ⊆ interior (closure s) := by mono
    _ = ∅ := hs

[Yaël Dillies]

I would make the proof be Set.eq_empty_of_subset_empty <| by grw [ht]; exact hs, but otherwise it looks good!

[Lara Toledano]

Thanks again @Yaël Dillies. I landed on

@[gcongr]
lemma IsNowhereDense.mono [TopologicalSpace X] {s t : Set X} (ht : t ⊆ s) (hs : IsNowhereDense s) :
    IsNowhereDense t := Set.eq_empty_of_subset_empty <| by grw [ht]; rw [hs]

where your exact needed to be a rw. I also had to switch the order of the variables in order to add the @[gcongr] tag.

I notice that IsMeagre.mono is not tagged. In order to add @[gcongr], one would first have to refactor it as above. Is this a refactor that is planned for the future, or is there a reason not to use @[gcongr] here? Are there other examples of @[gcongr] lemmas for predicates?

[Lara Toledano]

I am now working on my first PR. The first thing I need to figure out is: to which file should each lemma be added?

The first lemma I am considering is the following

lemma Topology.IsInducing.isNowhereDense_image {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y]
    (hf : Topology.IsInducing f) {s : Set X} (h : IsNowhereDense s) : IsNowhereDense (f '' s) := sorry

Since almost all theorems about IsNowhereDense are found in Mathlib.Topology.GDelta.Basic, I thought it might be a good fit. However, I would need to import (Mathlib.Topology.Defs.Induced)[https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Defs/Induced.html] first.

How can I find out whether or not some new import would introduce a cycle and break the project, without trying to build to whole project on my own machine?

[Yaël Dillies]

Lara Toledano said:

I notice that IsMeagre.mono is not tagged. In order to add @[gcongr], one would first have to refactor it as above. Is this a refactor that is planned for the future, or is there a reason not to use @[gcongr] here? Are there other examples of @[gcongr] lemmas for predicates?

gcongr is relatively new at the scale of mathlib, so there are many missing annotations. Please PR the ones you see are missing! and swapping assumptions to make a lemma eligible for gcongr is definitely fair game.

[Yaël Dillies]

Lara Toledano said:

How can I find out whether or not some new import would introduce a cycle and break the project, without trying to build to whole project on my own machine?

Build cycles are resolved first, so lake build will very quickly complain if you have introduced one

[Lara Toledano]

Yaël Dillies said:

gcongr is relatively new at the scale of mathlib, so there are many missing annotations. Please PR the ones you see are missing! and swapping assumptions to make a lemma eligible for gcongr is definitely fair game.

My first PR :tada: : refactor: add gcongr tag to IsMeagre.mono

I assume switching assumptions will break some things. I am now waiting for the CI tests to tell me what I broke so I can try and fix it.

[Yaël Dillies]

Tip: You can write #32686 and Zulip will display it as #32686

[Lara Toledano]

Yaël Dillies said:

Today is your lucky day:

import Mathlib

open scoped Pointwise RightActions

example (a : ℕ) (s : Set ℕ) : MulOpposite.op a • s = s <• a := rfl

PR to add this info in the GroupTheory/Coset docs #32718

[Kevin Buzzard]

@Lara Toledano thanks! Can you add your github username to your Zulip profile so the maintainers can keep track of who our contributors are?

[Lara Toledano]

Should I mention each PR in this thread? #32740 #32742

[Lara Toledano]

#32745