Zulip Chat Archive

Stream: maths

Topic: filtered colimits


view this post on Zulip Reid Barton (Dec 21 2018 at 20:13):

Has anyone been working with filtered colimits? Perhaps @Ramon Fernandez Mir @Kevin Buzzard?

view this post on Zulip Reid Barton (Dec 21 2018 at 20:14):

In particular, I need the formula for a filtered colimit of sets shown at https://stacks.math.columbia.edu/tag/04AX before Lemma 4.19.2 and perhaps someone has already done this

view this post on Zulip Kevin Buzzard (Dec 21 2018 at 21:58):

We (and @Kenny Lau ) recently did arbitrary colimits via some tensor product construction. I think Kenny took filtered colimits of commutative rings at some point because even though I tried my hardest to avoid it, I think I ultimately needed them when defining the structure sheaf on Spec(A) (the issue is extending the sheaf from basic opens to an arbitrary open).

view this post on Zulip Kevin Buzzard (Dec 21 2018 at 22:11):

https://github.com/leanprover/mathlib/pull/118

view this post on Zulip Kevin Buzzard (Dec 21 2018 at 22:13):

Minor discussion on 17th May about directed systems around line 25. Note that this PR got closed.

view this post on Zulip Kevin Buzzard (Dec 21 2018 at 22:13):

Kenny -- will this PR be resurrected one day? I need it for schemes.


Last updated: May 11 2021 at 16:22 UTC