Lean define groups

Question

This is a follow-up question of Lean pass type as parameter

I tried jmc's suggestion, which seemed to work, but then I got stuck at another point. The original purpose of the question was to define the categories of groups and rings, but now apparently I am unable to define group morphisms:

class group :=
(set: Type)
(add: set → set → set)

infix + := group.add

class group_morphism (G H: group) :=
(f: G.set → H.set)
(additive: ∀ g h : G.set, f(g + h) = (f g) + (f h))

I get an error at the first +. Lean seems to think that this refers to H.add, whereas it is supposed to refer to G.add.

Answer 1

The issue is that group should not be a class. If you look at the type of group.add, by #check @group.addyou will get

group.add : Π [c : group], group.set → group.set → group.set

The square brackets around c : group indicate that this is an implicit argument that will be inferred by type class inference. You won't have to explicitly type this argument, but Lean will try to work out what it is. Type class inference works best for types where there is only one inhabitant you ever want to use.

In mathlib the definition of group is closer to

class group (set : Type) :=
(add : set → set → set)

On a particular type, there is usually only one group structure you want to refer to, so in mathlib, a type like add_group int has only one inhabitant you care about.

Lean automatically chose H as the canonical representative of the type group, but this is not the one you wanted.

So usually when you deal with groups the type and the group structure are kept as separate objects, they are not put into a pair. However for category theory, the usual approach doesn't work, an object is a pair of a type and a group structure.

The setup in mathlib is closer to the following. The coe_to_sort tells Lean how to take a group_obj and interpret it as a Type without having explicitly write G.set, the group_obj_group instance tells Lean how to automatically infer the group structure on the type of a group_obj

class group (set : Type) :=
(add: set → set → set)

structure group_obj :=
(set : Type)
(group : group set)

instance coe_to_sort : has_coe_to_sort group_obj :=
{ S := Type, 
  coe := group_obj.set }

instance group_obj_group (G : group_obj) : group G := G.group

infix `+` := group.add

structure group_morphism (G H : group_obj) :=
(f: G → H)
(additive: ∀ g h : G.set, f(g + h) = (f g) + (f h))

Answer 2

You are redefining the + notation which will very quickly lead to headaches. Have a polymorphic + notation is very helpful. (How will you denote the addition in a ring?)

Further points:

• you should use structure instead of class
• mathematically, you are defining monoids and monoid homs, not groups and group homs

This works though

(set: Type)
(add: set → set → set)

def add {G : group} := group.add G

class group_morphism (G H: group) :=
(f: G.set → H.set)
(additive: ∀ g h : G.set, f(add g h) = add (f g) (f h))