Zulip Chat Archive

Stream: new members

Topic: Forgetful functor from Group to Set


view this post on Zulip Jordan Brown (Aug 01 2020 at 23:31):

Is there an easy way to extract the underlying set from a group? I have looked at the mathlib source code defining the group structure, but it is not clear to me how to extract the base set.

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:32):

the mathematical statement "G is a group" translates to (G : Type*) [group G] in Lean

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:32):

G itself is the "underlying set"

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:33):

group G means "we have a group structure on G"

view this post on Zulip Kenny Lau (Aug 01 2020 at 23:33):

first thing first, "set" means type

view this post on Zulip Adam Topaz (Aug 02 2020 at 00:25):

If you want the functorial part too, i.e. the function underlying a morphism of groups, you can use \u= f (a coercion to function) where f is the morphism

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:25):

don't actually type out the arrow

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:25):

use type ascription instead

view this post on Zulip Kenny Lau (Aug 02 2020 at 00:26):

i.e. (f : G \to H)

view this post on Zulip Adam Topaz (Aug 02 2020 at 00:33):

I agree with Kenny, but sometimes it's faster to type something like \lam f, \u= f instead of the full type ascription. Anyway, it's good to be familiar with both.

view this post on Zulip Yury G. Kudryashov (Aug 04 2020 at 06:49):

There are bundled groups in mathlib, see docs#Group but they are not widely used.

view this post on Zulip Scott Morrison (Aug 04 2020 at 07:15):

If you do use them, then you just want forget Group, which is a functor from Group to Type.


Last updated: May 12 2021 at 23:13 UTC