Subgroup.exists_left_complement'_of_coprime
theorem Subgroup.exists_left_complement'_of_coprime :
∀ {G : Type u} [inst : Group G] {N : Subgroup G} [inst_1 : N.Normal],
(Nat.card ↥N).Coprime N.index → ∃ H, H.IsComplement' N
The Schur-Zassenhaus theorem for normal subgroups states that for any group `G` and a normal subgroup `N` of `G`, if the order of `N` (represented by `Nat.card ↥N`) is coprime to the index of `N` in `G` (represented by `N.index`), then there exists a subgroup `H` of `G` which is a left complement of `N`. In the language of group theory, a left complement of a subgroup `N` in `G` is a subgroup `H` such that every element in `G` can be uniquely written as the product of an element of `N` and an element of `H`. The function `H.IsComplement' N` checks if `H` is a left complement of `N`.
More concisely: If a normal subgroup `N` of a group `G` has coprime order and index, then there exists a subgroup `H` of `G` that is a left complement of `N`, i.e., every element in `G` can be uniquely written as the product of an element from `N` and an element from `H`.
|
Subgroup.exists_right_complement'_of_coprime
theorem Subgroup.exists_right_complement'_of_coprime :
∀ {G : Type u} [inst : Group G] {N : Subgroup G} [inst_1 : N.Normal],
(Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
This is the Schur-Zassenhaus theorem for normal subgroups. The theorem states that for any group G and a normal subgroup N of G, if the order of N (represented as `Nat.card ↥N`, the cardinality of N as a natural number) is coprime with its index in G (represented as `N.index`), then there exists a subgroup H of G that is a right complement of N. In other words, if the number of elements in N and the number of cosets of N in G have no common factors other than 1, then we can find a subgroup H such that every element in G can be uniquely expressed as the product of an element from N and an element from H.
More concisely: If a normal subgroup N of a group G has coprime order and index, then there exists a subgroup H of G such that every element in G can be written uniquely as the product of an element from N and an element from H.
|
Subgroup.exists_left_complement'_of_coprime_of_fintype
theorem Subgroup.exists_left_complement'_of_coprime_of_fintype :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {N : Subgroup G} [inst_2 : N.Normal],
(Fintype.card ↥N).Coprime N.index → ∃ H, H.IsComplement' N
The **Schur-Zassenhaus** theorem for normal subgroups is as follows: Given any group `G` that is finite, if there exists a normal subgroup `N` of `G` such that the order of `N` is coprime to the index of `N` in `G`, then there exists another subgroup `H` of `G` that is a left complement of `N`. In other words, for any such `N`, we can find an `H` such that every element in `G` can be uniquely expressed as a product of an element in `H` and an element in `N`.
More concisely: If a finite group `G` has a normal subgroup `N` of coprime order and index, then `N` has a left complement in `G`, that is, there exists a subgroup `H` such that every element in `G` can be written uniquely as a product of an element in `H` and an element in `N`.
|
Subgroup.SchurZassenhausInduction.step7
theorem Subgroup.SchurZassenhausInduction.step7 :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {N : Subgroup G} [inst_2 : N.Normal],
(Fintype.card ↥N).Coprime N.index →
(∀ (G' : Type u) [inst : Group G'] [inst_3 : Fintype G'],
Fintype.card G' < Fintype.card G →
∀ {N' : Subgroup G'} [inst_4 : N'.Normal],
(Fintype.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H') →
(∀ (H : Subgroup G), ¬N.IsComplement' H) → N.IsCommutative
This theorem, referred to as Subgroup.SchurZassenhausInduction.step7, states that given any type `G` with a group structure and a finite number of elements, and a normal subgroup `N` of `G`, if the cardinality of `N` (number of elements in the subgroup) and the index of `N` in `G` are coprime, then for every type `G'` with a group structure and a finite number of elements such that the cardinality of `G'` is less than the cardinality of `G`, and for every normal subgroup `N'` of `G'` where the cardinality of `N'` and its index in `G'` are coprime, there exists some subgroup `H'` which is a complement to `N'` in `G'`. Assuming that there is no such subgroup `H` in `G` that is a complement to `N`, then this theorem shows that `N` is commutative.
In simpler terms, it deals with a specific induction step in the proof of the Schur-Zassenhaus theorem in group theory, which states that every finite group `G` that has a normal subgroup `N` of order `n` and the number of cosets of `N` in `G` (i.e., the index) is m, such that `n` and `m` are coprime, then `G` has a subgroup `H` of order `m` such that `G` is the internal direct product of `N` and `H`. The theorem shows that in the absence of such a subgroup `H`, the subgroup `N` must be commutative.
More concisely: Given a finite group `G` with a normal subgroup `N` of coprime order and index, if there is no subgroup `H` of `G` with order equal to the index such that `G` is the internal direct product of `N` and `H`, then `N` is a commutative subgroup.
|
Subgroup.exists_right_complement'_of_coprime_of_fintype
theorem Subgroup.exists_right_complement'_of_coprime_of_fintype :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {N : Subgroup G} [inst_2 : N.Normal],
(Fintype.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
The Schur-Zassenhaus theorem for normal subgroups states that if we have a subgroup `N` of a group `G` which is normal and its order is coprime to its index in `G`, then there exists another subgroup `H` in `G` which behaves as a right complement to `N`. Here, the order of a subgroup is the number of its elements and is represented by `Fintype.card ↥N`. The index of a subgroup `N` in a group `G` is the number of distinct left or right cosets of `N` in `G`. A subgroup `H` is a right complement of `N` in `G` if every element in `G` can be uniquely written as the product of an element in `N` and an element in `H`.
More concisely: If a normal subgroup `N` of a group `G` has order coprime to its index, then it has a right complement subgroup `H` such that every element in `G` can be written uniquely as the product of an element in `N` and an element in `H`.
|