Forgetful functor from Group to Set

Stream: new members

[Jordan Brown]

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]

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

[Kenny Lau]

G itself is the "underlying set"

[Kenny Lau]

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

[Kenny Lau]

first thing first, "set" means type

[Adam Topaz]

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]

don't actually type out the arrow

[Kenny Lau]

use type ascription instead

[Kenny Lau]

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

[Adam Topaz]

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]

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

[Scott Morrison]

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