extremally disconnected sets

Stream: condensed mathematics

[Johan Commelin]

If anyone is looking for something to get started with the second half: we'll need the definition of extremally disconnected sets and the fact that they are projective objects in Profinite.
Here's a tiny bit that starts on this (from way before LTE was a thing): https://github.com/ImperialCollegeLondon/condensed-sets/blob/master/src/extremally_disconnected.lean

[Johan Commelin]

Feel free to copy-pasta this into the LTE repo, but it could also go directly to mathlib.

[Damiano Testa]

Johan, I am happy to create a PR to mathlib, but why don't you want to do it yourself? Is there some trap?

[Johan Commelin]

No, it's just that it isn't finished yet.

[Johan Commelin]

I think I only did one direction of "extr.disc = projective"

[Damiano Testa]

Ok, I updated the code, since some lemmas had changed names, others were already in mathlib!

PR #8196

[Patrick Massot]

Now we'll need a linter checking that nobody writes "extremely disconnected" instead of "extremally disconnected".

[Patrick Massot]

(and then a brain linter to prevent me from reading extremely anyway).

[Adam Topaz]

def compact_t2.projective : Prop :=
  Π {Y Z : Type u} [topological_space Y] [topological_space Z],
  by exactI Π [compact_space Y] [t2_space Y] [compact_space Z] [t2_space Z],
  by exactI Π {f : X → Z} {g : Y → Z} (hf : continuous f) (hg : continuous g)
    (g_sur : surjective g),
  ∃ h : X → Y, continuous h ∧ g ∘ h = f

Don't you think it would be better to just use docs#CompHaus?

[Adam Topaz]

and maybe docs#category_theory.projective

[Adam Topaz]

(I guess we would have to prove that epi = surjective in CompHaus, but this should be easy)

[Johan Commelin]

Certainly! This code is very old.

[Johan Commelin]

@Damiano Testa Do you feel like implementing these changes? (I can understand if you are too busy with the order refactor, and such.)

[Damiano Testa]

I will give it a go and will let you know if I need help!

[Damiano Testa]

Especially the CompHaus part seems doable. I am not sure about the categorical notion of projectivity, since I never used categories in Lean.

[Damiano Testa]

In fact, here is the first issue that I come across.

I changed the definition of compact_t2.projective to

def compact_t2.projective : Prop :=
  Π {Y Z : CompHaus},
  by exactI Π {f : X → Z} {g : Y → Z} (hf : continuous f) (hg : continuous g)
    (g_sur : surjective g),
  ∃ h : X → Y, continuous h ∧ g ∘ h = f

Lean now does not like let h : stone_cech X → Y := stone_cech_extend ht since

type mismatch at application
  stone_cech_extend ht
term
  ht
has type
  continuous t
but is expected to have type
  continuous ?m_5
Additional information:
/home/damiano/Matematica/Lean/mathlib_poly-reverse/src/topology/extremally_disconnected.lean:85:30: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    stone_cech_extend ?m_8
  has type
    stone_cech ?m_1 → ?m_3 : Type ?
  but is expected to have type
    stone_cech X → ↥Y : Type (max u u_1)

I believe that this has to do with some weird "coercion to sort" business that is going on. Is there an easy fix for this, or should I consider proving a version of stone_cech_extend that would apply with the current context?

[Johan Commelin]

Use CompHaus.{u}. I think the issue is that you've got stuff in different universes.

[Damiano Testa]

Thanks Johan! This fixed the first issue!

I had noticed that Y Z were assumed in the same universe the first time around, but disregarded it with the change...

(Btw, this solves completely the first broken proof.)

[Damiano Testa]

The second issue, in the second and last broken proof, appears similar, then:

  rcases h continuous_id f_cont f_sur with ⟨g, hg, g_sec⟩,

gives error

type mismatch at application
  h continuous_id
term
  continuous_id
has type
  continuous id
but is expected to have type
  continuous ?m_2

[Johan Commelin]

Hmm, what is the context here?

[Damiano Testa]

state:
X : CompHaus,
h : compact_t2.projective ↥X,
U : set ↥X,
hU : is_open U,
Z₁ : set (↥X × bool) := Uᶜ.prod {tt},
Z₂ : set (↥X × bool) := (closure U).prod {ff},
Z : set (↥X × bool) := Z₁ ∪ Z₂,
hZ₁ : is_closed Z₁,
hZ₂ : is_closed Z₂,
hZ : is_closed Z,
h_compl : (subtype.val ⁻¹' Z₂)ᶜ = subtype.val ⁻¹' Z₁,
f : ↥Z → ↥X := prod.fst ∘ subtype.val,
f_cont : continuous f,
f_sur : surjective f,
_inst : compact_space ↥Z
⊢ is_open (closure U)

[Damiano Testa]

Maybe Z should be made into a CompHaus?

[Johan Commelin]

Hmm, maybe life becomes easier if you switch to CompHaus (the category) and the categorical version of projective at the same time.

[Johan Commelin]

Because now you have objects in the category, but you are not using the morphisms.

[Damiano Testa]

Ok, makes sense. I will try to make the change, but any pointer would be appreciated!

[Johan Commelin]

Otoh, it's not clear to me that we want this statement in CompHaus instead of Profinite. And if we bundle... then we need to choose (or do both)

[Johan Commelin]

The unbundled version didn't care.

[Damiano Testa]

For this approach, would that not also require X to be in CompHaus, somewhat defeating the purpose? I may be not understanding the Lean-categorical side of the story, though...

[Damiano Testa]

Ok, maybe I am being silly: you would require the map between Y and Z to be in the CompHaus category and the others outside?

[Johan Commelin]

The problem is: if X : CompHaus, then you cannot have X : Profinite.

[Johan Commelin]

Whereas with (X : Type) [compact_space X] [t2_space X] you could always add [totally_disconnected_space X] whenever you need it.

[Damiano Testa]

I am starting to think that, at this level, it might make sense to keep the assumptions split around. Maybe bundling can come later, once all the preparatory stuff is done?

[Johan Commelin]

I agree. But I only have intuition to back that up.

[Johan Commelin]

In general mathlib seems to follow the pattern "treat unbundled first", and then "bundle it up"

[Johan Commelin]

(And when we don't, it looks like we regret it later. See e.g., the bundled hom refactor. We're kinda thinking that maybe we want to resurrect the unbundled stuff [although not as typeclasses, but ordinary predicates] and have both approaches here as well.)

[Adam Topaz]

This can all be handled with the fact that the forgetful functor from Profinite to CompHaus reflects epimorphisms.

[Johan Commelin]

Sure, but you don't want to do that every time you use it, right?

[Adam Topaz]

What do you mean? Just add an instance

[Johan Commelin]

hmm, maybe I'm confused about what you want to do...

[Johan Commelin]

Are you talking about restating everything for Profinite with 1-line proofs that reduce it to CompHaus?

[Adam Topaz]

Okay, now I'm confused. What's the endgame for this?

[Johan Commelin]

At some point we want to show that Cond(Ab) has enough projectives. And this will be an ingredient.

[Johan Commelin]

I haven't thought hard about how to get to :this: in Lean.

[Adam Topaz]

If I recall correctly, the consensus is to define Cond(Type) as sheaves on Profinite?

[Adam Topaz]

(as opposed to, say, sheaves on CompHaus)

[Johan Commelin]

Yes, I think sheaves on Profinite seems to be the best approach.

[Johan Commelin]

Balancing in the middle between ExtrDisc and CompHaus.

[Damiano Testa]

So, if I am following the discussion, we will want to bundle Profinite more than ExtrDisc and CompHaus, right? If so, does this mean that the PR above does not need change?

[Johan Commelin]

We already have Profinite and CompHaus as categories in mathlib. ExtrDisc would be a follow-up PR.

[Johan Commelin]

It's not clear to me what the best Lean definition of "projective space" is. The categorical predicate only works for bundled objects. My intuition says we might want to go unbundled before going bundled.

[Adam Topaz]

If all we care about is existence, then we don't really need all this stuff. By some adjunctions you would know that $\mathbb{Z}[T]$ is projective when $T$ is a projective object of Profinite, and now you just have to prove that there are enough such projective objects, which you can get as a consequence of the StoneCech adjunction

[Adam Topaz]

The only thing that has me slightly concerned is the argument using Zorn's lemma at the bottom of page 12 of Condensed.pdf. I feel like this will create a universe bump.

[Peter Scholze]

I think Zorn's lemma is overkill there, don't worry about this.

[Adam Topaz]

Well, I think my worry about the universe bump is unrelated to Zorn.

[Peter Scholze]

Hmm, I guess one question is what your definition of "a class of objects generates" is. What is your definition?

[Adam Topaz]

I don't think we have such a definition yet in mathlib

[Adam Topaz]

But even if we define the notion of a generating class as saying something like "$Hom(X_i,-)$, $i \in I$ are jointly faithful", won't we have to take a large colimit to obtain a projective presentation of a given condensed abelian group?

[Peter Scholze]

I don't think it's large. I think the index category is the category of pairs of a compact projective $X_i$ and a map $X_i\to M$. This is still small.

[Peter Scholze]

Well, it's small in this $\kappa$-small setting

[Peter Scholze]

But aren't you kind of following that? Where $\kappa$ is some universe cutoff?

[Adam Topaz]

Hmm... in lean, unless we're very careful, this would involve quantifying as something like: Forall X : Cond(Ab.{u}), [compact_projective X], blah, which will force us into universe level u + 1.

[Peter Scholze]

Hmm. OK, I think I'd have to learn much more about how Lean handles universes to comment on this

[Adam Topaz]

A minimized bit of code is probably something like this:

set_option pp.universes true

universes u

#check Σ (X : Type u), X
-- Σ (X : Type u), X : Type (u+1)

[Peter Scholze]

Hmm I think you should somewhere ensure that your extremally disconnected sets are in a smaller universe than your abelian groups

[Peter Scholze]

Did you already account for that?

[Adam Topaz]

Peter Scholze said:

Did you already account for that?

I don't think so.

[Adam Topaz]

And the only way to do that is to start everything off with Cond(Ab.{u+1}).

[Adam Topaz]

@Bhavik Mehta what do you think?

[Bhavik Mehta]

My instinct would be to use the small predicate rather than adjust the universe levels, but I'll need to think about this a little

[Bhavik Mehta]

My primary concern is whether the universe solution is good enough - I'd like to verify that Prop 1.7 works and we don't hit the issue mentioned in Warning 2.14; if that is an issue then my existing definition of Cond won't be good enough

[Johan Commelin]

But with our pyknotic setup, I don't think Warning 2.14 will be a problem, right? Or are you saying that the problem is still there, but now on a universe level? I guess so...

[Bhavik Mehta]

Johan Commelin said:

But with our pyknotic setup, I don't think Warning 2.14 will be a problem, right? Or are you saying that the problem is still there, but now on a universe level? I guess so...

I'm saying that I'm not (yet) convinced the problem is gone in our setup

[Johan Commelin]

@Adam Topaz @Damiano Testa What is the plan with #8196 ? Would it be better to keep the code in the LTE repo for now? Then it can evolve a bit, and once it is mature and the api is complete, then we PR it to mathlib?

[Damiano Testa]

That is ok for me.

Besides, I have not found much time to devote to Lean this summer and probably the situation will not change for the month of August, so slowing down is a bit of a necessity for me!

[Adam Topaz]

I'm still not sure whether we actually need this definition in LTE. I'm under the impression that all we care about is that these things are projective objects in, say, Profinite. Do we ever actually need the following characterization?

class extremally_disconnected : Prop :=
(open_closure : ∀ U : set X, is_open U → is_open (closure U))

[Johan Commelin]

I don't think so.

[Adam Topaz]

So my suggestion is to just use [is_projective X] for X : Profinite when we need it.

[Johan Commelin]

I think that what we need is: extr.disc = projective in Profinite and also that stone-cech is extr.disc.
Together, that gives us enough projectives.

[Adam Topaz]

I guess we should prove that the stone cech compactification of a discrete set is projective in Profinite, but that should be easy

[Johan Commelin]

We'll also need ExtrDisc as a category. Do you just want to define it as the subtype

{X : Profinite // is_projective X}

[Adam Topaz]

Why do we need it as a category?

[Johan Commelin]

To show that Cond(Foo) is the same as certain presheaves on ExtrDisc

[Johan Commelin]

That way we can get [enough_projectives Cond(Ab)]

[Johan Commelin]

If I understand things correctly...

[Adam Topaz]

Right, but for this we just take a presheaf on Profinite and ask for some condition in terms of [is_projective X], etc., which we prove is equivalent to the sheaf condition.

[Johan Commelin]

Also, proving that Cond(Ab) is an abelian category might be easier if we work with sheaves on ExtrDisc.

[Johan Commelin]

Ok... do you think you can stub that out?

[Adam Topaz]

Sure.

[Johan Commelin]

Feel free to use as many sorrys as you want.

[Adam Topaz]

I guess if sheafifying is easier over ExtrDisc then that's one good reason to have this.

[Adam Topaz]

import category_theory.preadditive.projective
import condensed.condensed

namespace Profinite

open category_theory
open category_theory.limits

-- TODO: generalize
instance : projective (⊥_ Profinite) :=
{ factors := λ E X f e _, ⟨limits.initial.to _, by simp⟩ }

instance : has_initial (as_small Profinite) := sorry

universe v
variables {C : Type*} [category.{v+1} C] (F : (as_small.{v+1} Profinite.{v})ᵒᵖ ⥤ C)

-- I assume we want this to be a prop, but `is_terminal` and `preserves_limits_of_shape`
-- both contain data.
structure extr_sheaf_cond : Prop :=
(is_terminal : nonempty (is_terminal (F.obj (opposite.op (⊥_ _)))))
(preserves : ∀ (X Y : as_small.{v+1} Profinite.{v}) [projective X] [projective Y],
  nonempty (preserves_limit (pair (opposite.op X) (opposite.op Y)) F))

def proetale_topology' : grothendieck_topology (as_small.{v+1} Profinite.{v}) :=
sorry

theorem extr_sheaf_iff : extr_sheaf_cond F ↔ presheaf.is_sheaf proetale_topology' F := sorry

end Profinite

This is more-or-less what I had in mind.

[Adam Topaz]

Unfortunately, we will have to deal with this as_small nonsense :expressionless:

[Adam Topaz]

(pushed to condensed/proj_cond.lean on master)

[Johan Commelin]

merci!

[Johan Commelin]

@Adam Topaz If we ever define analytic rings $(\mathcal A, \mathcal M)$ in lean, then we'll probably want $\mathcal M$ to be a mathlib functor from ExtrDisc to condensed $\mathcal A$-modules.
(This definition is somewhere on my mental todo-list/roadmap.)

[Johan Commelin]

The alternative would be to make $\mathcal M$ a hands-on functorial pi-type defined for (X : Profinite) [is_projective X]

[Adam Topaz]

@Johan Commelin that's one option. Another is to have some general construction which builds a Cond foo from such a pi-type satisfying something like extr_sheaf_cond.

[Johan Commelin]

On paper, $\mathcal M$ has type $\text{extr.disc.} \to \text{Mod}^{\text{cond}}_{\mathcal A}$.

[Adam Topaz]

I thought this can be extended to Profinite in a formal way, for example by expressing X : Profinite as a quotient of $\beta X^\delta$ where $X^\delta$ is the underlying set with the discrete topology.

[Adam Topaz]

I.e. $X$ is a colimit of $\beta (\beta X^\delta \times_X \beta X^\delta) \rightrightarrows \beta X^\delta$.

[Johan Commelin]

The correct values of $\mathcal M$ on general profinite sets will be "derived", in the sense that they land in the derived category but not necessarily in the heart. Only for extr.disc do you get honest modules.

[Adam Topaz]

Ah ok.

[Adam Topaz]

Wait, so how does the left adjoint from Proposition 7.5 of condensed.pdf reconcile with your comment @Johan Commelin ?

[Johan Commelin]

Ha, I might have misunderstood things... @Peter Scholze would you mind correcting/explaining?

[Johan Commelin]

Ooh wait. That left adjoint is colimit preserving. So it preserves colimits of modules. But that doesn't mean that $\underline{\mathcal A}[S]$ is the colimit of $\underline{\mathcal A}[T_j]$,
where $S$ is profinite, and a colimit of some extr.disc $T_j$ as Adam sketched above.

[Adam Topaz]

The functor $Mod_{\underline{\mathcal{A}}} \to Cond(Set)$ has a left adjoint $S \mapsto \underline{\mathcal{A}}[S]$, right?

[Johan Commelin]

yeah, I just realized that... so what I'm saying is nonsense

[Johan Commelin]

which means that I'm still confused

[Adam Topaz]

(latex + zulip = hard)

[Peter Scholze]

The question is whether you want the left adjoint on the abelian level, or on the derived level. On the abelian level, what Adam said is correct. But in general, to compute the correct functor on the derived level, you have to use hypercovers $S_\bullet\to S$ by extremally disconnecteds and then write down the whole complex $\mathcal M[S_\bullet]$. Very often, it turns out that this lives in degree $0$ when it does on extremally disconnecteds -- I think in all cases I've ever considered -- but there's no reason this is always the case.

[Peter Scholze]

(See also the related Warning 7.6)

[Johan Commelin]

For the record: I'm working on showing that stone_cech is projective.

[Adam Topaz]

Sounds good. Some of the proofs from src#Compactum should be similar

[Johan Commelin]

@Adam Topaz does lean already know that an epi in Profinite is surjective?

[Adam Topaz]

More or less, but not in those terms. I have somewhere in LTE that surjective implies a topological quotient map in Profinite

[Johan Commelin]

I have an epi, and I need to show that it is surjective. I hope this follows out of the discrete_quotient stuff somehow?

[Adam Topaz]

Maybe... But I think there is more to it... I can help more in about an hour (on mobile right now)

[Patrick Massot]

Will we need that extremally disconnected implies projective in CompHaus? It looks like knowing we enough projectives will be... enough.

[Patrick Massot]

Otherwise this is clearly something I could do.

[Johan Commelin]

I think #8613 is all we need for now

[Patrick Massot]

You mean you don't even need #8196?

[Johan Commelin]

Adam convinced me that we probably won't need it.

[Patrick Massot]

It's currently in a somewhat weird state of being half done.

[Patrick Massot]

And half-way between a natural concrete statement and something nicely packaged in category theory.

[Johan Commelin]

I agree. So I don't think that PR should go into mathlib as is.

[Johan Commelin]

Let me tag it as WIP

[Johan Commelin]

Ooh, I see now that you reviewed it yesterday.

[Patrick Massot]

I didn't really review it, I flagged small local optimizations.

[Patrick Massot]

But I didn't comment on the overall structure and statements.