Exact functors

Stream: condensed mathematics

[Adam Topaz]

Did we ever decide (in LTE and/or mathlib) how to talk about exact functors?

[Johan Commelin]

Not really. I think the idea was to say that they preserve finite (co)limits.

[Johan Commelin]

But it hasn't been connected to exact.

[Riccardo Brasca]

We have docs#category_theory.abelian.functor.preserves_exact_of_preserves_finite_colimits_of_epi and the dual docs#category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono

[Adam Topaz]

Nice, okay that should do it.

[Johan Commelin]

@Riccardo Brasca Ooh, yes of course. Why did I forget about those!? Thanks for the pointers.

[Adam Topaz]

I started an AB4.lean file which seems to be needed:
https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/ab4.lean

[Adam Topaz]

We'll probably need to show that coproduct_functor is exact given AB4.

[Johan Commelin]

Is this a missing piece for showing that Ext sends coproducts to products?

[Adam Topaz]

Yeah

[Adam Topaz]

This is what's needed to show that homology commutes with coproducts.

[Adam Topaz]

(it's not true in general!)

[Adam Topaz]

https://mathoverflow.net/a/146941

[Johan Commelin]

Ok, and so we need to show that Ab satisfies AB4

[Johan Commelin]

But we don't need it for Cond(Ab), if I understand it correctly.

[Adam Topaz]

No, I think we do need it for Cond(Ab).

[Adam Topaz]

Aren't we dealing with complexes of condensed abelian groups?

[Johan Commelin]

But to compute Ext^n(foo, bar) you only take homology of a complex of abelian groups, right?

[Adam Topaz]

Oh, I should have specified -- we need this to show that a coproduct of quasi-isos is a quasi-iso.

[Adam Topaz]

Is that true without AB4?

[Adam Topaz]

Here is the target lemma:
https://github.com/leanprover-community/lean-liquid/blob/ba6f0cadbe3a895dcbaf5a70e0b1c18a42c05ea6/src/for_mathlib/derived/ext_coproducts.lean#L239

[Adam Topaz]

(is GH down?)

[Johan Commelin]

I see. I agree that AB4 certainly helps. I don't know if it is strictly necessary, but I guess it is.

[Filippo A. E. Nuccio]

In Tohoku Grothendieck works with sheaves on Top, but there he observes that sheaves in abelian groups satisfy AB5, hence AB4. Is this not enough to deduce AB4 for Cond Ab?

[Adam Topaz]

Oh, AB4 for Cond Ab should be pretty easy to prove.

[Adam Topaz]

That's not the issue, rather the issue is whether we need to prove it :)

[Filippo A. E. Nuccio]

Ah ok, I see. It sounded strange that it might not be true...

[Kevin Buzzard]

Essentially every abelian category "extra axiom" is true for Cond Ab!

[Adam Topaz]

And even better they all follow from
https://github.com/leanprover-community/lean-liquid/blob/d3188794d3b2232ff7c68c3b5e83ef2cef10d58c/src/condensed/extr/equivalence.lean#L371

[Kevin Buzzard]

For an arbitrary category C (with finite products or whatever one needs for sheaves), one can consider C-valued sheaves on extremely disconnected sets or profinite sets or compact Hausdorff sets, with the topologies we use on these categories. Are these things all the same in this generality?

[Peter Scholze]

Only if C has all limits

[Peter Scholze]

I think in general C-sheaves on CHaus are a full subcategory of C-sheaves on ProFin are a full subcategory of C-sheaves on ExtrDisc, and the essential images are given by those sheaves where the limit that wants to define the value on some compact Hausdorff (resp. profinite) actually exists in C.

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/e948977da669ce56998eaa819ed5c402c0fb7002/src/condensed/ab4.lean#L178

[Kevin Buzzard]

Good old AB4_of_preserves_colimits_of_reflects_limits_of_AB4

[Adam Topaz]

What's the stacks tag for that lemma? ;)

[Kevin Buzzard]

I wonder if the Stacks proof contains lines such as swap, { rintro i _ ⟨⟨⟨⟩⟩⟩, dsimp, simp, dsimp, simp },

[Kevin Buzzard]

This really is all about knowing the correct abstractions in category theory isn't it. Very well done.