## Stream: new members

### Topic: Forgetful functor from Group to Set

#### 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.

#### Kenny Lau (Aug 01 2020 at 23:32):

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

#### Kenny Lau (Aug 01 2020 at 23:32):

G itself is the "underlying set"

#### Kenny Lau (Aug 01 2020 at 23:33):

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

#### Kenny Lau (Aug 01 2020 at 23:33):

first thing first, "set" means type

#### 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

#### Kenny Lau (Aug 02 2020 at 00:25):

don't actually type out the arrow

#### Kenny Lau (Aug 02 2020 at 00:26):

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

#### 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.

#### Yury G. Kudryashov (Aug 04 2020 at 06:49):

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

#### 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