Abelian sheaves

Stream: condensed mathematics

[Adam Topaz]

We will need a way to go back and forth between abelian group objects in CondensedType and Condensed Ab.
I made some initial definitions along these lines here:
https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/abelian_group_object.lean

There are a few sorry's about proving certain presheaves are sheaves.
I think it's important to use explicit products and terminal objects here, so we can feed them into the monoidal category constructor and not have to deal with the trouble of going back and forth between the category theoretic product in the category Type* and the usual type-theoretic product.

[Adam Topaz]

@Johan Commelin have you made any progress in this direction? I didn't find anything in the repo, but I may have missed it.

[Johan Commelin]

Sorry, haven't gotten around to it yet :sad: :see_no_evil:

[Adam Topaz]

No worries. Let me know what you think about the code in the linked file.

[Adam Topaz]

I think it's a reasonable approach.

[Johan Commelin]

I just read through it. I think it's a pretty smooth approach. LGTM

[Adam Topaz]

Some brave soul might try to prove that for F : SheafOfTypes.Ab T and U : C\op, the type F.val.obj U has an abelian group structure.

[Adam Topaz]

And for the restriction maps associated to the sheaf, I'm now a bit sad we don't have is_add_monoid_hom...

[Johan Commelin]

We do have it, right? It's in deprecated/ and it's no longer a class, and at some point in the future it will move back into mathlib proper.

[Yaël Dillies]

Will it? I understood Kevin figured out it wasn't worth it.

[Adam Topaz]

Oh, I thought Kevin got rid of those things. I'm probably wrong.

[Johan Commelin]

I think it's exactly "edge" cases like this why we should keep them around.

[Johan Commelin]

But since they are now structures instead of classes, they are probably more useful, because more explicit. And it gives us dot-notation, etc...

[Kevin Buzzard]

When I started on that refactor I was pretty convinced that there would be occasional cases when the structures would be useful. As time went on I became much less convinced, but I'm open to being convinced again!

[Kevin Buzzard]

For example I'm pretty sure that we could remove all the import deprecated.* from mathlib, if someone could be bothered. I just got tired of it, I pushed the imports much further down the tree but couldn't quite face finishing the job.

[Adam Topaz]

Quick status update: presheaves taking values in an abelian category are abelian
https://github.com/leanprover-community/lean-liquid/blob/4095445272684705da80405a9df74060bc4bcf0f/src/for_mathlib/abelian_sheaves/functor_category.lean#L240

The case of sheaves is now a little closer.

[Johan Commelin]

The only thing you now need is the isomorphism theorem in the case of sheaves, right?

[Johan Commelin]

All the rest is done, if I understand correctly

[Adam Topaz]

well, the cokernels in sheaves involved sheafification, so it's a little more complicated to obtain the isomorphism theorem for sheaves.

[Johan Commelin]

Sure. But once you have that, you would be done, right?

[Adam Topaz]

I think so... I'm trying now.

[Adam Topaz]

We'll find out whether there are other hangups soon enough

[Adam Topaz]

Okay, so there is an actual hangup -- we need the fact that sheafification is left exact (in the sense that it preserves finite limits). This follows from the fact that finite limits commute with filtered colimits in Type* (and hence any of the concrete categories we have around in the context of sheafification), but it will require some more serious work to actually get this result.

[Johan Commelin]

Aah, bummer. Good catch.

[Scott Morrison]

https://leanprover-community.github.io/mathlib_docs/category_theory/limits/filtered_colimit_commutes_finite_limit.html#top

[Scott Morrison]

(Perhaps I even had this application in mind, I forget. :-)

[Adam Topaz]

instance presheaf_to_Sheaf_preserves_finite_limits (K : Type (max v u))
  [small_category K] [fin_category K] [has_limits_of_shape K D] :
  preserves_limits_of_shape K (presheaf_to_Sheaf J D) :=

is now sorry free... but it's a mess...

[Adam Topaz]

And even more good news... the following are both sorry free as well!

instance abelian : abelian (Sheaf J A) :=
abelian_of_coim_to_im (λ F G η, infer_instance)

and

instance : abelian (Condensed Ab.{u+1}) :=
begin
  delta Condensed,
  -- I don't know why this is needed either...
  apply @category_theory.Sheaf.abelian.{(u+2) u (u+1)}
    Profinite.{u} _ proetale_topology Ab.{u+1} _ _ _ _ _ _ _ _,
end

It's still very messy... I hope I'll have some time soon to get this in better shape for mathlib.

[Kevin Buzzard]

Did you do that stuff I was working very slowly on? The finite products iff binary and 0 product thing?

[Adam Topaz]

@Kevin Buzzard no I didn't. This abelian category instance is for sheaves on an arbitrary site taking values in any (sufficiently concrete, whatever that means) abelian category

[Kevin Buzzard]

I did finite products -> empty product and am about half way through finite products -> binary products. I've been held up by a time-critical task :-(

[Adam Topaz]

We will still need the finite product stuff to see that sheaves on profinite can be computed easily using exteremally dosconnecteds

[Johan Commelin]

Awesome! Thanks a lot @Adam Topaz

[Johan Commelin]

That's one more milestone out of the way.

[Adam Topaz]

I worked on the adjunction between condensed sets and condensed abelian groups today.

I got

def Ab_to_Type_adjunction : Type_to_Ab ⊣ Ab_to_Type := ...

with

def Type_to_Ab : CondensedSet ⥤ Condensed Ab := ...
def Ab_to_Type : Condensed Ab ⥤ CondensedSet := ...

toward the bottom of condensed/adjunctions.lean.

The only sorrys remaining in the proof of this adjunction are in the file for_mathlib/sheafify_forget.lean about the compatibility of the forgetful functor and sheafification. If anyone wants to practice their lean category theory chops, please feel free to take a look at that file!

[Adam Topaz]

The sheafification compatibility is here: #10510

[Johan Commelin]

Great, thanks a lot!

[Adam Topaz]

Here is a PR for the adjunction in general:
#10541

[Johan Commelin]

I will review it later tonight. I'm on a call now.

[Adam Topaz]

No rush

[Johan Commelin]

I left a review of the PR it depends upon

[Adam Topaz]

:ping_pong: #10541 :thank_you:

[Johan Commelin]

Thanks for the reminder. It's on the queue now

[Adam Topaz]

Mecri!

[Andrew Yang]

Do we / will we know that sheafification preserves finite limits?

[Johan Commelin]

instance sheafification_preserves_finite_limits (K : Type (max v u))
  [small_category K] [fin_category K] [has_limits_of_shape K D] :
  preserves_limits_of_shape K (sheafification J D) :=
by { delta sheafification, apply_instance }

[Johan Commelin]

In src/for_mathlib/abelian_sheaves/left_exact.lean of the LTE repo

[Johan Commelin]

Kudos to Adam

[Andrew Yang]

I now notice that this is just above :sweat_smile:
I guess pullbacks of sheaves aren't as far as I thought.

[Adam Topaz]

@Andrew Yang the fact that Sheaf_to_presheaf creates limits is already in mathlib, and that's enough to obtain limits (in particular, pullbacks) in Sheaf J A. Is this what you're looking for?

[Andrew Yang]

By pullback I meant the inverse image functor. Not the categorical one.
I'm looking for the left-exactness of the pullback functor, of which the left-exact-ness of sheafification is the final piece missing.
Not that I'll need this result right now though. There's still plenty of things to push into mathlib before I could use it to do more stuff.

[Adam Topaz]

Andrew Yang said:

Do we / will we know that sheafification preserves finite limits?

Thanks Johan for reviewing #11252 ! @Andrew Yang this will be in mathlib in a couple of hours ;)

[Johan Commelin]

@Adam Topaz Did you also do the adjunction between sheaves of types (aka sets) and sheaves of {abelian groups, R-modules, etc}, that forgets in one direction, and takes the free sheaf in the other direction?

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/185f86120c3c78e6bd276bac89dd9f977ed328c9/src/condensed/adjunctions.lean#L53

[Adam Topaz]

Or in general docs#category_theory.Sheaf.adjunction_to_types

[Adam Topaz]

If you want to consider Sheaf J Type* instead of SheafOfTypes J, you can use docs#category_theory.Sheaf.adjunction