Zulip Chat Archive

Stream: Copenhagen Masterclass 2023

Topic: Gleason

Filippo A. E. Nuccio (Jun 26 2023 at 11:09):

Here is a two-pages long with the argument for Gleason by Rainwater, and I am happy to work on this.

Nikolas Kuhn (Jun 26 2023 at 11:10):

I'm down.

Dagur Asgeirsson (Jun 26 2023 at 11:12):

I'll join

David Ang (Jun 26 2023 at 11:21):

I'm interested in joining - where is everybody?

Nikolas Kuhn (Jun 26 2023 at 11:24):

In the ground floor in some room

Filippo A. E. Nuccio (Jun 26 2023 at 11:29):

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/ExtremallyDisconnected.html#CompactT2.Projective.extremallyDisconnected

Dagur Asgeirsson (Jun 26 2023 at 11:34):

1255454110.pdf
Gleason's paper

Filippo A. E. Nuccio (Jun 26 2023 at 15:07):

@Dagur Ásgeirsson It seems that everything in E is implicit now...does it make sense to you? I think @David Ang is trying to work with it....

Dagur Asgeirsson (Jun 26 2023 at 15:09):

No it should depend on the same things as three

Dagur Asgeirsson (Jun 26 2023 at 15:10):

three must use continuity of f and phi, right?

Dagur Asgeirsson (Jun 26 2023 at 15:11):

Maybe not with the sorried proof as is, but eventually it will

Filippo A. E. Nuccio (Jun 26 2023 at 15:11):

Let me check...

Filippo A. E. Nuccio (Jun 26 2023 at 15:12):

I'll leave it to @David Ang who is left to me

David Ang (Jun 26 2023 at 15:19):

f and phi are also implicit in three

Dagur Asgeirsson (Jun 26 2023 at 15:20):

Yes but once the proof is done it will have used hf and hphi

Nikolas Kuhn (Jun 26 2023 at 15:37):

Yes, it will use that preimages of points in D -> A are closed. So technically, it only uses that pi_1 is continuous, which we might want to state anyway?

Filippo A. E. Nuccio (Jun 26 2023 at 15:37):

OK, I have destructured the proof of the existence of ρ into gleason21, gleason22 and three lemmas for gleason23_?. @David Ang is picking up gleason21.

Filippo A. E. Nuccio (Jun 26 2023 at 15:38):

@Nikolas Kuhn , I think we need to align the statement of three with the hypothesis h_subsets that shows up in gleason_inj and gleason_cont.

Filippo A. E. Nuccio (Jun 26 2023 at 15:38):

But I do not want to touch the statement without your agreement.

Filippo A. E. Nuccio (Jun 26 2023 at 15:39):

Now the first is

∀ (E₀ : Set (D φ f)),
 E₀ ⊂ E → CompactSpace E₀ → ¬ ((π₁ φ f)'' E₀) = Set.univ

and the second is

(h_subsets : ∀ (E₀ : Set E), ¬ E₀ = ⊤ → IsClosed E₀ → ¬ (r '' E₀ = ⊤))

Nikolas Kuhn (Jun 26 2023 at 15:40):

I pushed the last version, so feel free to change things around

Filippo A. E. Nuccio (Jun 26 2023 at 15:41):

Ok, let me have a look

Nikolas Kuhn (Jun 26 2023 at 15:41):

I recommend making the statement for E and the one for E_0 so that they are compatible via Zorn's lemma.

Nikolas Kuhn (Jun 26 2023 at 15:41):

I.e. so that apply zorn_superset just works.

Filippo A. E. Nuccio (Jun 26 2023 at 15:41):

What do you mean?

Filippo A. E. Nuccio (Jun 26 2023 at 15:42):

I have pulled

Filippo A. E. Nuccio (Jun 26 2023 at 15:44):

OK, I think my questions are:

  1. In the statement of three, would it be painful to replace E₀ ⊂ E with ¬ E₀ = ⊤?
  2. And to replace CompactSpace E₀ with IsClosed E₀
  3. (Surely not, but to replace Set.univ with ⊤)?

Nikolas Kuhn (Jun 26 2023 at 15:48):

  1. would require some effort.
  2. is actually better.

Filippo A. E. Nuccio (Jun 26 2023 at 15:51):

So, what do you suggest?

Filippo A. E. Nuccio (Jun 26 2023 at 15:51):

I can live with the strict inclusion if you so prefer. For 2., what is better?

Nikolas Kuhn (Jun 26 2023 at 16:01):

IsClosed is better. Right now I'm converting to that anyway.

Nikolas Kuhn (Jun 26 2023 at 16:02):

Ooh but you want it to be closed in E? That would not be straightforward

Dagur Asgeirsson (Jun 26 2023 at 16:52):

It’s probably best prove whatever is most compatible with Zorn first, and if we need some modification of the statement we should easily be able to deduce it, right?

Dagur Asgeirsson (Jun 26 2023 at 19:14):

Filippo A. E. Nuccio said:

OK, I have destructured the proof of the existence of ρ into gleason21, gleason22 and three lemmas for gleason23_?. David Ang is picking up gleason21.

Working on gleason22. Also it was missing openness hypotheses

Dagur Asgeirsson (Jun 26 2023 at 19:19):

gleason22 is done

Dagur Asgeirsson (Jun 26 2023 at 19:22):

I'll start working on the sorries in gleason23_inj

Dagur Asgeirsson (Jun 26 2023 at 19:37):

gleason23_inj done

Dagur Asgeirsson (Jun 26 2023 at 19:40):

gleason23_cont was true by assumption

Dagur Asgeirsson (Jun 26 2023 at 19:49):

I've pushed a commit where now everything actually depends on variables and we have no red errors left

Dagur Asgeirsson (Jun 26 2023 at 20:30):

OK, I'm done for tonight. I made some progress defining the homeomorphism but we need to decide what to do with phrasing of three before we can continue.

Nikolas Kuhn (Jun 26 2023 at 21:27):

I just pushed some version of three with some sorries.

I didn't find a good existing Lemma for showing that a chain of nonempty closed subsets of a compact space has nonempty intersection.

Filippo A. E. Nuccio (Jun 26 2023 at 21:27):

Thanks @Dagur Ásgeirsson impressive! We will discuss tomorrow, thanks.

Filippo A. E. Nuccio (Jun 26 2023 at 21:27):

Nikolas Kuhn said:

I just pushed some version of three with some sorries.

I didn't find a good existing Lemma for showing that a chain of nonempty closed subsets of a compact space has nonempty intersection.

So, the Lemma we discussed today was not enough?

Nikolas Kuhn (Jun 26 2023 at 21:28):

It's enough, but filling out the assumptions is complicated.

Filippo A. E. Nuccio (Jun 26 2023 at 21:28):

Is it in the pushed version?

Nikolas Kuhn (Jun 26 2023 at 21:30):

yes, it should be up now. It also added a hf' hypothesis to everything. In the last proof one needs to introduce some argument that shows Epi f \to Function.Surjective _

Filippo A. E. Nuccio (Jun 26 2023 at 21:30):

can you point to the line?

Nikolas Kuhn (Jun 26 2023 at 21:30):

I added some sorrys there.

Nikolas Kuhn (Jun 26 2023 at 21:31):

212 and 214

Nikolas Kuhn (Jun 26 2023 at 21:32):

Showing this is probably necessary from a math viewpoint

Filippo A. E. Nuccio (Jun 26 2023 at 21:32):

but are you speaking about the lemma gleason? I thought you were working on three

Nikolas Kuhn (Jun 26 2023 at 21:38):

Yes I am, I just fixed the points that broke through my update (inserting the variable hf' in various places, since it is now used in three).

Nikolas Kuhn (Jun 27 2023 at 05:39):

three compiles now without sorries. Will clean it up a bit later. I added a lemma that \pi_1 is continuous, which is needed:

lemma two_half : Continuous (π₁ φ f) := by
  sorry

Anyone is welcome to fill that in.

Dagur Asgeirsson (Jun 27 2023 at 05:41):

It’s easy, something like Continuous.comp continuous_fst continuously_subtype_val

Dagur Asgeirsson (Jun 27 2023 at 06:59):

Just pushed a proof of lemma five

Filippo A. E. Nuccio (Jun 27 2023 at 14:06):

@David Ang How is it going with the PR?

David Ang (Jun 27 2023 at 14:06):

Still refactoring!

David Ang (Jun 27 2023 at 14:07):

I pushed a bit of stuff for now

Filippo A. E. Nuccio (Jun 27 2023 at 14:21):

Thanks!

David Ang (Jul 08 2023 at 19:39):

#5634 is ready for review, but the location of the coercion lemmas are probably not the best

Filippo A. E. Nuccio (Jul 10 2023 at 12:05):

I had a look, is there something in particular that bothers you?

David Ang (Jul 10 2023 at 16:30):

Nothing in particular. There is not much API for doing these kinds of monadic coercion, and the lemmas I wrote down are the minimal necessary for the proof. As such I sprinkled them in random locations (e.g. in Data.Set.Functor just for the Monad instance).

Last updated: Dec 20 2023 at 11:08 UTC