## Stream: general

### Topic: descending universes

#### Kevin Buzzard (Jul 19 2018 at 17:32):

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 (Jul 19 2018 at 17:34):

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 (Jul 19 2018 at 17:36):

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

#### Kevin Buzzard (Jul 19 2018 at 17:38):

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

#### Kevin Buzzard (Jul 19 2018 at 17:39):

Actually everything is abelian

#### Kevin Buzzard (Jul 19 2018 at 17:39):

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 (Jul 19 2018 at 17:41):

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

#### Kevin Buzzard (Jul 19 2018 at 17:41):

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

#### Johan Commelin (Jul 19 2018 at 18:12):

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 (Jul 19 2018 at 18:22):

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

#### Johan Commelin (Jul 19 2018 at 18:33):

But that's non-abelian...

#### Patrick Massot (Jul 19 2018 at 18:33):

indeed

Last updated: May 12 2021 at 04:19 UTC