Subgroups
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Eléonore Mangel, Maša Žaucer, Elisabeth Bonnevier, Julian KG, Victor Blanchi, fernabnor and louismntnu.
Created on 2022-03-18.
Last modified on 2023-09-21.
module group-theory.subgroups where
Imports
open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers open import foundation.binary-relations open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalence-relations open import foundation.equivalences open import foundation.function-types open import foundation.identity-types open import foundation.injective-maps open import foundation.large-binary-relations open import foundation.powersets open import foundation.propositions open import foundation.sets open import foundation.subtype-identity-principle open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.groups open import group-theory.homomorphisms-groups open import group-theory.integer-powers-of-elements-groups open import group-theory.semigroups open import group-theory.subsets-groups open import order-theory.large-posets open import order-theory.large-preorders open import order-theory.order-preserving-maps-large-posets open import order-theory.order-preserving-maps-large-preorders open import order-theory.posets open import order-theory.preorders
Definitions
Subgroups
module _ {l1 l2 : Level} (G : Group l1) (P : subset-Group l2 G) where contains-unit-prop-subset-Group : Prop l2 contains-unit-prop-subset-Group = P (unit-Group G) contains-unit-subset-Group : UU l2 contains-unit-subset-Group = type-Prop contains-unit-prop-subset-Group is-prop-contains-unit-subset-Group : is-prop contains-unit-subset-Group is-prop-contains-unit-subset-Group = is-prop-type-Prop contains-unit-prop-subset-Group is-closed-under-multiplication-prop-subset-Group : Prop (l1 ⊔ l2) is-closed-under-multiplication-prop-subset-Group = Π-Prop ( type-Group G) ( λ x → Π-Prop ( type-Group G) ( λ y → hom-Prop (P x) (hom-Prop (P y) (P (mul-Group G x y))))) is-closed-under-multiplication-subset-Group : UU (l1 ⊔ l2) is-closed-under-multiplication-subset-Group = type-Prop is-closed-under-multiplication-prop-subset-Group is-prop-is-closed-under-multiplication-subset-Group : is-prop is-closed-under-multiplication-subset-Group is-prop-is-closed-under-multiplication-subset-Group = is-prop-type-Prop is-closed-under-multiplication-prop-subset-Group is-closed-under-inverses-prop-subset-Group : Prop (l1 ⊔ l2) is-closed-under-inverses-prop-subset-Group = Π-Prop ( type-Group G) ( λ x → hom-Prop (P x) (P (inv-Group G x))) is-closed-under-inverses-subset-Group : UU (l1 ⊔ l2) is-closed-under-inverses-subset-Group = type-Prop is-closed-under-inverses-prop-subset-Group is-prop-is-closed-under-inverses-subset-Group : is-prop is-closed-under-inverses-subset-Group is-prop-is-closed-under-inverses-subset-Group = is-prop-type-Prop is-closed-under-inverses-prop-subset-Group is-subgroup-prop-subset-Group : Prop (l1 ⊔ l2) is-subgroup-prop-subset-Group = prod-Prop ( contains-unit-prop-subset-Group) ( prod-Prop ( is-closed-under-multiplication-prop-subset-Group) ( is-closed-under-inverses-prop-subset-Group)) is-subgroup-subset-Group : UU (l1 ⊔ l2) is-subgroup-subset-Group = type-Prop is-subgroup-prop-subset-Group is-prop-is-subgroup-subset-Group : is-prop is-subgroup-subset-Group is-prop-is-subgroup-subset-Group = is-prop-type-Prop is-subgroup-prop-subset-Group
The type of all subgroups of a group
Subgroup : (l : Level) {l1 : Level} (G : Group l1) → UU ((lsuc l) ⊔ l1) Subgroup l G = type-subtype (is-subgroup-prop-subset-Group {l2 = l} G) module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where subset-Subgroup : subset-Group l2 G subset-Subgroup = inclusion-subtype (is-subgroup-prop-subset-Group G) H type-Subgroup : UU (l1 ⊔ l2) type-Subgroup = type-subtype subset-Subgroup inclusion-Subgroup : type-Subgroup → type-Group G inclusion-Subgroup = inclusion-subtype subset-Subgroup is-emb-inclusion-Subgroup : is-emb inclusion-Subgroup is-emb-inclusion-Subgroup = is-emb-inclusion-subtype subset-Subgroup emb-inclusion-Subgroup : type-Subgroup ↪ type-Group G emb-inclusion-Subgroup = emb-subtype subset-Subgroup is-in-Subgroup : type-Group G → UU l2 is-in-Subgroup = is-in-subtype subset-Subgroup is-closed-under-eq-Subgroup : {x y : type-Group G} → is-in-Subgroup x → (x = y) → is-in-Subgroup y is-closed-under-eq-Subgroup = is-closed-under-eq-subtype subset-Subgroup is-closed-under-eq-Subgroup' : {x y : type-Group G} → is-in-Subgroup y → (x = y) → is-in-Subgroup x is-closed-under-eq-Subgroup' = is-closed-under-eq-subtype' subset-Subgroup is-in-subgroup-inclusion-Subgroup : (x : type-Subgroup) → is-in-Subgroup (inclusion-Subgroup x) is-in-subgroup-inclusion-Subgroup x = pr2 x is-prop-is-in-Subgroup : (x : type-Group G) → is-prop (is-in-Subgroup x) is-prop-is-in-Subgroup = is-prop-is-in-subtype subset-Subgroup is-subgroup-Subgroup : is-subgroup-subset-Group G subset-Subgroup is-subgroup-Subgroup = pr2 H contains-unit-Subgroup : contains-unit-subset-Group G subset-Subgroup contains-unit-Subgroup = pr1 is-subgroup-Subgroup is-closed-under-multiplication-Subgroup : is-closed-under-multiplication-subset-Group G subset-Subgroup is-closed-under-multiplication-Subgroup = pr1 (pr2 is-subgroup-Subgroup) is-closed-under-inverses-Subgroup : is-closed-under-inverses-subset-Group G subset-Subgroup is-closed-under-inverses-Subgroup = pr2 (pr2 is-subgroup-Subgroup) is-closed-under-inverses-Subgroup' : (x : type-Group G) → is-in-Subgroup (inv-Group G x) → is-in-Subgroup x is-closed-under-inverses-Subgroup' x p = is-closed-under-eq-Subgroup ( is-closed-under-inverses-Subgroup (inv-Group G x) p) ( inv-inv-Group G x) is-in-subgroup-left-factor-Subgroup : (x y : type-Group G) → is-in-Subgroup (mul-Group G x y) → is-in-Subgroup y → is-in-Subgroup x is-in-subgroup-left-factor-Subgroup x y p q = is-closed-under-eq-Subgroup ( is-closed-under-multiplication-Subgroup ( mul-Group G x y) ( inv-Group G y) ( p) ( is-closed-under-inverses-Subgroup y q)) ( is-retraction-right-div-Group G y x) is-in-subgroup-right-factor-Subgroup : (x y : type-Group G) → is-in-Subgroup (mul-Group G x y) → is-in-Subgroup x → is-in-Subgroup y is-in-subgroup-right-factor-Subgroup x y p q = is-closed-under-eq-Subgroup ( is-closed-under-multiplication-Subgroup ( inv-Group G x) ( mul-Group G x y) ( is-closed-under-inverses-Subgroup x q) ( p)) ( is-retraction-left-div-Group G x y) is-closed-under-powers-int-Subgroup : (k : ℤ) (x : type-Group G) → is-in-Subgroup x → is-in-Subgroup (integer-power-Group G k x) is-closed-under-powers-int-Subgroup (inl zero-ℕ) x H = is-closed-under-eq-Subgroup' ( is-closed-under-inverses-Subgroup x H) ( right-unit-law-mul-Group G (inv-Group G x)) is-closed-under-powers-int-Subgroup (inl (succ-ℕ k)) x H = is-closed-under-multiplication-Subgroup ( inv-Group G x) ( integer-power-Group G (inl k) x) ( is-closed-under-inverses-Subgroup x H) ( is-closed-under-powers-int-Subgroup (inl k) x H) is-closed-under-powers-int-Subgroup (inr (inl star)) x H = contains-unit-Subgroup is-closed-under-powers-int-Subgroup (inr (inr zero-ℕ)) x H = is-closed-under-eq-Subgroup' H (right-unit-law-mul-Group G x) is-closed-under-powers-int-Subgroup (inr (inr (succ-ℕ k))) x H = is-closed-under-multiplication-Subgroup ( x) ( integer-power-Group G (inr (inr k)) x) ( H) ( is-closed-under-powers-int-Subgroup (inr (inr k)) x H) is-emb-subset-Subgroup : {l1 l2 : Level} (G : Group l1) → is-emb (subset-Subgroup {l2 = l2} G) is-emb-subset-Subgroup G = is-emb-inclusion-subtype (is-subgroup-prop-subset-Group G)
The underlying group of a subgroup
module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where type-group-Subgroup : UU (l1 ⊔ l2) type-group-Subgroup = type-subtype (subset-Subgroup G H) map-inclusion-Subgroup : type-group-Subgroup → type-Group G map-inclusion-Subgroup = inclusion-subtype (subset-Subgroup G H) eq-subgroup-eq-group : is-injective map-inclusion-Subgroup eq-subgroup-eq-group {x} {y} = map-inv-is-equiv (is-emb-inclusion-Subgroup G H x y) set-group-Subgroup : Set (l1 ⊔ l2) pr1 set-group-Subgroup = type-group-Subgroup pr2 set-group-Subgroup = is-set-type-subtype (subset-Subgroup G H) (is-set-type-Group G) mul-Subgroup : (x y : type-group-Subgroup) → type-group-Subgroup pr1 (mul-Subgroup x y) = mul-Group G (pr1 x) (pr1 y) pr2 (mul-Subgroup x y) = is-closed-under-multiplication-Subgroup G H (pr1 x) (pr1 y) (pr2 x) (pr2 y) associative-mul-Subgroup : (x y z : type-group-Subgroup) → Id ( mul-Subgroup (mul-Subgroup x y) z) ( mul-Subgroup x (mul-Subgroup y z)) associative-mul-Subgroup x y z = eq-subgroup-eq-group ( associative-mul-Group G (pr1 x) (pr1 y) (pr1 z)) unit-Subgroup : type-group-Subgroup pr1 unit-Subgroup = unit-Group G pr2 unit-Subgroup = contains-unit-Subgroup G H left-unit-law-mul-Subgroup : (x : type-group-Subgroup) → Id (mul-Subgroup unit-Subgroup x) x left-unit-law-mul-Subgroup x = eq-subgroup-eq-group (left-unit-law-mul-Group G (pr1 x)) right-unit-law-mul-Subgroup : (x : type-group-Subgroup) → Id (mul-Subgroup x unit-Subgroup) x right-unit-law-mul-Subgroup x = eq-subgroup-eq-group (right-unit-law-mul-Group G (pr1 x)) inv-Subgroup : type-group-Subgroup → type-group-Subgroup pr1 (inv-Subgroup x) = inv-Group G (pr1 x) pr2 (inv-Subgroup x) = is-closed-under-inverses-Subgroup G H (pr1 x) (pr2 x) left-inverse-law-mul-Subgroup : ( x : type-group-Subgroup) → Id ( mul-Subgroup (inv-Subgroup x) x) ( unit-Subgroup) left-inverse-law-mul-Subgroup x = eq-subgroup-eq-group (left-inverse-law-mul-Group G (pr1 x)) right-inverse-law-mul-Subgroup : (x : type-group-Subgroup) → Id ( mul-Subgroup x (inv-Subgroup x)) ( unit-Subgroup) right-inverse-law-mul-Subgroup x = eq-subgroup-eq-group (right-inverse-law-mul-Group G (pr1 x)) semigroup-Subgroup : Semigroup (l1 ⊔ l2) pr1 semigroup-Subgroup = set-group-Subgroup pr1 (pr2 semigroup-Subgroup) = mul-Subgroup pr2 (pr2 semigroup-Subgroup) = associative-mul-Subgroup group-Subgroup : Group (l1 ⊔ l2) pr1 group-Subgroup = semigroup-Subgroup pr1 (pr1 (pr2 group-Subgroup)) = unit-Subgroup pr1 (pr2 (pr1 (pr2 group-Subgroup))) = left-unit-law-mul-Subgroup pr2 (pr2 (pr1 (pr2 group-Subgroup))) = right-unit-law-mul-Subgroup pr1 (pr2 (pr2 group-Subgroup)) = inv-Subgroup pr1 (pr2 (pr2 (pr2 group-Subgroup))) = left-inverse-law-mul-Subgroup pr2 (pr2 (pr2 (pr2 group-Subgroup))) = right-inverse-law-mul-Subgroup
The inclusion of the underlying group of a subgroup into the ambient group
module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where preserves-mul-inclusion-Subgroup : preserves-mul-Group ( group-Subgroup G H) ( G) ( map-inclusion-Subgroup G H) preserves-mul-inclusion-Subgroup x y = refl preserves-unit-inclusion-Subgroup : preserves-unit-Group ( group-Subgroup G H) ( G) ( map-inclusion-Subgroup G H) preserves-unit-inclusion-Subgroup = refl preserves-inverses-inclusion-Subgroup : preserves-inverses-Group ( group-Subgroup G H) ( G) ( map-inclusion-Subgroup G H) preserves-inverses-inclusion-Subgroup x = refl hom-inclusion-Subgroup : type-hom-Group (group-Subgroup G H) G pr1 hom-inclusion-Subgroup = inclusion-Subgroup G H pr2 hom-inclusion-Subgroup = preserves-mul-inclusion-Subgroup
Properties
Extensionality of the type of all subgroups
module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where has-same-elements-Subgroup : {l3 : Level} → Subgroup l3 G → UU (l1 ⊔ l2 ⊔ l3) has-same-elements-Subgroup K = has-same-elements-subtype ( subset-Subgroup G H) ( subset-Subgroup G K) extensionality-Subgroup : (K : Subgroup l2 G) → (H = K) ≃ has-same-elements-Subgroup K extensionality-Subgroup = extensionality-type-subtype ( is-subgroup-prop-subset-Group G) ( is-subgroup-Subgroup G H) ( λ x → pair id id) ( extensionality-subtype (subset-Subgroup G H)) refl-has-same-elements-Subgroup : has-same-elements-Subgroup H refl-has-same-elements-Subgroup = refl-has-same-elements-subtype (subset-Subgroup G H) has-same-elements-eq-Subgroup : (K : Subgroup l2 G) → (H = K) → has-same-elements-Subgroup K has-same-elements-eq-Subgroup K = map-equiv (extensionality-Subgroup K) eq-has-same-elements-Subgroup : (K : Subgroup l2 G) → has-same-elements-Subgroup K → (H = K) eq-has-same-elements-Subgroup K = map-inv-equiv (extensionality-Subgroup K)
The containment relation of subgroups
leq-prop-Subgroup : {l1 l2 l3 : Level} (G : Group l1) → Subgroup l2 G → Subgroup l3 G → Prop (l1 ⊔ l2 ⊔ l3) leq-prop-Subgroup G H K = leq-prop-subtype ( subset-Subgroup G H) ( subset-Subgroup G K) leq-Subgroup : {l1 l2 l3 : Level} (G : Group l1) → Subgroup l2 G → Subgroup l3 G → UU (l1 ⊔ l2 ⊔ l3) leq-Subgroup G H K = subset-Subgroup G H ⊆ subset-Subgroup G K refl-leq-Subgroup : {l1 : Level} (G : Group l1) → is-reflexive-Large-Relation (λ l → Subgroup l G) (leq-Subgroup G) refl-leq-Subgroup G H = refl-leq-subtype (subset-Subgroup G H) transitive-leq-Subgroup : {l1 : Level} (G : Group l1) → is-transitive-Large-Relation (λ l → Subgroup l G) (leq-Subgroup G) transitive-leq-Subgroup G H K L = transitive-leq-subtype ( subset-Subgroup G H) ( subset-Subgroup G K) ( subset-Subgroup G L) antisymmetric-leq-Subgroup : {l1 : Level} (G : Group l1) → is-antisymmetric-Large-Relation (λ l → Subgroup l G) (leq-Subgroup G) antisymmetric-leq-Subgroup G H K α β = eq-has-same-elements-Subgroup G H K (λ x → (α x , β x)) Subgroup-Large-Preorder : {l1 : Level} (G : Group l1) → Large-Preorder (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) type-Large-Preorder (Subgroup-Large-Preorder G) l2 = Subgroup l2 G leq-prop-Large-Preorder (Subgroup-Large-Preorder G) H K = leq-prop-Subgroup G H K refl-leq-Large-Preorder (Subgroup-Large-Preorder G) = refl-leq-Subgroup G transitive-leq-Large-Preorder (Subgroup-Large-Preorder G) = transitive-leq-Subgroup G Subgroup-Preorder : {l1 : Level} (l2 : Level) (G : Group l1) → Preorder (l1 ⊔ lsuc l2) (l1 ⊔ l2) Subgroup-Preorder l2 G = preorder-Large-Preorder (Subgroup-Large-Preorder G) l2 Subgroup-Large-Poset : {l1 : Level} (G : Group l1) → Large-Poset (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) large-preorder-Large-Poset (Subgroup-Large-Poset G) = Subgroup-Large-Preorder G antisymmetric-leq-Large-Poset (Subgroup-Large-Poset G) = antisymmetric-leq-Subgroup G Subgroup-Poset : {l1 : Level} (l2 : Level) (G : Group l1) → Poset (l1 ⊔ lsuc l2) (l1 ⊔ l2) Subgroup-Poset l2 G = poset-Large-Poset (Subgroup-Large-Poset G) l2 preserves-order-subset-Subgroup : {l1 l2 l3 : Level} (G : Group l1) (H : Subgroup l2 G) (K : Subgroup l3 G) → leq-Subgroup G H K → (subset-Subgroup G H ⊆ subset-Subgroup G K) preserves-order-subset-Subgroup G H K = id subset-subgroup-hom-large-poset-Group : {l1 : Level} (G : Group l1) → hom-Large-Poset ( id) ( Subgroup-Large-Poset G) ( powerset-Large-Poset (type-Group G)) map-hom-Large-Preorder ( subset-subgroup-hom-large-poset-Group G) = subset-Subgroup G preserves-order-hom-Large-Preorder ( subset-subgroup-hom-large-poset-Group G) = preserves-order-subset-Subgroup G
Every subgroup induces two equivalence relations
The equivalence relation where x ~ y
if and only if x⁻¹ y ∈ H
module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where right-sim-Subgroup : (x y : type-Group G) → UU l2 right-sim-Subgroup x y = is-in-Subgroup G H (left-div-Group G x y) is-prop-right-sim-Subgroup : (x y : type-Group G) → is-prop (right-sim-Subgroup x y) is-prop-right-sim-Subgroup x y = is-prop-is-in-Subgroup G H (left-div-Group G x y) prop-right-eq-rel-Subgroup : (x y : type-Group G) → Prop l2 pr1 (prop-right-eq-rel-Subgroup x y) = right-sim-Subgroup x y pr2 (prop-right-eq-rel-Subgroup x y) = is-prop-right-sim-Subgroup x y refl-right-sim-Subgroup : is-reflexive right-sim-Subgroup refl-right-sim-Subgroup x = tr ( is-in-Subgroup G H) ( inv (left-inverse-law-mul-Group G x)) ( contains-unit-Subgroup G H) symmetric-right-sim-Subgroup : is-symmetric right-sim-Subgroup symmetric-right-sim-Subgroup x y p = tr ( is-in-Subgroup G H) ( inv-left-div-Group G x y) ( is-closed-under-inverses-Subgroup G H ( left-div-Group G x y) ( p)) transitive-right-sim-Subgroup : is-transitive right-sim-Subgroup transitive-right-sim-Subgroup x y z p q = tr ( is-in-Subgroup G H) ( mul-left-div-Group G x y z) ( is-closed-under-multiplication-Subgroup G H ( left-div-Group G x y) ( left-div-Group G y z) ( q) ( p)) right-eq-rel-Subgroup : Equivalence-Relation l2 (type-Group G) pr1 right-eq-rel-Subgroup = prop-right-eq-rel-Subgroup pr1 (pr2 right-eq-rel-Subgroup) = refl-right-sim-Subgroup pr1 (pr2 (pr2 right-eq-rel-Subgroup)) = symmetric-right-sim-Subgroup pr2 (pr2 (pr2 right-eq-rel-Subgroup)) = transitive-right-sim-Subgroup
The equivalence relation where x ~ y
if and only if xy⁻¹ ∈ H
module _ {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G) where left-sim-Subgroup : (x y : type-Group G) → UU l2 left-sim-Subgroup x y = is-in-Subgroup G H (right-div-Group G x y) is-prop-left-sim-Subgroup : (x y : type-Group G) → is-prop (left-sim-Subgroup x y) is-prop-left-sim-Subgroup x y = is-prop-is-in-Subgroup G H (right-div-Group G x y) prop-left-eq-rel-Subgroup : (x y : type-Group G) → Prop l2 pr1 (prop-left-eq-rel-Subgroup x y) = left-sim-Subgroup x y pr2 (prop-left-eq-rel-Subgroup x y) = is-prop-left-sim-Subgroup x y refl-left-sim-Subgroup : is-reflexive left-sim-Subgroup refl-left-sim-Subgroup x = tr ( is-in-Subgroup G H) ( inv (right-inverse-law-mul-Group G x)) ( contains-unit-Subgroup G H) symmetric-left-sim-Subgroup : is-symmetric left-sim-Subgroup symmetric-left-sim-Subgroup x y p = tr ( is-in-Subgroup G H) ( inv-right-div-Group G x y) ( is-closed-under-inverses-Subgroup G H ( right-div-Group G x y) ( p)) transitive-left-sim-Subgroup : is-transitive left-sim-Subgroup transitive-left-sim-Subgroup x y z p q = tr ( is-in-Subgroup G H) ( mul-right-div-Group G x y z) ( is-closed-under-multiplication-Subgroup G H ( right-div-Group G x y) ( right-div-Group G y z) ( q) ( p)) left-eq-rel-Subgroup : Equivalence-Relation l2 (type-Group G) pr1 left-eq-rel-Subgroup = prop-left-eq-rel-Subgroup pr1 (pr2 left-eq-rel-Subgroup) = refl-left-sim-Subgroup pr1 (pr2 (pr2 left-eq-rel-Subgroup)) = symmetric-left-sim-Subgroup pr2 (pr2 (pr2 left-eq-rel-Subgroup)) = transitive-left-sim-Subgroup
Recent changes
- 2023-09-21. Egbert Rijke. The classification of cyclic rings (#757).
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-10. Egbert Rijke and Fredrik Bakke. Cyclic groups (#723).
- 2023-08-21. Egbert Rijke and Fredrik Bakke. Cyclic groups (#697).
- 2023-08-07. Egbert Rijke. Normalizers, normal closures, normal cores, and centralizers (#693).