Subgroups generated by families of elements

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-13.
Last modified on 2023-11-24.

module group-theory.subgroups-generated-by-families-of-elements-groups where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.images
open import foundation.images-subtypes
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.subtypes
open import foundation.universal-property-image
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.images-of-group-homomorphisms
open import group-theory.subgroups
open import group-theory.subgroups-generated-by-subsets-groups
open import group-theory.subsets-groups
open import group-theory.trivial-subgroups

Idea

Consider a family (xᵢ)ᵢ of elements in a group G. The subgroup generated by (xᵢ)ᵢ is the subgroup generated by the subset of all the elements of the form xᵢ for some i in the indexing type of (xᵢ)ᵢ. In other words, the subgroup generated by (xᵢ)ᵢ is the least subgroup that contains all the elements xᵢ. In informal writing, the subgroup generated by the family of elements (xᵢ)ᵢ is denoted by ⟨xᵢ⟩

Definitions

The predicate of being a subgroup generated by a family of elements

module _
  {l1 l2 l3 : Level} (G : Group l1) {I : UU l2} (x : I → type-Group G)
  (H : Subgroup l3 G)
  where

  is-subgroup-generated-by-family-of-elements-Group : UUω
  is-subgroup-generated-by-family-of-elements-Group =
    {l4 : Level} (K : Subgroup l4 G) →
    leq-Subgroup G H K ↔ ((i : I) → is-in-Subgroup G K (x i))

  contains-element-is-subgroup-generated-by-family-of-elements-Group :
    is-subgroup-generated-by-family-of-elements-Group →
    (i : I) → is-in-Subgroup G H (x i)
  contains-element-is-subgroup-generated-by-family-of-elements-Group
    U =
    forward-implication (U H) (refl-leq-Subgroup G H)

  leq-subgroup-is-subgroup-generated-by-family-of-elements-Group :
    is-subgroup-generated-by-family-of-elements-Group →
    {l4 : Level} (K : Subgroup l4 G) (k : (i : I) → is-in-Subgroup G K (x i)) →
    leq-Subgroup G H K
  leq-subgroup-is-subgroup-generated-by-family-of-elements-Group U K =
    backward-implication (U K)

The subgroup generated by a family of elements in a group

module _
  {l1 l2 : Level} (G : Group l1) {I : UU l2} (x : I → type-Group G)
  where

  generating-subset-subgroup-family-of-elements-Group : subset-Group (l1 ⊔ l2) G
  generating-subset-subgroup-family-of-elements-Group = subtype-im x

  subgroup-family-of-elements-Group : Subgroup (l1 ⊔ l2) G
  subgroup-family-of-elements-Group =
    subgroup-subset-Group G generating-subset-subgroup-family-of-elements-Group

  subset-subgroup-family-of-elements-Group : subset-Group (l1 ⊔ l2) G
  subset-subgroup-family-of-elements-Group =
    subset-Subgroup G subgroup-family-of-elements-Group

  is-in-subgroup-family-of-elements-Group : type-Group G → UU (l1 ⊔ l2)
  is-in-subgroup-family-of-elements-Group =
    is-in-Subgroup G subgroup-family-of-elements-Group

  is-closed-under-eq-subgroup-family-of-elements-Group :
    {x y : type-Group G} → is-in-subgroup-family-of-elements-Group x →
    x ＝ y → is-in-subgroup-family-of-elements-Group y
  is-closed-under-eq-subgroup-family-of-elements-Group =
    is-closed-under-eq-Subgroup G subgroup-family-of-elements-Group

  is-closed-under-eq-subgroup-family-of-elements-Group' :
    {x y : type-Group G} → is-in-subgroup-family-of-elements-Group y →
    x ＝ y → is-in-subgroup-family-of-elements-Group x
  is-closed-under-eq-subgroup-family-of-elements-Group' =
    is-closed-under-eq-Subgroup' G subgroup-family-of-elements-Group

  contains-unit-subgroup-family-of-elements-Group :
    contains-unit-subset-Group G subset-subgroup-family-of-elements-Group
  contains-unit-subgroup-family-of-elements-Group =
    contains-unit-Subgroup G subgroup-family-of-elements-Group

  is-closed-under-multiplication-subgroup-family-of-elements-Group :
    is-closed-under-multiplication-subset-Group G
      subset-subgroup-family-of-elements-Group
  is-closed-under-multiplication-subgroup-family-of-elements-Group =
    is-closed-under-multiplication-Subgroup G subgroup-family-of-elements-Group

  is-closed-under-inverses-subgroup-family-of-elements-Group :
    is-closed-under-inverses-subset-Group G
      subset-subgroup-family-of-elements-Group
  is-closed-under-inverses-subgroup-family-of-elements-Group =
    is-closed-under-inverses-Subgroup G subgroup-family-of-elements-Group

  abstract
    is-subgroup-generated-by-family-of-elements-subgroup-family-of-elements-Group :
      is-subgroup-generated-by-family-of-elements-Group G x
        subgroup-family-of-elements-Group
    is-subgroup-generated-by-family-of-elements-subgroup-family-of-elements-Group
      H =
      logical-equivalence-reasoning
        leq-Subgroup G subgroup-family-of-elements-Group H
        ↔ generating-subset-subgroup-family-of-elements-Group ⊆
          subset-Subgroup G H
          by
          is-subgroup-generated-by-subset-subgroup-subset-Group G
            ( subtype-im x)
            ( H)
        ↔ ((i : I) → is-in-Subgroup G H (x i))
          by is-image-subtype-subtype-im x (subset-Subgroup G H)

  abstract
    contains-element-subgroup-family-of-elements-Group :
      (i : I) → is-in-subgroup-family-of-elements-Group (x i)
    contains-element-subgroup-family-of-elements-Group i =
      contains-subset-subgroup-subset-Group G
        ( generating-subset-subgroup-family-of-elements-Group)
        ( x i)
        ( unit-trunc-Prop (i , refl))

  abstract
    leq-subgroup-family-of-elements-Group :
      {l : Level} (H : Subgroup l G) →
      ((i : I) → is-in-Subgroup G H (x i)) →
      leq-Subgroup G subgroup-family-of-elements-Group H
    leq-subgroup-family-of-elements-Group H =
      backward-implication
        ( is-subgroup-generated-by-family-of-elements-subgroup-family-of-elements-Group
          H)

Properties

Any two subgroups generated by the same family of elements contain the same elements

module _
  {l1 l2 l3 l4 : Level} (G : Group l1) {I : UU l2} (x : I → type-Group G)
  (H : Subgroup l3 G)
  (Hu : is-subgroup-generated-by-family-of-elements-Group G x H)
  (K : Subgroup l4 G)
  (Ku : is-subgroup-generated-by-family-of-elements-Group G x K)
  where

  has-same-elements-is-subgroup-generated-by-family-of-elements-Group :
    has-same-elements-Subgroup G H K
  pr1 (has-same-elements-is-subgroup-generated-by-family-of-elements-Group y) =
    leq-subgroup-is-subgroup-generated-by-family-of-elements-Group G x H Hu K
      ( contains-element-is-subgroup-generated-by-family-of-elements-Group G x
        ( K)
        ( Ku))
      ( y)
  pr2 (has-same-elements-is-subgroup-generated-by-family-of-elements-Group y) =
    leq-subgroup-is-subgroup-generated-by-family-of-elements-Group G x K Ku H
      ( contains-element-is-subgroup-generated-by-family-of-elements-Group G x
        ( H)
        ( Hu))
      ( y)

Any subgroup that has the same elements as the subgroup generated by a family of elements x satisfies the universal property of the subgroup generated by the family of elements x

module _
  {l1 l2 l3 : Level} (G : Group l1) {I : UU l2} (x : I → type-Group G)
  (H : Subgroup l3 G)
  where

  is-subgroup-generated-by-family-of-elements-has-same-elements-Subgroup :
    has-same-elements-Subgroup G (subgroup-family-of-elements-Group G x) H →
    is-subgroup-generated-by-family-of-elements-Group G x H
  is-subgroup-generated-by-family-of-elements-has-same-elements-Subgroup p U =
    logical-equivalence-reasoning
      leq-Subgroup G H U
      ↔ subtype-im x ⊆ subset-Subgroup G U
        by
        is-subgroup-generated-by-subset-has-same-elements-Subgroup G
          ( subtype-im x)
          ( H)
          ( p)
          ( U)
      ↔ ((i : I) → is-in-Subgroup G U (x i))
        by
        is-image-subtype-subtype-im x (subset-Subgroup G U)

The image of the subgroup ⟨x⟩ generated by a family of elements x under a group homomorphism f is the subgroup ⟨f ∘ x⟩ generated by the family of elements f ∘ x

There are three ways to state this fact:

  1. The image of the subgroup ⟨x⟩ under the group homomorphism f has the same elements as the subgroup ⟨f ∘ x⟩.
  2. The subgroup ⟨f ∘ x⟩ satisfies the universal property of the image of the group ⟨x⟩ under the group homomorphism f.
  3. The image of the subgroup ⟨x⟩ under the group homomorphism f satisfies the universal property of the subgroup generated by the family of elements f ∘ x.
module _
  {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
  {I : UU l3} (x : I → type-Group G)
  where

  compute-image-subgroup-family-of-elements-Group :
    has-same-elements-Subgroup H
      ( im-hom-Subgroup G H f (subgroup-family-of-elements-Group G x))
      ( subgroup-family-of-elements-Group H (map-hom-Group G H f ∘ x))
  compute-image-subgroup-family-of-elements-Group h =
    logical-equivalence-reasoning
      is-in-im-hom-Subgroup G H f (subgroup-family-of-elements-Group G x) h
      ↔ is-in-subgroup-subset-Group H
          ( im-subtype (map-hom-Group G H f) (subtype-im x))
          ( h)
        by
        compute-image-subgroup-subset-Group G H f (subtype-im x) h
      ↔ is-in-subgroup-family-of-elements-Group H (map-hom-Group G H f ∘ x) h
        by
        inv-iff
          ( has-same-elements-subgroup-subset-has-same-elements-subset-Group H
            ( subtype-im (map-hom-Group G H f ∘ x))
            ( im-subtype (map-hom-Group G H f) (subtype-im x))
            ( compute-subtype-im-comp (map-hom-Group G H f) x)
            ( h))

  is-image-subgroup-family-of-elements-Group :
    is-image-subgroup-hom-Group G H f
      ( subgroup-family-of-elements-Group G x)
      ( subgroup-family-of-elements-Group H (map-hom-Group G H f ∘ x))
  is-image-subgroup-family-of-elements-Group =
    is-image-subgroup-has-same-elements-Subgroup G H f
      ( subgroup-family-of-elements-Group G x)
      ( subgroup-family-of-elements-Group H (map-hom-Group G H f ∘ x))
      ( compute-image-subgroup-family-of-elements-Group)

  is-subgroup-generated-by-family-of-elements-image-subgroup-family-of-elements-Group :
    is-subgroup-generated-by-family-of-elements-Group H
      ( map-hom-Group G H f ∘ x)
      ( im-hom-Subgroup G H f (subgroup-family-of-elements-Group G x))
  is-subgroup-generated-by-family-of-elements-image-subgroup-family-of-elements-Group =
    is-subgroup-generated-by-family-of-elements-has-same-elements-Subgroup H
      ( map-hom-Group G H f ∘ x)
      ( im-hom-Subgroup G H f (subgroup-family-of-elements-Group G x))
      ( inv-iff ∘ compute-image-subgroup-family-of-elements-Group)

The subgroup ⟨xᵢ⟩ is trivial if and only if unit-Group G ＝ xᵢ for every i

module _
  {l1 l2 : Level} (G : Group l1) {I : UU l2} (x : I → type-Group G)
  where

  is-trivial-subgroup-family-of-elements-Group :
    ((i : I) → is-unit-Group' G (x i)) →
    is-trivial-Subgroup G (subgroup-family-of-elements-Group G x)
  is-trivial-subgroup-family-of-elements-Group =
    leq-subgroup-family-of-elements-Group G x (trivial-Subgroup G)

  is-family-of-units-is-trivial-subgroup-family-of-elements-Group :
    is-trivial-Subgroup G (subgroup-family-of-elements-Group G x) →
    (i : I) → is-unit-Group' G (x i)
  is-family-of-units-is-trivial-subgroup-family-of-elements-Group H i =
    H (x i) (contains-element-subgroup-family-of-elements-Group G x i)

Recent changes