descending universes

Stream: general

[Kevin Buzzard]

My universe issue with perfectoid spaces has become: if I have X : Type u and (Y : Type v) [group Y] and an injection f : X -> Y then I want a group G : Type u and an injection i:X -> G and an injective group homomorphism j:G -> Y with ji=f. Morally I want G to be "the subgroup of Y generated by the image of f, except in universe u". How does one construct that sort of thing? I've never worried about this sort of question before.

[Kevin Buzzard]

I guess that WLOG Y is generated, as a group, by the image of f, and then j would be a bijection -- but I don't know if this helps.

[Reid Barton]

Well, in this case, you can take the free group on X modulo whatever relations are true after applying f.

[Kevin Buzzard]

Oh that'll do for me. Are free groups in Lean?

[Kevin Buzzard]

Actually everything is abelian

[Kevin Buzzard]

but making a free group as a subset of maps from X to the integers, for example -- would that bump up the universe level by 1?

[Reid Barton]

No, only quantifying over types (belong to the same universe as X) would do that.

[Kevin Buzzard]

yes you're right. Thanks Reid -- this is perfect!

[Johan Commelin]

Kevin, so you could use finsupp for the free groups. The would be additive, so you need to extract a multiplicative group out of it afterwards...

[Patrick Massot]

https://github.com/leanprover/mathlib/blob/master/group_theory/free_group.lean

[Johan Commelin]

But that's non-abelian...

[Patrick Massot]

indeed