Zulip Chat Archive

Stream: general

Topic: descending universes


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 17:38):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 17:39):

Actually everything is abelian

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jul 19 2018 at 17:41):

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

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 17:41):

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

view this post on Zulip 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...

view this post on Zulip Patrick Massot (Jul 19 2018 at 18:22):

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

view this post on Zulip Johan Commelin (Jul 19 2018 at 18:33):

But that's non-abelian...

view this post on Zulip Patrick Massot (Jul 19 2018 at 18:33):

indeed


Last updated: May 12 2021 at 04:19 UTC