Filtered colimits of condensed sets

Stream: condensed mathematics

[Adam Topaz]

I've been working on proving that filtered colimits of condensed sets can be computed by taking colimits pointwise (i.e. no sheafification required) in the file condensed/filtered_colimits.lean. This file now has 10 sorry's, which are essentially about checking that some diagrams commute (all sorry's are props).

[Adam Topaz]

These sorrys all lead to the following theorem

lemma is_sheaf_colimit_presheaf :
  presheaf.is_sheaf proetale_topology (colimit (F ⋙ Sheaf_to_presheaf _ _)) :=

[Adam Topaz]

And finally it all culminates in

@[simps]
noncomputable
def filtered_cocone : cocone F :=
{ X := ⟨colimit (F ⋙ Sheaf_to_presheaf _ _), is_sheaf_colimit_presheaf _⟩,
  ι :=
  { app := λ j, Sheaf.hom.mk $ colimit.ι (F ⋙ Sheaf_to_presheaf _ _) j,
    naturality' := ... } }

noncomputable
def filtered_cocone_is_colimit : is_colimit (filtered_cocone F) :=
{ desc := λ S, Sheaf.hom.mk $ colimit.desc (F ⋙ Sheaf_to_presheaf _ _)
    ((Sheaf_to_presheaf _ _).map_cocone S),
  fac' := ...,
  uniq' := ... }

[Adam Topaz]

Any help with the sorrys in this fiile would be much appreciated!

[Adam Topaz]

There are now a few additional sorties at the bottom of condensed/ab.lean.

[Kevin Buzzard]

I tried looking at the first one on the commute home and its statement was over a page long! I figured out what the statement of the lemma itself said but then realised I'd just missed my stop :-)

[Johan Commelin]

Oops, your Lean addiction is starting to derail your life in serious ways :rofl:

[Adam Topaz]

condensed/filtered_colimits.lean is sorry-free.
As a bonus, we now also have the following sorry-free

instance Condensed_Ab_to_CondensedSet_preserves_limits_of_shape_of_filtered :
  preserves_colimits_of_shape J Condensed_Ab_to_CondensedSet.{u} :=

(the forgetful functor from condensed abelian groups to condensed sets preserves filtered colimits)

[Kevin Buzzard]

This is so cool that we can do this stuff. This sort of thing is a real stress test for the category theory library. And the final theorem about the ext groups will be a stress test for the homological algebra library.

[Kevin Buzzard]

We see filtered colimits in this work -- do cofiltered limits ever show up naturally?

[Adam Topaz]

See the bottom of condensed/ab :)

[Adam Topaz]

They're in some sense the main type of colimit we consider: It's a colimit of condensed sets inddexed by $\mathbb{R}_{\geq 0}$.

[Adam Topaz]

Oops, I misrread your cofiltered limits as filtered colimits.

[Adam Topaz]

For all limits, we already know that the forgetful functor to condensed sets preserves those by general nonsense (since it's a right adjoint)

[Johan Commelin]

Cool! Another todo that can be ticked off!

[Adam Topaz]

Kevin Buzzard said:

This is so cool that we can do this stuff. This sort of thing is a real stress test for the category theory library. And the final theorem about the ext groups will be a stress test for the homological algebra library.

I must say that this was not as smooth as I would have liked.
Most of the proofs here involved using the fact that some functor preserves colimits, but the diagrams were essentially alwasy (d)simplified, so rewriting with is_colimit.fac or whatever almost never worked. I had to manually do

have := (is_colimit_of_preserves foo bar).fac _ baz,
dsimp at this, slice_lhs m n { rw this }, clear this

about 37 times.
It's not that bad, but I wish the automation could somehow do this for us.