Formalization of Specific Groups

Stream: mathlib4

[AlumKal]

In mathlib, Klein four-group and dihedral groups are formalized in different ways:

class IsKleinFour (G : Type*) [Group G] : Prop where
  card_four : Nat.card G = 4
  exponent_two : Monoid.exponent G = 2

inductive DihedralGroup (n : ℕ) : Type
  | r : ZMod n → DihedralGroup n
  | sr : ZMod n → DihedralGroup n
  deriving DecidableEq

As a beginner in Lean, I wonder what are the pros and cons of these two types of definition.

[Kevin Buzzard]

Those are different things. One is a predicate (the one that begins with Is); it eats a group and produces the true-false statement "I am isomorphic to the Klein 4 group". The other is a definition; it says "you want an example of a dihedral group, i.e. a concrete group? Here it is". Throughout the algebra part of mathlib there are examples of mathematical concepts (localization, tensor product, algebraic closure) where we have both ideas (the predicate and the definition) implemented in Lean. For example if I have fields $K\subseteq L$ then we have the predicate docs#IsAlgClosure ; IsAlgClosure K L says "the given field $L$ is an algebraic closure of $K$". But if you only have $K$ and want to invoke the theorem that every field has an algebraic closure then you can use docs#AlgebraicClosure -- AlgebraicClosure K is an explicit algebraic closure of K.

The analogue in group theory would be: when you say "the symmetric group" do you mean "the actual permutations of ${1,2,\ldots,n}$" or do you mean "any old group which is isomorphic to a symmetric group". Formalised mathematics has to distinguish between these two concepts, but it needs them both.

[Kevin Buzzard]

The exercise you could do in Lean is to prove that the concrete definition satisfies the predicate, like this:

import Mathlib

example : IsKleinFour (DihedralGroup 2) := by
  constructor
  · sorry
  · sorry