Stream: maths

Topic: direct limits and bundled homs

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?

Yury G. Kudryashov (Apr 08 2020 at 03:36):

Should I reuse some definitions from category_theory/?

Yury G. Kudryashov (Apr 08 2020 at 03:55):

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

Scott Morrison (Apr 08 2020 at 07:24):

So... this stuff is already pretty duplicated.

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.

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