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 2024-04-25.
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:
- The subgroup
im f ⟨S⟩has the same elements as the subgroup⟨im f S⟩. - The subgroup
⟨im f S⟩satisfies the universal property of the image of the group⟨S⟩under the group homomorphismf. - The subgroup
im f ⟨S⟩satisfies the universal property of the subgroup generated by the subsetim f SofH.
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⟩
| |
∨ ∨
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
- 2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-10-19. Fredrik Bakke. Level-universe compatibility patch (#862).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).