Subgroups of finite groups

module finite-group-theory.subgroups-finite-groups where
Imports
open import finite-group-theory.finite-groups
open import finite-group-theory.finite-semigroups

open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalence-relations
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.decidable-subgroups
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.semigroups
open import group-theory.subgroups

open import univalent-combinatorics.decidable-subtypes
open import univalent-combinatorics.finite-types

Idea

A finite subgroup of a finite group G is a decidable subgroup of G.

Definitions

Decidable subsets of groups

decidable-subset-Group-𝔽 :
  (l : Level) {l1 : Level} (G : Group-𝔽 l1)  UU (lsuc l  l1)
decidable-subset-Group-𝔽 l G =
  decidable-subset-Group l (group-Group-𝔽 G)

is-set-decidable-subset-Group-𝔽 :
  (l : Level) {l1 : Level} (G : Group-𝔽 l1) 
  is-set (decidable-subset-Group-𝔽 l G)
is-set-decidable-subset-Group-𝔽 l G =
  is-set-decidable-subset-Group l (group-Group-𝔽 G)

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (P : decidable-subset-Group-𝔽 l2 G)
  where

  subset-decidable-subset-Group-𝔽 : subset-Group l2 (group-Group-𝔽 G)
  subset-decidable-subset-Group-𝔽 =
    subset-decidable-subset-Group (group-Group-𝔽 G) P

Finite subgroups of finite groups

By default, finite subgroups of finite groups are considered to be decidable. Indeed, one can prove that if a subgroup of a finite group has a finite underlying type, then it must be a decidable subgroup.

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (P : decidable-subset-Group-𝔽 l2 G)
  where

  contains-unit-decidable-subset-finite-group-Prop : Prop l2
  contains-unit-decidable-subset-finite-group-Prop =
    contains-unit-decidable-subset-group-Prop
      ( group-Group-𝔽 G)
      ( P)

  contains-unit-decidable-subset-Group-𝔽 : UU l2
  contains-unit-decidable-subset-Group-𝔽 =
    contains-unit-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

  is-prop-contains-unit-decidable-subset-Group-𝔽 :
    is-prop contains-unit-decidable-subset-Group-𝔽
  is-prop-contains-unit-decidable-subset-Group-𝔽 =
    is-prop-contains-unit-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

  is-closed-under-mul-decidable-subset-finite-group-Prop : Prop (l1  l2)
  is-closed-under-mul-decidable-subset-finite-group-Prop =
    is-closed-under-mul-decidable-subset-group-Prop
      ( group-Group-𝔽 G)
      ( P)

  is-closed-under-mul-decidable-subset-Group-𝔽 : UU (l1  l2)
  is-closed-under-mul-decidable-subset-Group-𝔽 =
    is-closed-under-mul-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

  is-prop-is-closed-under-mul-decidable-subset-Group-𝔽 :
    is-prop is-closed-under-mul-decidable-subset-Group-𝔽
  is-prop-is-closed-under-mul-decidable-subset-Group-𝔽 =
    is-prop-is-closed-under-mul-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

  is-closed-under-inv-decidable-subset-finite-group-Prop : Prop (l1  l2)
  is-closed-under-inv-decidable-subset-finite-group-Prop =
    is-closed-under-inv-decidable-subset-group-Prop
      ( group-Group-𝔽 G)
      ( P)

  is-closed-under-inv-decidable-subset-Group-𝔽 : UU (l1  l2)
  is-closed-under-inv-decidable-subset-Group-𝔽 =
    is-closed-under-inv-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

  is-prop-is-closed-under-inv-decidable-subset-Group-𝔽 :
    is-prop is-closed-under-inv-decidable-subset-Group-𝔽
  is-prop-is-closed-under-inv-decidable-subset-Group-𝔽 =
    is-prop-is-closed-under-inv-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

  is-subgroup-decidable-subset-finite-group-Prop : Prop (l1  l2)
  is-subgroup-decidable-subset-finite-group-Prop =
    is-subgroup-decidable-subset-group-Prop
      ( group-Group-𝔽 G)
      ( P)

  is-subgroup-decidable-subset-Group-𝔽 : UU (l1  l2)
  is-subgroup-decidable-subset-Group-𝔽 =
    is-subgroup-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

  is-prop-is-subgroup-decidable-subset-Group-𝔽 :
    is-prop is-subgroup-decidable-subset-Group-𝔽
  is-prop-is-subgroup-decidable-subset-Group-𝔽 =
    is-prop-is-subgroup-decidable-subset-Group
      ( group-Group-𝔽 G)
      ( P)

Subgroup-𝔽 :
  (l : Level) {l1 : Level} (G : Group-𝔽 l1)  UU (lsuc l  l1)
Subgroup-𝔽 l G = Decidable-Subgroup l (group-Group-𝔽 G)

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (H : Subgroup-𝔽 l2 G)
  where

  decidable-subset-Subgroup-𝔽 : decidable-subset-Group l2 (group-Group-𝔽 G)
  decidable-subset-Subgroup-𝔽 =
    decidable-subset-Decidable-Subgroup (group-Group-𝔽 G) H

  subset-Subgroup-𝔽 : subset-Group l2 (group-Group-𝔽 G)
  subset-Subgroup-𝔽 = subset-Decidable-Subgroup (group-Group-𝔽 G) H

  is-subgroup-subset-Subgroup-𝔽 :
    is-subgroup-subset-Group (group-Group-𝔽 G) subset-Subgroup-𝔽
  is-subgroup-subset-Subgroup-𝔽 =
    is-subgroup-subset-Decidable-Subgroup (group-Group-𝔽 G) H

  subgroup-Subgroup-𝔽 : Subgroup l2 (group-Group-𝔽 G)
  subgroup-Subgroup-𝔽 = subgroup-Decidable-Subgroup (group-Group-𝔽 G) H

  type-Subgroup-𝔽 : UU (l1  l2)
  type-Subgroup-𝔽 = type-Decidable-Subgroup (group-Group-𝔽 G) H

  is-finite-type-Subgroup-𝔽 : is-finite type-Subgroup-𝔽
  is-finite-type-Subgroup-𝔽 =
    is-finite-type-subset-𝔽 (finite-type-Group-𝔽 G) decidable-subset-Subgroup-𝔽

  finite-type-Subgroup-𝔽 : 𝔽 (l1  l2)
  finite-type-Subgroup-𝔽 =
    finite-type-subset-𝔽 (finite-type-Group-𝔽 G) decidable-subset-Subgroup-𝔽

  inclusion-Subgroup-𝔽 : type-Subgroup-𝔽  type-Group-𝔽 G
  inclusion-Subgroup-𝔽 = inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

  is-emb-inclusion-Subgroup-𝔽 : is-emb inclusion-Subgroup-𝔽
  is-emb-inclusion-Subgroup-𝔽 =
    is-emb-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

  emb-inclusion-Subgroup-𝔽 : type-Subgroup-𝔽  type-Group-𝔽 G
  emb-inclusion-Subgroup-𝔽 =
    emb-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

  is-in-Subgroup-𝔽 : type-Group-𝔽 G  UU l2
  is-in-Subgroup-𝔽 = is-in-Decidable-Subgroup (group-Group-𝔽 G) H

  is-in-subgroup-inclusion-Subgroup-𝔽 :
    (x : type-Subgroup-𝔽)  is-in-Subgroup-𝔽 (inclusion-Subgroup-𝔽 x)
  is-in-subgroup-inclusion-Subgroup-𝔽 =
    is-in-subgroup-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

  is-prop-is-in-Subgroup-𝔽 :
    (x : type-Group-𝔽 G)  is-prop (is-in-Subgroup-𝔽 x)
  is-prop-is-in-Subgroup-𝔽 =
    is-prop-is-in-Decidable-Subgroup (group-Group-𝔽 G) H

  contains-unit-Subgroup-𝔽 :
    contains-unit-subset-Group (group-Group-𝔽 G) subset-Subgroup-𝔽
  contains-unit-Subgroup-𝔽 =
    contains-unit-Decidable-Subgroup (group-Group-𝔽 G) H

  is-closed-under-mul-Subgroup-𝔽 :
    is-closed-under-mul-subset-Group (group-Group-𝔽 G) subset-Subgroup-𝔽
  is-closed-under-mul-Subgroup-𝔽 =
    is-closed-under-mul-Decidable-Subgroup (group-Group-𝔽 G) H

  is-closed-under-inv-Subgroup-𝔽 :
    is-closed-under-inv-subset-Group (group-Group-𝔽 G) subset-Subgroup-𝔽
  is-closed-under-inv-Subgroup-𝔽 =
    is-closed-under-inv-Decidable-Subgroup (group-Group-𝔽 G) H

is-emb-decidable-subset-Subgroup-𝔽 :
  {l1 l2 : Level} (G : Group-𝔽 l1) 
  is-emb (decidable-subset-Subgroup-𝔽 {l2 = l2} G)
is-emb-decidable-subset-Subgroup-𝔽 G =
  is-emb-decidable-subset-Decidable-Subgroup (group-Group-𝔽 G)

The underlying group of a decidable subgroup

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (H : Subgroup-𝔽 l2 G)
  where

  type-group-Subgroup-𝔽 : UU (l1  l2)
  type-group-Subgroup-𝔽 = type-Subgroup-𝔽 G H

  map-inclusion-group-Subgroup-𝔽 :
    type-group-Subgroup-𝔽  type-Group-𝔽 G
  map-inclusion-group-Subgroup-𝔽 = inclusion-Subgroup-𝔽 G H

  is-emb-inclusion-group-Subgroup-𝔽 :
    is-emb map-inclusion-group-Subgroup-𝔽
  is-emb-inclusion-group-Subgroup-𝔽 = is-emb-inclusion-Subgroup-𝔽 G H

  eq-subgroup-eq-Group-𝔽 :
    {x y : type-Subgroup-𝔽 G H} 
    ( inclusion-Subgroup-𝔽 G H x  inclusion-Subgroup-𝔽 G H y)  x  y
  eq-subgroup-eq-Group-𝔽 =
    eq-decidable-subgroup-eq-group (group-Group-𝔽 G) H

  set-group-Subgroup-𝔽 : Set (l1  l2)
  set-group-Subgroup-𝔽 = set-group-Decidable-Subgroup (group-Group-𝔽 G) H

  mul-Subgroup-𝔽 : (x y : type-Subgroup-𝔽 G H)  type-Subgroup-𝔽 G H
  mul-Subgroup-𝔽 = mul-Decidable-Subgroup (group-Group-𝔽 G) H

  associative-mul-Subgroup-𝔽 :
    (x y z : type-Subgroup-𝔽 G H) 
    mul-Subgroup-𝔽 (mul-Subgroup-𝔽 x y) z 
    mul-Subgroup-𝔽 x (mul-Subgroup-𝔽 y z)
  associative-mul-Subgroup-𝔽 =
    associative-mul-Decidable-Subgroup (group-Group-𝔽 G) H

  unit-Subgroup-𝔽 : type-Subgroup-𝔽 G H
  unit-Subgroup-𝔽 = unit-Decidable-Subgroup (group-Group-𝔽 G) H

  left-unit-law-mul-Subgroup-𝔽 :
    (x : type-Subgroup-𝔽 G H)  mul-Subgroup-𝔽 unit-Subgroup-𝔽 x  x
  left-unit-law-mul-Subgroup-𝔽 =
    left-unit-law-mul-Decidable-Subgroup (group-Group-𝔽 G) H

  right-unit-law-mul-Subgroup-𝔽 :
    (x : type-Subgroup-𝔽 G H)  mul-Subgroup-𝔽 x unit-Subgroup-𝔽  x
  right-unit-law-mul-Subgroup-𝔽 =
    right-unit-law-mul-Decidable-Subgroup (group-Group-𝔽 G) H

  inv-Subgroup-𝔽 : type-Subgroup-𝔽 G H  type-Subgroup-𝔽 G H
  inv-Subgroup-𝔽 = inv-Decidable-Subgroup (group-Group-𝔽 G) H

  left-inverse-law-mul-Subgroup-𝔽 :
    ( x : type-Subgroup-𝔽 G H) 
    mul-Subgroup-𝔽 (inv-Subgroup-𝔽 x) x  unit-Subgroup-𝔽
  left-inverse-law-mul-Subgroup-𝔽 =
    left-inverse-law-mul-Decidable-Subgroup (group-Group-𝔽 G) H

  right-inverse-law-mul-Subgroup-𝔽 :
    (x : type-Subgroup-𝔽 G H) 
    mul-Subgroup-𝔽 x (inv-Subgroup-𝔽 x)  unit-Subgroup-𝔽
  right-inverse-law-mul-Subgroup-𝔽 =
    right-inverse-law-mul-Decidable-Subgroup (group-Group-𝔽 G) H

  finite-semigroup-Subgroup-𝔽 : Semigroup-𝔽 (l1  l2)
  pr1 finite-semigroup-Subgroup-𝔽 = finite-type-Subgroup-𝔽 G H
  pr1 (pr2 finite-semigroup-Subgroup-𝔽) = mul-Subgroup-𝔽
  pr2 (pr2 finite-semigroup-Subgroup-𝔽) = associative-mul-Subgroup-𝔽

  finite-group-Subgroup-𝔽 : Group-𝔽 (l1  l2)
  pr1 finite-group-Subgroup-𝔽 = finite-semigroup-Subgroup-𝔽
  pr1 (pr1 (pr2 finite-group-Subgroup-𝔽)) = unit-Subgroup-𝔽
  pr1 (pr2 (pr1 (pr2 finite-group-Subgroup-𝔽))) = left-unit-law-mul-Subgroup-𝔽
  pr2 (pr2 (pr1 (pr2 finite-group-Subgroup-𝔽))) = right-unit-law-mul-Subgroup-𝔽
  pr1 (pr2 (pr2 finite-group-Subgroup-𝔽)) = inv-Subgroup-𝔽
  pr1 (pr2 (pr2 (pr2 finite-group-Subgroup-𝔽))) =
    left-inverse-law-mul-Subgroup-𝔽
  pr2 (pr2 (pr2 (pr2 finite-group-Subgroup-𝔽))) =
    right-inverse-law-mul-Subgroup-𝔽

semigroup-Subgroup-𝔽 :
  {l1 l2 : Level} (G : Group-𝔽 l1)  Subgroup-𝔽 l2 G  Semigroup (l1  l2)
semigroup-Subgroup-𝔽 G H =
  semigroup-Semigroup-𝔽 (finite-semigroup-Subgroup-𝔽 G H)

group-Subgroup-𝔽 :
  {l1 l2 : Level} (G : Group-𝔽 l1)  Subgroup-𝔽 l2 G  Group (l1  l2)
group-Subgroup-𝔽 G H = group-Group-𝔽 (finite-group-Subgroup-𝔽 G H)

The inclusion homomorphism of the underlying finite group of a finite subgroup into the ambient group

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (H : Subgroup-𝔽 l2 G)
  where

  preserves-mul-inclusion-group-Subgroup-𝔽 :
    preserves-mul-Group
      ( group-Subgroup-𝔽 G H)
      ( group-Group-𝔽 G)
      ( inclusion-Subgroup-𝔽 G H)
  preserves-mul-inclusion-group-Subgroup-𝔽 =
    preserves-mul-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

  preserves-unit-inclusion-group-Subgroup-𝔽 :
    preserves-unit-Group
      ( group-Subgroup-𝔽 G H)
      ( group-Group-𝔽 G)
      ( inclusion-Subgroup-𝔽 G H)
  preserves-unit-inclusion-group-Subgroup-𝔽 =
    preserves-unit-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

  preserves-inverses-inclusion-group-Subgroup-𝔽 :
    preserves-inverses-Group
      ( group-Subgroup-𝔽 G H)
      ( group-Group-𝔽 G)
      ( inclusion-Subgroup-𝔽 G H)
  preserves-inverses-inclusion-group-Subgroup-𝔽 =
    preserves-inverses-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

  inclusion-group-Subgroup-𝔽 :
    type-hom-Group (group-Subgroup-𝔽 G H) (group-Group-𝔽 G)
  inclusion-group-Subgroup-𝔽 =
    hom-inclusion-Decidable-Subgroup (group-Group-𝔽 G) H

Properties

Extensionality of the type of all subgroups

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (H : Subgroup-𝔽 l2 G)
  where

  has-same-elements-Subgroup-𝔽 :
    {l3 : Level}  Subgroup-𝔽 l3 G  UU (l1  l2  l3)
  has-same-elements-Subgroup-𝔽 =
    has-same-elements-Decidable-Subgroup (group-Group-𝔽 G) H

  extensionality-Subgroup-𝔽 :
    (K : Subgroup-𝔽 l2 G)  (H  K)  has-same-elements-Subgroup-𝔽 K
  extensionality-Subgroup-𝔽 =
    extensionality-Decidable-Subgroup (group-Group-𝔽 G) H

Every finite subgroup induces two equivalence relations

The equivalence relation where x ~ y if and only if there exists u : H such that xu = y

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (H : Subgroup-𝔽 l2 G)
  where

  right-sim-Subgroup-𝔽 : (x y : type-Group-𝔽 G)  UU l2
  right-sim-Subgroup-𝔽 = right-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  is-prop-right-sim-Subgroup-𝔽 :
    (x y : type-Group-𝔽 G)  is-prop (right-sim-Subgroup-𝔽 x y)
  is-prop-right-sim-Subgroup-𝔽 =
    is-prop-right-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  prop-right-eq-rel-Subgroup-𝔽 :
    (x y : type-Group-𝔽 G)  Prop l2
  prop-right-eq-rel-Subgroup-𝔽 =
    prop-right-eq-rel-Decidable-Subgroup (group-Group-𝔽 G) H

  refl-right-sim-Subgroup-𝔽 :
    is-reflexive-Rel-Prop prop-right-eq-rel-Subgroup-𝔽
  refl-right-sim-Subgroup-𝔽 =
    refl-right-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  symm-right-sim-Subgroup-𝔽 :
    is-symmetric-Rel-Prop prop-right-eq-rel-Subgroup-𝔽
  symm-right-sim-Subgroup-𝔽 =
    symm-right-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  trans-right-sim-Subgroup-𝔽 :
    is-transitive-Rel-Prop prop-right-eq-rel-Subgroup-𝔽
  trans-right-sim-Subgroup-𝔽 =
    trans-right-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  right-eq-rel-Subgroup-𝔽 : Eq-Rel l2 (type-Group-𝔽 G)
  right-eq-rel-Subgroup-𝔽 =
    right-eq-rel-Decidable-Subgroup (group-Group-𝔽 G) H

The equivalence relation where x ~ y if and only if there exists u : H such that ux = y

module _
  {l1 l2 : Level} (G : Group-𝔽 l1) (H : Subgroup-𝔽 l2 G)
  where

  left-sim-Subgroup-𝔽 : (x y : type-Group-𝔽 G)  UU l2
  left-sim-Subgroup-𝔽 = left-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  is-prop-left-sim-Subgroup-𝔽 :
    (x y : type-Group-𝔽 G)  is-prop (left-sim-Subgroup-𝔽 x y)
  is-prop-left-sim-Subgroup-𝔽 =
    is-prop-left-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  prop-left-eq-rel-Subgroup-𝔽 : (x y : type-Group-𝔽 G)  Prop l2
  prop-left-eq-rel-Subgroup-𝔽 =
    prop-left-eq-rel-Decidable-Subgroup (group-Group-𝔽 G) H

  refl-left-sim-Subgroup-𝔽 :
    is-reflexive-Rel-Prop prop-left-eq-rel-Subgroup-𝔽
  refl-left-sim-Subgroup-𝔽 =
    refl-left-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  symmetric-left-sim-Subgroup-𝔽 :
    is-symmetric-Rel-Prop prop-left-eq-rel-Subgroup-𝔽
  symmetric-left-sim-Subgroup-𝔽 =
    symmetric-left-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  transitive-left-sim-Subgroup-𝔽 :
    is-transitive-Rel-Prop prop-left-eq-rel-Subgroup-𝔽
  transitive-left-sim-Subgroup-𝔽 =
    transitive-left-sim-Decidable-Subgroup (group-Group-𝔽 G) H

  left-eq-rel-Subgroup-𝔽 : Eq-Rel l2 (type-Group-𝔽 G)
  left-eq-rel-Subgroup-𝔽 =
    left-eq-rel-Decidable-Subgroup (group-Group-𝔽 G) H