Characterization of sheaves on ExtDisc

Stream: Copenhagen Masterclass 2023

[Filippo A. E. Nuccio]

I am working on it, together with @Riccardo Brasca and @Dagur Ásgeirsson . We are in the common space right below the Auditorium.

[Dagur Asgeirsson]

https://dagur.sites.ku.dk/files/2022/01/condensed-foundations.pdf section 1.2.3

[Filippo A. E. Nuccio]

So, we did not advance much but if you want you can pull

[Dagur Asgeirsson]

Cool! I guess one project is to write the correct, error-free statement of dagur115_vi_to_sheaf?

[Riccardo Brasca]

Yep

[Dagur Asgeirsson]

The statement of dagur115_vi_to_sheaf now makes sense. But it's only for sheaves of types. I think this is what we should work with and then deduce it for more general categories from that

[Dagur Asgeirsson]

Lemma one' is proved! I'll push after lunch

[Riccardo Brasca]

Great!

[Riccardo Brasca]

Do you think it also work for Profinite and CompHaus?

[Riccardo Brasca]

it is it true, right?)

[Riccardo Brasca]

lemma isSheafForDagurSieveSingle {X : ExtrDisc} {S : Presieve X} (hS : S ∈ DagurSieveSingle X)
    (F : ExtrDisc.{u}ᵒᵖ ⥤ Type (u+1)) : IsSheafFor F S

is done (modulo the fact that CompHaus preserves Epi).

[Riccardo Brasca]

https://mathoverflow.net/questions/408839/is-a-closed-subset-of-an-extremally-disconnected-set-again-extremally-disconnect

@Dagur Ásgeirsson

[Dagur Asgeirsson]

Oh! Then we have to fix the proof that dagurCoverage is a coverage

[Dagur Asgeirsson]

I.e. ExtrDisc probably doesn’t have “pullbacks of right mono”

[Dagur Asgeirsson]

I’ll think more about this tonight or tomorrow

[Dagur Asgeirsson]

We should probably just use the "weak pullbacks" that Adam was talking about

[Dagur Asgeirsson]

Ok @Filippo A. E. Nuccio , we should forget about HasPullbackOfRightMono. The argument in my thesis that dagurCoverage is a coverage works if you replace the word "closed" by "clopen"

[Dagur Asgeirsson]

Indeed, any clopen subset of an ExtrDisc is ExtrDisc

[Dagur Asgeirsson]

Unfortunately, I think this means that the stuff you guys have written about isPullbackPresieve doesn't apply to ExtrDisc

[Riccardo Brasca]

I think that isPullbackPresieve is fine. The second (or the first one, I don't know) it is surely a pullback presieve

[Riccardo Brasca]

The point is that it may not be a coverage

[Riccardo Brasca]

Or you mean we need to change the definition of DagurSieve?

[Riccardo Brasca]

Coverage

[Filippo A. E. Nuccio]

Oh, I see. Then probably keeping on working on the proof that this is a Coverage does not really make sense. What do you think @Dagur Ásgeirsson ?

[Riccardo Brasca]

I am more or less convinced that what I did it's ok if it is a coverage

[Riccardo Brasca]

Independently on how you prove it

[Filippo A. E. Nuccio]

Well, the problem is that I am sceptical that it be a coverage in the mathlib sense.

[Filippo A. E. Nuccio]

(I mean, if we really have a counterexample of a closed not clopen that does not turn out to be ExtrDisc)

[Filippo A. E. Nuccio]

@Dagur Ásgeirsson I was thinking that actually things could (perhaps) be savaged. The images of an isomorphic finite presentation of an ExtrDisc as disjoint unions will probably be clopen, not only closed, by compactness. No? In that case, we could keep the strategy, including the HasPullbackOfRightMono.

[Filippo A. E. Nuccio]

I want to stress that I am not particularly in love with that class, just that it seemed to work from the abstract point of view. :broken_heart:

[Dagur Asgeirsson]

Yes it they are definitely clopen and so the thing is definitely a coverage! I’m also thinking now that the HasPullbackOfRightMono approach works

[Dagur Asgeirsson]

I’m not entirely sure though

[Riccardo Brasca]

Maybe we need a class HasPullbackOfDagurIsIso

[Riccardo Brasca]

Seriously, Profinite and CompHaus have HasPullbackOfWhatever

[Riccardo Brasca]

(for obvious reasons)

[Riccardo Brasca]

then we need to take pullback wrt to those particular morphisms

[Riccardo Brasca]

We need to take pullbacks wrt to natural morphisms from coproduts. Maybe those tautologically always exists

[Riccardo Brasca]

to coproduct

[Filippo A. E. Nuccio]

I think that a sensible thing to do now is to convince ourselves that ExtrDisc HasPullBackOrRightMono.

[Riccardo Brasca]

but this is surely false, isn't it?

[Riccardo Brasca]

take the inclusion of a closed not extremally disconnected set

[Filippo A. E. Nuccio]

Riccardo Brasca said:

but this is surely false, isn't it?

No, see @Dagur Ásgeirsson 's reply to my comment that the images of a finite isomorphism from a disjoint unions are (probably?) clopen instead of closed.

[Filippo A. E. Nuccio]

Since clopen in ExtrDisc are still ExtrDisc, we could carry on the previous strategy, which we thought it would work because we believed "closed in ED implies ED" (and those images were certainly closed)

[Riccardo Brasca]

I mean, mono is not enough, inclusion of clopen is OK

[Filippo A. E. Nuccio]

Not sure to understand

[Riccardo Brasca]

Maybe I am confused

[Filippo A. E. Nuccio]

Oh, I see what you mean.

[Riccardo Brasca]

A mono is the inclusion of a subset right? A subset that of course is in ExtrDisc (since the mono is a morphism in the category)

[Filippo A. E. Nuccio]

Yes, you are right. Probably the correct class is HasCoverageofSievesHavePullbacks

[Filippo A. E. Nuccio]

(or something like this) saying that there exists a collection of (pre)sieves made up of arrows along which arbitrary pull-backs exist. And this condition would be satisfied by DagurSieveIso by the above description about clopens.

[Johan Commelin]

I'm not following the details of the discussion, but I think Adam wrote Mathlib/CategoryTheory/Sites/Coherent.lean in order to get the coverage on ExtrDisc as smoothly as possible.

[Johan Commelin]

The remaining bit amounts to showing that ExtrDisc is precoherent

[Riccardo Brasca]

I just had a beer with him, and he's a little confused too :grinning:

[Johan Commelin]

Due to the beer?

[Filippo A. E. Nuccio]

Oh no! This would be false for DagurSieveSingle, but that case can be savaged by using that objects in ED are projective.... I think we are heading towards a class IsEquivtoExtrDisc...

[Riccardo Brasca]

No, precoherent is perfectly fine

[Filippo A. E. Nuccio]

Ah ok

[Filippo A. E. Nuccio]

And where did Adam's confusion come from?

[Riccardo Brasca]

The point is the following: we would like to replace (meaning they're the same topology) the precoherent topology on ExtrDiscr with the topology generated by what we call the DagurCoverage

[Riccardo Brasca]

Now, to specify a coverage I have to give you the Presieve

[Filippo A. E. Nuccio]

Ah sure, then I follow. But why, at the end of the day?

[Riccardo Brasca]

those will be of type 1 or type 2

[Filippo A. E. Nuccio]

I mean, if we can show ExtrDisc is Precoherent, can't we live with the precoherent coverage?

[Riccardo Brasca]

type 1 are Presieve corresponding to inclusion to disjoint union

[Riccardo Brasca]

type 2 are made by a single Epi

[Filippo A. E. Nuccio]

Or the problem is that it does not give us the explicit description that we need to "simply" test AB5 for presheaves ( easy!)+$\varepsilon$?

[Riccardo Brasca]

The point is that we are able to prove (meaning we have a Lean proof) that this coverage generates the coherent topology

[Riccardo Brasca]

IF it is a coverege

[Riccardo Brasca]

No no, I just mean he's not completely sure it is a coverage

[Filippo A. E. Nuccio]

Yeah sure. But again: why do we want to simplify our life through the DagurCoverage? If the Precoherent condition is met, why can't we simply work with the Coherent coverage as Johan suggests?

[Filippo A. E. Nuccio]

I thought that the problem came from the fact that the coherent coverage does not give us a sufficiently nice and explicit description of when a presheaf is actually a sheaf, and this is needed for the strategy that we sketched today to prove AB5 for Cond.

[Riccardo Brasca]

to prove that a presheaf that presevers (co?)products is a sheaf

[Filippo A. E. Nuccio]

Yeah, ok.

[Riccardo Brasca]

I guess I have to read the real definition of docs#CategoryTheory.Coverage (something I should have done before probably)

[Filippo A. E. Nuccio]

Well, let's say that the true problem lies in checking pullback there. Because you need to show the FactorsThrough condition, and since the presieves in the covering are not required to satisfy any up-wards condition, you have really little room to play around. As soon as you have a map T-->Y to the base, and you try to "pull-back" a sieve on Yto T to construct a sieve on T, you create new maps, and these are most likely outside the sieve you started with, precisely because it is not upwards closed.

[Filippo A. E. Nuccio]

But I am optimistic about the DagurCoverage still being a coverage...

[Dagur Asgeirsson]

I am convinced that dagurCoverage is a coverage, because ExtrDisc “HasPullbackOfRightOpenMono”; the covering maps in sieves of type 1 are open monos

[Riccardo Brasca]

The def is

pullback : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Presieve X) (_ : S ∈ covering X),
    ∃ (T : Presieve Y), T ∈ covering Y ∧ T.FactorsThruAlong S f

[Riccardo Brasca]

to prove this I would start by a case splitting on _ : S ∈ ...

[Dagur Asgeirsson]

What I mean is that the proof of this is in my thesis, the only problem is that it says closed where it should say clopen

[Filippo A. E. Nuccio]

Yes, indeed, I think that the strategy we currently have is OK. I really believe we should discuss this in front of a blackboard, but I am optimistic that everything can be salvaged.

[Johan Commelin]

salvaged* I hope

[Filippo A. E. Nuccio]

Indeed... :rofl: :rofl:

[Filippo A. E. Nuccio]

Hacking with (pre)coverages for 2 days is not helping my mental health :sweat_smile:

[Filippo A. E. Nuccio]

@Dagur Ásgeirsson @Riccardo Brasca I think I will call it a night. See you tomorrow!

[Dagur Asgeirsson]

Good night! We'll figure it out tomorrow

[Riccardo Brasca]

Same here! I just merged master (to have some results we need) so don't forget to pull

[Adam Topaz]

@Johan Commelin what Dagur Filippo and Riccardo are working on is showing that the Grothendieck topology generated by the coherent coverage is also the one generated by a different coverage where covers are either singleton epis or inclusions of components of a finite coproduct. I don’t know exactly what the issue is because I haven’t been working with them but I’m guessing that the second thing might not be a coverage?

For example if I take a cover associated to $X + Y$ (coproduct) and a random map $Z \to X + Y$, then it’s not clear to me how to get such a cover over Z which factors through the two-arrow-presieve associated to the incl of X and Y over that given map. But the characterization of the sheaf condition in terms of products doesn’t necessarily need a coverage.

I think something that has a better chance of working is the one where covering presieves are given by finite coproducts of finite families of epis.

[Adam Topaz]

In LTE we did this using the very explicit description in terms of jointly surjective families, but it would be nice to have a more conceptual (and more general) categorical formulation!

[Adam Topaz]

Ah now I see the map $Z \to X + Y$ is ok, because you have a decomposition of $Z$ as the coproduct of the preimage of $X$ and the preimage of $Y$, and that splits $Z$ into a disjoint union which factors over the $X$ and $Y$, so it's ok :)

[Adam Topaz]

And if you start with an epi $X \to Y$ and a map $Z \to Y$ you pullback in CompHaus and take a projective presentation of the pullback to obtain an epi.

[Riccardo Brasca]

Let me see if I become obsessed with this or I prefer to sleep

[Dagur Asgeirsson]

Adam Topaz said:

And if you start with an epi $X \to Y$ and a map $Z \to Y$ you pullback in CompHaus and take a projective presentation of the pullback to obtain an epi.

Can't you just take the identity of $Z$ and use projectivity?

[Adam Topaz]

Ah yeah that works too!

[Adam Topaz]

Although it shouldn't matter at the end of the day :)

[Adam Topaz]

I guess the key point here is that if $\iota : X \to X \coprod Y$ where $X$ and $Y$ are extrdisc and $f : Z \to X \coprod Y$ is any map from an extrdic, then the pullback of $\iota$ and $f$ in CompHaus is again an extrdisc.

[Adam Topaz]

So perhaps the easiest way to formalize this is by saying something like HasPullback (Sigma.\iota _ _) f for any f and Sigma.\iota the inclusion for a finite coproduct.

[Riccardo Brasca]

Yes, I totally agree

[Adam Topaz]

I've run killall lean like 10 times and I still have have 15 lean processes running somehow. Time to shut down the computer. See you all tomorrow!

[Dagur Asgeirsson]

I'm working on proving that for f and i maps in ExtrDisc where OpenEmbedding i, then HasPullback f i

[Riccardo Brasca]

I think the statement we need is

lemma foo {α : Type} {Y : C} [Fintype α] {Z : α → C} {π : (a : α) → Z a ⟶ X}
    (f : Y ⟶ X) (H : IsIso (Sigma.desc π)) (a : α) : HasPullback f (π a) := by
  sorry

[Riccardo Brasca]

with C =ExtrDisc

[Riccardo Brasca]

I have the impression that we need that coproducts commute with pullbacks: we start with a covering of type $\{ X_i \}_i \xrightarrow{\sim} \coprod X_i$ and we have $f : Y \to X$. Now, the $Y_i := Y \times_X X_i$ exist, at least in ExtrDiscr, and using pullback.fst we get a morphism $Y_i \to Y$, so a morphism $\coprod Y_i \to Y$, but why is this an iso?

[Riccardo Brasca]

(we need it to be an iso to show that it is still in the covering)

[Riccardo Brasca]

This should follow by the explicit description of the pullback in this case (that is the pullback in Top) but maybe there is a more direct argument

[David Michael Roberts]

Adam Topaz said:

Johan Commelin what Dagur Filippo and Riccardo are working on is showing that the Grothendieck topology generated by the coherent coverage is also the one generated by a different coverage where covers are either singleton epis or inclusions of components of a finite coproduct. I don’t know exactly what the issue is because I haven’t been working with them but I’m guessing that the second thing might not be a coverage?

For the sake of terminology/keywords, the second thing is superextensive. The "inclusions of components of a finite coproduct" is the extensive pretopology/coverage. They also come in infinitary versions.

[Riccardo Brasca]

Thanks! So it seems that what we need is that ExtrDiscr is an extensive category. This more or less by definition means that the DagurSieveIso form a coverage (known as the extensive coverage)

[Filippo A. E. Nuccio]

I totally agree with @Riccardo Brasca that one point where I got stuck in proving that FactorsThru property of the Dagur "coverage" was in showing that the morphism $\coprod Y_i\to Y$ is an iso. Shuold I add this to the file and try to finish the proof with that? The classes needed for ExtrDisc would still be the existence of pullback for embeddings (or the weaker foo suggested by Riccardo) plus the extensivity.

[Riccardo Brasca]

Is the following true? Take an extensive category C (whatever this means exactly) that is also docs#CategoryTheory.Precoherent. Than the coherent topology, meaning the topology generated by docs#CategoryTheory.coherentCoverage, is generated by the union of the extensive coverage and the coverage given by one single morphism that is an effective epi (is this the regular coverage? I don't know)

[Riccardo Brasca]

Filippo A. E. Nuccio said:

I totally agree with Riccardo Brasca that one point where I got stuck in proving that FactorsThru property of the Dagur "coverage" was in showing that the morphism $\coprod Y_i\to Y$ is an iso. Shuold I add this to the file and try to finish the proof with that? The classes needed for ExtrDisc would still be the existence of pullback for embeddings (or the weaker foo suggested by Riccardo) plus the extensivity.

foo is needed, but not enough I think.

[Filippo A. E. Nuccio]

Why not?

[Riccardo Brasca]

It's just the existence of the pullback, you need that the pullback interacts well with disjoint union (this is not automatic)

[Filippo A. E. Nuccio]

But isnt' it the extensivity?

[Riccardo Brasca]

yes

[Filippo A. E. Nuccio]

That's what I meant by " foo plus the extensivity"

[Riccardo Brasca]

Sorry, then I agree

[Riccardo Brasca]

foo is inside extensivity

[Filippo A. E. Nuccio]

Ah, I though that extensivity was that if the pullback exists, then it commutes with iso (in the sense that the pullback is again an iso)

[Riccardo Brasca]

"Pullbacks of finite-coproduct injections along arbitrary morphisms exist and finite coproducts are disjoint and stable under pullback."

[Filippo A. E. Nuccio]

Sorry, then I agree :smile:

[Filippo A. E. Nuccio]

Ah, but as a matter of fact the first bit is exactly HasPullBackofMono

[Filippo A. E. Nuccio]

(restricted to Mono that are finite-coproducts)

[Dagur Asgeirsson]

We need open monos?

[Riccardo Brasca]

It is weaker, isn't it?

[Filippo A. E. Nuccio]

Riccardo Brasca said:

It is weaker, isn't it?

What is "it"?

[Filippo A. E. Nuccio]

Dagur Ásgeirsson said:

We need open monos?

I think we need clopen monos, rather.

[Riccardo Brasca]

We never consider an arbitrary mono, only those appearing as $X_i \to \coprod X_i$

[Dagur Asgeirsson]

monos are automatically closed

[Filippo A. E. Nuccio]

Ah right.

[Dagur Asgeirsson]

all continuous maps in fact

[Filippo A. E. Nuccio]

So you are asking if open Monos is enough? The argument we sketched yesterday using that in the finite coproduct case the injections from every piece of a DagurIso sieve are open by compactness shuold show it is enough.

[Dagur Asgeirsson]

I'm working on proving pullbacks exist for open monos

[Dagur Asgeirsson]

which should be enough, right?

[Filippo A. E. Nuccio]

OK, I will then try to add the hypothesis and close the proof that the Dagur coverage is indeed one? @Riccardo Brasca , what are you working on? Have you already added something?

[Filippo A. E. Nuccio]

I have just pushed a statement of a lemma Extensivity with which I can close the first half of DagurCoverage (the piece that has to do with DagurIso)

[Riccardo Brasca]

In which file?

[Filippo A. E. Nuccio]

dagur

[Filippo A. E. Nuccio]

Well, to be honest I still need that a IsIso is a Mono, which is certailny true but I was too lazy to look at it in the library.

[Filippo A. E. Nuccio]

See line 86

[Riccardo Brasca]

Wow, we have docs#CategoryTheory.FinitaryExtensive !

[Riccardo Brasca]

This is probably the right way of stating things, but our approach is more direct

[Filippo A. E. Nuccio]

OK guys, I am sorry but there are some errors related (probably) to universes. DagurSpecial should be useless by now.

[Riccardo Brasca]

No problem, in any case I will only work on OpenEmbedding

[Dagur Asgeirsson]

We’ll figure out the universe issues eventually, it’s probably for very stupid reasons anyway

[Riccardo Brasca]

The idea of using the explicit construction is the good one.

lemma DagurOpenEmbedding {α : Type} [Fintype α] (Z : α → ExtrDisc.{u}) (a : α) :
    OpenEmbedding (Sigma.ι Z a) := by

is done.

[Filippo A. E. Nuccio]

I agree,

def dagurCoverage  [HasFiniteCoproducts C] [HasPullbackOfRightMono C] (h_proj : EverythingIsProjective C)  (h_ext : Extensivity C)
    : Coverage C

is done and sorry-free, and this implies

lemma final (A : Type (u+2)) [Category.{u+1} A] {F : ExtrDisc.{u}ᵒᵖ ⥤ A}
    (hF : PreservesFiniteProducts F) : Presheaf.IsSheaf (coherentTopology ExtrDisc) F :=

which is also sorry-free (provided we can prove that EverythingIsProjective in ExtrDisc, which is Gleason; and Extensivity ExtrDisc which should follow from @Riccardo Brasca 's message above)

[Filippo A. E. Nuccio]

Unfortunately, though, the above def dagurCoverage does not work for CompHaus because EverythingIsProjective CompHaus is certainly false. In particular, the file CompHaus.ExplicitSheaves has an error.

[Filippo A. E. Nuccio]

Also , after playing a bit with universe variables, the file dagur.lean compiles quickly again.

[Riccardo Brasca]

Well final is certainly false for Profinite and CompHaus

[Filippo A. E. Nuccio]

Yes, exactly.

[Riccardo Brasca]

I am pretty sure that the coverage is still a coverage, but for a different reason

[Riccardo Brasca]

We can with this later

[Filippo A. E. Nuccio]

I just wanted to mention that we do not even have a dagurCoverage for CompHaus or Profinite and we need to do something about the file. At any rage, for ExtrDisc the coverage is a coverage.

[Riccardo Brasca]

We can just comment everything gives an error

[Riccardo Brasca]

Let's make final really sorry free

[Filippo A. E. Nuccio]

Riccardo Brasca said:

We can just comment everything gives an error

Can I let you do this since you were the one mainly working in the CompHaus folder?

[Riccardo Brasca]

For example ATM lean does not know that ExtrDiscr has coproducts

[Riccardo Brasca]

Sure

[Riccardo Brasca]

(it does? We need only finite coprodutcts, but there is sorried instance about arbitrary ones)

[Riccardo Brasca]

Wait, the disjoint union of compact is hardly compact

[Riccardo Brasca]

If they're infinitely many

[Riccardo Brasca]

Well, it's not so important

[Filippo A. E. Nuccio]

I am not sure I will work much during the week-end, but one low-hanging fuit is the EveythingIsProjective lemma from what we did in the Gleasonfolder.

[Riccardo Brasca]

Don't worry, enjoy Copenaghen

[Filippo A. E. Nuccio]

Riccardo Brasca said:

If they're infinitely many

Well, at any rate as you see from the code-snippet above dagurCoverage requires HasFiniteCoproducts so this is really not a problem.

[Riccardo Brasca]

Yes yes, those are not a problem at all. I am just curious now, since it has coproducts it means that the forgetful functor does not preserve them, and it's an interesting thing

[Jon Eugster]

Riccardo Brasca said:

(it does? We need only finite coprodutcts, but there is sorried instance about arbitrary ones)

I proved that instance about ExtrDisc having finite coproducts. It is on an open PR, feel free to merge that PR to master.

On that PR I also commented out the instance about arbitrary coproducts in ExtrDisc as I'm not sure it's true. And if I understand correctly, @Riccardo Brasca confirms that it's not true, don't you?

[Riccardo Brasca]

I don't know, surely if it is true it is not the disjoint union. Anyway we only need the finite case, thanks!

[David Michael Roberts]

The category of compact Hausdorff spaces is cocomplete. Without checking, I presume you take the Stone-Čech compactification of the disjoint union in Top. The universal property of the compactification gives rise to the universal map needed by the definition of the colimit.

[David Michael Roberts]

This is easier to see for coproducts, coequalisers needs Hausdorffification, which is not simple to construct.

[David Michael Roberts]

Here's a fun fact I've not seen mentioned elsewhere: extremally disconnected spaces are the projective objects in the category of Hausdorff regular spaces https://doi.org/10.2307/2035286

[David Michael Roberts]

Since the Stone–Čech compactification of a an extremally disconnected space is extremally disconnected (if I believe the unsourced comment here: https://math.stackexchange.com/questions/2814978/%c4%8cech-stone-compactification-of-extremally-disconnected-space?rq=1), this should means that arbitrary coproducts of compact Hausdorff extremally disconnected (=Stonean) spaces are given by the Stone–Čech compactification of the disjoint union.

[Riccardo Brasca]

FYI I just merged master in dagur_ExtrDiscExplicitSheaves. Don't forget to pull

[Adam Topaz]

David Michael Roberts said:

Since the Stone–Čech compactification of a an extremally disconnected space is extremally disconnected (if I believe the unsourced comment here: https://math.stackexchange.com/questions/2814978/%c4%8cech-stone-compactification-of-extremally-disconnected-space?rq=1), this should means that arbitrary coproducts of compact Hausdorff extremally disconnected (=Stonean) spaces are given by the Stone–Čech compactification of the disjoint union.

Another way to see this is to use Gleason's theorem along with the fact that an arbitrary coproduct of projectives is again projective (in any category). (Hence no need to use an unsourced comment :))

[Riccardo Brasca]

Which coproduct? I mean, in which category? CompHaus does not have coproducts, right?

[Johan Commelin]

It has finite ones

[Johan Commelin]

But that's probably not what Adam was talking about...

[Riccardo Brasca]

Yes, finite are fine in all three categories (ExtrDisc, Profinite and CompHaus), and this is done in the repo.

[Riccardo Brasca]

There was a sorried instance about arbitrary coproduct in ExtrDiscr, that it is probably true via Stone-Cech, but I dont see how to apply Gleason

[Riccardo Brasca]

In any case we don't need it, I am just curious

[Adam Topaz]

CompHaus has all colimits ;)

[Adam Topaz]

(They’re the stonecech compactification of the topological colimit)

[Adam Topaz]

And thus ExtrDisc has all coproducts by Gleason

[Adam Topaz]

I have some time at the airport… I’ll try to do this while I wait

[Riccardo Brasca]

Let me stress that we don't need it. BTW this sorry

def presentation (X : CompHaus) : ExtrDisc where
  compHaus := (projectivePresentation X).p
  extrDisc := sorry

in ExtrDisc.Basic is done, right?

[Adam Topaz]

That should follow from Gleason (even the direction of Gleason that’s in mathlib)

[Riccardo Brasca]

@Dagur Ásgeirsson @Filippo A. E. Nuccio I made a little clean-up, moving stuff around. Now the construction of pullbacks in ExtrDisc is in its own file. Here is the situation: I think final depends on three sorry:

• Extensivity_ExtrDisc in ExtrDisc.ExplicitSheaves: I am working on it.
• isPullbackSieve_DagurSieveIso and isSheafForDagurSieveIso both in Sieves.dagur. These should be relatively easy given what we already have. (In any case we should move this file, since it is for ExtrDiscr)

The file Sieves.DagurSpecial contains a bunch of sorry, but it is not used anywhere, we can ignore it.

[Riccardo Brasca]

Adam Topaz said:

That should follow from Gleason (even the direction of Gleason that’s in mathlib)

Let me do it.

[Riccardo Brasca]

https://github.com/adamtopaz/CopenhagenMasterclass2023/pull/22

[Adam Topaz]

Feel free to merge once CI is happy

[Riccardo Brasca]

I guess you forgot this line

[Adam Topaz]

Oops :oops:

[Adam Topaz]

I’m sure it’s not the only one

[Adam Topaz]

do you think the power plug on my flight will be able to keep my laptop alive for 8 hours with lean running?

[Riccardo Brasca]

I guess we will see later :D

[Riccardo Brasca]

In my flight with WestJet we had real plugs

[Adam Topaz]

https://github.com/adamtopaz/CopenhagenMasterclass2023/blob/762fb49ca640fa663e82a7a94afc8d8e72c7748a/ExtrDisc/Coproducts.lean#L52

I still have 6 hours in my flight... what's next?

[Riccardo Brasca]

Does this implies that if pullback f g exists in ExtrDiscr than CompHaus commute with it?

[Adam Topaz]

no, this is just for coproducts (over arbitrary sufficiently small types, not just finite ones)

[Riccardo Brasca]

Ah sure, Discrete, not Fintype or whatever

[Riccardo Brasca]

BTW pushing from 30000 feet in the air is really cool

[Adam Topaz]

Where have you been working on the ExtrDisc sheaf condition?

[Adam Topaz]

It seems that the equivalence Sheaf ExtrDisc foobar \equiv Condensed foobar is sorry-free!

[Riccardo Brasca]

Here is our final theorem, in case you want to use to prove stuff about sheaves on condensed

theorem final (A : Type (u+2)) [Category.{u+1} A] {F : ExtrDisc.{u}ᵒᵖ ⥤ A}
    (hF : PreservesFiniteProducts F) : Presheaf.IsSheaf (coherentTopology ExtrDisc) F := sorry

[Adam Topaz]

You probably want to also assume [HasFiniteBiproducts A].

[Adam Topaz]

You probably want to also assume [HasFiniteBiproducts A].

[Adam Topaz]

Oh wait no nevermind that's needed for the colimit stuff

[Riccardo Brasca]

I am pretty sure we don't need it. Of course something depends on sorried statement, but this is the only one that mentions a category different from Type u, and its proof is sorry free.

[Adam Topaz]

no, you're right, you don't need it for just this statement.

[Nikolas Kuhn]

What is left for AB5 now? Are there any stray sorries that are not actively worked on?

[Adam Topaz]

the proof of AB5 for CondensedAb is actually quite technical to formalize IIRC. I can start on that assuming the theorem that Riccardo mentioned.

[Adam Topaz]

Pushing

import ExtrDisc.Coherent
import Condensed.Equivalence

namespace ExtrDisc

open CategoryTheory Limits

universe u

theorem sheafCondition (A : Type (u+2)) [Category.{u+1} A] (F : ExtrDisc.{u}ᵒᵖ ⥤ A) :
  Nonempty (PreservesFiniteProducts F) ↔
  Presheaf.IsSheaf (coherentTopology ExtrDisc) F := sorry

end ExtrDisc

to Condensed/ExtrDiscSheafCondition.lean

[Riccardo Brasca]

Is it true that the forgetful functor to CompHaus preserves pullback? Assuming the existence in `ExtrDisc

[Adam Topaz]

I'm not sure.

[Nikolas Kuhn]

I think yes: If you have a diagram Y -> Z <- X, suppose you have a fiber product V_E in ExtrDisc and let V_C be the one in CompHaus with free resolution P(V_C). Using the universal property in CompHaus, you have a continuous map p: V_E -> V_C, which you can check to be surjective. But using the universal property of V_E, you have a unique (since it is determined by its projections to Y and X) lift of the map P(V_C) -> V_C to a map P(V_C) -> V_E. By the construction of the Stone Cech compactification, this means that V_E -> V_C must be bijective, hence an iso by compactness.

[Filippo A. E. Nuccio]

@Riccardo Brasca @Adam Topaz @Dagur Ásgeirsson Thanks for moving things around and closing some sorries. I have tried to follow the thread but could not get if there are still things missing for the equivalence. The AB5 is another thread, no? I am asking simply to make it easier to understand what remains to be done...

[Riccardo Brasca]

Riccardo Brasca said:

Dagur Ásgeirsson Filippo A. E. Nuccio I made a little clean-up, moving stuff around. Now the construction of pullbacks in ExtrDisc is in its own file. Here is the situation: I think final depends on three sorry:

• Extensivity_ExtrDisc in ExtrDisc.ExplicitSheaves: I am working on it.
• isPullbackSieve_DagurSieveIso and isSheafForDagurSieveIso both in Sieves.dagur. These should be relatively easy given what we already have. (In any case we should move this file, since it is for ExtrDiscr)

The file Sieves.DagurSpecial contains a bunch of sorry, but it is not used anywhere, we can ignore it.

@Filippo A. E. Nuccio nobody is working on those I think

[Filippo A. E. Nuccio]

(Not that I will tonight... I was simply trying to understand :smile: )

[Riccardo Brasca]

Extensivity for ExtrDisc is done, so its Dagur coverage is officially a coverage.

def foo : Coverage ExtrDisc.{u} := dagurCoverage ExtrDisc EverythingProj_ExtrDisc
  Extensivity_ExtrDisc

#print axioms foo -- 'foo' depends on axioms: [Quot.sound, propext, Classical.choice]

[Riccardo Brasca]

Tomorrow I will clean up my code, there is a lot of useless stuff.

[Riccardo Brasca]

We are really close to final. The two remaining sorry are both in Sieves.Dagur.lean and should be quite easy (maybe even very easy).

[Riccardo Brasca]

(deleted)

[Adam Topaz]

Great! How far away is the proof that this coverage generates the same topology as the coherent coverage?

[Adam Topaz]

I'm curious to see precisely what's used in that argument. Is it true for any precoherent category? (My guess is that some additional conditions are needed.)

[Adam Topaz]

I mean, for foo to be a coverage the category needs some additional conditions as well.

[Adam Topaz]

But I'm not sure whether those alone suffice.

[Riccardo Brasca]

Adam Topaz said:

Great! How far away is the proof that this coverage generates the same topology as the coherent coverage?

This is already done, sorry free.

[Adam Topaz]

Awesome!

[Adam Topaz]

I assume you use the explicit description using joint surjectivity for that?

[Adam Topaz]

At least we should come up with some abstraction that works for CompHaus, Profinite and ExtrDisc at the same time.

[Riccardo Brasca]

The thing is the following: the presieves we consider are of type 1 or type 2:

• type 1: given by Sigma.desc, assuming it is an iso
• type 2: one single morphism, that is an epi

First of all we need to prove that it is a coverage. I am almost sure that docs#Mathlib.CategoryTheory.Extensive implies that presieves of type 1 form a coverage and it is probably the good abstraction. We proved that it is a coverage by hand.

For type 2 it's less clear to me. I think the standard name is the regular coverage, taking one single regular epi. For ExtrDisc it doesn't matter and the presieves form a coverage because every object is projective. I think for CompHaus and Profinite this follows by the existence of pullbacks, but I didn't check. @Filippo A. E. Nuccio was working in this. Maybe in general we need a regular category, or whatever.

In the proof that the Dagur topology is the same as the coherent one I think we use effectiveEpiFamily_tfae, so I don't know if there is a good abstraction for that. I again suspect that this can be related to regular categories, but my guess is purely based on what people talk about in the nlab.

[Adam Topaz]

the thing is, regular categories are usually assume to have all finite limits, so that's too restrictive for ExtrDisc.

[Riccardo Brasca]

I am less sure about that part, but the point is to ensure that presieves given by a single (regular/effective/whatever) epi form a coverage.

[Riccardo Brasca]

For ExtriDiscr it is because of projectivity of every object, that is a strange property.

[Riccardo Brasca]

BTW one of the two sorry above is done.

[Riccardo Brasca]

So it only remains

lemma isSheafForDagurSieveIso {X : C} {S : Presieve X} (hS : S ∈ DagurSieveIso X)
    {F : Cᵒᵖ ⥤ Type max u v} (hF : PreservesFiniteProducts F) : Presieve.IsSheafFor F S :=

(DagurSieveIso are presieves of type 1 above). The idea is to use docs#CategoryTheory.Equalizer.Presieve.sheaf_condition (but since the result in mathlib assumes C has pullback I had to generalize it by assuming only that the pullback of arrows in the presieve exist)

[Adam Topaz]

Riccardo Brasca said:

For ExtriDiscr it is because of projectivity of every object, that is a strange property.

Yes, this is one way to see this for ExtrDisc. But there's another, which might generalize more widely (in terms of those "weak" pullbacks I mentioned last week): If f : X -> Y is an epi, and g : Z -> Y any morphism, you can pullback in CompHaus and resolve in ExtrDisc to see that singleton epis form a coverage.

[Adam Topaz]

So in some sense for any epi f and any g, there is some weak pullback of f and g which is an epi. I say "some" because those weak pullbacks are not unique upto iso like pullbacks are.

[Riccardo Brasca]

Riccardo Brasca said:

So it only remains

lemma isSheafForDagurSieveIso {X : C} {S : Presieve X} (hS : S ∈ DagurSieveIso X)
    {F : Cᵒᵖ ⥤ Type max u v} (hF : PreservesFiniteProducts F) : Presieve.IsSheafFor F S :=

(DagurSieveIso are presieves of type 1 above). The idea is to use docs#CategoryTheory.Equalizer.Presieve.sheaf_condition (but since the result in mathlib assumes C has pullback I had to generalize it by assuming only that the pullback of arrows in the presieve exist)

I am going to sleep, but I think this one is false in general (but true for ExtrDisc and friends): morally it is true because in the usual diagram we take $U_i \times_X U_j$, and by definition of our presieve we have $X = \coprod U_i$, so the pullback is the final object (being empty it's initial in C, but we work with Cᵒᵖ) and in particular F sends it to a singleton. But in general there is no reason for the pullback to be final, see docs#CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen. In our case it shuld be easy to do it by hand.

[Riccardo Brasca]

I really think that the way to go for sieves of type 1 is with extensive categories... but I am too lazy to do it

[Filippo A. E. Nuccio]

I might give it a try in the afternoon, unless @Riccardo Brasca or @Dagur Ásgeirsson or @Adam Topaz (or anyone else...) is already working on it.

[Dagur Asgeirsson]

I’m not working on anything at the moment. Great to see that it’s almost done!

[Riccardo Brasca]

@Filippo A. E. Nuccio I think you can do something similar to what you already did to prove that the coverage is a coverage: find some sort of categorical assumption (see my message above) and prove it.

[Riccardo Brasca]

Then we can prove that ExtrDisc has this property

[Filippo A. E. Nuccio]

Yes, that's what I had in mind -- and why I proposed to go for it. I'll keep you posted.

[Riccardo Brasca]

I think that a good start is

lemma isSheafForDagurSieveIso {X : C} {S : Presieve X} (hS : S ∈ DagurSieveIso X)
    {F : Cᵒᵖ ⥤ Type max u v} (hF : PreservesFiniteProducts F) : Presieve.IsSheafFor F S := by
  refine' (Equalizer.Presieve.sheaf_condition' F <| isPullbackSieve_DagurSieveIso hS).2 _
  rcases hS with ⟨α, _, Z, π, hS, HIso⟩
  rw [Limits.Types.type_equalizer_iff_unique]
  intro y hy
  sorry

[Riccardo Brasca]

What I am doing atm is just replacing the definition of the sieve of type 1 with the one that gives the coproduct definitionally. It's not necessary, but it is surely nice to have.

[Filippo A. E. Nuccio]

But are you also keeping the old one, just in case?

[Filippo A. E. Nuccio]

Using a ' or something?

[Riccardo Brasca]

I am not pushing anything, so don't worry

[Riccardo Brasca]

I mean, I will push it only when everything works

[Filippo A. E. Nuccio]

But at any rate what do you mean that you "replace" the definition? In the dagur file as well? So you need to fix the prove that it is a coverage?

[Riccardo Brasca]

Yes, but again, I am doing it.

[Riccardo Brasca]

The proof will just became easier

[Riccardo Brasca]

Mmm, forget about this, I now think it doesn't work.

[Riccardo Brasca]

It's possible that we don't need any particular categorical assumption here.

lemma isSheafForDagurSieveIso {X : C} {S : Presieve X} (hS : S ∈ DagurSieveIso X)
    {F : Cᵒᵖ ⥤ Type max u v} (hF : PreservesFiniteProducts F) : Presieve.IsSheafFor F S := by
  refine' (Equalizer.Presieve.sheaf_condition' F <| isPullbackSieve_DagurSieveIso hS).2 _
  rcases hS with ⟨α, _, Z, π, hS, HIso⟩
  rw [Limits.Types.type_equalizer_iff_unique]
  dsimp [Equalizer.FirstObj]
  intro y hy
  sorry

Now, goal is

∃! x, Equalizer.forkMap F (fun {Y} {f} => S f) x = y

and the type of y is ∏ fun f => F.obj f.fst.op (in this product f satisfies S). The point is that there is an iso (since F preserves products)

φ : ∏ fun f : ΣY, { f : Y ⟶ X // S f } => F.obj (op f.1) ≅ F.obj (∏ fun f : ΣY, { f : Y ⟶ X // S f } => (op f.1))

and we can use the assumption of S to transport φ yto F.obj X.op.

[Riccardo Brasca]

Atm the I am trying to prove the instance

have : Finite (ΣY, { f : Y ⟶ X // S f })

since otherwise we cannot even speak about φ

[Riccardo Brasca]

Does anyone see a quick way of proving the finiteness? It is surprisingly annoying...

[Filippo A. E. Nuccio]

The elements in the { are in bijection with alpha, right?

[Riccardo Brasca]

Mathematically yes, but is difficult to convince Lean

[Filippo A. E. Nuccio]

Sure, sure, I was starting mathematically. I want to make sure we agree on what goes on :smile:

[Riccardo Brasca]

The problem is that all types are dependent, so forget about sets

[Riccardo Brasca]

Ah, I am stupid: π is surjective from α to what we want.

[Riccardo Brasca]

I am now working on isSheafForDagurSieveIso. Still not clear if it is easy or not.

[Riccardo Brasca]

If someone wants to help I am now stuck because of this question

[Dagur Asgeirsson]

I'll start working on this again tomorrow. Do I understand correctly that once the remaining sorry in isSheafForDagurSieveIso is closed, we have a complete proof of final in ExtrDisc/ExplicitSheaves?

@Riccardo Brasca do you want me to work on something related to that sorry? If that's close to done and you think you'll finish that by yourself, then I can start fixing Profinite/ExplicitSheaves and CompHaus/ExplicitSheaves. When that's done, we should make some TFAE statements for being a condensed set. Anything else?

[Riccardo Brasca]

Let me see if I can finish it in the next 48 hours

[Riccardo Brasca]

OK I now think there is something quite subtle. Let me explain, and hopefully I will also understand better.

We start with an object X in a category C (with some properties) and a presieve S : Presieve X such that hS : S ∈ DagurSieveIso X. Given a functor F : Cᵒᵖ ⥤ Type max u v such that PreservesFiniteProducts F, we want to show that Presieve.IsSheafFor F S.

Since S ∈ DagurSieveIso X, we have that S = Presieve.ofArrows Z π, where α is a Fintype, Z : α → C and (a : α) → Z a ⟶ X. Moreover, we have IsIso (Sigma.desc π)`. So far so good.

The assumptions on C imply that isPullbackSieve S, so we can use the analogue of docs#CategoryTheory.Equalizer.Presieve.sheaf_condition (we have already proved this). Via docs#CategoryTheory.Limits.Types.type_equalizer_iff_unique what we have to prove now is the usual equalizer condition, I mean this one.

The math proof, following the notations of the Stack project ($U$ is our X and $U_i$ is Z a), is pretty simple: we have $y \in \prod_{i \in I} \mathcal F(U_i)$ such that $\mathrm{pr}_0^\ast (y) = \mathrm{pr}_1^\ast (y)$, and we have to prove that there is a unique $z \in \mathcal F(U)$ such that its image is $y$. Now, we don't care about the condition (that morally is always satisfied since our covering is disjoint), and we use that, since $\mathcal F$ sends coproduct to product we have that $\prod_{i \in I} \mathcal F(U_i) \cong \mathcal F(U)$ and we're done.

In Lean, things are a little more complicated, since X is not literally the disjoint union, it is only isomorphic via Sigma.desc π, but this is not a real problem. Let me be totally precise. We have isomorphisms (I mean, we have in Lean)

 F.obj (∏ fun a => (op <| Z a)) ≅  ∏ fun a => F.obj (op <| Z a)

∐ Z ≅ X

(∐ Z).op ≅ ∏ fun z => (Z z).op

so everything looks good, except that all these product/coproduct are indexed over α, and this is not the index set of the product in stack project! The index set there is given by S, so to be again completely precise in Lean it is (let me call it T)

T := Σ(Y : C), { f : Y ⟶ X // S f }

It is easy to construct a function v : α → T, that sends a to the arrow π a in the sigma type, and by definition this function is surjective. But it is not injective in general! Indeed π can a priori very well give two times the same morphism. At the beginning I thought this was not the case since Sigma.desc π is an iso, but if we have a ≠ b such that Z a = Z b = ∅, then a and b are sent to the same element in T.

So the point is the following: we have y with type

∏ fun (f : T) => F.obj f.fst.op

and we need to construct a term of type F.obj X.op. We can use the isos above (or their variations for T instead of α), but at some point we need to produce a function v : T → α (for example the right inverse of v above). Being the right inverse will prove that our element is sent to y or that it is the only one that can be sent to y (it's too late to understand this), but not the other condition. What do you think?

Sorry for the very long message, it is mainly useful to myself I guess.

[Dagur Asgeirsson]

Mathematically, it's fine because the only way this happens is in the case you mention where a ≠ b with Z a = Z b = ∅. And you seem to be on the right track, you just need to show that the function v : α → T induces an isomorphism on the products?

[Dagur Asgeirsson]

I really mean v : α → T, no need to produce a function in the other direction. The isomorphism on the products is the only thing you need, right?

[Dagur Asgeirsson]

I'll start working on Profinite/ExplicitSheaves and CompHaus/ExplicitSheaves

[Riccardo Brasca]

Sure, I am not saying there is a mathematical problem , only a Lean one

[Dagur Asgeirsson]

I know. But you agree about the direction of the map v?

[Riccardo Brasca]

Oh, I didn't read your message carefully, but I was to prove exactly that. To be precise we need that it is an iso and its inverse is the morphism already in the diagram

[Riccardo Brasca]

I mean, not its inverse

[Riccardo Brasca]

But that it is compatible with the given morphism

[Dagur Asgeirsson]

To do Profinite/ExplicitSheaves etc. I'm defining a dagurCoverage' [HasFiniteCoproducts C] [HasPullbacks C] (h_ext : Extensivity C). We don't have that anywhere yet, right?

[Riccardo Brasca]

Not exactly, but most of the proof should be the same

[Riccardo Brasca]

@Filippo A. E. Nuccio should know

[Dagur Asgeirsson]

Yeah the first half is identical, but in the second half I use the pullback instead of projectivity

[Riccardo Brasca]

The coverage is the same, so maybe it's convenient to write a lemma that says the set of sieves form a coverage

[Filippo A. E. Nuccio]

I am in a meeting now, I will read the thread in the afternoon (if it is not too late....)

[Dagur Asgeirsson]

Pushing dagurCoverage' for categories with pullback now. I define it in dagur.lean just below dagurCoverage

[Riccardo Brasca]

The proofs of one and one' worked perfectly well for Profinite and CompHaus, so if dagurCoverage' is the same as dagurCoverage (except for the proof the Prop valued part) they should work too.

[Dagur Asgeirsson]

Yes those are done. "Sorried" in the commit messages meant that extensivity and epi_pullback_of_epi are sorried. I'm working on that now

[Dagur Asgeirsson]

It seems like it should be enough to prove extensivity for CompHaus and then deduce it for Profinite and ExtrDisc by proving that the property is preserved by pullback-and-finite-coproduct-preserving functors

[Dagur Asgeirsson]

We should also come up with a good way to state the equalizer condition for a single surjection for the explicit properties a presheaf on Profinite/CompHaus has to satisfy to be a condensed set

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

Forget my last message

[Riccardo Brasca]

Parentheses are messed up :man_facepalming:

[Dagur Asgeirsson]

I just pushed some progress on extensivity of CompHaus

[Dagur Asgeirsson]

There is one annoying sorry in extensivity_injective

[Dagur Asgeirsson]

exact Sigma.subtype_ext Hfst hR works in the analogue for ExtrDisc, but for some reason it doesn't work in CompHaus...

[Dagur Asgeirsson]

Maybe someone wants to take a look

[Kevin Buzzard]

Where exactly is this pushed?

[Dagur Asgeirsson]

On branch dagur_ExtrDiscExplicitSheaves of the Copenhagen repo

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Not exactly, but most of the proof should be the same

Yes, I confirm that we did not have them. But it seems they are on their way....

[Dagur Asgeirsson]

Dagur Ásgeirsson said:

There is one annoying sorry in extensivity_injective

I've been fighting with Lean about this sorry for the last few hours... I'm stopping now and I'll push my progress if someone wants to take a look. Also, extensivity_explicit is kind of slow, I don't know why

[Riccardo Brasca]

I am also fighting a little with Lean :)

I've pushed the iso between products and coprodut in the opposite category, and there is a sorry here that we need.

[Riccardo Brasca]

It's the fact that the iso sends the inclusion to the projection, or the other way around and it is hopefully true...

[Riccardo Brasca]

This small lemma is done.

[Riccardo Brasca]

I've pushed some progress towards the last sorry in Dagur.lean. The file is a mess ATM, hopefully I will be able to finish it tomorrow. In any case I will clean it up.

[Riccardo Brasca]

Boom!

theorem final (A : Type (u+2)) [Category.{u+1} A] {F : ExtrDisc.{u}ᵒᵖ ⥤ A}
    (hF : PreservesFiniteProducts F) : Presheaf.IsSheaf (coherentTopology ExtrDisc) F := by
  rw [← one']
  exact fun E => (Presieve.isSheaf_coverage _ _).2 <| fun S hS => isSheafFor_of_Dagur hS
    ⟨fun J inst => have := hF.1; compPreservesLimitsOfShape _ _⟩

#print axioms final --'final' depends on axioms: [Quot.sound, propext, Classical.choice]

[Riccardo Brasca]

I will clean up the proof tomorrow. There is room for quite a lot of PR to mathlib :)

[Kevin Buzzard]

That's a great milestone! It was one of the "key results" which Adam and I wanted to get done. The other one is AB5 for Condensed Ab :-)

[Riccardo Brasca]

@Dagur Ásgeirsson In my opinion we should define two coverages, not only two types of presieves. Indeed, they mix in exactly only proof (the fact that together they generate the coherent topology)

• for the first one to be a coverage we used HasPullbackOfIsIsodesc and Extensivity. The first one is obviously true if there are pullbacks and the second one follows by the explicit description of the pullback in ExtrDisc (the same strategy works in Profinte and CompHaus). If we want to go deep in the categorical rabbit hole then extensive categories are the way (we need "inclusions in the coproduct are disjoint " and "something like that). In any case the interesting thing is that we have proved the following

CategoryTheory.isSheafForDagurSieveIso.{u, v} {C : Type u} [inst✝ : Category C] [inst✝¹ : HasFiniteCoproducts C]
  [inst✝² : HasPullbackOfIsIsodesc C] {X : C} {S : Presieve X} (hS : S ∈ DagurSieveIso X) {F : Cᵒᵖ ⥤ Type (max u v)}
  (hF : PreservesFiniteProducts F) : Presieve.IsSheafFor F S

in particular we don't need to know anything like extensivity (this is about one particular presieve, so no coverage is involved), and HasPullbackOfIsIsodesc is very reasonable, since it is implied by HasPullbacks. This was quite hard to prove, but it is the "trivial" statement that a presheaf that sends finite disjoint unions to products satisfies the sheaf condition for a covering given by a disjoint union.

• the second coverage is a coverage if EverythingIsProjective, and in this case the sheaf condition is automatic. This is a very specific condition that miraculously holds for ExtrDisc but we can forget about it. You are working on the fact that HasPullback implies that this is a coverage, right? I think we also need something like effectiveEpiFamily_tfae, but I don't see exactly a good generalization (it should be something related to regular epi). For the condition of being a sheaf wrt to this presieve I don't think there is anything very interesting, we be more explicit using Equalizer.Presieve.sheaf_condition' (or the mathlib version without ' if the category has pullbacks) and Limits.Types.type_equalizer_iff_unique but that's it in my opinion.

[David Michael Roberts]

Split epis automatically form a coverage for an even sillier reason, though it's not enough to get a pretopology: Given a split epi p:A -> B, with section s:B->A, and a map f:C->B, then the required cover of C is the identity map (which is a split epi), and then the map sf:C->B->A completes the commutative square.

[David Michael Roberts]

You don't need pullbacks, but perhaps you need those for a different reason, eg that the superextensive pretopology is actually a pretopology, not just a coverage.

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Dagur Ásgeirsson In my opinion we should define two coverages, not only two types of presieves. Indeed, they mix in exactly only proof (the fact that together they generate the coherent topology)

• for the first one to be a coverage we used HasPullbackOfIsIsodesc and Extensivity. The first one is obviously true if there are pullbacks and the second one follows by the explicit description of the pullback in ExtrDisc (the same strategy works in Profinte and CompHaus). If we want to go deep in the categorical rabbit hole then extensive categories are the way (we need "inclusions in the coproduct are disjoint " and "something like that). In any case the interesting thing is that we have proved the following

CategoryTheory.isSheafForDagurSieveIso.{u, v} {C : Type u} [inst✝ : Category C] [inst✝¹ : HasFiniteCoproducts C]
  [inst✝² : HasPullbackOfIsIsodesc C] {X : C} {S : Presieve X} (hS : S ∈ DagurSieveIso X) {F : Cᵒᵖ ⥤ Type (max u v)}
  (hF : PreservesFiniteProducts F) : Presieve.IsSheafFor F S

in particular we don't need to know anything like extensivity (this is about one particular presieve, so no coverage is involved), and HasPullbackOfIsIsodesc is very reasonable, since it is implied by HasPullbacks. This was quite hard to prove, but it is the "trivial" statement that a presheaf that sends finite disjoint unions to products satisfies the sheaf condition for a covering given by a disjoint union.

• the second coverage is a coverage if EverythingIsProjective, and in this case the sheaf condition is automatic. This is a very specific condition that miraculously holds for ExtrDisc but we can forget about it. You are working on the fact that HasPullback implies that this is a coverage, right? I think we also need something like effectiveEpiFamily_tfae, but I don't see exactly a good generalization (it should be something related to regular epi). For the condition of being a sheaf wrt to this presieve I don't think there is anything very interesting, we be more explicit using Equalizer.Presieve.sheaf_condition' (or the mathlib version without ' if the category has pullbacks) and Limits.Types.type_equalizer_iff_unique but that's it in my opinion.

But how would you concretely use them? So you would construct these two "collections" of sieves, and adding some adapted hypotheses each of them becomes a coverage?

[Riccardo Brasca]

What do you mean? My point is just about not duplicating all the proofs.

[Filippo A. E. Nuccio]

Sure, but I do not understand how you would do this concretely.

[Filippo A. E. Nuccio]

Perhaps my problem is to understand what are the two coverages you are speaking about.

[Riccardo Brasca]

Sieves given disjoint union and sieves given by a single coverage

[Riccardo Brasca]

We can have a typeclass "type one is a coverage", and define the coverage on any category with this instance (tautologically)

[Riccardo Brasca]

And then provide various instances

[Filippo A. E. Nuccio]

But for "disjoint unions" do you require epi or iso (for single epi, I guess, no?)

[Riccardo Brasca]

Sigma.desc is an iso

[Riccardo Brasca]

I have the impression that when they form a coverage, for any reason, they have good properties

[Filippo A. E. Nuccio]

But then you need something like the coverage generated by two coverages, right? I mean, for ExtrDisc, neither coverage generates the top alone, you need both.

[Dagur Asgeirsson]

A union of two coverages is a coverage, right?

[Riccardo Brasca]

Yes, that's the point

[Riccardo Brasca]

Set-theoretic union

[Dagur Asgeirsson]

But anyway, the thing I'm struggling with is extensivity of CompHaus, the rest is basically done (except finding a good statement for the sheaf condition for a single epi, right now it's not ideal, you can look in CompHaus/ExplicitSheaves)

[Riccardo Brasca]

I can have a look, but the same proof should work, right?

[Riccardo Brasca]

The coproduct is still the disjoint union

[Dagur Asgeirsson]

Well, for ExtrDisc the pullback was defined as a subtype, so you could use Sigma.subtype_ext. Now that doesn't work and if I use Sigma.ext I have to prove a HEq

[Filippo A. E. Nuccio]

Oh no, an Heq seems bad! I can also have a look, unless @Riccardo Brasca is already on it.

[Riccardo Brasca]

I didn't start, so go aheaed

[Riccardo Brasca]

but Heq is almost surely a bad idea

[Dagur Asgeirsson]

Yeah I know, I'm trying to add some API for CompHaus.finiteCoproduct to prove when a map out of a finite coproduct is injective. Right now the old proof is commented below

[Dagur Asgeirsson]

I think I have something now that will work

[Riccardo Brasca]

It's strange that the subtype thing does not work here

[Dagur Asgeirsson]

I think I can write my map out of the coproduct as a Sigma.map, and there are some lemmas about injectivity of those

[Dagur Asgeirsson]

No nevermind

[Dagur Asgeirsson]

I misunderstood

[Dagur Asgeirsson]

Either of you go ahead and take a look!

[Dagur Asgeirsson]

Riccardo Brasca said:

It's strange that the subtype thing does not work here

It's not strange that Sigma.subtype_ext doesn't work, because the components of the sigma aren't subtypes

[Riccardo Brasca]

I mean, it's strange it works for ExtrDisc and not in the other cases

[Dagur Asgeirsson]

No because in ExtrDisc we defined the pullback not as usual, but as a subtype

[Dagur Asgeirsson]

But actually in this case it's a subtype of the product, so maybe one could make Sigma.subtype_ext work by tweaking the first part of the proof

[Riccardo Brasca]

Ah sure. We can do exactly the same though, using docs#CompHaus.pullback

[Dagur Asgeirsson]

That is what we're using

[Riccardo Brasca]

I should probably stop saying nonsense and looking at the code

[Dagur Asgeirsson]

Btw, my finiteCoproduct.injective_of is of course not true. But when trying to prove it, I think I found a way to prove extensivity_injective

[Riccardo Brasca]

I still don't understand exactly why the proof doesn't work for CompHaus. In both cases we uses explicit limits, so the pullback is a subtype of the product. The difference seems that Lean, for CompHaus, goes via Top or something like that.

[Riccardo Brasca]

Ah, the explicit definition of the pullback is not the same

[Dagur Asgeirsson]

OK, I have a proof of extensivity_injective

[Dagur Asgeirsson]

Pretty ugly, but it works

[Dagur Asgeirsson]

It's pushed

[Riccardo Brasca]

great!

[Dagur Asgeirsson]

So CompHaus/ExplicitSheaves is now sorry-free, but we don't have the analogous statement to final in ExtrDisc/ExplicitSheaves.

[Dagur Asgeirsson]

I'll work on Profinite/ExplicitSheaves now, trying to deduce extensivity and epi_pullback_of_epi from CompHaus

[Riccardo Brasca]

What do you think of a typeclass hasDagurCoverage saying that DagurCoverage is a coverage? Having that and HasPullbackOfIsIsodesc all the proofs about DagurSieveIso should work

[Riccardo Brasca]

and we avoid duplicating the code

[Dagur Asgeirsson]

Dagur Ásgeirsson said:

I'll work on Profinite/ExplicitSheaves now, trying to deduce extensivity and epi_pullback_of_epi from CompHaus

Actually maybe I'll just duplicate everything. We already have Profinite.finiteCoproduct and Profinite.pullback

[Dagur Asgeirsson]

Riccardo Brasca said:

What do you think of a typeclass hasDagurCoverage saying that DagurCoverage is a coverage? Having that and HasPullbackOfIsIsodesc all the proofs about DagurSieveIso should work

We will still have to duplicate some code to prove hasDagurCoverage for all three sites

[Riccardo Brasca]

Sure, that part has to be done

[Dagur Asgeirsson]

But I would be fine with it, it would at least reduce the three identical proofs of one' to one proof

[Adam Topaz]

Does [HasDagurCoverage C] [Precoherent C] imply that the Dagur coverage generates the coherent topology?

[Dagur Asgeirsson]

Our proof uses epi_iff_surjective

[Dagur Asgeirsson]

I mean, the explicit description of EffectiveEpiFamily

[Adam Topaz]

yeah, that's what I figured.

[Adam Topaz]

I think the statement is true for the category of projectives in any coherent category.

[Adam Topaz]

And certainly in a coherent category the statement is true

[Adam Topaz]

But I still don't know of a natural categorical criterion which ensures that this holds.

[Dagur Asgeirsson]

Does every coherent category satisfy extensivity?

[Riccardo Brasca]

Tne nlab says "If C is extensive, then its coherent topology is generated by the regular topology together with the extensive topology. "

[Riccardo Brasca]

The extensive topology is generated by what we call DagurSieveIso

[Dagur Asgeirsson]

Where
regular topology = the one generated by DagurSieveSingle
extensive topology = generated by DagurSieveIso?

[Riccardo Brasca]

and the regular topology in our cases coincides with the one generated by DagurSieveSingle

[Riccardo Brasca]

But the definitions are different, as the name suggest the regular topology uses regular epi (just one, as in DagurSieveSingle)

[Riccardo Brasca]

To be honest I am not even sure that in our cases "regular epi iff epi", but I think so

[Adam Topaz]

yes, that's true for comphaus / profinite / extrdic

[Riccardo Brasca]

Dagur Ásgeirsson said:

Does every coherent category satisfy extensivity?

Dagur Ásgeirsson said:

Does every coherent category satisfy extensivity?

almost

[Dagur Asgeirsson]

OK, just pushed Profinite/ExplicitSheaves. Duplicated a lot of the explicit limit API from CompHaus

[Dagur Asgeirsson]

Now in isSheafFor_of_Dagur in CompHaus/ExplicitSheaves and Profinite/ExplicitSheaves, the additional hypothesis on the presheaf is just

(hFecs : ∀ {S : Presieve X} (_ : S ∈ DagurSieveSingle X), IsSheafFor F S)

but we want it to be something like

(hFecs : EqualizerCondition F)

where EqualizerCondition is the explicit sheaf condition for a single surjection in a way that's nice to work with. In LTE, this was

def equalizer_condition : Prop := ∀
(X B : Profinite.{w}) (π : X ⟶ B) (surj : function.surjective π),
function.bijective (map_to_equalizer P π (Profinite.pullback.fst π π) (Profinite.pullback.snd π π)
    (Profinite.pullback.condition _ _))

[Dagur Asgeirsson]

Any opinions on this?

[Riccardo Brasca]

Yes, that's better

[Riccardo Brasca]

It should be easy, right?

[Dagur Asgeirsson]

Yeah I think so

[Riccardo Brasca]

Just use Equalizer.Presieve.sheaf_condition and Limits.Types.type_equalizer_iff_unique

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

nonsense, sorry

[Dagur Asgeirsson]

Just pushed some progress, I've reduced it to two stupid sorries about commutativity of some diagrams with isomorphisms between objects and products over a singleton. We might need some more more API for the explicit limits in CompHaus

[Riccardo Brasca]

I am not sure I will time tomorrow, and I am going to Leiden on Sunday (also Filippo), so we will probably be a little slow.

[Filippo A. E. Nuccio]

I am also finishing preparing my talk for there, so I am already very slow :snail:

[Dagur Asgeirsson]

No worries. Have fun in Leiden!

[Dagur Asgeirsson]

Ok the stupid sorries are done

[Dagur Asgeirsson]

We now also have:

theorem final (A : Type (u+2)) [Category.{u+1} A] {F : CompHaus.{u}ᵒᵖ ⥤ A}
    (hF : PreservesFiniteProducts F)
    (hF' : ∀ (E : A), EqualizerCondition (F ⋙ coyoneda.obj (op E))) :
  Presheaf.IsSheaf (coherentTopology CompHaus) F := by
  rw [← one']
  refine' fun E => (Presieve.isSheaf_coverage _ _).2 _
  intro B S hS
  apply isSheafFor_of_Dagur hS
  · exact ⟨fun J inst => have := hF.1; compPreservesLimitsOfShape _ _⟩
  · exact hF' E

theorem final' (A : Type (u+2)) [Category.{u+1} A] {G : A ⥤ Type (u+1)}
    [HasLimits A] [PreservesLimits G] [ReflectsIsomorphisms G]
    {F : CompHaus.{u}ᵒᵖ ⥤ A}
    (hF : PreservesFiniteProducts (F ⋙ G)) (hF' : EqualizerCondition (F ⋙ G)) :
    Presheaf.IsSheaf (coherentTopology CompHaus) F := by
  rw [Presheaf.isSheaf_iff_isSheaf_forget (coherentTopology CompHaus) F G,
    isSheaf_iff_isSheaf_of_type, ← one', Presieve.isSheaf_coverage]
  intro B S' hS
  exact isSheafFor_of_Dagur hS hF hF'

#print axioms final
-- 'CompHaus.final' depends on axioms: [Quot.sound, propext, Classical.choice]

#print axioms final'
-- 'CompHaus.final'' depends on axioms: [propext, Quot.sound, Classical.choice]

and its analogue for Profinite

[Dagur Asgeirsson]

Here, final is not very helpful, and in all cases of interest I think final' is more useful

[Dagur Asgeirsson]

I'm planning on cleaning up our code now (in particular rename everything that's called dagur-something), and then merge it into master

[Dagur Asgeirsson]

I've opened a PR and it passes CI, but I'll keep pushing to the branch until the code is a bit nicer

[Dagur Asgeirsson]

Our code is now merged into master

[Dagur Asgeirsson]

Here is a dictionary:

• DagurOpenEmbedding = openEmbedding_ι
• DagurSieveIso = ExtensiveSieve
• DagurSieveSingle = RegularSieve
• dagurCoverage/ dagurCoverage' = ExtensiveRegularCoverage/ExtensiveRegularCoverage'
• isSheafFor_of_Dagur = isSheafFor_of_extensiveRegular
• one' = extensiveRegular_generates_coherent

[Riccardo Brasca]

Wow, thanks!

[Riccardo Brasca]

A bit sad for our beloved dagur coverage, but that's life

[Riccardo Brasca]

I can guess your answer but... Are we really sure we don't need a for_mathlib folder?

[Dagur Asgeirsson]

Everything is going in mathlib!

[Riccardo Brasca]

I agree, but I mean a folder with stuff that is ready to be PRed

[Dagur Asgeirsson]

Yes that would be nice

[Dagur Asgeirsson]

For example ExtrDisc/Gleason is ready to be PRed to mathlib. I'm just gonna add everything in that file to the file Mathlib/Topology/ExtremallyDisconnected and open a PR

[Dagur Asgeirsson]

Then we can create a Mathlib/Topology/Category/ExtrDisc/Basic which imports that file

[Dagur Asgeirsson]

Oh I see @David Ang already has a branch gleason on mathlib

[Dagur Asgeirsson]

But there the file has some sorries. Is it an older version of our ExtrDisc/Gleason?

[David Ang]

Dagur Ásgeirsson said:

Oh I see David Ang already has a branch gleason on mathlib

I'm almost done with this and it should be ready for review by the weekend. The old code had a lot of definitions that's only used once in the proof so I was trying to refactor everything to make the argument more readable.

[Dagur Asgeirsson]

Is the one remaining sorry hard? Is it not something we already have in the Copenhagen repo?

[Riccardo Brasca]

The statement in the Copenhagen repo is surely sorry free (since we use it, and our result is sorry free)

[David Ang]

The proof is basically @Nikolas Kuhn's proof in the Copenhagen repo, so the main idea is already sorry-free. However the current code was a statement about a very specific compact space D' that we defined for the proof, and I was trying to refactor it to be a general statement about compact spaces for the PR to mathlib. I encountered some technical set-type issues and I've solved all of them yesterday, but the code might involve stupid hacks like these:

variable {A : Type u} {B : Set A} {C : Set B}
private lemma mem_coe_of_mem {a : A} (ha : a ∈ B) (ha' : ⟨a, ha⟩ ∈ C) : a ∈ (C : Set A) := ⟨_, ⟨⟨_, rfl⟩, _, ⟨ha', rfl⟩, rfl⟩⟩
private lemma coe_subset : (C : Set A) ⊆ B := by rintro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩; convert ha
private lemma mem_of_mem_coe {a : A} (ha : a ∈ (C : Set A)) : ⟨a, coe_subset ha⟩ ∈ C := by rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩; convert ha

private lemma isClosed_trans [TopologicalSpace A] (hC : IsClosed C) (hB : IsClosed B) :
    IsClosed (C : Set A) := by
  rcases isClosed_induced_iff.mp hC with ⟨D, hD, rfl⟩
  convert IsClosed.inter hB hD
  ext
  exact ⟨fun h => ⟨coe_subset h, mem_of_mem_coe h⟩, fun ⟨hB, hD⟩ => mem_coe_of_mem hB hD⟩

The issue was about converting between C as a subset of B, which is a subset of a type A, and C as a subset of A.

[Dagur Asgeirsson]

I think "stupid hacks like these" belong in mathlib. These are very useful statements when doing topology

[David Ang]

I wasn't 100% sure about that - if you try to investigate the types of the lemmas you see a lot of Lean.Internal.coeM which is not used much (if at all) in the rest of mathlib from what I can tell.

[Dagur Asgeirsson]

Ah ok I see

[Alex J. Best]

From when I spoke about these lemmas with Kevin I felt that there should exist some coercion doing what is needed for these lemmas, perhaps it's just that we need to make a nice looking coercion with higher priority rather than using the one that comes from Set being a monad or whatever the weird one is