colimits commute with colimits

Stream: condensed mathematics

[Johan Commelin]

Do we actually know that colimits commute with colimits? I need to show that A → A^{⊕n} commutes with filtered colimits, and would like this to be automatic.

[Adam Topaz]

The limit version is in category_theory/limit/fubini. Looks like we don't have the colimit version.

[Adam Topaz]

But since you're using biproducts, it might be easier to do a one-off construction.

[Adam Topaz]

I can write something up real quick.

[Johan Commelin]

@Adam Topaz I've done that part...

[Johan Commelin]

But github didn't let me push it

[Adam Topaz]

Oh ok.

[Johan Commelin]

Now it worked!

[Adam Topaz]

Is GH down?

[Johan Commelin]

Half an hour ago I got errors

[Johan Commelin]

So I first went for a run

[Johan Commelin]

bors still seems to be down...

[Johan Commelin]

instance eval_functor_preserves_filtered_colimits (BD : data) [preserves_filtered_colimits F] :
  preserves_filtered_colimits ((eval_functor F).obj BD) :=
{ preserves_filtered_colimits := by introsI; apply_instance }

This shows that the Q'-construction preserves filtered colimits.

• It is currently parameterised by a functor F. This should be specialized to ℤ[_] later on. We still need to show that ℤ[_] preserves filtered colimits.
• For https://leanprover-community.github.io/liquid/sect0009.html#homology-Qprime we will also need to show that homology commutes with filtered colimits. That's the missing piece to tick off that box.

[Johan Commelin]

@Andrew Yang That second • should be well within the reach of your mathematical toolkit.

[Johan Commelin]

[And once again, I can't push to github :sad:]

[Johan Commelin]

Mirabile dictu, I managed to push a minute ago!

[Andrew Yang]

Great! will start looking at them tomorrow

[Adam Topaz]

$\mathbb{Z}[-]$ is by definition a left adjoint, so it preserves all colimits for free! (unless you're talking about a different functor?)

[Adam Topaz]

I guess what we're actually missing is the fact that the functor from PFPNG to Condensed Set can be computed as the colimit of the condensed sets associated to the profinite levels of the given PFPNG.

[Johan Commelin]

@Adam Topaz We mostly need to decide which implementation we use. Maybe we need multiple isomorphic versions of ℤ[_].

[Adam Topaz]

Do we have the CHPNG version of $\mathbb{Z}[-]$ yet?

[Johan Commelin]

I think @Damiano Testa made a start on it.

[Johan Commelin]

Or actually, he's defining ℤ[T⁻¹][S], I think. (For finite S.)

[Damiano Testa]

What I have is mostly contained in Lbar.finsupp_instance and src/Lbar/kernel_truncate.lean.

The first file shows that S-indexed polynomials (in x^1, but viewed as polynomials in x) are a pseudo_normed_group.

The second file is a beginning of showing that the kernel of the truncation map from Laurent measures to Lbar actually gives rise to S-indexed polynomials.

[Damiano Testa]

And S is a Fintype.

[Damiano Testa]

(The S-indexed polynomials are really the tails of the Laurent series.)

[Adam Topaz]

I started on the definition of $\mathbb{Z}[S]$ in terms of profinitely filtered pseudo normed groups in the folder free_pfpng.
The file free_pfpng/basic has a few very simple sorry's that I don't have time to finish off right now.

[Adam Topaz]

I've added the following stub for Prop 2.1 of analytic.pdf in free_pfpng/main:

/-- Prop 2.1 of Analytic.pdf -/
def free_pfpng_profinite_iso :
  free_pfpng_profinite ⋙
  ProFiltPseuNormGrp₁.enlarging_functor ⋙
  ProFiltPseuNormGrp.to_CompHausFilt ⋙
  CompHausFiltPseuNormGrp.to_Condensed ≅
  Profinite_to_Condensed ⋙ CondensedSet_to_Condensed_Ab := sorry

[Johan Commelin]

Thanks for attacking this

[Johan Commelin]

Should we have

def ProFiltPseuNormGrp₁.to_Condensed :=
  ProFiltPseuNormGrp₁.enlarging_functor ⋙
  ProFiltPseuNormGrp.to_CompHausFilt ⋙
  CompHausFiltPseuNormGrp.to_Condensed

[Adam Topaz]

Sure. Maybe as an abbreviation?

[Johan Commelin]

Adam Topaz said:

$\mathbb{Z}[-]$ is by definition a left adjoint, so it preserves all colimits for free! (unless you're talking about a different functor?)

We actually need ℤ[-] as functor Condensed Ab ⥤ Condensed Ab. So you have to compose with forget. So I guess you really need to consider filtered colimits, right?