# Zulip Chat Archive

## Stream: new members

### Topic: Feedback on a PR draft

#### Matias Heikkilä (Oct 18 2023 at 20:08):

I thought I'd try to make an occasional small contribution to mathlib4. The Stone-Cech compactification seems like it could use some additions, so I thought I'd try working on that. Here is one small fact about $\beta X$. There are some opportunities for futher work in this direction too.

How does it look at a glance? Seems like quite a bit of work compared to the proof on the paper, but I couldn't easily golf it further. I do have some specific questions about certain parts of that proof, but I thought I'd first ask if this looks anywhere near ok first.

#### Alex J. Best (Oct 18 2023 at 20:10):

It looks quite reasonable yes, I'll make some line by line comments on the PR

#### Rémy Degenne (Oct 18 2023 at 20:15):

If you want to merge this to mathlib you should open a PR from a branch on the mathlib repository, not from a fork. See https://leanprover-community.github.io/contribute/index.html

#### Matias Heikkilä (Oct 18 2023 at 20:16):

Thanks a lot @Alex J. Best , feedback much appreciated! I see that there are quite a few formatting issues. There was no automatic lean formatter the last time I checked. Is that still the case?

#### Alex J. Best (Oct 18 2023 at 20:17):

Yes unfortutely we don't have an auto-formatter, just some simple python scripts in `scripts/lint-style.sh`

that you can use (they can fix some very simple formatting errors for you, but not many)

#### Matias Heikkilä (Oct 18 2023 at 20:18):

Thanks @Rémy Degenne, I used to have access to mathlib in Lean3 times, but I didn't seem to automatically have one for mathlib4

#### Matias Heikkilä (Oct 18 2023 at 20:19):

Happy to open a PR there though if I'm added

#### Matias Heikkilä (Oct 18 2023 at 20:20):

Alex J. Best said:

Yes unfortutely we don't have an auto-formatter, just some simple python scripts in

`scripts/lint-style.sh`

that you can use (they can fix some very simple formatting errors for you, but not many)

Too bad, having a job as a SWE I couldn't imagine getting through a week without `prettier`

. It is what it is, I guess

#### Rémy Degenne (Oct 18 2023 at 20:24):

@Matias Heikkilä Invite sent.

#### Matias Heikkilä (Oct 18 2023 at 20:26):

I this would a be a suitable place to ask a couple of specific questions, I would like to know what's going on here

```
let Z := ULift.{u} <| Set.Icc (0 : ℝ) 1
```

It's not something I could have ever come up with myself, I saw @Adam Topaz writing that elsewhere, and just fiddled around with it until it did what I wanted. Given the following lines:

```
haveI : CompactSpace Z := Homeomorph.ulift.symm.compactSpace
haveI : T2Space Z := Homeomorph.ulift.symm.t2Space
```

I can sort of undrstand that we are identifying `Icc 0 1`

as a space with some properties we need, but I don't know what `ULift.{u}`

even means. I see the docstring, but unfortunately I don't really understand it :D

#### Adam Topaz (Oct 18 2023 at 20:27):

`ULift`

is just a way to lift a type from one universe level to another. docs#ULift

#### Anatole Dedecker (Oct 18 2023 at 20:28):

Do you know about universes?

#### Adam Topaz (Oct 18 2023 at 20:28):

So, if you want to construct the "interval" as an object of the category `Top.{u}`

of topological spaces whose underlying type is at universe level `u`

, then you will need to use such a `ULift`

.

#### Adam Topaz (Oct 18 2023 at 20:30):

There is a brief discussion about universes at the following link, in case it helps: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html?highlight=universes#types-as-objects

#### Matias Heikkilä (Oct 18 2023 at 20:31):

Thanks @Adam Topaz , perhaps I should read a bit to be able to make better questions

#### Matias Heikkilä (Oct 18 2023 at 20:35):

I can "sort of" get that we are identifying the same thing in a different way there, but I think I'll need to get a bit deeper into it before I could produce anything useful without copying other people's code.

#### Matias Heikkilä (Oct 18 2023 at 20:37):

I'll work through your comments @Alex J. Best, and open an improved version of the same thing as a PR in the mathlib4 repo as suggested by Rémy above.

#### Matias Heikkilä (Oct 18 2023 at 21:01):

Ok moved things here and linked the not-implemented comments from the other PR

#### Kevin Buzzard (Oct 18 2023 at 21:52):

If you are used to thinking about mathematics set-theoretically then probably you never used universes, which are inaccessible cardinals in set theory. Most mathematicians never need to leave universe 0, which can be thought of as the class of all sets. But in Lean universes are there so people use them just because they're there.

#### Matias Heikkilä (Oct 19 2023 at 04:38):

Thanks @Kevin Buzzard, that’s indeed my case. A nice learning opportunity here

#### Kevin Buzzard (Oct 19 2023 at 07:35):

I think the only other thing worth saying is that lean's universes are much easier to grok than set theory's inaccessible cardinals. Lean's universes come from the fact that the system simply demands that every single term most have a type, so the type of pi is the reals, and the type of the reals is `Type`

, but then the type of `Type`

has to be a thing so it's `Type 1`

, and the type of `Type 1`

is `Type 2`

etc. That's why they're there, to satisfy an axiom of the system. And you can't have the type of `Type`

being `Type`

or else you can do an analogue of Russell's "set of all sets that don't contain themselves" and get a contradiction. So these `Type n`

worlds are just bigger and bigger models of mathematics and the way mathlib is developed the theorems are all valid in all of them, but you have to use these `ULift`

functions to move between them

#### Matias Heikkilä (Oct 25 2023 at 16:03):

I reconsidered this a little bit, and thought that instead of proving an isolated fact about $\beta X$, it would perhaps be better to take a step back and make a bigger improvement in this file: The space $\beta X$ comes with a natural map $e : X \to \beta X$, but in order to get many of the interesting topology facts about $\beta X$ you need this map to be an embedding. I think that, while mathlib currently has that $e$ is an embedding for a discrete $X$, the general case is missing.

I was able to force my way through a really messy proof proof that $e$ is an embedding in the usual generality of $X$, which is actually kinda cool, because the quotient construction it uses seems pretty nonstandard to me. While the proof is very low quality code, I thought it’s not worth it to try and improve it in isolation. I thought I’d use it as a reference, gradually build the same result in better organized PRs and dig out the useful lemmas that are atm scattered around randomly. I guess an upside of having even a messy proof is that it perhaps explains a bit what I’m trying to do.

Thoughts? For starters I sketched a definition of the “usual generality” mentioned above.

#### Patrick Massot (Oct 25 2023 at 17:21):

We don't really want this map to be an embedding in general, we want its universal property (which is `stoneCechExtend`

and its properties).

#### Patrick Massot (Oct 25 2023 at 17:24):

And the construction that is currently in Mathlib is rather directly tailored to guarantee this universal property in a very clean way. It also has the advantage of being very parallel to the construction of the completion of a uniform space (which is a completely analogous result, exhibiting complete and separated spaces as a reflexive subcategory, just as Stone-Cech does for compact separated spaces).

#### Matias Heikkilä (Oct 25 2023 at 17:54):

Thanks for the feedback. It’s well known that this universal property characterises $\beta X$ up to homeomorphism for “$T_{3.5}$ spaces”. This is actually what I originally wanted to add, but I couldn’t get the proof to work without $e$ being an embedding. So I wondered if, without altering the construction at all, it’s an embedding for this same class of spaces. This indeed seems to be the case

#### Matias Heikkilä (Oct 25 2023 at 17:55):

I don’t know if there is some easy other way to get this uniqueness I have overlooked

#### Patrick Massot (Oct 25 2023 at 17:59):

I don't understand what you mean. What would be the statement of that characterization? The obvious statement follows by abstract non-sense as usual so I guess you mean something else.

#### Matias Heikkilä (Oct 25 2023 at 18:30):

I probably just mean the obvious statement :face_palm: well I did get through the embedding proof though, could there be anything worthwhile in that?

#### Matias Heikkilä (Oct 25 2023 at 19:12):

i.e. a proof for

```
theorem denseEmbedding_stoneCechUnit [TopologicalSpace α] [T1Space α] [CompletelyRegularSpace α] :
@DenseEmbedding _ _ _ _ (stoneCechUnit : α → StoneCech α)
```

with

```
class CompletelyRegularSpace (α : Type u) [TopologicalSpace α] [T1Space α] : Prop where
completely_regular :
∀ (x : α), ∀ (K : Set α) (_: IsClosed K), Disjoint K {x} →
∃ (f : C(α, ℝ)), EqOn f 0 {x} ∧ EqOn f 1 K ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1
```

#### Patrick Massot (Oct 25 2023 at 19:13):

Having a criterion ensuring the map into Stone-Cech is an embedding sounds interesting in its own right. It will probably need to live in a different file because that file currently probably doesn't import real numbers. This is a nice aspect of the construction in Mathlib: the Stone-Cech compactification lives purely in general topology, there is no need to build real numbers first.

#### Patrick Massot (Oct 25 2023 at 19:14):

Your definition of `CompletelyRegularSpace`

looks very weird. Why writing `Disjoint K {x}`

instead of `x \notin K`

? Or `EqOn f 0 {x}`

instead of `f x = 0`

??

#### Patrick Massot (Oct 25 2023 at 19:14):

Using bundled continuous functions is also clearly the wrong choice here.

#### Patrick Massot (Oct 25 2023 at 19:15):

`C(α, ℝ)`

is meant to be use only if you want extra structure on this type (for instance a topology), not when you want to talk about a single continuous function.

#### Matias Heikkilä (Oct 25 2023 at 19:25):

Thanks again for the feedback. This definition is based on the statement of theorem `exists_continuous_zero_one_of_closed`

. I can see how it's unnecessarily complicated in this case though, and I probably clinged too hard to the bit of similarity these situations have.

#### Matias Heikkilä (Oct 25 2023 at 19:36):

I was planning to break this into smaller PRs. I'm hoping it's then possible to bring it to mathlib-level quality with reasonable amount of reviewer feedback

#### Patrick Massot (Oct 25 2023 at 20:07):

Matias Heikkilä said:

I probably just mean the obvious statement :face_palm: well I did get through the embedding proof though, could there be anything worthwhile in that?

I think that discussing "the obvious statement" without ever stating it isn't very productive, so I wrote some Lean code. I put everything in `Type`

to avoid distracting universe issues. First I define what it means that a compact separated `Y`

has the universal property of a compactification of `X`

. Then I build a homeomorphism between any two such compactifications `Y`

and `Y'`

, using only the definition (this is the abstract non-sense proof I was referring to). It would be easy to prove there is only one such homeomorphism compactible with the `j`

maps. Then I prove that Stone-Cech has this property. Is that the uniqueness that you wanted?

#### Patrick Massot (Oct 25 2023 at 20:07):

```
import Mathlib
noncomputable section
class CompactificationData (X : Type) [TopologicalSpace X]
(Y : Type) [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] where
j : X → Y
j_cont : Continuous j
extend {Z : Type} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
(f : X → Z) (hf : Continuous f) : Y → Z
cont_extend {Z : Type} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
{f : X → Z} (hf : Continuous f) : Continuous (extend f hf)
extend_extends {Z : Type} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z]
{f : X → Z} (hf : Continuous f) : extend f hf ∘ j = f
unique_extend {Z : Type} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z] {f : X → Z}
(hf : Continuous f) {g : Y → Z} (g_extends : g ∘ j = f) (cont_g : Continuous g) : g = extend f hf
open CompactificationData
def CompactificationData.compare {X : Type} [TopologicalSpace X]
{Y : Type} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
{Y' : Type} [TopologicalSpace Y'] [T2Space Y'] [CompactSpace Y']
[CompactificationData X Y] [CompactificationData X Y'] : Homeomorph Y Y' where
toFun := extend (j : X → Y') j_cont
invFun := extend (j : X → Y) j_cont
left_inv := by
set toMap : Y → Y' := extend (j : X → Y') j_cont
set fromMap : Y' → Y := extend (j : X → Y) j_cont
suffices fromMap ∘ toMap = id from congrFun this
rw [unique_extend j_cont (Function.comp.left_id (j : X → Y)) continuous_id]
apply unique_extend
rw [Function.comp.assoc, extend_extends, extend_extends]
exact (cont_extend j_cont).comp (cont_extend j_cont)
right_inv := by
set toMap : Y → Y' := extend (j : X → Y') j_cont
set fromMap : Y' → Y := extend (j : X → Y) j_cont
suffices toMap ∘ fromMap = id from congrFun this
rw [unique_extend j_cont (Function.comp.left_id (j : X → Y')) continuous_id]
apply unique_extend
rw [Function.comp.assoc, extend_extends, extend_extends]
exact (cont_extend j_cont).comp (cont_extend j_cont)
continuous_toFun := cont_extend j_cont
continuous_invFun := cont_extend j_cont
def StoneCechData (X : Type) [TopologicalSpace X] : CompactificationData X (StoneCech X) where
j := stoneCechUnit
j_cont := continuous_stoneCechUnit
extend := fun f hf ↦ stoneCechExtend hf
cont_extend := continuous_stoneCechExtend
extend_extends := stoneCechExtend_extends
unique_extend := by
intros Z _ _ _ f hf g hg cont_g
beta_reduce
apply stoneCech_hom_ext cont_g (continuous_stoneCechExtend hf)
rw [hg, stoneCechExtend_extends hf]
```

#### Patrick Massot (Oct 25 2023 at 20:17):

Matias Heikkilä said:

I was planning to break this into smaller PRs. I'm hoping it's then possible to bring it to mathlib-level quality with reasonable amount of reviewer feedback

I'm sure this will work.

#### Matias Heikkilä (Oct 25 2023 at 20:23):

Patrick Massot said:

Matias Heikkilä said:

I probably just mean the obvious statement :face_palm: well I did get through the embedding proof though, could there be anything worthwhile in that?

I think that discussing "the obvious statement" without ever stating it isn't very productive, so I wrote some Lean code. I put everything in

`Type`

to avoid distracting universe issues. First I define what it means that a compact separated`Y`

has the universal property of a compactification of`X`

. Then I build a homeomorphism between any two such compactifications`Y`

and`Y'`

, using only the definition (this is the abstract non-sense proof I was referring to). It would be easy to prove there is only one such homeomorphism compactible with the`j`

maps. Then I prove that Stone-Cech has this property. Is that the uniqueness that you wanted?

This seems to be the thing I was originally interested in, yes. Thanks for the Lean code too!

Last updated: Dec 20 2023 at 11:08 UTC