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 $X \mapsto X^n$ (with $n$ 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