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-11-24.

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.images-subtypes
open import foundation.logical-equivalences
open import foundation.powersets
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.pullbacks-subtypes
open import foundation.singleton-subtypes
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.homomorphisms-groups
open import group-theory.images-of-group-homomorphisms
open import group-theory.normal-subgroups
open import group-theory.pullbacks-subgroups
open import group-theory.subgroups
open import group-theory.subsets-groups
open import group-theory.trivial-subgroups

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

open import order-theory.commuting-squares-of-galois-connections-large-posets
open import order-theory.commuting-squares-of-order-preserving-maps-large-posets
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 order-theory.similarity-of-elements-large-posets
open import order-theory.similarity-of-order-preserving-maps-large-posets

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)
  where

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

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

  contains-subgroup-generated-by-subset-is-subgroup-generated-by-sbset-Group :
    (α : is-subgroup-generated-by-subset-Group) 
    {l : Level} (U' : Subgroup l G)  (S  subset-Subgroup G U') 
    leq-Subgroup G U U'
  contains-subgroup-generated-by-subset-is-subgroup-generated-by-sbset-Group
    α U' =
    backward-implication (α U')

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 (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 (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 (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 (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 (s , x) u) =
    concat-list
      ( inv-formal-combination-subset-Group u)
      ( unit-list (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 (inl (inr star) , x) u) =
    ( preserves-concat-ev-formal-combination-subset-Group
      ( inv-formal-combination-subset-Group u)
      ( unit-list (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))
  preserves-inv-ev-formal-combination-subset-Group
    ( cons (inr star , x) u) =
    ( preserves-concat-ev-formal-combination-subset-Group
      ( inv-formal-combination-subset-Group u)
      ( unit-list (inl (inr star) , x))) 
    ( ap
      ( mul-Group' G
        ( 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))

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 (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' (l , p) (k , q)) =
    concat-list l k
  pr2 (is-closed-under-multiplication-subgroup-subset-Group' (l , p) (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 H K =
    apply-twice-universal-property-trunc-Prop H K
      ( subset-subgroup-subset-Group _)
      ( λ H' K' 
        unit-trunc-Prop
          ( is-closed-under-multiplication-subgroup-subset-Group' 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' (l , p)) =
    inv-formal-combination-subset-Group l
  pr2 (is-closed-under-inverses-subgroup-subset-Group' (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 H =
    apply-universal-property-trunc-Prop H
      ( subset-subgroup-subset-Group _)
      ( unit-trunc-Prop  is-closed-under-inverses-subgroup-subset-Group')

  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
      ( ( unit-list (inr star , s , H)) ,
        ( right-unit-law-mul-Group G (inclusion-subtype S (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 (inl (inr star) , s , K) c) =
    is-closed-under-multiplication-Subgroup G U
      ( is-closed-under-inverses-Subgroup G U (H s K))
      ( contains-formal-combinations-Subgroup U H c)
  contains-formal-combinations-Subgroup U H (cons (inr star , s , K) c) =
    is-closed-under-multiplication-Subgroup G U
      ( H s K)
      ( contains-formal-combinations-Subgroup U H c)

  leq-subgroup-subset-Group :
    {l : Level} (U : Subgroup l G)  (S  subset-Subgroup G U) 
    leq-Subgroup G subgroup-subset-Group U
  leq-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 (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 =
    leq-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))

  has-same-elements-subgroup-subset-has-same-elements-subset-Group :
    {l2 l3 : Level} (S : subset-Group l2 G) (T : subset-Group l3 G) 
    has-same-elements-subtype S T 
    has-same-elements-Subgroup G
      ( subgroup-subset-Group G S)
      ( subgroup-subset-Group G T)
  pr1
    ( has-same-elements-subgroup-subset-has-same-elements-subset-Group S T H x)
    =
    preserves-order-subgroup-subset-Group S T (forward-implication  H) x
  pr2
    ( has-same-elements-subgroup-subset-has-same-elements-subset-Group S T H x)
    =
    preserves-order-subgroup-subset-Group T S (backward-implication  H) x

  subgroup-subset-hom-large-poset-Group :
    hom-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

  is-subgroup-generated-by-subset-subgroup-subset-Group :
    {l2 : Level} (S : subset-Group l2 G) 
    is-subgroup-generated-by-subset-Group G S
      ( subgroup-subset-Group G S)
  pr1 (is-subgroup-generated-by-subset-subgroup-subset-Group S U) H =
    transitive-leq-subtype S
      ( subset-subgroup-subset-Group G S)
      ( subset-Subgroup G U)
      ( H)
      ( contains-subset-subgroup-subset-Group G S)
  pr2 (is-subgroup-generated-by-subset-subgroup-subset-Group S U) =
    leq-subgroup-subset-Group G S U

  subgroup-subset-galois-connection-Group :
    galois-connection-Large-Poset
      ( λ l2  l1  l2)
      ( λ l  l)
      ( 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 =
    is-subgroup-generated-by-subset-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)

Any subgroup H of G has the same elements as ⟨S⟩ if and only if H is generated by S

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

  is-subgroup-generated-by-subset-has-same-elements-Subgroup :
    has-same-elements-Subgroup G (subgroup-subset-Group G S) H 
    is-subgroup-generated-by-subset-Group G S H
  is-subgroup-generated-by-subset-has-same-elements-Subgroup s =
    is-lower-element-sim-galois-connection-Large-Poset
      ( powerset-Large-Poset (type-Group G))
      ( Subgroup-Large-Poset G)
      ( subgroup-subset-galois-connection-Group G)
      ( S)
      ( H)
      ( similar-has-same-elements-Subgroup G (subgroup-subset-Group G S) H s)

  is-subgroup-generated-by-subset-has-same-elements-Subgroup' :
    has-same-elements-Subgroup G H (subgroup-subset-Group G S) 
    is-subgroup-generated-by-subset-Group G S H
  is-subgroup-generated-by-subset-has-same-elements-Subgroup' s =
    is-lower-element-sim-galois-connection-Large-Poset
      ( powerset-Large-Poset (type-Group G))
      ( Subgroup-Large-Poset G)
      ( subgroup-subset-galois-connection-Group G)
      ( S)
      ( H)
      ( symmetric-sim-Large-Poset
        ( Subgroup-Large-Poset G)
        ( H)
        ( subgroup-subset-Group G S)
        ( similar-has-same-elements-Subgroup G H (subgroup-subset-Group G S) s))

  has-same-elements-is-subgroup-generated-by-subset-Subgroup :
    is-subgroup-generated-by-subset-Group G S H 
    has-same-elements-Subgroup G (subgroup-subset-Group G S) H
  has-same-elements-is-subgroup-generated-by-subset-Subgroup g =
    has-same-elements-similar-Subgroup G
      ( subgroup-subset-Group G S)
      ( H)
      ( sim-is-lower-element-galois-connection-Large-Poset
        ( powerset-Large-Poset (type-Group G))
        ( Subgroup-Large-Poset G)
        ( subgroup-subset-galois-connection-Group G)
        ( S)
        ( H)
        ( g))

If f : G → H is a group homomorphism, then im f ⟨S⟩ = ⟨im f S⟩

There are three ways to state this fact:

  1. The subgroup im f ⟨S⟩ has the same elements as the subgroup ⟨im f S⟩.
  2. The subgroup ⟨im f S⟩ satisfies the universal property of the image of the group ⟨S⟩ under the group homomorphism f.
  3. The subgroup im f ⟨S⟩ satisfies the universal property of the subgroup generated by the subset im f S of H.

Proof: We prove the first statement. Note that the square

                    pullback f
   subset-Group G <------------ subset-Group H
         ∧                            ∧
         |                            |
  K ↦ UK |                            | K ↦ UK
         |                            |
     Subgroup G <---------------- Subgroup H
                    pullback f

commutes by reflexivity. By the adjointness relations of Galois connections, this implies that the square

                    im f
    subset-Group G ------> subset-Group H
          |                      |
  S ↦ ⟨S⟩ |                      | S ↦ ⟨S⟩
          |                      |
          V                      V
      Subgroup G ----------> Subgroup H
                    im f

commutes. The remaining two statements follow directly from the fact that if a subgroup has the same elements as the image of a subgroup (resp. the subgroup generated by a subset), then it satisfies the universal property of the image of a subgroup (resp. the subgroup generated by a subset).

module _
  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
  where

  coherence-square-image-subgroup-subset-Group :
    coherence-square-hom-Large-Poset
      ( powerset-Large-Poset (type-Group G))
      ( Subgroup-Large-Poset G)
      ( powerset-Large-Poset (type-Group H))
      ( Subgroup-Large-Poset H)
      ( im-subtype-hom-Large-Poset (map-hom-Group G H f))
      ( subgroup-subset-hom-large-poset-Group G)
      ( subgroup-subset-hom-large-poset-Group H)
      ( im-subgroup-hom-large-poset-hom-Group G H f)
  coherence-square-image-subgroup-subset-Group =
    lower-coherence-square-upper-coherence-square-galois-connection-Large-Poset
      ( powerset-Large-Poset (type-Group G))
      ( Subgroup-Large-Poset G)
      ( powerset-Large-Poset (type-Group H))
      ( Subgroup-Large-Poset H)
      ( image-pullback-subtype-galois-connection-Large-Poset
        ( map-hom-Group G H f))
      ( subgroup-subset-galois-connection-Group G)
      ( subgroup-subset-galois-connection-Group H)
      ( image-pullback-galois-connection-Subgroup G H f)
      ( coherence-square-pullback-subset-Subgroup G H f)

  compute-image-subgroup-subset-Group :
    {l3 : Level} (S : subset-Group l3 G) 
    has-same-elements-Subgroup H
      ( im-hom-Subgroup G H f (subgroup-subset-Group G S))
      ( subgroup-subset-Group H (im-subtype (map-hom-Group G H f) S))
  compute-image-subgroup-subset-Group S =
    has-same-elements-similar-Subgroup H
      ( im-hom-Subgroup G H f (subgroup-subset-Group G S))
      ( subgroup-subset-Group H (im-subtype (map-hom-Group G H f) S))
      ( coherence-square-image-subgroup-subset-Group S)

  is-subgroup-generated-by-subset-image-subgroup-subset-Group :
    {l3 : Level} (S : subset-Group l3 G) 
    is-subgroup-generated-by-subset-Group H
      ( im-subtype (map-hom-Group G H f) S)
      ( im-hom-Subgroup G H f (subgroup-subset-Group G S))
  is-subgroup-generated-by-subset-image-subgroup-subset-Group S =
    is-subgroup-generated-by-subset-has-same-elements-Subgroup' H
      ( im-subtype (map-hom-Group G H f) S)
      ( im-hom-Subgroup G H f (subgroup-subset-Group G S))
      ( compute-image-subgroup-subset-Group S)

  is-image-im-subgroup-subset-Group :
    {l3 : Level} (S : subset-Group l3 G) 
    is-image-subgroup-hom-Group G H f
      ( subgroup-subset-Group G S)
      ( subgroup-subset-Group H (im-subtype (map-hom-Group G H f) S))
  is-image-im-subgroup-subset-Group S =
    is-image-subgroup-has-same-elements-Subgroup G H f
      ( subgroup-subset-Group G S)
      ( subgroup-subset-Group H (im-subtype (map-hom-Group G H f) S))
      ( compute-image-subgroup-subset-Group S)

The subgroup ⟨S⟩ is trivial if and only if S ⊆ {e}

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

  is-trivial-subgroup-subset-Group :
    S  subtype-standard-singleton-subtype (set-Group G) (unit-Group G) 
    is-trivial-Subgroup G (subgroup-subset-Group G S)
  is-trivial-subgroup-subset-Group =
    leq-subgroup-subset-Group G S (trivial-Subgroup G)

  leq-singleton-subtype-unit-is-trivial-subgroup-subset-Group :
    is-trivial-Subgroup G (subgroup-subset-Group G S) 
    S  subtype-standard-singleton-subtype (set-Group G) (unit-Group G)
  leq-singleton-subtype-unit-is-trivial-subgroup-subset-Group H =
    transitive-leq-subtype S
      ( subset-subgroup-subset-Group G S)
      ( subtype-standard-singleton-subtype (set-Group G) (unit-Group G))
      ( H)
      ( contains-subset-subgroup-subset-Group G S)

Recent changes