From d4865704149c43588030af1b37c22917b3cd443c Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sun, 8 Oct 2023 20:34:11 +0200 Subject: [PATCH] Nontrivial groups, and a correction of a statement in torsion-free groups (#815) This PR adds the notion of nontrivial groups to the library, and studies some properties of them. Furthermore, it corrects a statement made in the file about torsion-free groups. --------- Co-authored-by: Fredrik Bakke --- src/foundation/disjunction.lagda.md | 19 ++ src/group-theory.lagda.md | 2 + src/group-theory/nontrivial-groups.lagda.md | 185 ++++++++++++++++++ src/group-theory/subgroups.lagda.md | 79 ++++++++ src/group-theory/torsion-free-groups.lagda.md | 49 ++++- src/group-theory/trivial-groups.lagda.md | 72 +++++++ 6 files changed, 400 insertions(+), 6 deletions(-) create mode 100644 src/group-theory/nontrivial-groups.lagda.md create mode 100644 src/group-theory/trivial-groups.lagda.md diff --git a/src/foundation/disjunction.lagda.md b/src/foundation/disjunction.lagda.md index 6259b10545..5388d1e826 100644 --- a/src/foundation/disjunction.lagda.md +++ b/src/foundation/disjunction.lagda.md @@ -15,6 +15,7 @@ open import foundation.universe-levels open import foundation-core.coproduct-types open import foundation-core.decidable-propositions +open import foundation-core.empty-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.propositions @@ -112,3 +113,21 @@ abstract ( is-prop-type-Prop (conj-Prop (hom-Prop P R) (hom-Prop Q R))) ( elim-disj-Prop P Q R) ``` + +### The unit laws for disjunction + +```agda +module _ + {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) + where + + map-left-unit-law-disj-is-empty-Prop : + is-empty (type-Prop P) → type-disj-Prop P Q → type-Prop Q + map-left-unit-law-disj-is-empty-Prop f = + elim-disj-Prop P Q Q (ex-falso ∘ f , id) + + map-right-unit-law-disj-is-empty-Prop : + is-empty (type-Prop Q) → type-disj-Prop P Q → type-Prop P + map-right-unit-law-disj-is-empty-Prop f = + elim-disj-Prop P Q P (id , ex-falso ∘ f) +``` diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index aa2e241a63..a7f0482419 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -109,6 +109,7 @@ open import group-theory.monoids public open import group-theory.monomorphisms-concrete-groups public open import group-theory.monomorphisms-groups public open import group-theory.multiples-of-elements-abelian-groups public +open import group-theory.nontrivial-groups public open import group-theory.normal-closures-subgroups public open import group-theory.normal-cores-subgroups public open import group-theory.normal-subgroups public @@ -172,6 +173,7 @@ open import group-theory.transitive-concrete-group-actions public open import group-theory.transitive-group-actions public open import group-theory.trivial-concrete-groups public open import group-theory.trivial-group-homomorphisms public +open import group-theory.trivial-groups public open import group-theory.trivial-subgroups public open import group-theory.unordered-tuples-of-elements-commutative-monoids public open import group-theory.wild-representations-monoids public diff --git a/src/group-theory/nontrivial-groups.lagda.md b/src/group-theory/nontrivial-groups.lagda.md new file mode 100644 index 0000000000..baa7ef9e90 --- /dev/null +++ b/src/group-theory/nontrivial-groups.lagda.md @@ -0,0 +1,185 @@ +# Nontrivial groups + +```agda +module group-theory.nontrivial-groups where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.embeddings +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.logical-equivalences +open import foundation.negation +open import foundation.propositional-extensionality +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.unit-type +open import foundation.univalence +open import foundation.universe-levels + +open import group-theory.groups +open import group-theory.subgroups +open import group-theory.trivial-groups +``` + +
+ +## Idea + +A [group](group-theory.groups.md) is said to be **nontrivial** if there +[exists](foundation.existential-quantification.md) a nonidentity element. + +## Definitions + +### The predicate of being a nontrivial group + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + is-nontrivial-prop-Group : Prop l1 + is-nontrivial-prop-Group = + ∃-Prop (type-Group G) (λ x → ¬ (unit-Group G ＝ x)) + + is-nontrivial-Group : UU l1 + is-nontrivial-Group = + type-Prop is-nontrivial-prop-Group + + is-prop-is-nontrivial-Group : + is-prop is-nontrivial-Group + is-prop-is-nontrivial-Group = + is-prop-type-Prop is-nontrivial-prop-Group +``` + +### The predicate of not being the trivial group + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + is-not-trivial-prop-Group : Prop l1 + is-not-trivial-prop-Group = + neg-Prop' ((x : type-Group G) → unit-Group G ＝ x) + + is-not-trivial-Group : UU l1 + is-not-trivial-Group = + type-Prop is-not-trivial-prop-Group + + is-prop-is-not-trivial-Group : + is-prop is-not-trivial-Group + is-prop-is-not-trivial-Group = + is-prop-type-Prop is-not-trivial-prop-Group +``` + +## Properties + +### A group is not a trivial group if and only if it satisfies the predicate of not being trivial + +**Proof:** The proposition `¬ (is-trivial-Group G)` holds if and only if `G` is +not contractible, which holds if and only if `¬ ((x : G) → 1 ＝ x)`. + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + neg-is-trivial-is-not-trivial-Group : + is-not-trivial-Group G → ¬ (is-trivial-Group G) + neg-is-trivial-is-not-trivial-Group H p = H (λ x → eq-is-contr p) + + is-not-trivial-neg-is-trivial-Group : + ¬ (is-trivial-Group G) → is-not-trivial-Group G + is-not-trivial-neg-is-trivial-Group H p = H (unit-Group G , p) +``` + +### The map `subgroup-Prop G : Prop → Subgroup G` is an embedding for any nontrivial group + +Recall that the subgroup `subgroup-Prop G P` associated to a proposition `P` was +defined in [`group-theory.subgroups`](group-theory.subgroups.md). + +**Proof:** Suppose that `G` is a nontrivial group and `x` is a group element +such that `1 ≠ x`. Then `subgroup-Prop G P ＝ subgroup-Prop G Q` if and only if +`x ∈ subgroup-Prop G P ⇔ x ∈ subgroup-Prop G Q`, which holds if and only if +`P ⇔ Q` since `x` is assumed to be a nonidentity element. This shows that +`subgroup-Prop G : Prop → Subgroup G` is an injective map. Since it is an +injective maps between sets, it follows that `subgroup-Prop G` is an embedding. + +```agda +module _ + {l1 l2 : Level} (G : Group l1) + where + + abstract + is-emb-subgroup-prop-is-nontrivial-Group : + is-nontrivial-Group G → is-emb (subgroup-Prop {l2 = l2} G) + is-emb-subgroup-prop-is-nontrivial-Group H = + apply-universal-property-trunc-Prop H + ( is-emb-Prop _) + ( λ (x , f) → + is-emb-is-injective + ( is-set-Subgroup G) + ( λ {P} {Q} α → + eq-iff + ( λ p → + map-left-unit-law-disj-is-empty-Prop + ( Id-Prop (set-Group G) _ _) + ( Q) + ( f) + ( forward-implication + ( iff-eq (ap (λ T → subset-Subgroup G T x) α)) + ( inr-disj-Prop + ( Id-Prop (set-Group G) _ _) + ( P) + ( p)))) + ( λ q → + map-left-unit-law-disj-is-empty-Prop + ( Id-Prop (set-Group G) _ _) + ( P) + ( f) + ( backward-implication + ( iff-eq (ap (λ T → subset-Subgroup G T x) α)) + ( inr-disj-Prop + ( Id-Prop (set-Group G) _ _) + ( Q) + ( q)))))) +``` + +### If the map `subgroup-Prop G : Prop lzero → Subgroup l1 G` is an embedding, then `G` is not a trivial group + +**Proof:** Suppose that `subgroup-Prop G : Prop lzero → Subgroup l1 G` is an +embedding, and by way of contradiction suppose that `G` is trivial. Then it +follows that `Subgroup l1 G` is contractible. Since `subgroup-Prop G` is assumed +to be an embedding, it follows that `Prop lzero` is contractible. This +contradicts the fact that `Prop lzero` contains the distinct propositions +`empty-Prop` and `unit-Prop`. + +Note: Our handling of universe levels might be too restrictive here. + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + is-not-trivial-is-emb-subgroup-Prop : + is-emb (subgroup-Prop {l2 = lzero} G) → is-not-trivial-Group G + is-not-trivial-is-emb-subgroup-Prop H K = + backward-implication + ( iff-eq + ( is-injective-is-emb H + { x = empty-Prop} + { y = unit-Prop} + ( eq-is-contr (is-contr-subgroup-is-trivial-Group G (_ , K))))) + ( star) +``` diff --git a/src/group-theory/subgroups.lagda.md b/src/group-theory/subgroups.lagda.md index 1d6d8756ee..4245e7875d 100644 --- a/src/group-theory/subgroups.lagda.md +++ b/src/group-theory/subgroups.lagda.md @@ -13,6 +13,7 @@ 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.disjunction open import foundation.embeddings open import foundation.equivalence-relations open import foundation.equivalences @@ -21,6 +22,7 @@ open import foundation.identity-types open import foundation.injective-maps open import foundation.large-binary-relations open import foundation.powersets +open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtype-identity-principle @@ -499,6 +501,17 @@ preserves-order-hom-Large-Preorder preserves-order-subset-Subgroup G ``` +### The type of subgroups of a group is a set + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + is-set-Subgroup : {l2 : Level} → is-set (Subgroup l2 G) + is-set-Subgroup = is-set-type-Poset (Subgroup-Poset _ G) +``` + ### Every subgroup induces two equivalence relations #### The equivalence relation where `x ~ y` if and only if `x⁻¹ y ∈ H` @@ -608,3 +621,69 @@ module _ pr1 (pr2 (pr2 left-eq-rel-Subgroup)) = symmetric-left-sim-Subgroup pr2 (pr2 (pr2 left-eq-rel-Subgroup)) = transitive-left-sim-Subgroup ``` + +### Any proposition `P` induces a subgroup of any group `G` + +The subset consisting of elements `x : G` such that `(1 ＝ x) ∨ P` holds is +always a subgroup of `G`. This subgroup consists only of the unit element if `P` +is false, and it is the [full subgroup](group-theory.full-subgroups.md)`if`P` is +true. + +```agda +module _ + {l1 l2 : Level} (G : Group l1) (P : Prop l2) + where + + subset-subgroup-Prop : subset-Group (l1 ⊔ l2) G + subset-subgroup-Prop x = + disj-Prop (Id-Prop (set-Group G) (unit-Group G) x) P + + contains-unit-subgroup-Prop : + contains-unit-subset-Group G subset-subgroup-Prop + contains-unit-subgroup-Prop = + inl-disj-Prop (Id-Prop (set-Group G) (unit-Group G) (unit-Group G)) P refl + + is-closed-under-multiplication-subgroup-Prop' : + (x y : type-Group G) → + ((unit-Group G ＝ x) + type-Prop P) → + ((unit-Group G ＝ y) + type-Prop P) → + ((unit-Group G ＝ mul-Group G x y) + type-Prop P) + is-closed-under-multiplication-subgroup-Prop' ._ ._ (inl refl) (inl refl) = + inl (inv (left-unit-law-mul-Group G _)) + is-closed-under-multiplication-subgroup-Prop' ._ y (inl refl) (inr q) = + inr q + is-closed-under-multiplication-subgroup-Prop' x y (inr p) (inl β) = + inr p + is-closed-under-multiplication-subgroup-Prop' x y (inr p) (inr q) = + inr p + + is-closed-under-multiplication-subgroup-Prop : + is-closed-under-multiplication-subset-Group G subset-subgroup-Prop + is-closed-under-multiplication-subgroup-Prop x y H K = + apply-twice-universal-property-trunc-Prop H K + ( disj-Prop (Id-Prop (set-Group G) _ _) P) + ( λ H' K' → + unit-trunc-Prop + ( is-closed-under-multiplication-subgroup-Prop' x y H' K')) + + is-closed-under-inverses-subgroup-Prop' : + (x : type-Group G) → ((unit-Group G ＝ x) + type-Prop P) → + ((unit-Group G ＝ inv-Group G x) + type-Prop P) + is-closed-under-inverses-subgroup-Prop' ._ (inl refl) = + inl (inv (inv-unit-Group G)) + is-closed-under-inverses-subgroup-Prop' x (inr p) = + inr p + + is-closed-under-inverses-subgroup-Prop : + is-closed-under-inverses-subset-Group G subset-subgroup-Prop + is-closed-under-inverses-subgroup-Prop x H = + apply-universal-property-trunc-Prop H + ( disj-Prop (Id-Prop (set-Group G) _ _) P) + ( unit-trunc-Prop ∘ is-closed-under-inverses-subgroup-Prop' x) + + subgroup-Prop : Subgroup (l1 ⊔ l2) G + pr1 subgroup-Prop = subset-subgroup-Prop + pr1 (pr2 subgroup-Prop) = contains-unit-subgroup-Prop + pr1 (pr2 (pr2 subgroup-Prop)) = is-closed-under-multiplication-subgroup-Prop + pr2 (pr2 (pr2 subgroup-Prop)) = is-closed-under-inverses-subgroup-Prop +``` diff --git a/src/group-theory/torsion-free-groups.lagda.md b/src/group-theory/torsion-free-groups.lagda.md index bde44881b1..a265dbd1b5 100644 --- a/src/group-theory/torsion-free-groups.lagda.md +++ b/src/group-theory/torsion-free-groups.lagda.md @@ -7,21 +7,27 @@ module group-theory.torsion-free-groups where
Imports ```agda +open import elementary-number-theory.group-of-integers open import elementary-number-theory.nonzero-integers open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-pair-types +open import foundation.equivalences open import foundation.existential-quantification open import foundation.fundamental-theorem-of-identity-types open import foundation.identity-types open import foundation.propositions +open import foundation.pullbacks open import foundation.sets open import foundation.singleton-subtypes open import foundation.universe-levels open import group-theory.groups open import group-theory.integer-powers-of-elements-groups +open import group-theory.orders-of-elements-groups +open import group-theory.subgroups +open import group-theory.subgroups-generated-by-elements-groups open import group-theory.torsion-elements-groups ``` @@ -45,11 +51,17 @@ holds for all elements `x : G`. This condition can be formulated in several 2. The [subset](group-theory.subsets-groups.md) of `G` of [torsion elements](group-theory.torsion-elements-groups.md) is a [singleton subtype](foundation.singleton-subtypes.md). - -There is another closely related condition, which asserts that the -[image](foundation.images.md) of the map `order : G → subgroup ℤ` is a -[2-element type](univalent-combinatorics.2-element-types.md). Groups satisfying -this condition are _nontrivial_ torsion-free groups. +3. The map `p` in the [pullback square](foundation-core.pullbacks.md) + ```text + q + · ---------> Prop + | | + p| | P ↦ {k : ℤ ∣ (k ＝ 0) ∨ P} + V V + G -------> Subgroup ℤ + order + ``` + is an [equivalence](foundation.equivalences.md). ## Definitions @@ -79,7 +91,7 @@ module _ is-prop-is-torsion-free-Group = is-prop-type-Prop is-torsion-free-prop-Group ``` -### The group has a unique torsion element +### The predicate that a group has a unique torsion element ```agda module _ @@ -100,6 +112,31 @@ module _ is-prop-is-singleton-subtype (is-torsion-element-prop-Group G) ``` +### The predicate that the first projection of the pullback of `Prop lzero → Subgroup ℤ` along `order : G → Subgroup ℤ` is an equivalence + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + is-equiv-first-projection-pullback-subgroup-prop-prop-Group : + Prop (lsuc l1) + is-equiv-first-projection-pullback-subgroup-prop-prop-Group = + is-equiv-Prop + ( π₁ {f = subgroup-order-element-Group G} {g = subgroup-Prop ℤ-Group}) + + is-equiv-first-projection-pullback-subgroup-prop-Group : + UU (lsuc l1) + is-equiv-first-projection-pullback-subgroup-prop-Group = + type-Prop is-equiv-first-projection-pullback-subgroup-prop-prop-Group + + is-prop-is-equiv-first-projection-pullback-subgroup-prop-Group : + is-prop is-equiv-first-projection-pullback-subgroup-prop-Group + is-prop-is-equiv-first-projection-pullback-subgroup-prop-Group = + is-prop-type-Prop + ( is-equiv-first-projection-pullback-subgroup-prop-prop-Group) +``` + ## Properties ### The two definitions of torsion-free groups are equivalent diff --git a/src/group-theory/trivial-groups.lagda.md b/src/group-theory/trivial-groups.lagda.md new file mode 100644 index 0000000000..66840434a0 --- /dev/null +++ b/src/group-theory/trivial-groups.lagda.md @@ -0,0 +1,72 @@ +# Trivial groups + +```agda +module group-theory.trivial-groups where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.universe-levels + +open import group-theory.groups +open import group-theory.subgroups +open import group-theory.trivial-subgroups +``` + +
+ +## Idea + +A [group](group-theory.groups.md) is said to be **trivial** if its underlying +type is [contractible](foundation-core.contractible-types.md). In other words, a +group is trivial if it consists only of the unit element. + +## Definitions + +### The predicate of being a trivial group + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + is-trivial-prop-Group : Prop l1 + is-trivial-prop-Group = is-contr-Prop (type-Group G) + + is-trivial-Group : UU l1 + is-trivial-Group = type-Prop is-trivial-prop-Group + + is-prop-is-trivial-Group : is-prop is-trivial-Group + is-prop-is-trivial-Group = is-prop-type-Prop is-trivial-prop-Group +``` + +## Properties + +### The type of subgroups of a trivial group is contractible + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + is-contr-subgroup-is-trivial-Group : + is-trivial-Group G → is-contr (Subgroup l1 G) + pr1 (is-contr-subgroup-is-trivial-Group H) = + trivial-Subgroup G + pr2 (is-contr-subgroup-is-trivial-Group H) K = + eq-has-same-elements-Subgroup G + ( trivial-Subgroup G) + ( K) + ( λ x → + ( λ where refl → contains-unit-Subgroup G K) , + ( λ _ → + is-closed-under-eq-Subgroup G + ( trivial-Subgroup G) + ( contains-unit-Subgroup G (trivial-Subgroup G)) + ( eq-is-contr H))) +```