Subgroup.card_commutator_dvd_index_center_pow
theorem Subgroup.card_commutator_dvd_index_center_pow :
∀ (G : Type u_1) [inst : Group G] [inst_1 : Finite ↑(commutatorSet G)],
Nat.card ↥(commutator G) ∣
(Subgroup.center G).index ^ ((Subgroup.center G).index * Nat.card ↑(commutatorSet G) + 1)
This theorem states that for any group `G` that has `n` distinct commutator elements `[g₁, g₂]`, the cardinality of the commutator subgroup `G'` of `G` divides the quantity `(index of the center subgroup of G) ^ ((index of the center subgroup of G) * n + 1)`. Here, `n` is the number of commutator elements in the group `G`, and index of a subgroup is the number of its right cosets in the group. This theorem can be useful in studying the structure of the group and its associated subgroups.
More concisely: For any group G with n commutator elements, the order of its commutator subgroup divides (the index of its center subgroup)^((index of center subgroup)^n + 1).
|
Subgroup.closure_mul_image_eq_top'
theorem Subgroup.closure_mul_image_eq_top' :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : DecidableEq G] {R S : Finset G}
(hR : ↑R ∈ Subgroup.rightTransversals ↑H),
1 ∈ R →
Subgroup.closure ↑S = ⊤ →
Subgroup.closure ↑(Finset.image (fun g => ⟨g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹, ⋯⟩) (R * S)) =
⊤
**Schreier's Lemma**: Let `G` be a group with a subgroup `H`. If `R` is a finite set such that it forms a right transversal of `H` and includes the identity element, and if the group `G` is generated by a finite set `S`, then `H` is generated by the finite set obtained by mapping each element `g` of the product of `R` and `S` to the product of `g` and the inverse of the chosen representative of the right coset of `g` in `H`. This theorem asserts that the subgroup generated by this new finite set is the whole group.
More concisely: Given a group `G` with subgroup `H`, a finite right transversal `R` of `H` containing the identity element, and a generating set `S` for `G`, `H` is generated by the elements g h^(-1) for all g in the product of `R` and `S`, where `h` is the representative of the right coset of `g` in `H`.
|
Subgroup.closure_mul_image_eq_top
theorem Subgroup.closure_mul_image_eq_top :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {R S : Set G} (hR : R ∈ Subgroup.rightTransversals ↑H),
1 ∈ R →
Subgroup.closure S = ⊤ →
Subgroup.closure ((fun g => ⟨g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹, ⋯⟩) '' (R * S)) = ⊤
**Schreier's Lemma**: In the context of a group `G` and a subgroup `H` of `G`, if we have a set `R` that is a right transversal of `H` and contains the element `1`, and if the group `G` is generated by another set `S`, then the subgroup `H` is generated by the set obtained by multiplying each element of `R` with each element of `S` and then applying the function that maps each group element to the product of that element and the inverse of the corresponding representative chosen from its right coset. In other words, the closure of this new set equals the whole group `G`.
More concisely: If `G` is a group, `H` is a subgroup of `G`, `R` is a right transversal of `H` containing `1`, and `G` is generated by a set `S`, then `H` is generated by the set of products `r * s * r⁻¹` for all `r in R` and `s in S`.
|
Subgroup.card_commutator_le_of_finite_commutatorSet
theorem Subgroup.card_commutator_le_of_finite_commutatorSet :
∀ (G : Type u_1) [inst : Group G] [inst_1 : Finite ↑(commutatorSet G)],
Nat.card ↥(commutator G) ≤ Subgroup.cardCommutatorBound (Nat.card ↑(commutatorSet G))
This is Schur's theorem which states that for any group 'G', if the set of commutator elements of the group is finite, then the size of the commutator subgroup of 'G' is bounded by a certain function of the number of commutators. Precisely, the cardinality of the commutator subgroup is less than or equal to the value of the function `Subgroup.cardCommutatorBound` applied to the cardinality of the commutator set. The function `Subgroup.cardCommutatorBound` is defined as taking a natural number 'n' to the modulus of a complex number '(n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1)'.
More concisely: Schur's theorem states that for any group G, the size of its commutator subgroup is bounded by the value of the function (n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1), where n is the cardinality of its commutator set.
|
Subgroup.closure_mul_image_eq
theorem Subgroup.closure_mul_image_eq :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {R S : Set G} (hR : R ∈ Subgroup.rightTransversals ↑H),
1 ∈ R →
Subgroup.closure S = ⊤ →
Subgroup.closure ((fun g => g * (↑(Subgroup.MemRightTransversals.toFun hR g))⁻¹) '' (R * S)) = H
**Schreier's Lemma**: In the context of a group `G`, suppose `H` is a subgroup of `G`, `R` is a right transversal of `H` with the identity element `1` belonging in `R`, and `G` is generated by a set `S`. Then, the subgroup `H` is generated by the set obtained by multiplying each element of the Cartesian product of `R` and `S` with the inverse of the function `Subgroup.MemRightTransversals.toFun hR g` applied to the element, i.e., `H` is generated by the image of the set `(R * S)` under the function `g ↦ g * (toFun hR g)⁻¹`. This is known as Schreier's Lemma in group theory.
More concisely: Schreier's Lemma: A subgroup of a group generated by a set is also generated by the elements obtained by multiplying each element in the product of the subgroup's right transversal and the generating set, with the inverse of the corresponding right transversal element.
|