Subgroups generated by elements of a group

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-07-20.
Last modified on 2023-11-24.

module group-theory.subgroups-generated-by-elements-groups where
Imports 
open import elementary-number-theory.group-of-integers
open import elementary-number-theory.integers

open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.images-subtypes
open import foundation.logical-equivalences
open import foundation.singleton-subtypes
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.free-groups-with-one-generator
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.images-of-group-homomorphisms
open import group-theory.integer-powers-of-elements-groups
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

The subgroup generated by an element x of a group G is the subgroup generated by the standard singleton subset {x}. In other words, it is the least subgroup of G that contains the element x. In informal writing, the subgroup generated by x is denoted by ⟨x⟩.

Definitions

The predicate of being a subgroup generated by an element

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

  is-subgroup-generated-by-element-Group :
    {l2 : Level} (H : Subgroup l2 G) → UUω
  is-subgroup-generated-by-element-Group H =
    {l : Level} (K : Subgroup l G) → is-in-Subgroup G K x ↔ leq-Subgroup G H K

  contains-element-is-subgroup-generated-by-element-Group :
    {l2 : Level} (H : Subgroup l2 G) →
    is-subgroup-generated-by-element-Group H →
    is-in-Subgroup G H x
  contains-element-is-subgroup-generated-by-element-Group H α =
    backward-implication (α H) (refl-leq-Subgroup G H)

  leq-subgroup-is-subgroup-generated-by-element-Group :
    {l2 l3 : Level} (H : Subgroup l2 G) (K : Subgroup l3 G) →
    is-subgroup-generated-by-element-Group H →
    is-in-Subgroup G K x → leq-Subgroup G H K
  leq-subgroup-is-subgroup-generated-by-element-Group H K α =
    forward-implication (α K)

The subgroup generated by an element of a group

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

  generating-subset-subgroup-element-Group : subset-Group l1 G
  generating-subset-subgroup-element-Group =
    subtype-standard-singleton-subtype (set-Group G) x

  subgroup-element-Group : Subgroup l1 G
  subgroup-element-Group =
    subgroup-subset-Group G generating-subset-subgroup-element-Group

  subset-subgroup-element-Group : subset-Group l1 G
  subset-subgroup-element-Group = subset-Subgroup G subgroup-element-Group

  is-in-subgroup-element-Group : type-Group G → UU l1
  is-in-subgroup-element-Group = is-in-Subgroup G subgroup-element-Group

  is-closed-under-eq-subgroup-element-Group :
    {y z : type-Group G} → is-in-subgroup-element-Group y →
    y ＝ z → is-in-subgroup-element-Group z
  is-closed-under-eq-subgroup-element-Group =
    is-closed-under-eq-Subgroup G subgroup-element-Group

  is-closed-under-eq-subgroup-element-Group' :
    {y z : type-Group G} → is-in-subgroup-element-Group z →
    y ＝ z → is-in-subgroup-element-Group y
  is-closed-under-eq-subgroup-element-Group' =
    is-closed-under-eq-Subgroup' G subgroup-element-Group

  contains-unit-subgroup-element-Group :
    contains-unit-subset-Group G subset-subgroup-element-Group
  contains-unit-subgroup-element-Group =
    contains-unit-Subgroup G subgroup-element-Group

  is-closed-under-multiplication-subgroup-element-Group :
    is-closed-under-multiplication-subset-Group G subset-subgroup-element-Group
  is-closed-under-multiplication-subgroup-element-Group =
    is-closed-under-multiplication-Subgroup G subgroup-element-Group

  is-closed-under-inverses-subgroup-element-Group :
    is-closed-under-inverses-subset-Group G subset-subgroup-element-Group
  is-closed-under-inverses-subgroup-element-Group =
    is-closed-under-inverses-Subgroup G subgroup-element-Group

  abstract
    is-subgroup-generated-by-element-subgroup-element-Group :
      is-subgroup-generated-by-element-Group G x subgroup-element-Group
    is-subgroup-generated-by-element-subgroup-element-Group H =
      logical-equivalence-reasoning
        is-in-Subgroup G H x
        ↔ ( subtype-standard-singleton-subtype (set-Group G) x ⊆
            subset-Subgroup G H)
          by
          inv-iff
            ( is-least-subtype-containing-element-Set
              ( set-Group G)
              ( x)
              ( subset-Subgroup G H))
        ↔ leq-Subgroup G subgroup-element-Group H
          by
          inv-iff
            ( is-subgroup-generated-by-subset-subgroup-subset-Group G
              ( subtype-standard-singleton-subtype (set-Group G) x)
              ( H))

  abstract
    contains-element-subgroup-element-Group :
      is-in-subgroup-element-Group x
    contains-element-subgroup-element-Group =
      contains-subset-subgroup-subset-Group G
        ( subtype-standard-singleton-subtype (set-Group G) x)
        ( x)
        ( refl)

  abstract
    leq-subgroup-element-Group :
      {l : Level} (H : Subgroup l G) →
      is-in-Subgroup G H x → leq-Subgroup G subgroup-element-Group H
    leq-subgroup-element-Group H =
      forward-implication
        ( is-subgroup-generated-by-element-subgroup-element-Group H)

The image of the initial group homomorphism f : ℤ → G such that f(1) ＝ g

An alternative definition of the subgroup generated by one element g is as the image of the initial group homomorphism f : ℤ → G that satisfies f(1) ＝ g.

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

  image-hom-element-Group : Subgroup l1 G
  image-hom-element-Group = image-hom-Group ℤ-Group G (hom-element-Group G x)

  subset-image-hom-element-Group : subset-Group l1 G
  subset-image-hom-element-Group =
    subset-Subgroup G image-hom-element-Group

  is-in-image-hom-element-Group : type-Group G → UU l1
  is-in-image-hom-element-Group = is-in-Subgroup G image-hom-element-Group

  is-closed-under-eq-image-hom-element-Group :
    {y z : type-Group G} → is-in-image-hom-element-Group y →
    y ＝ z → is-in-image-hom-element-Group z
  is-closed-under-eq-image-hom-element-Group =
    is-closed-under-eq-Subgroup G image-hom-element-Group

  is-closed-under-eq-image-hom-element-Group' :
    {y z : type-Group G} → is-in-image-hom-element-Group z →
    y ＝ z → is-in-image-hom-element-Group y
  is-closed-under-eq-image-hom-element-Group' =
    is-closed-under-eq-Subgroup' G image-hom-element-Group

  is-image-image-hom-element-Group :
    is-image-hom-Group ℤ-Group G (hom-element-Group G x) image-hom-element-Group
  is-image-image-hom-element-Group =
    is-image-image-hom-Group ℤ-Group G (hom-element-Group G x)

  contains-values-image-hom-element-Group :
    (k : ℤ) → is-in-image-hom-element-Group (map-hom-element-Group G x k)
  contains-values-image-hom-element-Group =
    contains-values-image-hom-Group ℤ-Group G (hom-element-Group G x)

  contains-element-image-hom-element-Group :
    is-in-image-hom-element-Group x
  contains-element-image-hom-element-Group =
    is-closed-under-eq-image-hom-element-Group
      ( contains-values-image-hom-element-Group one-ℤ)
      ( right-unit-law-mul-Group G x)

  leq-image-hom-element-Group :
    {l : Level} (H : Subgroup l G) →
    is-in-Subgroup G H x → leq-Subgroup G image-hom-element-Group H
  leq-image-hom-element-Group H u =
    leq-image-hom-Group
      ( ℤ-Group)
      ( G)
      ( hom-element-Group G x)
      ( H)
      ( λ k → is-closed-under-powers-int-Subgroup G H k x u)

  is-subgroup-generated-by-element-image-hom-element-Group :
    is-subgroup-generated-by-element-Group G x image-hom-element-Group
  pr1 (is-subgroup-generated-by-element-image-hom-element-Group K) =
    leq-image-hom-element-Group K
  pr2 (is-subgroup-generated-by-element-image-hom-element-Group K) u =
    u x contains-element-image-hom-element-Group

Properties

The subgroup generated by an element g contains all the integer powers gᵏ

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

  contains-powers-subgroup-element-Group :
    (k : ℤ) → is-in-subgroup-element-Group G x (integer-power-Group G k x)
  contains-powers-subgroup-element-Group k =
    is-closed-under-powers-int-Subgroup G
      ( subgroup-element-Group G x)
      ( k)
      ( x)
      ( contains-element-subgroup-element-Group G x)

Any two subgroups generated by the same element contain the same elements

module _
  {l1 l2 l3 : Level} (G : Group l1) (x : type-Group G)
  (H : Subgroup l2 G) (Hu : is-subgroup-generated-by-element-Group G x H)
  (K : Subgroup l3 G) (Ku : is-subgroup-generated-by-element-Group G x K)
  where

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

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

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

  is-subgroup-generated-by-element-has-same-elements-Subgroup :
    has-same-elements-Subgroup G (subgroup-element-Group G x) H →
    is-subgroup-generated-by-element-Group G x H
  pr1 (is-subgroup-generated-by-element-has-same-elements-Subgroup p U) u =
    transitive-leq-Subgroup G H (subgroup-element-Group G x) U
      ( forward-implication
        ( is-subgroup-generated-by-element-subgroup-element-Group G x U)
        ( u))
      ( leq-has-same-elements-Subgroup' G (subgroup-element-Group G x) H p)
  pr2 (is-subgroup-generated-by-element-has-same-elements-Subgroup p U) q =
    q x
      ( forward-implication (p x) (contains-element-subgroup-element-Group G x))

The subgroup generated by an element has the same elements as the image of the intial group homomorphism ℤ → G mapping 1 to g

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

  has-same-elements-image-hom-element-subgroup-element-Group :
    has-same-elements-Subgroup G
      ( image-hom-element-Group G x)
      ( subgroup-element-Group G x)
  has-same-elements-image-hom-element-subgroup-element-Group =
    has-same-elements-is-subgroup-generated-by-element-Group G x
      ( image-hom-element-Group G x)
      ( is-subgroup-generated-by-element-image-hom-element-Group G x)
      ( subgroup-element-Group G x)
      ( is-subgroup-generated-by-element-subgroup-element-Group G x)

The image of the subgroup ⟨x⟩ generated by x under a group homomorphism f is the subgroup ⟨f(x)⟩ generated by the element 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 element f x.
module _
  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
  (x : type-Group G)
  where

  compute-image-subgroup-element-Group :
    has-same-elements-Subgroup H
      ( im-hom-Subgroup G H f (subgroup-element-Group G x))
      ( subgroup-element-Group H (map-hom-Group G H f x))
  compute-image-subgroup-element-Group h =
    logical-equivalence-reasoning
      is-in-im-hom-Subgroup G H f (subgroup-element-Group G x) h
      ↔ is-in-subgroup-subset-Group H
          ( im-subtype
            ( map-hom-Group G H f)
            ( subtype-standard-singleton-subtype (set-Group G) x))
          ( h)
        by
        compute-image-subgroup-subset-Group G H f
          ( subtype-standard-singleton-subtype (set-Group G) x)
          ( h)
      ↔ is-in-subgroup-element-Group H (map-hom-Group G H f x) h
        by
        inv-iff
          ( has-same-elements-subgroup-subset-has-same-elements-subset-Group H
            ( generating-subset-subgroup-element-Group H _)
            ( im-subtype
              ( map-hom-Group G H f)
              ( subtype-standard-singleton-subtype (set-Group G) x))
            ( compute-im-singleton-subtype
              ( set-Group G)
              ( set-Group H)
              ( map-hom-Group G H f)
              ( x))
            ( h))

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

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

The subgroup ⟨x⟩ is trivial if and only if unit-Group G ＝ x

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

  is-trivial-subgroup-unit-Group :
    is-trivial-Subgroup G (subgroup-element-Group G (unit-Group G))
  is-trivial-subgroup-unit-Group =
    leq-subgroup-element-Group G (unit-Group G) (trivial-Subgroup G) refl

  is-trivial-subgroup-element-Group :
    (x : type-Group G) →
    is-unit-Group' G x → is-trivial-Subgroup G (subgroup-element-Group G x)
  is-trivial-subgroup-element-Group ._ refl = is-trivial-subgroup-unit-Group

  is-unit-is-trivial-subgroup-element-Group :
    (x : type-Group G) →
    is-trivial-Subgroup G (subgroup-element-Group G x) → is-unit-Group' G x
  is-unit-is-trivial-subgroup-element-Group x H =
    H x (contains-element-subgroup-element-Group G x)

Recent changes