Perfect groups #
A group G is perfect if it equals its commutator subgroup, that is ⁅G, G⁆ = G.
Among the basic results, we show that
- a nontrivial perfect group is not solvable (
IsPerfect.not_isSolvable); - an abelian perfect group is trivial (
IsPerfect.subsingleton_of_isMulCommutative).
Main Definition #
Group.IsPerfect: a groupGis perfect if it equals its own commutator, that is⁅⊤, ⊤⁆ = ⊤, where⊤is the full subgroupG.
Main Theorems #
IsPerfect.map: The image of a perfect group under a monoid homomorphism is perfect.IsPerfect.instQuotientSubgroup: The quotient of a perfect group by a normal subgroup is perfect.IsPerfect.ofSurjective: The image of a perfect group under a surjective monoid homomorphism is perfect.
A group G is perfect if G equals its commutator subgroup ⁅G, G⁆.
- commutator_eq_top : commutator G = ⊤
The commutator of the group
Gwith itself is the whole groupG.
Instances
theorem
Subgroup.isPerfect_iff
{G : Type u_1}
[Group G]
{H : Subgroup G}
:
Group.IsPerfect ↥H ↔ ⁅H, H⁆ = H
theorem
Subgroup.commutator_eq_self
{G : Type u_1}
[Group G]
{H : Subgroup G}
[hH : Group.IsPerfect ↥H]
:
theorem
Group.IsPerfect.mem_commutator
{G : Type u_1}
[Group G]
[hP : IsPerfect G]
{g : G}
:
g ∈ commutator G
The trivial group is perfect.
theorem
Group.IsPerfect.not_isSolvable
(G : Type u_1)
[Group G]
[Nontrivial G]
[IsPerfect G]
:
¬IsSolvable G
theorem
Group.IsPerfect.not_isNilpotent
(G : Type u_1)
[Group G]
[Nontrivial G]
[IsPerfect G]
:
¬IsNilpotent G
theorem
Group.IsPerfect.not_isMulCommutative
(G : Type u_1)
[Group G]
[Nontrivial G]
[IsPerfect G]
:
instance
Group.IsPerfect.subsingleton_of_isMulCommutative
{G : Type u_1}
[Group G]
[hG : IsPerfect G]
[h_comm : IsMulCommutative G]
:
Subsingleton G
theorem
Group.IsPerfect.map
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
{H : Subgroup G}
(f : G →* G')
[IsPerfect ↥H]
:
IsPerfect ↥(Subgroup.map f H)