Group Finiteness

Table of Contents

1 Finiteness of groups of finite order

module GroupFiniteness where

This file is an application of the Homotopy Finiteness to semigroups and groups. The goal is to compute the number of groups of finite order up to isomorphism, and to analyze the computations of the proof to better understand what's going on.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import HomotopyFiniteness
import Lib.Groups

1.2 Semigroups of order

As a group is morally a semigroup augmented with the property is-group, we start by showing that semigroups of order n have a finite number of connected components (read: there is a finite number of semigroups of order n up to isomorphism). A semigroup of order n is a semigroup G such that there is a mere bijection between G and Fin n. 

Semigroup-of-Order (n : Nat) : U =
  Σ Semigroup (λG. mere-equiv (Fin n) (Semigroup/type G))

Recall that a Semigroup is defined as follows: ΣX: Set(has-assoc-op(X)). But as || Fin n ≅ X ||, X is a set; thus we have a redundant information. As such, we want to show that the type of semigroups of order n are equivalent to the following type. 

Semigroup-of-Order' (n : Nat) : U =
  Σ (Σ U (λX. mere-equiv (Fin n) X)) (λX. has-assoc-op X.1)

Indeed, it is easy to show that has-assoc-op is π0-finite; in fact, it is finite by finiteness of X. 

has-assoc-op/is-finite (X : U) : (H : is-finite X) → is-finite (has-assoc-op X) =
  rec-Prop-trunc
    ( count X)
    ( is-finite/Prop (has-assoc-op X))
    ( λH. Prop-trunc/unit
          ( count/closed-Sg
            ( X → X → X)
            ( is-assoc X)
            ( count/closed-Pi X
              ( λ_. X → X) H
              ( λ_. count/closed-Pi X
                ( λ_. X) H
                ( λ_. H)))          
            ( λh. count/closed-Pi X
                  ( λx. (y z : X) → Path X (h (h x y) z) (h x (h y z))) H
                  ( λx. count/closed-Pi X
                        ( λy. (z : X) → Path X (h (h x y) z) (h x (h y z))) H
                        ( λy. count/closed-Pi X
                              ( λz. Path X (h (h x y) z) (h x (h y z))) H
                              ( λz. count/is-decidable-is-countable
                                    ( Path X (h (h x y) z) (h x (h y z)))
                                    ( count/is-set X H
                                      ( h (h x y) z)
                                      ( h x (h y z)))
                                    ( count/has-decidable-eq X H
                                      ( h (h x y) z)
                                      ( h x (h y z)))))))))

Moreover, it is also easy to show that Σ(X: U)|| Fin n ≅ X || is πk-finite, forall k. First, we show that Σ(X: U)|| Fin n ≅ X || is contractible. Indeed, its center of contraction is (Fin n, refl-Equiv) and by univalence, any X such that || Fin n ≅ X ||, we have Fin n = X as we show a property. 

mere-equiv-Fin/is-conn-Set-trunc (n : Nat) : is-conn (Σ U (λX. mere-equiv (Fin n) X)) = 
  let center-of-contraction : Σ U (λX. mere-equiv (Fin n) X) = (Fin n, Prop-trunc/unit (Equiv/refl (Fin n))) in
  ( Set-trunc/unit (center-of-contraction),
    ( ind-Set-trunc/Prop
      ( Σ U (λX. mere-equiv (Fin n) X))
      ( λu. Set-trunc/eq/Prop
            ( Σ U (λX. mere-equiv (Fin n) X))
            ( Set-trunc/unit center-of-contraction) u)
      ( λu. let X : U = u.1 in
            rec-Prop-trunc
            ( Equiv (Fin n) X)
            ( Set-trunc/eq/Prop
              ( Σ U (λX'. mere-equiv (Fin n) X'))
              ( Set-trunc/unit center-of-contraction)
              ( Set-trunc/unit u))
            ( λe. Set-trunc/is-effective/inv-map
                  ( Σ U (λX'. mere-equiv (Fin n) X'))
                  ( center-of-contraction) u
                  ( Prop-trunc/unit
                    ( SgPath-prop U
                      ( mere-equiv (Fin n))
                      ( λX'. Prop-trunc/is-prop (Equiv (Fin n) X'))
                      ( center-of-contraction) u
                      ( equiv-to-path (Fin n) X e)))) u.2)))

Using this lemma, we show that Σ(X: U)Fin n ≅ X is πk finite for any k. 

mere-equiv-Fin/is-htpy-finite (n : Nat) : (k : Nat) → is-htpy-finite k (Σ U (mere-equiv (Fin n))) = split
  zero → is-contr/is-finite
          ( Set-trunc (Σ U (mere-equiv (Fin n))))
          ( mere-equiv-Fin/is-conn-Set-trunc n)
  suc k →
    ( mere-equiv-Fin/is-htpy-finite n zero,
      λX Y.
        is-htpy-finite/closed-Equiv
          ( Path (Σ U (mere-equiv (Fin n))) X Y)
          ( Path U X.1 Y.1)
          ( SgPath-prop/Equiv' U
            ( mere-equiv (Fin n))
            ( λZ. Prop-trunc/is-prop (Equiv (Fin n) Z)) X Y) k
          ( is-htpy-finite/closed-Equiv
            ( Path U X.1 Y.1)
            ( Equiv X.1 Y.1)
            ( univalence' X.1 Y.1) k
            ( is-finite/is-htpy-finite 
              ( Equiv X.1 Y.1)
              ( is-finite/is-finite-Equiv X.1 Y.1
                ( has-cardinality/is-finite X.1 (n, X.2))
                ( has-cardinality/is-finite Y.1 (n, Y.2))) k)))

As homotopy finiteness is closed under equivalence, the result follows if we can show that Semigroup-of-Order and Semigroup-of-Order' are equivalent. First, we show that Σ (Σ(X: U) is-set) || Fin n ≅ X || is equivalent to Σ(X: U)|| Fin n ≅ X || (i.e., we remove a redundant information). 

Semigroup-of-Order/Equiv/map (n : Nat) (t : Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1))
                                 : Σ U (mere-equiv (Fin n)) =
  (t.1.1, t.2)

Semigroup-of-Order/Equiv/inv-map (n : Nat) (t : Σ U (mere-equiv (Fin n)))
                                     :  (Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1)) =
  ( ( t.1, is-finite/is-set t.1 (has-cardinality/is-finite t.1 (n, t.2))),
    t.2)

Semigroup-of-Order/Equiv/right-htpy (n : Nat) (t : Σ U (mere-equiv (Fin n)))
                                        : Path (Σ U (mere-equiv (Fin n)))
                                               (Semigroup-of-Order/Equiv/map n (Semigroup-of-Order/Equiv/inv-map n t)) t =
  SgPath-prop U
    ( mere-equiv (Fin n))
    ( λX. Prop-trunc/is-prop (Equiv (Fin n) X))
    ( Semigroup-of-Order/Equiv/map n (Semigroup-of-Order/Equiv/inv-map n t)) t
    ( refl U t.1)

lock Prop-trunc/is-prop is-set/is-prop has-cardinality/is-finite is-finite/is-set
Semigroup-of-Order/Equiv/left-htpy (n : Nat) (t : Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1))
                                       : Path (Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1))
                                              (Semigroup-of-Order/Equiv/inv-map n (Semigroup-of-Order/Equiv/map n t)) t =
  SgPath-prop (Σ U is-set)
    ( λX. mere-equiv (Fin n) X.1)
    ( λX. Prop-trunc/is-prop (Equiv (Fin n) X.1))
    ( Semigroup-of-Order/Equiv/inv-map n (Semigroup-of-Order/Equiv/map n t)) t
    ( SgPath-prop U
      ( is-set)
      ( is-set/is-prop)
      ( Semigroup-of-Order/Equiv/inv-map n (Semigroup-of-Order/Equiv/map n t)).1 t.1
      ( refl U t.1.1))

Semigroup-of-Order/Equiv' (n : Nat) : Equiv (Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1)) (Σ U (mere-equiv (Fin n))) =
  has-inverse/Equiv
    ( Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1))
    ( Σ U (mere-equiv (Fin n)))
    ( Semigroup-of-Order/Equiv/map n)
    ( Semigroup-of-Order/Equiv/inv-map n,
      ( Semigroup-of-Order/Equiv/right-htpy n,
        Semigroup-of-Order/Equiv/left-htpy n))

Which straightforwardly implies the result. 

Semigroup-of-Order/Equiv (n : Nat) : Equiv (Semigroup-of-Order n) (Semigroup-of-Order' n) =
  Equiv/trans
    ( Semigroup-of-Order n)
    ( Σ (Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1)) (λt. has-assoc-op t.1.1))
    ( Semigroup-of-Order' n)
    ( Equiv/assoc-Sg
      ( Σ U is-set)
      ( λX. has-assoc-op X.1)
      ( λX. mere-equiv (Fin n) X.1))
    ( Sg/equiv-base
      ( Σ (Σ U is-set) (λX. mere-equiv (Fin n) X.1))
      ( Σ U (mere-equiv (Fin n)))
      ( λt. has-assoc-op t.1)
      ( Semigroup-of-Order/Equiv' n))      
unlock Prop-trunc/is-prop is-set/is-prop has-cardinality/is-finite is-finite/is-set

Combining these facts, we can show that Semigroup-of-Order n is homotopy finite forall k ∈ Nat. 

Semigroup-of-Order/is-htpy-finite (n : Nat) (k : Nat) : is-htpy-finite k (Semigroup-of-Order n) =
  is-htpy-finite/closed-Equiv
    ( Semigroup-of-Order n)
    ( Semigroup-of-Order' n)
    ( Semigroup-of-Order/Equiv n) k
    ( is-htpy-finite/closed-Sg
      ( Σ U (λX. mere-equiv (Fin n) X))
      ( λX. has-assoc-op X.1) k
      ( mere-equiv-Fin/is-htpy-finite n (suc k))
      ( λX. is-finite/is-htpy-finite
            ( has-assoc-op X.1)
            ( has-assoc-op/is-finite X.1
              ( has-cardinality/is-finite X.1 (n, X.2))) k))

In particular, it has a finite amount of connected components. 

Semigroup-of-Order/has-finite-connected-components (n : Nat) : is-htpy-finite zero (Semigroup-of-Order n) =
  Semigroup-of-Order/is-htpy-finite n zero

Hence, we can compute the number of semigroups of order n up to isomorphism. 

number-of-Semigroup-of-Order (n : Nat) : Nat =
  card
    ( Set-trunc (Semigroup-of-Order n))
    ( Semigroup-of-Order/has-finite-connected-components n)

1.3 Groups of order

Faithful to the definition of Semigroup-of-Order n, a group of order n is a group G such that there is a mere equivalence between Fin n and G. 

Group-of-Order (n : Nat) : U =
  Σ Group (λG. mere-equiv (Fin n) (Group/type G))

Though, like Semigroup-of-Order n, we will show that it is equivalent to the following definition. 

Group-of-Order' (n : Nat) : U =
  Σ (Semigroup-of-Order n) (λG. is-group G.1)

As we have already shown in the previous section that Semigroup-of-Order n is πk-finite for k ∈ Nat, we show that is-group is finite whenever the underlying type is finite in two steps. First, we show that is-unital is finite. 

is-unital/is-finite (G : Semigroup) (is-finite-G : is-finite (Semigroup/type G)) : is-finite (is-unital G) =
  rec-Prop-trunc
    ( count (Semigroup/type G))
    ( is-finite/Prop (is-unital G))
    ( λH. is-finite/closed-Sg'
          ( Semigroup/type G)
          ( λe. (left-unit-law G e) * (right-unit-law G e)) is-finite-G
          ( λe. count/closed-Prod
                ( left-unit-law G e)
                ( right-unit-law G e)
                ( count/closed-Pi
                  ( Semigroup/type G)
                  ( λy. Path (Semigroup/type G) (Semigroup/op G e y) y) H
                  ( λy. count/is-decidable-is-countable
                        ( Path (Semigroup/type G) (Semigroup/op G e y) y)
                        ( Semigroup/is-set G (Semigroup/op G e y) y)
                        ( count/has-decidable-eq
                          ( Semigroup/type G) H (Semigroup/op G e y) y)))
                ( count/closed-Pi
                  ( Semigroup/type G)
                  ( λx. Path (Semigroup/type G) (Semigroup/op G x e) x) H
                  ( λx. count/is-decidable-is-countable
                        ( Path (Semigroup/type G) (Semigroup/op G x e) x)
                        ( Semigroup/is-set G (Semigroup/op G x e) x)
                        ( count/has-decidable-eq
                        ( Semigroup/type G) H (Semigroup/op G x e) x))))) is-finite-G

And then, we show that is-group is also finite. 

is-group/is-finite (G : Semigroup) (is-finite-G : is-finite (Semigroup/type G)) : is-finite (is-group G) =
  rec-Prop-trunc
    ( count (Semigroup/type G))
    ( is-finite/Prop (is-group G))
    ( λH. is-finite/closed-Sg'
          ( is-unital G)
          ( is-group' G)
          ( is-unital/is-finite G is-finite-G)
          ( λe. count/closed-Sg
                ( Semigroup/map G G)
                ( λi. ((x : Semigroup/type G) → left-inv (G, e) x (i x)) * ((x : Semigroup/type G) → right-inv (G, e) x (i x)))
                ( count/closed-Pi
                  ( Semigroup/type G)
                  ( λ_. Semigroup/type G) H
                  ( λ_. H))
                ( λi. count/closed-Prod
                      ( (x : Semigroup/type G) → left-inv (G, e) x (i x))
                      ( (x : Semigroup/type G) → right-inv (G, e) x (i x))
                      ( count/closed-Pi
                        ( Semigroup/type G)
                        ( λx. left-inv (G, e) x (i x)) H
                        ( λx. count/is-decidable-is-countable
                              ( Path (Semigroup/type G) (Semigroup/op G (i x) x) e.1)
                              ( Semigroup/is-set G (Semigroup/op G (i x) x) e.1)
                              ( count/has-decidable-eq
                                ( Semigroup/type G) H (Semigroup/op G (i x) x) e.1)))
                      ( count/closed-Pi
                        ( Semigroup/type G)
                        ( λx. left-inv (G, e) (i x) x) H
                        ( λx. count/is-decidable-is-countable
                              ( Path (Semigroup/type G) (Semigroup/op G x (i x)) e.1)
                              ( Semigroup/is-set G (Semigroup/op G x (i x)) e.1)
                              ( count/has-decidable-eq
                                ( Semigroup/type G) H (Semigroup/op G x (i x)) e.1)))))) is-finite-G

As Group-of-Order n and Group-of-Order' n are equivalent: 

Group-of-Order/Equiv (n : Nat) : Equiv (Group-of-Order n) (Group-of-Order' n) =
  Equiv/assoc-Sg
    ( Semigroup)
    ( is-group)
    ( λG. mere-equiv (Fin n) (Semigroup/type G))

we can show that Group-of-Order is πk-finite for any k ∈ Nat. 

Group-of-Order/is-htpy-finite (n : Nat) (k : Nat) : is-htpy-finite k (Group-of-Order n) =
  is-htpy-finite/closed-Equiv
    ( Group-of-Order n)
    ( Group-of-Order' n)
    ( Group-of-Order/Equiv n) k
    ( is-htpy-finite/closed-Sg
      ( Semigroup-of-Order n)
      ( λG. is-group G.1) k
      ( Semigroup-of-Order/is-htpy-finite n (suc k))
      ( λG. is-finite/is-htpy-finite
            ( is-group G.1)
            ( is-group/is-finite G.1
              ( has-cardinality/is-finite (Semigroup/type G.1) (n, G.2))) k))

In particular, it has a finite amount of connected components. 

Group-of-Order/has-finite-connected-components (n : Nat) : is-htpy-finite zero (Group-of-Order n) =
  Group-of-Order/is-htpy-finite n zero

Hence, we can compute the number of groups of finite order n up to isomorphism. 

number-of-Group-of-Order (n : Nat) : Nat =
  card
    ( Set-trunc (Group-of-Order n))
    ( Group-of-Order/has-finite-connected-components n)

Author: Johann Rosain

Created: 2024-07-23 Tue 13:50

Validate