Explicit definition of tiny groups

Stream: Is there code for X?

[Jihoon Hyun]

Is there an explicit definitoin of non-trivial tiny groups, for example with cardinality 2, 3, 4, and possibly 5, 6, 7, and 8?

[Kenny Lau]

Jihoon Hyun said:

Is there an explicit definitoin of non-trivial tiny groups, for example with cardinality 2, 3, 4, and possibly 5, 6, 7, and 8?

QuaternionGroup, DihedralGroup

Personally I think it would be interesting to see a classification of groups of order <= 10 in mathlib! But i don't know if everyone else agrees.

[Kenny Lau]

Since we already have Sylow theory maybe it's even doable up to 60 (the first simple group)!

[Jihoon Hyun]

Kenny Lau said:

Since we already have Sylow theory maybe it's even doable up to 60 (the first simple group)!

That's probably too much for mathlib. I was just wondering if there is a definition of tiny groups, so that every element is explicit and anyone using it doesn't have to care about how it's constructed, for example the dihedral structure.

[Kenny Lau]

Jihoon Hyun said:

Kenny Lau said:

Since we already have Sylow theory maybe it's even doable up to 60 (the first simple group)!

That's probably too much for mathlib. I was just wondering if there is a definition of tiny groups, so that every element is explicit and anyone using it doesn't have to care about how it's constructed, for example the dihedral structure.

Yes, they're called r 0, r 1, r 2, sr 0, sr 1, sr 2.

[Michael Rothgang]

Kenny Lau said:

Jihoon Hyun said:

Is there an explicit definitoin of non-trivial tiny groups, for example with cardinality 2, 3, 4, and possibly 5, 6, 7, and 8?

QuaternionGroup, DihedralGroup

Personally I think it would be interesting to see a classification of groups of order <= 10 in mathlib! But i don't know if everyone else agrees.

FWIW, I would agree

[Kenny Lau]

Personally I don't see the point of just making abbreviations for small groups

[Jihoon Hyun]

Kenny Lau said:

Personally I don't see the point of just making abbreviations for small groups

Even for groups of order 2, there are $\mathbb{Z}_2$, $\mathbb{Z}^{\times}$, $\mathbb{Z}_{3}^{\times}$, and possibly more. All have different use cases, so why not have a classification of small groups and then give a single isomorphism to them, instead of making a small graph of isomorphisms?

[Yaël Dillies]

... but which isomorphism? :-)

[Jihoon Hyun]

Yaël Dillies said:

... but which isomorphism? :-)

The one from the group we have to the central group. By doing so we can make a group isomorphism from one group to the other by composing at most two isomorphism, while if not we might need to use more than that.

[Yaël Dillies]

What I mean to point out is that almost every group has non-trivial automorphisms. Therefore there isn't just "a single isomorphism" to the "central group". Eg $x \mapsto x^{-1} : C_3 \to C_3$ is a non-trivial automorphism, and therefore if you have some other group $G$ that's isomorphic to $C_3$ then it's not obvious which of the (two) isomorphisms $G \cong C_3$ you should be writing down.

[Jihoon Hyun]

Thanks for the clarification. It seems like small groups are already classified outside mathlib, so maybe I'll wait for that to be imported to mathlib.

[Kenny Lau]

Jihoon Hyun said:

Kenny Lau said:

Personally I don't see the point of just making abbreviations for small groups

Even for groups of order 2, there are $\mathbb{Z}_2$, $\mathbb{Z}^{\times}$, $\mathbb{Z}_{3}^{\times}$, and possibly more. All have different use cases, so why not have a classification of small groups and then give a single isomorphism to them, instead of making a small graph of isomorphisms?

I think there are some misunderstandings here. We might be thinking about things from different perspectives. What you think mathematically about classifying small groups might not be the same as what I'm thinking.

I don't want abbreviations, and I'm claiming that I can make the classification work without using abbreviations, I'll just choose the standard group called Multiplicative (ZMod 2) (actually this highlights another problem, which is "mathematically trivial": we currently have groups with multiplication, and add groups with addition!).

And my theorem will just look like, for all group G with Fintype G and Fintype.card G = 2, Nonempty (G isomorphism with Multiplicative (ZMod 2))

my point here is that we don't need to "unify the names", which is what you're proposing by providing a "central name".

[Kenny Lau]

Jihoon Hyun said:

Thanks for the clarification. It seems like small groups are already classified outside mathlib, so maybe I'll wait for that to be imported to mathlib.

do you have a link? it would also be helpful (to us both) to see how they translate it to lean

[Floris van Doorn]

A student of mine did a project where she classified the groups of order 8: https://github.com/lucia3125/LeanCourse23/tree/master/LeanCourse/Project

[Floris van Doorn]

(main result)

[Kenny Lau]

Nice. As expected, it's fine to just work with the names we currently have.

[Eric Wieser]

Instead of

        Nonempty (G ≃* Multiplicative (ZMod 8))
    ∨ Nonempty (G ≃* Multiplicative (ZMod 4) × Multiplicative (ZMod 2))
    ∨ Nonempty (G ≃* Multiplicative (ZMod 2) × Multiplicative (ZMod 2) × Multiplicative (ZMod 2))
    ∨ Nonempty (G ≃* DihedralGroup 4)
    ∨ Nonempty (G ≃* QuaternionGroup 2)

does it makes sense to have something like

import Mathlib

abbrev groups := ![
  Multiplicative (ZMod 8),
  Multiplicative (ZMod 4) × Multiplicative (ZMod 2),
  Multiplicative (ZMod 2) × Multiplicative (ZMod 2) × Multiplicative (ZMod 2),
  DihedralGroup 4,
  QuaternionGroup 2]

instance : ∀ i, Group (groups i) := by
  refine Fin.cons ?_ <| Fin.cons ?_ <| Fin.cons ?_ <| Fin.cons ?_ <| Fin.cons ?_ <| (Fin.elim0 ·) <;>
    (dsimp [groups]; infer_instance)

theorem groups_inj : (∀ i j, groups i ≃* groups j → i = j) := sorry

lemma groups_order_eight {G : Type*}[Group G][Fintype G](hG: Fintype.card G = 8):
    ∃ i, Nonempty (G ≃* groups i) := sorry
  ```

[Eric Wieser]

Or should be be using category theory and a skeleton category for classification results?

[Kenny Lau]

What we should be doing is an auxiliary type Classified n with API for easy use

[Kenny Lau]

once you have the API I don't really care if you're using skeleton or any other formulation

[Kenny Lau]

(actually skeleton might be bad, one bad thing about category is that they're not universe polymorphic, sadly)

[Eric Wieser]

I think you're in universe trouble whatever you do

[Kenny Lau]

No, group isomorphism is universe polymorphic

[Eric Wieser]

Sure, but my groups above is not

[Eric Wieser]

Nor will any Classified type you produce be

[Eric Wieser]

Here's the skeleton API:

import Mathlib


instance classification : Fintype
    {G : CategoryTheory.Skeleton Grp.{0} | ∃ i : Fintype G, Fintype.card G = 8} =
    CategoryTheory.toSkeleton '' {
      Grp.of <| Multiplicative (ZMod 8),
      Grp.of <| Multiplicative (ZMod 4) × Multiplicative (ZMod 2),
      Grp.of <| Multiplicative (ZMod 2) × Multiplicative (ZMod 2) × Multiplicative (ZMod 2),
      Grp.of <| DihedralGroup 4,
      Grp.of <| QuaternionGroup 2
    } := sorry

[Kim Morrison]

Tiny groups live in Type 0, I promise. :-) (In fact, Type 0 is even big enough for the monster. :-)

[Eric Wieser]

At any rate, any kind of classification that can be written as a chain of Nonemptys can be lifted into some maximal universe (which indeed happens to be 0 here)

[Kenny Lau]

Eric Wieser said:

Nor will any Classified type you produce be

import Mathlib

universe u

/-- A classification of groups of order `n`. -/
class Classified (n : ℕ) : Type 1 where
  (number : ℕ)
  (groups : Fin number → Type) [group : ∀ i, Group (groups i)]
  (distinct (i j) : groups i ≃ groups j → i = j)
  (classifies (G : Type u) [Group G] [Fintype G] (hg : Fintype.card G = n) :
    ∃ i, Nonempty (G ≃* groups i))

[Eric Wieser]

Right, all your groups live in Type, so also not universe polymorphic

[Eric Wieser]

Oh, your point was that you want polymorphism in the input G, not within the classifications

[Kenny Lau]

yes

[Aaron Liu]

There're all finite, so you can just Shrink them if you need to

[Kenny Lau]

import Mathlib

universe u

/-- A classification of groups of order `n`. -/
class Classified (n : ℕ) : Type 1 where
  number : ℕ
  groups : Fin number → Type
  group : ∀ i, Group (groups i)
  distinct (i j) : groups i ≃ groups j → i = j
  classifies (G : Type u) [Group G] [Fintype G] (hg : Fintype.card G = n) :
    ∃ i, Nonempty (G ≃* groups i)

namespace Classified

instance : Classified.{u} 0 where
  number := 0
  groups := nofun
  group := nofun
  distinct := nofun
  classifies _ _ _ _ := by aesop

end Classified

[Kenny Lau]

0 has been done for you :slight_smile: 1 is left as an exercise

[Jireh Loreaux]

Classified is wrong.

1. It never says the groups have order n
2. It says that if there is a bijection between them, then they're equal. It should say if they're isomorphic then they're equal.

[Eric Wieser]

Isn't 1 implied by classifies?

[Kenny Lau]

it isn't, there could still be junk values that G is just never isomorphic to

[Kenny Lau]

import Mathlib

universe u

/-- A classification of groups of order `n`. -/
class Classified (n : ℕ) : Type 1 where
  number : ℕ
  groups : Fin number → Type
  group (i) : Group (groups i)
  fintype (i) : Fintype (groups i)
  card (i) : Fintype.card (groups i) = n
  distinct (i j) : groups i ≃* groups j → i = j
  classifies (G : Type u) [Group G] [Fintype G] (hg : Fintype.card G = n) :
    ∃ i, Nonempty (G ≃* groups i)

attribute [instance] Classified.group Classified.fintype

namespace Classified

instance : Classified.{u} 0 where
  number := 0
  groups := nofun
  group := nofun
  fintype := nofun
  card := nofun
  distinct := nofun
  classifies _ _ _ _ := by aesop

lemma unique' {n : ℕ} (x y : Classified n) : ∃ e : Fin x.number ≃ Fin y.number,
    ∀ i, Nonempty (x.groups i ≃* y.groups (e i)) := by
  refine
  ⟨{ toFun i := (y.classifies (ULift <| x.groups i) (by simp [card])).choose
     invFun j := (x.classifies (ULift <| y.groups j) (by simp [card])).choose
     left_inv i := x.distinct _ _ sorry
     right_inv j := y.distinct _ _ sorry },
  fun i ↦ ⟨sorry⟩⟩

end Classified

[Kenny Lau]

now with a uniqueness lemma with 3 sorries!

[Kevin Buzzard]

This Classified class comes with the universe footgun; there's a universe in the fields which is not in the inputs, so the moment you forget to write Classified.{u} Lean starts timing out when attempting to figure out the maximally general universe set-up for declarations using it. Surely better to stick with the claim that we're classifying groups in Type and then if the user is unlucky enough to have a finite group in Type u then make it their problem to descend it to Type first.

[Jireh Loreaux]

Yes, this kind of pattern arises in other places too. The example that comes to mind (only because I happened to write it) is docs#TietzeExtension, where it would have been possible (and indeed, I originally did) to write the extension in terms of a closed embedding from a third type (instead of a from a closed subset) as in docs#ContinuousMap.exists_extension, but this would have involved a third universe parameter which is not really relevant to the type class. But after you have the class, you can write the universe polymorphic theorem that you want.

[Kenny Lau]

sounds like a problem with Lean...

[Kevin Buzzard]

Maybe, but it's still a footgun.

[Kenny Lau]

Actually, I can do better!

[Kenny Lau]

import Mathlib

universe u

/-- A classification of groups of order `n`. -/
class Classified (n : ℕ) : Type 1 where
  number : ℕ
  groups : Fin number → Type
  group (i) : Group (groups i)
  fintype (i) : Fintype (groups i)
  card (i) : Fintype.card (groups i) = n
  distinct (i j) : groups i ≃* groups j → i = j
  classifies' (G : Type) [Group G] [Fintype G] (hg : Fintype.card G = n) :
    ∃ i, Nonempty (G ≃* groups i)

attribute [instance] Classified.group Classified.fintype

namespace Classified

instance : Classified 0 where
  number := 0
  groups := nofun
  group := nofun
  fintype := nofun
  card := nofun
  distinct := nofun
  classifies' _ _ _ _ := by aesop

lemma classifies {n : ℕ} [Classified n] (G : Type u) [Group G] [Fintype G] (hg : Fintype.card G = n) :
    ∃ i, Nonempty (G ≃* groups (n := n) i) :=
  let ⟨i, ⟨e⟩⟩ := classifies' (n := n) (Shrink G) (by simp [hg]);
  ⟨i, ⟨Shrink.mulEquiv.symm.trans e⟩⟩

lemma unique' {n : ℕ} (x y : Classified n) : ∃ e : Fin x.number ≃ Fin y.number,
    ∀ i, Nonempty (x.groups i ≃* y.groups (e i)) := by
  refine
  ⟨{ toFun i := (y.classifies' (x.groups i) (by simp [card])).choose
     invFun j := (x.classifies' (y.groups j) (by simp [card])).choose
     left_inv i := x.distinct _ _ sorry
     right_inv j := y.distinct _ _ sorry },
  fun i ↦ ⟨sorry⟩⟩

end Classified

[Kenny Lau]

Thanks a lot for the reminder, you only have to classify groups in Type 0, and you automatically get that groups in Type u are still classified!

[Kenny Lau]

@Kevin Buzzard

[Jz Pan]

Actually your Classified can live in Type 0 but you need to do some stupid things

[Jz Pan]

Just like here Sequence.NonIsoSubgroupsSymm

[Kenny Lau]

I'm not sure the "stupid things" is worth it

[Kenny Lau]

you can just use unique to Shrink it if you really wanted to

[Jz Pan]

I mean you can realize every group of order n as a subgroup of S_n of order n, so you don't need to mention Type at all in Classified

[Jz Pan]

Just like the link I gave in sequencelib

[Kenny Lau]

i want my defeqs to Multiplicative ZMod 37

[Jz Pan]

Kenny Lau said:

i want my defeqs to Multiplicative ZMod 37

(A group of order 37) ≃* (some stupid internal thing but is unique) ≃* Multiplicative ZMod 37

[Kenny Lau]

but how would Classified generate Muliplicative ZMod 37

[Jz Pan]

Kenny Lau said:

but how would Classified generate Muliplicative ZMod 37

You call classification on (A group of order 37) and Multiplicative ZMod 37, get two isomorphisms, then compose them

[Kenny Lau]

hmm... that could work ...

[Thomas Browning]

Floris van Doorn said:

A student of mine did a project where she classified the groups of order 8: https://github.com/lucia3125/LeanCourse23/tree/master/LeanCourse/Project

From this it should be pretty easy to get groups of order <= 11 since we have docs#IsPGroup.commGroupOfCardEqPrimeSq and docs#isZGroup_iff_exists_mulEquiv (group of squarefree order is a semidirect product of cyclic groups).

[Kenny Lau]

but what about 8? :slight_smile:

[Kevin Buzzard]

8 is done -- see above

[Kenny Lau]

ah, sorry I misunderstood