Zulip Chat Archive

Stream: maths

Topic: Inductive limits


view this post on Zulip Sebastien Gouezel (Feb 05 2019 at 15:07):

What is the current status of inductive limits with respect to mathlib? I have a sequence of isometric embeddings i n : C n -> C (n+1) for n : nat, and I want to get the inductive limit as a metric space in which all C n embed isometrically. I can definitely do it by hand, but if the direct limit in Set is already there it might be fun to try to use it. And if mathlib is ready for a categoric framework with metric spaces as objects and isometric embeddings as maps, why not!

view this post on Zulip Reid Barton (Feb 05 2019 at 15:10):

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/limits/types.lean#L49 has the colimit of a general diagram of types. You can specialize the index category to nat (which is a poset, and therefore automatically a category).
I also have the more specific description of the equivalence relation on a filtered colimit of types in a form which is more or less ready to PR.

view this post on Zulip Sebastien Gouezel (Feb 05 2019 at 15:12):

Do you know the joke that, when you ask a question to a category theorist and you listen to his answer, then after that you don't understand your own question any more? :)

view this post on Zulip Sebastien Gouezel (Feb 05 2019 at 15:14):

To be honest, I don't know what a cocone is, or a colimit, but I would very much like to see how the general framework works in a super-concrete setting just like the one I asked, on Set.

view this post on Zulip Sebastien Gouezel (Feb 05 2019 at 15:16):

Btw, for what I am asking #PR585 by Kenny would be very useful.

view this post on Zulip Johan Commelin (Feb 05 2019 at 15:28):

inductive limits are special cases of colimits

view this post on Zulip Reid Barton (Feb 05 2019 at 15:45):

And a cocone is the thing that shows up in the statement of the universal property: another object together with compatible maps from all the objects in the diagram (the C n).

view this post on Zulip Reid Barton (Feb 05 2019 at 15:49):

Is the statement you need just that there exists a metric space in which all the C n embed isometrically and compatibly with the give maps i n?

view this post on Zulip Sebastien Gouezel (Feb 05 2019 at 18:02):

Is the statement you need just that there exists a metric space in which all the C n embed isometrically and compatibly with the give maps i n?

Yes, exactly. Note that the category of metric spaces and isometric embeddings is not really well behaved, for instance if you have two embeddings FY : X -> Y and FZ : X -> Z, then there are several non-isometric ways to complete the square, but there is a maximal one, so universal properties would be expressed in terms of 1-Lipschitz maps instead of isometries.
But for limits along nat everything is fine (as the embeddings are injection, it is just an increasing sequence of spaces, and you take the union)


Last updated: May 06 2021 at 18:20 UTC