mathlib3 documentation

group_theory.subgroup.simple

Simple groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Tags #

subgroup, subgroups

source
@[instance]
def is_simple_group.to_nontrivial (G : Type u_1) [group G] [self : is_simple_group G] :
nontrivial G
source
@[class]
structure is_simple_group (G : Type u_1) [group G] :
Prop

A group is simple when it has exactly two normal subgroups.

Instances of this typeclass
source
@[class]
structure is_simple_add_group (A : Type u_2) [add_group A] :
Prop

An add_group is simple when it has exactly two normal add_subgroups.

source
@[instance]
def is_simple_add_group.to_nontrivial (A : Type u_2) [add_group A] [self : is_simple_add_group A] :
nontrivial A
source
theorem subgroup.normal.eq_bot_or_eq_top {G : Type u_1} [group G] [is_simple_group G] {H : subgroup G} (Hn : H.normal) :
H = ⊥ ∨ H = ⊤
source
theorem add_subgroup.normal.eq_bot_or_eq_top {G : Type u_1} [add_group G] [is_simple_add_group G] {H : add_subgroup G} (Hn : H.normal) :
H = ⊥ ∨ H = ⊤
source
@[protected, instance]
def is_simple_add_group.subgroup.is_simple_order {C : Type u_1} [add_comm_group C] [is_simple_add_group C] :
is_simple_order (add_subgroup C)
source
@[protected, instance]
def is_simple_group.subgroup.is_simple_order {C : Type u_1} [comm_group C] [is_simple_group C] :
is_simple_order (subgroup C)
source
theorem is_simple_add_group.is_simple_add_group_of_surjective {G : Type u_1} [add_group G] {H : Type u_2} [add_group H] [is_simple_add_group G] [nontrivial H] (f : G →+ H) (hf : function.surjective ⇑f) :
is_simple_add_group H
source
theorem is_simple_group.is_simple_group_of_surjective {G : Type u_1} [group G] {H : Type u_2} [group H] [is_simple_group G] [nontrivial H] (f : G →* H) (hf : function.surjective ⇑f) :
is_simple_group H