Zulip Chat Archive

Stream: condensed mathematics

Topic: Filtered colimits commute with finite limits


Adam Topaz (Jul 07 2022 at 19:09):

We need the fact that filtered limits commute with finite limits in condensed sets.
I added a skeleton for this in condensed/filtered_limits_commute_with... with the following main sorry:

lemma is_iso_colim_to_lim_component (S : Profinite.{u}ᵒᵖ) :
  is_iso ((colim_to_lim F).val.app S) :=
begin
  /-
  The forgetful functor to presheaves preserves filtered colimits and all limits,
  while the same holds for evaluation, hence this morphism should be isomoprhic to
  `colimit_limit_to_limit_colimit` which is an isomorphism.
  -/
  sorry
end

The proof should use the fact that evaluation of a condensed set at any profinite set preserves filtered colimits and all limits to reduce the issue to the usual claim that filtered colimits commute with finite limits in the category of sets.

The main place we need this iis in showing that the functor XXnX \mapsto X^n (with nn finite) preserves filtered colimits, and the relevant sorry is located in the file condensed/bd_ses:

instance pow_functor_preserves_filtered_colimits (n : ) :
  preserves_filtered_colimits
  (pow_functor CondensedSet.{u} (ulift.{u+1} (fin n))) := sorry

Any help would be much appreciated here!

Adam Topaz (Jul 07 2022 at 20:09):

(the sorries have been moved to condensed/filtered_limits_commute_with...)

Johan Commelin (Jul 08 2022 at 03:05):

I tried to look at the first one. There seems to be bit of general API missing about preserving limits in a functorial manner.

Johan Commelin (Jul 08 2022 at 08:44):

I've made some progress here

Johan Commelin (Jul 08 2022 at 08:44):

I'll push in a moment.

Johan Commelin (Jul 08 2022 at 11:53):

This sorry is now closed

Adam Topaz (Jul 08 2022 at 13:01):

Nice!

Adam Topaz (Jul 08 2022 at 13:07):

Are you also working on the remaining sorries in that file?

Johan Commelin (Jul 08 2022 at 13:12):

No, I switched to Qprime_isoms2

Johan Commelin (Jul 08 2022 at 13:12):

Note that there is only 1 sorry left in your file. About powers preserving filtered colimits.

Adam Topaz (Jul 08 2022 at 13:13):

right

Adam Topaz (Jul 08 2022 at 13:13):

the last SES I built yesterday involved this

Adam Topaz (Jul 08 2022 at 14:10):

Okay, this file is now sorry-free.

Johan Commelin (Jul 08 2022 at 22:24):

Great! What's left for the Q' SES?

Adam Topaz (Jul 08 2022 at 22:28):

Glue!

Johan Commelin (Jul 08 2022 at 22:59):

Great! Can you state the glue? Then I can try to kill the sorries.

Adam Topaz (Jul 08 2022 at 23:04):

I probably won't t have time this weekend, but I'll give it a go on Monday


Last updated: Dec 20 2023 at 11:08 UTC