functor from top spaces to condensed sets

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

I was seeing what went into constructing the functor from top spaces to condensed sets. A sheaf condition needs to be checked. Right now I have this:

X: TopCat
S: Type u
B: CompHaus
α: Type
inst✝: Fintype α
Y: α → CompHaus
F: (a : α) → Y a ⟶ B
hF: EffectiveEpiFamily Y F
⊢ Presieve.IsSheafFor ((Functor.op compHausToTop ⋙ yoneda.obj X) ⋙ coyoneda.obj S.op) (Presieve.ofArrows Y F)

I don't know whether introducing S was a good idea. Do we have that a sheaf T on Top is just one satisfying T(finite coprod) = finite prod, and T well-behaved on pullback maps coming from quotients?

[Riccardo Brasca]

The characterization with equalizers is docs#CategoryTheory.Presheaf.isSheaf_iff_isSheaf' and friends

[Riccardo Brasca]

We have several related notions and I am playing quite a lot with them for ExtrDiscr (that complicates things since it doesn't have pullbacks)

[Riccardo Brasca]

Note that you can get rid of yoneda using docs#CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget

[Kevin Buzzard]

I was trying to do precisely this but Lean complains that it can't find Full (yoneda.obj X)

[Adam Topaz]

docs#CategoryTheory.Yoneda.yonedaFull

[Dagur Asgeirsson]

Shouldn’t we use the easy ExtrDisc sheaf condition when defining this functor?

[Adam Topaz]

Yeah probably

[Adam Topaz]

It would be much easier to check the sheaf condition

[Adam Topaz]

Much easier means essentially trivial once we know that extrdisc to top preserves finite coproducts (which is still missing IIRC)

[Dagur Asgeirsson]

We still might want to prove the sheaf condition for CompHaus (or Profinite) to know the S-valued points of a topological space regarded as a condensed set, for S : CompHaus. Or is there an easier way to do that? If we just define a presheaf on ExtrDisc and prove that it’s a sheaf, then we only know that the associated condensed set, when regarded as a presheaf on CompHaus is right Kan extended from the one on ExtrDisc

[Adam Topaz]

Yeah good point. How close is “dagurification”?

[Kevin Buzzard]

Adam Topaz said:

docs#CategoryTheory.Yoneda.yonedaFull

That's proving that yoneda is full, not (yoneda S).

[Adam Topaz]

whoops

[Adam Topaz]

Why don't you use the multiequalizer condition instead?

[Kevin Buzzard]

Riccardo Brasca said:

Note that you can get rid of yoneda using docs#CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget

This turned out to be more interesting than I imagined! The type of this (with universes switched on) is

CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget.{v₁, u₁, u₂} {C : Type u₁} [inst✝ : Category.{v₁, u₁} C]
  {A : Type u₂} [inst✝¹ : Category.{max v₁ u₁, u₂} A] (J : GrothendieckTopology.{v₁, u₁} C)
...

and we want to apply it with C = CompHaus.{u} (so v1=u and u1=u+1, it's a large category) and A = Type u (because we have X : CompHaus.{u} and the morphism from C^op to A is yoneda.obj X). But this is not possible! Because the category instance on A has morphisms in Type u but the universes in the declaration force the morphisms to be in type Max v1 u1 which is Type (u+1) in the application :-)

[Kevin Buzzard]

In fact the declaration itself is

theorem isSheaf_iff_isSheaf_forget (s : A ⥤ Type max v₁ u₁) [HasLimits A] [PreservesLimits s] ...

!

[Kevin Buzzard]

While you've all been thinking about sheaves, I've been totally nerdsniped and am wrestling with universes, trying to make Dagur's strange-looking wish come true (universes may go down as well as up). Right now this is kind of impossible to do in mathlib master because some choices of universes meant that we had to solve u=u+1 :-/ I'm currently trying to generalise things (i.e. fix them up) at branch kbuzzard-universe-gen.

[Scott Morrison]

Note that this same definition is implicated in the whole "forwarding porting !3#19153 is a nightmare / can we modify Lean's universe unification" train wreck that has been occupying too much of my attention. :-)

[Kevin Buzzard]

Scott what do you think of the changes in my branch? I've got not idea whether it's nearly compiling or hopeless.