Feedback on a PR draft

Stream: new members

[Matias Heikkilä]

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]

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

[Rémy Degenne]

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ä]

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]

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ä]

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ä]

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

[Matias Heikkilä]

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]

@Matias Heikkilä Invite sent.

[Matias Heikkilä]

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]

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

[Anatole Dedecker]

Do you know about universes?

[Adam Topaz]

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]

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ä]

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

[Matias Heikkilä]

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ä]

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ä]

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

[Kevin Buzzard]

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ä]

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

[Kevin Buzzard]

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ä]

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]

We don't really want this map to be an embedding in general, we want its universal property (which is stoneCechExtendand its properties).

[Patrick Massot]

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ä]

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ä]

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

[Patrick Massot]

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ä]

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ä]

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]

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]

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]

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

[Patrick Massot]

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ä]

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ä]

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]

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]

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]

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ä]

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!