Sheafification

Stream: condensed mathematics

[Adam Topaz]

I started working toward sheafification in a general context (i.e. for sheaves on a site $\mathcal{C}$ taking values in a category $\mathcal{D}$ where $\mathcal{D}$ has enough (co)limits).

the code I have so far is in the mathlib branch branch#sites-sheafification

so far, I have the construction of $\mathcal{F}^+$ following the discussion here stacks#00W1

The proof that $\mathcal{F}^+$ is functorial is much to painful right now. If anyone wants to have a go at simplifying and breaking up some of the proofs into smaller pieces, that would be very helpful!

[Adam Topaz]

There is one point where this diverges from the page on the stacks project -- I don't assume that $\mathcal{C}$ has pullbacks, so instead of using the pullback to obtain the relations among the local sections, I instead mimic the definition of docs#category_theory.presieve.family_of_elements.compatible

[Andrew Yang]

Hi, I'm quite interested in this (or at least in the results of this that I could use elsewhere).
Is there any updates on this? / Is there anything I could help?

[Adam Topaz]

@Andrew Yang one point to note here is that (contrary to what I wrote above) having enough (co)limits in the target category (even all limits and colimits) is not enough. There is an additional condition that's required saying that certain products commute with certain colimits. The nlab calls this the "IPC property" see the bottom of nlab#sheafification

So for now, I think it would be better to just work with Type* valued presheaves to get things moving along.

[Andrew Yang]

Which part of the proof would break?

[Andrew Yang]

Does it still work for concrete categories with a forgetful functor that preserves limits and filtered colimits? (which is what I was looking for)

[Adam Topaz]

Maybe one needs the forgetful functor to reflect isomorphisms as well?

[Adam Topaz]

I think that's a reasonable setting: A concrete category where the forgetful functor preserves limits, filtered colimits, and reflects isos. This will take care of the algebraic categories for example

[Adam Topaz]

There may be some additional conditions required on the site itself so that the colimit diagrams are actually filtered.

[Andrew Yang]

If I'm not mistaken, the colimit seems to be filtered as intersections of two covering sieves is still covering.

[Adam Topaz]

Oh yes of course.

[Andrew Yang]

In fact I've already played with some of your code over at branch#erd1/sites-sheafification, and in particularly showed that such forgetful functors preserve the constructed plus. I suppose it would be useful when we want to show that plus plus is a sheaf for such concrete categories.

[Adam Topaz]

Great!

[Reid Barton]

Maybe for generality you should allow a whole family of jointly conservative functors which preserve [...], to include locally finitely presentable categories. (For general locally presentable categories the sheafification will also exist but I guess it might not be computed by the same formula.)

[Reid Barton]

I guess it probably also works if you have a conservative functor (preserving limits + filtered colimits) to a topos, even one that's not lfp?

[Johan Commelin]

@Reid Barton Does your example include the family "S : ExtrDisc ↦ (evaluate condensed sets at S)"?

[Johan Commelin]

It that the kind of thing you have in mind?

[Reid Barton]

Yes. Or even evaluation at all profinite sets or all compact Hausdorff spaces if you like. Those all preserve filtered colimits because the topology is generated by finite covering families

[Reid Barton]

The other thing I had in mind was just something like simplicial sets

[Andrew Yang]

@Adam Topaz Hi, are you still working on it / planning to work on it?
If not, I can adopt this project since I'll probably need the results when working on the AG library in the near future.

[Adam Topaz]

@Andrew Yang Yes, I am still working on it (but a lot slower than usual since the two classes I'm teaching both have midterms this week). I decided to switch up the definition a bit by defining the notion of a "multiequalizer" which essentially computes the equalizer of the map between the products as a single limit. The API is much smoother with this.

[Andrew Yang]

That's great! Probably the gluing of stuff should also use such an API as it is also an equalizer between products.

[Adam Topaz]

for now I have the code for this new approach in a branch of LTE
https://github.com/leanprover-community/lean-liquid/compare/sheafification_stuff

Since you say this will be useful for you in the near future, I will start opening mathlib PRs sooner rather than later.

[Adam Topaz]

Here is the first one: #10169

[Adam Topaz]

The following is now sorry free:

def adjunction : (presheaf_to_Sheaf D J) ⊣ (Sheaf_to_presheaf J D) := ...

In the following general context:

universes w v u
variables {C : Type u} [category.{v} C] {D : Type w}
  [category.{max v u} D] {J : grothendieck_topology C}

variables [has_limits D] [has_colimits D]
variables [concrete_category.{max v u} D]
variables [preserves_limits (forget D)]
variables [∀ (X : C), preserves_colimits_of_shape (J.cover X)ᵒᵖ (forget D)]
variables [reflects_isomorphisms (forget D)]

(The categories J.cover X are all cofiltered, so their opposites are filtered, hence the preserving colimits assumption holds true for all of the usual algebraic categories)

[Adam Topaz]

I'll push to LTE's master, but it will require some serious cleanup work to get this into mathlib.

[Adam Topaz]

(Oh, and the [has_colimits D] can also be relaxed... I was just lazy ;))

[Adam Topaz]

Oh, and you can now add the following to the mix too:

lemma reflective : is_iso (adjunction D J).counit :=
nat_iso.is_iso_of_is_iso_app _

[Adam Topaz]

@Andrew Yang I'm still planning to make mathlib PRs for this, but the next one I was working on got stuck because of the following silly issue:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/iso.20to.20is_iso.20for.20types/near/261068565

[Johan Commelin]

@Adam Topaz Wow, thanks a lot! We can tick of another speedbump!

[Adam Topaz]

@Johan Commelin , thanks for reviewing my last couple of PRs. The next one is not so easy :) #10284

[Adam Topaz]

:ping_pong: #10294

[Adam Topaz]

And another ;) #10297

[Adam Topaz]

And the final one... #10303

[Adam Topaz]

Here's the next one for colimits of sheaves: #10334

[Johan Commelin]

That's going really smooth. Which is very nice to see