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-09-26.
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.logical-equivalences open import foundation.powersets open import foundation.propositional-truncations open import foundation.propositions 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.normal-subgroups open import group-theory.subgroups open import group-theory.subsets-groups open import lists.concatenation-lists open import lists.lists 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 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) (H : S ⊆ subset-Subgroup G U) where is-subgroup-generated-by-subset-Group : UUω is-subgroup-generated-by-subset-Group = {l : Level} (U' : Subgroup l G) → S ⊆ subset-Subgroup G U' → subset-Subgroup G U ⊆ subset-Subgroup G U'
The adjoint relation 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 adjoint-relation-subgroup-generated-by-subset-Group : UUω adjoint-relation-subgroup-generated-by-subset-Group = {l : Level} (U' : Subgroup l G) → (leq-Subgroup G U U') ↔ (S ⊆ subset-Subgroup G U') contains-subset-adjoint-relation-subset-generated-by-subset-Group : adjoint-relation-subgroup-generated-by-subset-Group → S ⊆ subset-Subgroup G U contains-subset-adjoint-relation-subset-generated-by-subset-Group α = forward-implication (α U) (refl-leq-Subgroup G U) is-subgroup-generated-by-subset-adjoint-relation-Group : (α : adjoint-relation-subgroup-generated-by-subset-Group) → is-subgroup-generated-by-subset-Group G S U ( contains-subset-adjoint-relation-subset-generated-by-subset-Group α) is-subgroup-generated-by-subset-adjoint-relation-Group α U' = backward-implication (α U') adjoint-relation-is-subgroup-generated-by-subset-Group : (H : S ⊆ subset-Subgroup G U) → is-subgroup-generated-by-subset-Group G S U H → adjoint-relation-subgroup-generated-by-subset-Group pr1 (adjoint-relation-is-subgroup-generated-by-subset-Group H α K) L x y = L x (H x y) pr2 (adjoint-relation-is-subgroup-generated-by-subset-Group H α K) = α K
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 (pair (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 (pair (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 (pair (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 (pair (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 (pair s x) u) = concat-list ( inv-formal-combination-subset-Group u) ( unit-list (pair (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 (pair (inl (inr star)) x) u) = ( preserves-concat-ev-formal-combination-subset-Group ( inv-formal-combination-subset-Group u) ( unit-list (pair (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 ( inv-Group G (inclusion-subtype S x)) ( ev-formal-combination-subset-Group u))))) preserves-inv-ev-formal-combination-subset-Group ( cons (pair (inr star) x) u) = ( preserves-concat-ev-formal-combination-subset-Group ( inv-formal-combination-subset-Group u) ( unit-list (pair (inl (inr star)) x))) ∙ ( ( ap ( λ y → mul-Group G ( y) ( 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 (inclusion-subtype S x) ( ev-formal-combination-subset-Group u)))))
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 (pair 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' x y ( pair l p) (pair k q)) = concat-list l k pr2 ( is-closed-under-multiplication-subgroup-subset-Group' x y ( pair l p) (pair 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 x y H K = apply-universal-property-trunc-Prop H ( subset-subgroup-subset-Group (mul-Group G x y)) ( λ H' → apply-universal-property-trunc-Prop K ( subset-subgroup-subset-Group (mul-Group G x y)) ( λ K' → unit-trunc-Prop ( is-closed-under-multiplication-subgroup-subset-Group' x y 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' x (pair l p)) = inv-formal-combination-subset-Group l pr2 (is-closed-under-inverses-subgroup-subset-Group' x (pair 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 x H = apply-universal-property-trunc-Prop H ( subset-subgroup-subset-Group (inv-Group G x)) ( unit-trunc-Prop ∘ is-closed-under-inverses-subgroup-subset-Group' x) 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 ( pair ( unit-list (pair (inr star) (pair s H))) ( right-unit-law-mul-Group G (inclusion-subtype S (pair 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 (pair (inl (inr star)) (pair s K)) c) = is-closed-under-multiplication-Subgroup G U ( inv-Group G (inclusion-subtype S (pair s K))) ( ev-formal-combination-subset-Group c) ( is-closed-under-inverses-Subgroup G U s (H s K)) ( contains-formal-combinations-Subgroup U H c) contains-formal-combinations-Subgroup ( U) ( H) ( cons (pair (inr star) (pair s K)) c) = is-closed-under-multiplication-Subgroup G U ( inclusion-subtype S (pair s K)) ( ev-formal-combination-subset-Group c) ( H s K) ( contains-formal-combinations-Subgroup U H c) is-subgroup-generated-by-subset-subgroup-subset-Group : is-subgroup-generated-by-subset-Group G S ( subgroup-subset-Group) ( contains-subset-subgroup-subset-Group) is-subgroup-generated-by-subset-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 (pair 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 = is-subgroup-generated-by-subset-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)) subgroup-subset-hom-large-poset-Group : hom-set-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 adjoint-relation-subgroup-subset-Group : {l2 : Level} (S : subset-Group l2 G) → adjoint-relation-subgroup-generated-by-subset-Group G S ( subgroup-subset-Group G S) adjoint-relation-subgroup-subset-Group S = adjoint-relation-is-subgroup-generated-by-subset-Group G S ( subgroup-subset-Group G S) ( contains-subset-subgroup-subset-Group G S) ( is-subgroup-generated-by-subset-subgroup-subset-Group G S) subgroup-subset-galois-connection-Group : galois-connection-Large-Poset ( λ l2 → l1 ⊔ l2) ( id) ( 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 = adjoint-relation-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)
Recent changes
- 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).
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-08-07. Egbert Rijke. Normalizers, normal closures, normal cores, and centralizers (#693).
- 2023-07-20. Egbert Rijke. cyclic groups (#684).