Universal Property of Z[p] as a Group

Stream: mathlib4

[Qi Ge]

Hi all, docs#PadicInt.lift implemented the universal property of Z[p] as a ring but I need the result for groups. Is there an easy way to go about this?

[Qi Ge]

Never mind! I just checked the code and PadicInt.lift is very modular. Getting a makeshift lift should be easy!

[Adam Topaz]

The functor from the category of commutative rings to the category of abelian groups preserves limits. I’m quite sure we have that in one way or another in the category theory library. So if you can state the assertion the the p-adic ints are a certain limit in the category of commutative rings, using the categorical machinery, then you could use this categorical result to get what you want.

[Qi Ge]

Adam Topaz said:

The functor from the category of commutative rings to the category of abelian groups preserves limits. I’m quite sure we have that in one way or another in the category theory library. So if you can state the assertion the the p-adic ints are a certain limit in the category of commutative rings, using the categorical machinery, then you could use this categorical result to get what you want.

I'm worried it can be complicated to get from type theory statement to category theory and then getting back... Is something like this done somewhere I can can reference?

[Adam Topaz]

Let’s do it when we meet tomorrow :)