Groups up to isomorphism

Stream: maths

[Alex Meiburg]

I thought I would try writing down a definition of OEIS's A000001. Here's my attempt. Could I possibly get advice on whether this is formalization is correct, and -- since I'm sure there has to be -- a cleaner way of formalizing it?

import Mathlib

def groups_are_isomorphic : Setoid (Group T) :=
  Setoid.mk (fun G H ↦ Nonempty (@MulEquiv T T G.toMul H.toMul)) ⟨
    fun _ ↦ instNonemptyOfInhabited,
    fun {G _} ⟨σ⟩ ↦ ⟨@MulEquiv.symm _ _ G.toMul _ σ⟩,
    fun {G H _} ⟨σ⟩ ⟨τ⟩ ↦ ⟨@MulEquiv.trans _ _ _ G.toMul H.toMul _ σ τ ⟩⟩

def GroupUpToIso T := @Quotient (Group T) groups_are_isomorphic

noncomputable def A000001 : ℕ → ℕ :=
  fun n ↦ Nat.card (GroupUpToIso (Fin n))

[Alex Meiburg]

In particular dealing with two separate group instances on the same type seems to have made a mess of typeclasses. Hence the abundant manual arguments to things, to say which Group structure to use where. (I also think that the inference could be smarter; σ.symm and σ.trans could have worked on their own, if the resolution had been slightly smarter about it!)

[Alex Meiburg]

I did think about something like

def groups_are_isomorphic : Setoid (Σ T, Group T) :=
  Setoid.mk (fun ⟨T1,G⟩ ⟨T2,H⟩ ↦ Nonempty (T1 ≃* T2)) ⟨
    fun _ ↦ instNonemptyOfInhabited,
    fun {G H} ⟨σ⟩ ↦ σ.symm,
    sorry⟩

def GroupUpToIso := @Quotient (Σ T, Group T) groups_are_isomorphic

instead, but that leads to other type inference errors :P

[Yury G. Kudryashov]

Are you sure you want to use multiple group structures on the same type?

[Alex Meiburg]

No, I'm not. If there's a better way to express "the type of groups up to isomorphism" I would greatly prefer that. :)

[Yury G. Kudryashov]

We have docs#Grp for bundled groups. Let me see if we have the quotient by docs#CategoryTheory.Iso

[Yury G. Kudryashov]

See docs#CategoryTheory.isomorphismClasses

[Yury G. Kudryashov]

Of course, this way you have to rely on category theory. If you want to go with your second definition, I suggest that you add instance (G : Σ T, Group T) : Group G.1 := G.2, then use fun G H ↦ Nonempty (G.1 ≃* H.1) for the relation.

[Yury G. Kudryashov]

Using ⟨T1,G⟩ ⟨T2,H⟩ makes it use match which may make it more difficult for Lean to deal with defeq.

[Yury G. Kudryashov]

With category theory, it should be possible to define the sequence using the preimage of the one-element set {Quot.mk _ (Fin n)} under isomorphismClasses.map (forget Grp).

[Yury G. Kudryashov]

BTW, we don't have an equivalence between isomorphismClasses.obj (Type u) and Cardinal.{u} yet.

[Yury G. Kudryashov]

Of course, the category theory approach is highly non-computable while your first approach is computable (not sure about the second one).

[Alex Meiburg]

Well. Relatively "computable". :)
Without even knowing that the number of groups is finite, I think it's pretty far from computable.
Maybe if I show that the GroupsUpToIso is Finite for any Finite T, it could actually become computable. (Albeit quite slow.) Hmmm.

[Alex Meiburg]

I think I will stay away from the category theory if possible. ;) Although maybe bundling somehow fixes my issues, without getting too categorical.

[Yury G. Kudryashov]

docs#Grp is exactly a pair of a type and a group structure on it.

[Yury G. Kudryashov]

And CategoryTheory.isIsomorphicSetoid is the right setoid on this type.

[Yury G. Kudryashov]

So, unless you want to use multiple Group structures on the same type, it's easier to work with Grp rather than a custom bundled type.

[Johan Commelin]

Using Grp does involve a quantification over the universe. I don't particularly care. But of course this function Nat -> Nat can avoid it, as Alex demonstrated.

[Johan Commelin]

Personally, I think having the "ugly" definition that uses multiple structures on Fin n is totally fine.
There should just be a bunch of API around it so that you can prove that A000001 4 = 2 without having to use Fin 4.

[Scott Carnahan]

If you're okay with invoking Cayley's theorem, you can try to enumerate transitive order n subgroups of permutations on n letters up to isomorphism. This at least gives you finiteness.