Subgroups generated by subsets of groups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Eléonore Mangel, Amélia Liao, Maša Žaucer and Gregor Perčič.

Created on 2022-04-21.
Last modified on 2023-09-26.

module group-theory.subgroups-generated-by-subsets-groups where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.unit-type
open import foundation.universe-levels

open import group-theory.conjugation
open import group-theory.groups
open import group-theory.normal-subgroups
open import group-theory.subgroups
open import group-theory.subsets-groups

open import lists.concatenation-lists
open import lists.lists

open import order-theory.galois-connections-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders

open import univalent-combinatorics.standard-finite-types

Idea

If S is a subset of a group G, then the subgroup generated by S is the least subgroup containing S. This idea expresses the universal property of the subgroup generated by a subset of a group. We will construct it as the type of finite combinations of elements in S and of inverses of elements in S. In informal writing we will write (S) for the subgroup generated by S.

Definitions

The universal property of subgroups generated by a subset of a group

module _
  {l1 l2 l3 : Level} (G : Group l1) (S : subset-Group l2 G)
  (U : Subgroup l3 G) (H : S ⊆ subset-Subgroup G U)
  where

  is-subgroup-generated-by-subset-Group : UUω
  is-subgroup-generated-by-subset-Group =
    {l : Level} (U' : Subgroup l G) →
    S ⊆ subset-Subgroup G U' →
    subset-Subgroup G U ⊆ subset-Subgroup G U'

The adjoint relation of subgroups generated by a subset of a group

module _
  {l1 l2 l3 : Level} (G : Group l1) (S : subset-Group l2 G)
  (U : Subgroup l3 G)
  where

  adjoint-relation-subgroup-generated-by-subset-Group : UUω
  adjoint-relation-subgroup-generated-by-subset-Group =
    {l : Level} (U' : Subgroup l G) →
    (leq-Subgroup G U U') ↔ (S ⊆ subset-Subgroup G U')

  contains-subset-adjoint-relation-subset-generated-by-subset-Group :
    adjoint-relation-subgroup-generated-by-subset-Group →
    S ⊆ subset-Subgroup G U
  contains-subset-adjoint-relation-subset-generated-by-subset-Group α =
    forward-implication (α U) (refl-leq-Subgroup G U)

  is-subgroup-generated-by-subset-adjoint-relation-Group :
    (α : adjoint-relation-subgroup-generated-by-subset-Group) →
    is-subgroup-generated-by-subset-Group G S U
      ( contains-subset-adjoint-relation-subset-generated-by-subset-Group α)
  is-subgroup-generated-by-subset-adjoint-relation-Group α U' =
    backward-implication (α U')

  adjoint-relation-is-subgroup-generated-by-subset-Group :
    (H : S ⊆ subset-Subgroup G U) →
    is-subgroup-generated-by-subset-Group G S U H →
    adjoint-relation-subgroup-generated-by-subset-Group
  pr1 (adjoint-relation-is-subgroup-generated-by-subset-Group H α K) L x y =
    L x (H x y)
  pr2 (adjoint-relation-is-subgroup-generated-by-subset-Group H α K) =
    α K

Construction of subgroups generated by a subset of a group

Formal combinations of elements in S

module _
  {l1 l2 : Level} (G : Group l1) (S : subset-Group l2 G)
  where

  formal-combination-subset-Group : UU (l1 ⊔ l2)
  formal-combination-subset-Group = list (Fin 2 × type-subtype S)

  ev-formal-combination-subset-Group :
    formal-combination-subset-Group → type-Group G
  ev-formal-combination-subset-Group nil = unit-Group G
  ev-formal-combination-subset-Group (cons (pair (inl (inr star)) x) l) =
    mul-Group G
      ( inv-Group G (inclusion-subtype S x))
      ( ev-formal-combination-subset-Group l)
  ev-formal-combination-subset-Group (cons (pair (inr star) x) l) =
    mul-Group G (inclusion-subtype S x) (ev-formal-combination-subset-Group l)

  preserves-concat-ev-formal-combination-subset-Group :
    (u v : formal-combination-subset-Group) →
    Id
      ( ev-formal-combination-subset-Group (concat-list u v))
      ( mul-Group G
        ( ev-formal-combination-subset-Group u)
        ( ev-formal-combination-subset-Group v))
  preserves-concat-ev-formal-combination-subset-Group nil v =
    inv (left-unit-law-mul-Group G (ev-formal-combination-subset-Group v))
  preserves-concat-ev-formal-combination-subset-Group
    ( cons (pair (inl (inr star)) x) u)
    ( v) =
    ( ap
      ( mul-Group G (inv-Group G (inclusion-subtype S x)))
      ( preserves-concat-ev-formal-combination-subset-Group u v)) ∙
      ( inv
        ( associative-mul-Group G
          ( inv-Group G (inclusion-subtype S x))
          ( ev-formal-combination-subset-Group u)
          ( ev-formal-combination-subset-Group v)))
  preserves-concat-ev-formal-combination-subset-Group
    ( cons (pair (inr star) x) u)
    ( v) =
    ( ap
      ( mul-Group G (inclusion-subtype S x))
      ( preserves-concat-ev-formal-combination-subset-Group u v)) ∙
      ( inv
        ( associative-mul-Group G
          (inclusion-subtype S x)
          ( ev-formal-combination-subset-Group u)
          ( ev-formal-combination-subset-Group v)))

  inv-formal-combination-subset-Group :
    formal-combination-subset-Group → formal-combination-subset-Group
  inv-formal-combination-subset-Group nil = nil
  inv-formal-combination-subset-Group (cons (pair s x) u) =
    concat-list
      ( inv-formal-combination-subset-Group u)
      ( unit-list (pair (succ-Fin 2 s) x))

  preserves-inv-ev-formal-combination-subset-Group :
    (u : formal-combination-subset-Group) →
    Id
      ( ev-formal-combination-subset-Group
        ( inv-formal-combination-subset-Group u))
      ( inv-Group G (ev-formal-combination-subset-Group u))
  preserves-inv-ev-formal-combination-subset-Group nil =
    inv (inv-unit-Group G)
  preserves-inv-ev-formal-combination-subset-Group
    ( cons (pair (inl (inr star)) x) u) =
    ( preserves-concat-ev-formal-combination-subset-Group
      ( inv-formal-combination-subset-Group u)
      ( unit-list (pair (inr star) x))) ∙
      ( ( ap
        ( λ y →
          mul-Group G y (mul-Group G (inclusion-subtype S x) (unit-Group G)))
        ( preserves-inv-ev-formal-combination-subset-Group u)) ∙
        ( ( ap
          ( mul-Group G (inv-Group G (ev-formal-combination-subset-Group u)))
          ( ( right-unit-law-mul-Group G (inclusion-subtype S x)) ∙
            ( inv (inv-inv-Group G (inclusion-subtype S x))))) ∙
          ( inv
            ( distributive-inv-mul-Group G
              ( inv-Group G (inclusion-subtype S x))
              ( ev-formal-combination-subset-Group u)))))
  preserves-inv-ev-formal-combination-subset-Group
    ( cons (pair (inr star) x) u) =
    ( preserves-concat-ev-formal-combination-subset-Group
      ( inv-formal-combination-subset-Group u)
      ( unit-list (pair (inl (inr star)) x))) ∙
      ( ( ap
        ( λ y →
          mul-Group G
          ( y)
          ( mul-Group G (inv-Group G (inclusion-subtype S x)) (unit-Group G)))
        ( preserves-inv-ev-formal-combination-subset-Group u)) ∙
        ( ( ap
          ( mul-Group G (inv-Group G (ev-formal-combination-subset-Group u)))
          ( right-unit-law-mul-Group G (inv-Group G (inclusion-subtype S x)))) ∙
          ( inv
            ( distributive-inv-mul-Group G
              (inclusion-subtype S x)
              ( ev-formal-combination-subset-Group u)))))

The subgroup generated by a subset of a group

  subset-subgroup-subset-Group' : type-Group G → UU (l1 ⊔ l2)
  subset-subgroup-subset-Group' x =
    fiber ev-formal-combination-subset-Group x

  subset-subgroup-subset-Group : subset-Group (l1 ⊔ l2) G
  subset-subgroup-subset-Group x =
    trunc-Prop (subset-subgroup-subset-Group' x)

  is-in-subgroup-subset-Group : type-Group G → UU (l1 ⊔ l2)
  is-in-subgroup-subset-Group x =
    type-Prop (subset-subgroup-subset-Group x)

  contains-unit-subgroup-subset-Group :
    contains-unit-subset-Group G subset-subgroup-subset-Group
  contains-unit-subgroup-subset-Group = unit-trunc-Prop (pair nil refl)

  is-closed-under-multiplication-subgroup-subset-Group' :
    (x y : type-Group G) →
    subset-subgroup-subset-Group' x → subset-subgroup-subset-Group' y →
    subset-subgroup-subset-Group' (mul-Group G x y)
  pr1
    ( is-closed-under-multiplication-subgroup-subset-Group' x y
      ( pair l p) (pair k q)) =
    concat-list l k
  pr2
    ( is-closed-under-multiplication-subgroup-subset-Group' x y
      ( pair l p) (pair k q)) =
    ( preserves-concat-ev-formal-combination-subset-Group l k) ∙
      ( ap-mul-Group G p q)

  is-closed-under-multiplication-subgroup-subset-Group :
    is-closed-under-multiplication-subset-Group G subset-subgroup-subset-Group
  is-closed-under-multiplication-subgroup-subset-Group x y H K =
    apply-universal-property-trunc-Prop H
      ( subset-subgroup-subset-Group (mul-Group G x y))
      ( λ H' →
        apply-universal-property-trunc-Prop K
          ( subset-subgroup-subset-Group (mul-Group G x y))
          ( λ K' →
            unit-trunc-Prop
              ( is-closed-under-multiplication-subgroup-subset-Group'
                  x y H' K')))

  is-closed-under-inverses-subgroup-subset-Group' :
    (x : type-Group G) →
    subset-subgroup-subset-Group' x →
    subset-subgroup-subset-Group' (inv-Group G x)
  pr1 (is-closed-under-inverses-subgroup-subset-Group' x (pair l p)) =
    inv-formal-combination-subset-Group l
  pr2 (is-closed-under-inverses-subgroup-subset-Group' x (pair l p)) =
    ( preserves-inv-ev-formal-combination-subset-Group l) ∙
      ( ap (inv-Group G) p)

  is-closed-under-inverses-subgroup-subset-Group :
    is-closed-under-inverses-subset-Group G subset-subgroup-subset-Group
  is-closed-under-inverses-subgroup-subset-Group x H =
    apply-universal-property-trunc-Prop H
      ( subset-subgroup-subset-Group (inv-Group G x))
      ( unit-trunc-Prop ∘ is-closed-under-inverses-subgroup-subset-Group' x)

  subgroup-subset-Group : Subgroup (l1 ⊔ l2) G
  pr1 subgroup-subset-Group = subset-subgroup-subset-Group
  pr1 (pr2 subgroup-subset-Group) = contains-unit-subgroup-subset-Group
  pr1 (pr2 (pr2 subgroup-subset-Group)) =
    is-closed-under-multiplication-subgroup-subset-Group
  pr2 (pr2 (pr2 subgroup-subset-Group)) =
    is-closed-under-inverses-subgroup-subset-Group

  contains-subset-subgroup-subset-Group :
    S ⊆ subset-subgroup-subset-Group
  contains-subset-subgroup-subset-Group s H =
    unit-trunc-Prop
      ( pair
        ( unit-list (pair (inr star) (pair s H)))
        ( right-unit-law-mul-Group G (inclusion-subtype S (pair s H))))

  contains-formal-combinations-Subgroup :
    {l3 : Level} (U : Subgroup l3 G) → S ⊆ subset-Subgroup G U →
    (x : formal-combination-subset-Group) →
    is-in-Subgroup G U (ev-formal-combination-subset-Group x)
  contains-formal-combinations-Subgroup U H nil =
    contains-unit-Subgroup G U
  contains-formal-combinations-Subgroup U H
    ( cons (pair (inl (inr star)) (pair s K)) c) =
    is-closed-under-multiplication-Subgroup G U
      ( inv-Group G (inclusion-subtype S (pair s K)))
      ( ev-formal-combination-subset-Group c)
      ( is-closed-under-inverses-Subgroup G U s (H s K))
      ( contains-formal-combinations-Subgroup U H c)
  contains-formal-combinations-Subgroup
    ( U)
    ( H)
    ( cons (pair (inr star) (pair s K)) c) =
    is-closed-under-multiplication-Subgroup G U
      ( inclusion-subtype S (pair s K))
      ( ev-formal-combination-subset-Group c)
      ( H s K)
      ( contains-formal-combinations-Subgroup U H c)

  is-subgroup-generated-by-subset-subgroup-subset-Group :
    is-subgroup-generated-by-subset-Group G S
      ( subgroup-subset-Group)
      ( contains-subset-subgroup-subset-Group)
  is-subgroup-generated-by-subset-subgroup-subset-Group U' K x H =
    apply-universal-property-trunc-Prop H (subset-Subgroup G U' x) P
    where
    P : subset-subgroup-subset-Group' x → is-in-Subgroup G U' x
    P (pair c refl) = contains-formal-combinations-Subgroup U' K c

The subset relation is preserved by generating subgroups

module _
  {l1 : Level} (G : Group l1)
  where

  preserves-order-subgroup-subset-Group :
    {l2 l3 : Level} (S : subset-Group l2 G) (T : subset-Group l3 G) →
    S ⊆ T →
    leq-Subgroup G (subgroup-subset-Group G S) (subgroup-subset-Group G T)
  preserves-order-subgroup-subset-Group S T H =
    is-subgroup-generated-by-subset-subgroup-subset-Group G S
      ( subgroup-subset-Group G T)
      ( transitive-leq-subtype
        ( S)
        ( T)
        ( subset-subgroup-subset-Group G T)
        ( contains-subset-subgroup-subset-Group G T)
        ( H))

  subgroup-subset-hom-large-poset-Group :
    hom-set-Large-Poset
      ( λ l2 → l1 ⊔ l2)
      ( powerset-Large-Poset (type-Group G))
      ( Subgroup-Large-Poset G)
  subgroup-subset-hom-large-poset-Group =
    make-hom-Large-Preorder
      ( subgroup-subset-Group G)
      ( preserves-order-subgroup-subset-Group)

The Galois connection S ↦ (S)

module _
  {l1 : Level} (G : Group l1)
  where

  adjoint-relation-subgroup-subset-Group :
    {l2 : Level} (S : subset-Group l2 G) →
    adjoint-relation-subgroup-generated-by-subset-Group G S
      ( subgroup-subset-Group G S)
  adjoint-relation-subgroup-subset-Group S =
    adjoint-relation-is-subgroup-generated-by-subset-Group G S
      ( subgroup-subset-Group G S)
      ( contains-subset-subgroup-subset-Group G S)
      ( is-subgroup-generated-by-subset-subgroup-subset-Group G S)

  subgroup-subset-galois-connection-Group :
    galois-connection-Large-Poset
      ( λ l2 → l1 ⊔ l2)
      ( id)
      ( powerset-Large-Poset (type-Group G))
      ( Subgroup-Large-Poset G)
  lower-adjoint-galois-connection-Large-Poset
    subgroup-subset-galois-connection-Group =
    subgroup-subset-hom-large-poset-Group G
  upper-adjoint-galois-connection-Large-Poset
    subgroup-subset-galois-connection-Group =
    subset-subgroup-hom-large-poset-Group G
  adjoint-relation-galois-connection-Large-Poset
    subgroup-subset-galois-connection-Group S =
    adjoint-relation-subgroup-subset-Group S

Properties

If S is closed under conjugation, then (S) is normal

module _
  {l1 l2 : Level} (G : Group l1)
  (S : subset-Group l2 G) (H : is-closed-under-conjugation-subset-Group G S)
  where

  conjugation-formal-combination-subset-Group :
    type-Group G →
    formal-combination-subset-Group G S → formal-combination-subset-Group G S
  conjugation-formal-combination-subset-Group x nil = nil
  conjugation-formal-combination-subset-Group x (cons (b , y , s) z) =
    cons
      ( (b , conjugation-Group G x y , H x y s))
      ( conjugation-formal-combination-subset-Group x z)

  preserves-conjugation-ev-formal-combination-subset-Group :
    (x : type-Group G) (l : formal-combination-subset-Group G S) →
    ev-formal-combination-subset-Group G S
      ( conjugation-formal-combination-subset-Group x l) ＝
    conjugation-Group G x (ev-formal-combination-subset-Group G S l)
  preserves-conjugation-ev-formal-combination-subset-Group x nil =
    inv (conjugation-unit-Group G x)
  preserves-conjugation-ev-formal-combination-subset-Group x
    ( cons (inl (inr star) , y , s) l) =
    ( ap-mul-Group G
      ( inv (conjugation-inv-Group G x y))
      ( preserves-conjugation-ev-formal-combination-subset-Group x l)) ∙
    ( inv
      ( distributive-conjugation-mul-Group G x
        ( inv-Group G y)
        ( ev-formal-combination-subset-Group G S l)))
  preserves-conjugation-ev-formal-combination-subset-Group x
    ( cons (inr star , y , s) l) =
    ( ap
      ( mul-Group G (conjugation-Group G x y))
      ( preserves-conjugation-ev-formal-combination-subset-Group x l)) ∙
    ( inv
      ( distributive-conjugation-mul-Group G x y
        ( ev-formal-combination-subset-Group G S l)))

  is-normal-is-closed-under-conjugation-subgroup-subset-Group' :
    (x y : type-Group G) → subset-subgroup-subset-Group' G S y →
    subset-subgroup-subset-Group' G S (conjugation-Group G x y)
  pr1
    ( is-normal-is-closed-under-conjugation-subgroup-subset-Group' x ._
      ( l , refl)) =
    conjugation-formal-combination-subset-Group x l
  pr2
    ( is-normal-is-closed-under-conjugation-subgroup-subset-Group' x ._
      ( l , refl)) =
    preserves-conjugation-ev-formal-combination-subset-Group x l

  is-normal-is-closed-under-conjugation-subgroup-subset-Group :
    is-normal-Subgroup G (subgroup-subset-Group G S)
  is-normal-is-closed-under-conjugation-subgroup-subset-Group x (y , h) =
    apply-universal-property-trunc-Prop h
      ( subset-subgroup-subset-Group G S (conjugation-Group G x y))
      ( unit-trunc-Prop ∘
        is-normal-is-closed-under-conjugation-subgroup-subset-Group' x y)

Recent changes