Mathlib.GroupTheory.Subgroup.Simple

Module docstring

{"# Simple groups

This file defines IsSimpleGroup G, a class indicating that a group has exactly two normal subgroups.

Main definitions

IsSimpleGroup G, a class indicating that a group has exactly two normal subgroups.

Tags

subgroup, subgroups

IsSimpleGroup structure

extends Nontrivial G

Full source

/-- A `Group` is simple when it has exactly two normal `Subgroup`s. -/
class IsSimpleGroup : Prop extends Nontrivial G where
  /-- Any normal subgroup is either `⊥` or `⊤` -/
  eq_bot_or_eq_top_of_normal : ∀ H : Subgroup G, H.Normal → H = ⊥ ∨ H = ⊤

Simple group

Informal description

A group $G$ is called simple if it has exactly two normal subgroups: the trivial subgroup and $G$ itself.

IsSimpleAddGroup structure

extends Nontrivial A

Full source

/-- An `AddGroup` is simple when it has exactly two normal `AddSubgroup`s. -/
class IsSimpleAddGroup : Prop extends Nontrivial A where
  /-- Any normal additive subgroup is either `⊥` or `⊤` -/
  eq_bot_or_eq_top_of_normal : ∀ H : AddSubgroup A, H.Normal → H = ⊥ ∨ H = ⊤

Simple additive group

Informal description

An additive group $ A $ is simple if it has exactly two normal additive subgroups: the trivial subgroup and $ A $ itself. This means there are no non-trivial proper normal additive subgroups in $ A $.

IsSimpleGroup.instIsSimpleOrderSubgroup instance

{C : Type*} [CommGroup C] [IsSimpleGroup C] : IsSimpleOrder (Subgroup C)

Full source

@[to_additive]
instance {C : Type*} [CommGroup C] [IsSimpleGroup C] : IsSimpleOrder (Subgroup C) :=
  ⟨fun H => H.normal_of_comm.eq_bot_or_eq_top⟩

Subgroup Lattice of a Simple Commutative Group is Simple

Informal description

For any commutative group $C$ that is simple, the lattice of subgroups of $C$ forms a simple order. That is, the only subgroups of $C$ are the trivial subgroup and $C$ itself.

IsSimpleGroup.isSimpleGroup_of_surjective theorem

{H : Type*} [Group H] [IsSimpleGroup G] [Nontrivial H] (f : G →* H) (hf : Function.Surjective f) : IsSimpleGroup H

Full source

@[to_additive]
theorem isSimpleGroup_of_surjective {H : Type*} [Group H] [IsSimpleGroup G] [Nontrivial H]
    (f : G →* H) (hf : Function.Surjective f) : IsSimpleGroup H :=
  ⟨fun H iH => by
    refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_
    · rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
    · rw [← comap_top f] at h
      exact comap_injective hf h⟩

Surjective Homomorphism Preserves Simplicity of Groups

Informal description

Let $G$ and $H$ be groups, with $G$ being simple and $H$ being nontrivial. If $f \colon G \to H$ is a surjective group homomorphism, then $H$ is also a simple group.