# Zulip Chat Archive

## Stream: maths

### Topic: Inductive limits

#### 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!

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

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

#### 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`

.

#### Sebastien Gouezel (Feb 05 2019 at 15:16):

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

#### Johan Commelin (Feb 05 2019 at 15:28):

inductive limits are special cases of colimits

#### 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`

).

#### 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`

?

#### 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