Inductive limits

Stream: maths

[Sebastien Gouezel]

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!

[Reid Barton]

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.

[Sebastien Gouezel]

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? :)

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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

[Johan Commelin]

inductive limits are special cases of colimits

[Reid Barton]

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

[Reid Barton]

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?

[Sebastien Gouezel]

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)