Subgroups generated by subsets of groups
module group-theory.subgroups-generated-by-subsets-groups where
Imports
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.functions open import foundation.identity-types 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.full-subgroups open import group-theory.groups open import group-theory.subgroups open import lists.concatenation-lists open import lists.lists 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.
Definitions
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 : (l : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l) is-subgroup-generated-by-subset-Group l = (U' : Subgroup l G) → S ⊆ subset-Subgroup G U' → subset-Subgroup G U ⊆ subset-Subgroup G U'
Construction of subgroups generated by a subset of a group
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))))) subset-subgroup-subset-Group' : type-Group G → UU (l1 ⊔ l2) subset-subgroup-subset-Group' x = fib 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) contains-unit-subgroup-subset-Group : type-Prop (subset-subgroup-subset-Group (unit-Group G)) contains-unit-subgroup-subset-Group = unit-trunc-Prop (pair nil refl) is-closed-under-mul-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-mul-subgroup-subset-Group' x y ( pair l p) (pair k q)) = concat-list l k pr2 ( is-closed-under-mul-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-mul-subgroup-subset-Group : (x y : type-Group G) → type-Prop (subset-subgroup-subset-Group x) → type-Prop (subset-subgroup-subset-Group y) → type-Prop (subset-subgroup-subset-Group (mul-Group G x y)) is-closed-under-mul-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-mul-subgroup-subset-Group' x y H' K'))) is-closed-under-inv-subgroup-subset-Group' : (x : type-Group G) → subset-subgroup-subset-Group' x → subset-subgroup-subset-Group' (inv-Group G x) pr1 (is-closed-under-inv-subgroup-subset-Group' x (pair l p)) = inv-formal-combination-subset-Group l pr2 (is-closed-under-inv-subgroup-subset-Group' x (pair l p)) = ( preserves-inv-ev-formal-combination-subset-Group l) ∙ ( ap (inv-Group G) p) is-closed-under-inv-subgroup-subset-Group : (x : type-Group G) → type-Prop (subset-subgroup-subset-Group x) → type-Prop (subset-subgroup-subset-Group (inv-Group G x)) is-closed-under-inv-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-inv-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-mul-subgroup-subset-Group pr2 (pr2 (pr2 subgroup-subset-Group)) = is-closed-under-inv-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-mul-Subgroup G U ( inv-Group G (inclusion-subtype S (pair s K))) ( ev-formal-combination-subset-Group c) ( is-closed-under-inv-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-mul-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 : (l : Level) → is-subgroup-generated-by-subset-Group G S ( subgroup-subset-Group) ( contains-subset-subgroup-subset-Group) ( l) is-subgroup-generated-by-subset-subgroup-subset-Group l 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 is-generating-subset-Group : UU (l1 ⊔ l2) is-generating-subset-Group = is-full-Subgroup G subgroup-subset-Group