Zulip Chat Archive

Stream: maths

Topic: direct limits and bundled homs


view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 03:35):

I'd like to rewrite algebra/direct_limit using bundled homs. Is there somebody already working on it?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 03:36):

Should I reuse some definitions from category_theory/?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 03:55):

For me this is a part of the quest "get rid of is_ring_hom"

view this post on Zulip Scott Morrison (Apr 08 2020 at 07:24):

So... this stuff is already pretty duplicated.

view this post on Zulip Scott Morrison (Apr 08 2020 at 07:24):

I've never stopped to look very hard, but you might look at the algebra/category/*/limits.lean and algebra/category/*/colimits.lean files.

view this post on Zulip Scott Morrison (Apr 08 2020 at 07:25):

What is missing the categorical setup is anything about filtered limits


Last updated: May 18 2021 at 06:15 UTC