# Subgroups generated by families of elements

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-13.

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)