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)

theorem CommGroup.isSimpleGroup_iff_isCoatom {G : Type u_1} [CommGroup G] {M : Subgroup G} : IsSimpleGroup (G ⧸ M) ↔ IsCoatom 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} : IsSimpleAddGroup (G ⧸ M) ↔ IsCoatom M

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.