Simplicity of quotient groups #
This file characterizes when a quotient group is simple.
Main results #
Group.isSimpleGroup_of_isCoatom: the quotient of a group by a normal coatom of the subgroup lattice is simple.CommGroup.isSimpleGroup_iff_isCoatom: a subgroup of a commutative group is a coatom in the subgroup lattice iff the quotient by it is simple.
theorem
Group.isSimpleGroup_of_isCoatom
{G : Type u_1}
[Group G]
{M : Subgroup G}
[M.Normal]
(h : IsCoatom M)
:
IsSimpleGroup (G ⧸ M)
The quotient by a normal coatom is a simple group.
theorem
AddGroup.isSimpleAddGroup_of_isCoatom
{G : Type u_1}
[AddGroup G]
{M : AddSubgroup G}
[M.Normal]
(h : IsCoatom M)
:
IsSimpleAddGroup (G ⧸ M)
A subgroup of a commutative group is maximal (a coatom in the subgroup lattice) iff the quotient
by it is simple. Group analogue of isSimpleModule_iff_isCoatom.
theorem
AddCommGroup.isSimpleAddGroup_iff_isCoatom
{G : Type u_1}
[AddCommGroup G]
{M : AddSubgroup G}
:
A subgroup of an additive commutative group is maximal (a coatom in the subgroup
lattice) iff the quotient by it is simple. Additive group analogue of
isSimpleModule_iff_isCoatom.