Zulip Chat Archive

Stream: maths

Topic: filtered colimits

Reid Barton (Dec 21 2018 at 20:13):

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

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

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).

Kevin Buzzard (Dec 21 2018 at 22:11):

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

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.

Kevin Buzzard (Dec 21 2018 at 22:13):

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

Last updated: Dec 20 2023 at 11:08 UTC