How are groups (as in group theory) usually represented in Coq?

Saw a way like

```
Structure my_group := My_Group {
(* domain *)
dom: Type;
(* symbols: constants and operators *)
e: dom; (* Identity element *)
inv: dom -> dom; (* Inverse element *)
op: dom -> dom -> dom; (* Operation *)
(* axioms: properties on the symbols *)
opE: forall x:dom, op x e = x;
opInv: forall x, op x (inv x) = e;
opComm: forall x y:dom, op x y = op y x;
opAssoc: forall x y z:dom, op (op x y) z = op x (op y z);
}.
```

Is it how it's usually done?

I suppose mathcomp would have more stuff related to groups?

Mathcomp has a lot of results about finite groups. They key choice is to have a groupType, not unlike yours, and then (finite) sets inside this type which are groups and are the main object of your theorems. These "sub groups" share the operation, because of the common group type, so intersecting them makes sense. You move to another groupType when that changes, eg when you quotient.

There is a stream dedicated to math comp, if you want to know more, that would be the right place.

I don't know much about group theory actually. Was trying to learn its basics. Been reading a book, but thought it would be more exciting to actually try out the stuff in coq.

Does anyone know of a 'learn group theory with coq' tutorial or something along those lines?

There's https://github.com/UniMath/SymmetryBook which uses informal homotopy type theory

If you use this representation, you'll eventually have to axiomatise quotienting of `Type`

s and function extensionality. This is probably the best way to go (as opposed to setoids) if your aim is to learn group theory.

Last updated: Jan 28 2023 at 05:02 UTC