Abstract finite groups

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-05-25.
Last modified on 2023-09-10.

module finite-algebra.finite-groups where
Imports 
open import finite-algebra.finite-monoids
open import finite-algebra.finite-semigroups

open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.commuting-elements-groups
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups

open import structured-types.pointed-types

open import univalent-combinatorics.cartesian-product-types
open import univalent-combinatorics.dependent-function-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types

Idea

An abstract finite group is a finite group in the usual algebraic sense, i.e., it consists of a finite type equipped with a unit element e, a binary operation x, y ↦ xy, and an inverse operation x ↦ x⁻¹ satisfying the group laws

  (xy)z = x(yz)      (associativity)
     ex = x          (left unit law)
     xe = x          (right unit law)
   x⁻¹x = e          (left inverse law)
   xx⁻¹ = e          (right inverse law)

Definition

The condition that a finite semigroup is a finite group

is-group-𝔽 :
  {l : Level} (G : Semigroup-𝔽 l) → UU l
is-group-𝔽 G = is-group (semigroup-Semigroup-𝔽 G)

The type of groups

Group-𝔽 :
  (l : Level) → UU (lsuc l)
Group-𝔽 l = Σ (Semigroup-𝔽 l) is-group-𝔽

compute-group-𝔽 :
  {l : Level} → (G : Group l) → is-finite (type-Group G) → Group-𝔽 l
pr1 (compute-group-𝔽 G f) = compute-semigroup-𝔽 (semigroup-Group G) f
pr2 (compute-group-𝔽 G f) = is-group-Group G

module _
  {l : Level} (G : Group-𝔽 l)
  where

  finite-semigroup-Group-𝔽 : Semigroup-𝔽 l
  finite-semigroup-Group-𝔽 = pr1 G

  semigroup-Group-𝔽 : Semigroup l
  semigroup-Group-𝔽 = semigroup-Semigroup-𝔽 finite-semigroup-Group-𝔽

  is-group-Group-𝔽 : is-group-𝔽 finite-semigroup-Group-𝔽
  is-group-Group-𝔽 = pr2 G

  group-Group-𝔽 : Group l
  pr1 group-Group-𝔽 = semigroup-Group-𝔽
  pr2 group-Group-𝔽 = is-group-Group-𝔽

  finite-type-Group-𝔽 : 𝔽 l
  finite-type-Group-𝔽 = finite-type-Semigroup-𝔽 finite-semigroup-Group-𝔽

  type-Group-𝔽 : UU l
  type-Group-𝔽 = type-Semigroup semigroup-Group-𝔽

  is-finite-type-Group-𝔽 : is-finite type-Group-𝔽
  is-finite-type-Group-𝔽 = is-finite-type-Semigroup-𝔽 finite-semigroup-Group-𝔽

  set-Group-𝔽 : Set l
  set-Group-𝔽 = set-Group group-Group-𝔽

  is-set-type-Group-𝔽 : is-set type-Group-𝔽
  is-set-type-Group-𝔽 = is-set-type-Group group-Group-𝔽

  has-associative-mul-Group-𝔽 : has-associative-mul type-Group-𝔽
  has-associative-mul-Group-𝔽 = has-associative-mul-Group group-Group-𝔽

  mul-Group-𝔽 : type-Group-𝔽 → type-Group-𝔽 → type-Group-𝔽
  mul-Group-𝔽 = mul-Group group-Group-𝔽

  ap-mul-Group-𝔽 :
    {x x' y y' : type-Group-𝔽} (p : Id x x') (q : Id y y') →
    Id (mul-Group-𝔽 x y) (mul-Group-𝔽 x' y')
  ap-mul-Group-𝔽 = ap-mul-Group group-Group-𝔽

  mul-Group-𝔽' : type-Group-𝔽 → type-Group-𝔽 → type-Group-𝔽
  mul-Group-𝔽' = mul-Group' group-Group-𝔽

  commute-Group-𝔽 : type-Group-𝔽 → type-Group-𝔽 → UU l
  commute-Group-𝔽 = commute-Group group-Group-𝔽

  associative-mul-Group-𝔽 :
    (x y z : type-Group-𝔽) →
    Id (mul-Group-𝔽 (mul-Group-𝔽 x y) z) (mul-Group-𝔽 x (mul-Group-𝔽 y z))
  associative-mul-Group-𝔽 = associative-mul-Group group-Group-𝔽

  is-unital-Group-𝔽 : is-unital-Semigroup semigroup-Group-𝔽
  is-unital-Group-𝔽 = is-unital-Group group-Group-𝔽

  monoid-Group-𝔽 : Monoid l
  monoid-Group-𝔽 = monoid-Group group-Group-𝔽

  finite-monoid-Group-𝔽 : Monoid-𝔽 l
  pr1 finite-monoid-Group-𝔽 = finite-semigroup-Group-𝔽
  pr2 finite-monoid-Group-𝔽 = is-unital-Group-𝔽

  unit-Group-𝔽 : type-Group-𝔽
  unit-Group-𝔽 = unit-Group group-Group-𝔽

  is-unit-Group-𝔽 : type-Group-𝔽 → UU l
  is-unit-Group-𝔽 = is-unit-Group group-Group-𝔽

  is-prop-is-unit-Group-𝔽 : (x : type-Group-𝔽) → is-prop (is-unit-Group-𝔽 x)
  is-prop-is-unit-Group-𝔽 = is-prop-is-unit-Group group-Group-𝔽

  is-unit-finite-group-Prop : type-Group-𝔽 → Prop l
  is-unit-finite-group-Prop = is-unit-group-Prop group-Group-𝔽

  left-unit-law-mul-Group-𝔽 :
    (x : type-Group-𝔽) → Id (mul-Group-𝔽 unit-Group-𝔽 x) x
  left-unit-law-mul-Group-𝔽 = left-unit-law-mul-Group group-Group-𝔽

  right-unit-law-mul-Group-𝔽 :
    (x : type-Group-𝔽) → Id (mul-Group-𝔽 x unit-Group-𝔽) x
  right-unit-law-mul-Group-𝔽 = right-unit-law-mul-Group group-Group-𝔽

  pointed-type-Group-𝔽 : Pointed-Type l
  pointed-type-Group-𝔽 = pointed-type-Group group-Group-𝔽

  has-inverses-Group-𝔽 : is-group' semigroup-Group-𝔽 is-unital-Group-𝔽
  has-inverses-Group-𝔽 = has-inverses-Group group-Group-𝔽

  inv-Group-𝔽 : type-Group-𝔽 → type-Group-𝔽
  inv-Group-𝔽 = inv-Group group-Group-𝔽

  left-inverse-law-mul-Group-𝔽 :
    (x : type-Group-𝔽) → Id (mul-Group-𝔽 (inv-Group-𝔽 x) x) unit-Group-𝔽
  left-inverse-law-mul-Group-𝔽 = left-inverse-law-mul-Group group-Group-𝔽

  right-inverse-law-mul-Group-𝔽 :
    (x : type-Group-𝔽) → Id (mul-Group-𝔽 x (inv-Group-𝔽 x)) unit-Group-𝔽
  right-inverse-law-mul-Group-𝔽 = right-inverse-law-mul-Group group-Group-𝔽

  inv-unit-Group-𝔽 :
    Id (inv-Group-𝔽 unit-Group-𝔽) unit-Group-𝔽
  inv-unit-Group-𝔽 = inv-unit-Group group-Group-𝔽

Properties

There is a finite number of ways to equip a finite type with a structure of group

module _
  {l : Level}
  (X : 𝔽 l)
  where

  structure-group-𝔽 : UU l
  structure-group-𝔽 =
    Σ (structure-semigroup-𝔽 X) (λ s → is-group-𝔽 (X , s))

  compute-structure-group-𝔽 :
    structure-group-𝔽 → Group-𝔽 l
  pr1 (compute-structure-group-𝔽 (s , g)) = (X , s)
  pr2 (compute-structure-group-𝔽 (s , g)) = g

  is-finite-structure-group-𝔽 :
    is-finite (structure-group-𝔽)
  is-finite-structure-group-𝔽 =
    is-finite-Σ
      ( is-finite-structure-semigroup-𝔽 X)
      ( λ s →
        is-finite-Σ
          ( is-finite-is-unital-Semigroup-𝔽 (X , s))
          ( λ u →
            is-finite-Σ
              ( is-finite-Π
                ( is-finite-type-𝔽 X)
                ( λ _ → is-finite-type-𝔽 X))
              ( λ i →
                is-finite-prod
                  ( is-finite-Π
                    ( is-finite-type-𝔽 X)
                    ( λ x → is-finite-eq-𝔽 X))
                  ( is-finite-Π
                    ( is-finite-type-𝔽 X)
                    ( λ x → is-finite-eq-𝔽 X)))))

Recent changes