Subgroups generated by elements of a group

Content created by Egbert Rijke and Fredrik Bakke

Created on 2023-07-20.
Last modified on 2023-09-12.

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.identity-types
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.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

Idea

The subgroup generated by an element g of a group G is the subgroup generated by the standard singleton subset {g}. In other words, it is the least subgroup of G that contains the element g.

Definitions

The predicate of being a subgroup generated by an element

module _
  {l1 : Level} (G : Group l1) (g : 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 g ↔ 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 g
  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 g → 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) (g : type-Group G)
  where

  subgroup-element-Group : Subgroup l1 G
  subgroup-element-Group =
    subgroup-subset-Group G
      ( subtype-standard-singleton-subtype (set-Group G) g)

  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 :
    {x y : type-Group G} → is-in-subgroup-element-Group x →
    x ＝ y → is-in-subgroup-element-Group y
  is-closed-under-eq-subgroup-element-Group =
    is-closed-under-eq-Subgroup G subgroup-element-Group

  is-closed-under-eq-subgroup-element-Group' :
    {x y : type-Group G} → is-in-subgroup-element-Group y →
    x ＝ y → is-in-subgroup-element-Group x
  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-inv-subgroup-element-Group :
    is-closed-under-inv-subset-Group G subset-subgroup-element-Group
  is-closed-under-inv-subgroup-element-Group =
    is-closed-under-inv-Subgroup G subgroup-element-Group

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

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

  abstract
    leq-subgroup-element-Group :
      {l : Level} (H : Subgroup l G) →
      is-in-Subgroup G H g → 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) (g : type-Group G)
  where

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

  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 :
    {x y : type-Group G} → is-in-image-hom-element-Group x →
    x ＝ y → 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-closed-under-eq-image-hom-element-Group' :
    {x y : type-Group G} → is-in-image-hom-element-Group y →
    x ＝ y → is-in-image-hom-element-Group x
  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 g) image-hom-element-Group
  is-image-image-hom-element-Group =
    is-image-image-hom-Group ℤ-Group G (hom-element-Group G g)

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

  contains-element-image-hom-element-Group :
    is-in-image-hom-element-Group g
  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 g)

  leq-image-hom-element-Group :
    {l : Level} (H : Subgroup l G) →
    is-in-Subgroup G H g → 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 g)
      ( H)
      ( λ k → is-closed-under-powers-int-Subgroup G H k g u)

  is-subgroup-generated-by-element-image-hom-element-Group :
    is-subgroup-generated-by-element-Group G g 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 g 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) (g : type-Group G)
  where

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

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

module _
  {l1 l2 l3 : Level} (G : Group l1) (g : type-Group G)
  (H : Subgroup l2 G) (Hu : is-subgroup-generated-by-element-Group G g H)
  (K : Subgroup l3 G) (Ku : is-subgroup-generated-by-element-Group G g 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 x) =
    leq-subgroup-is-subgroup-generated-by-element-Group G g H K Hu
      ( contains-element-is-subgroup-generated-by-element-Group G g K Ku)
      ( x)
  pr2 (has-same-elements-is-subgroup-generated-by-element-Group x) =
    leq-subgroup-is-subgroup-generated-by-element-Group G g K H Ku
      ( contains-element-is-subgroup-generated-by-element-Group G g H Hu)
      ( 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) (g : type-Group G)
  where

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

Recent changes