Documentation

Mathlib.GroupTheory.Subgroup.Simple

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

class IsSimpleGroup (G : Type u_1) [Group G] extends Nontrivial G :

A Group is simple when it has exactly two normal Subgroups.

exists_pair_ne : ∃ (x : G) (y : G), x ≠ y
eq_bot_or_eq_top_of_normal (H : Subgroup G) : H.Normal → H = ⊥ ∨ H = ⊤
Any normal subgroup is either ⊥ or ⊤

Instances

theorem isSimpleGroup_iff (G : Type u_1) [Group G] :

IsSimpleGroup G ↔ Nontrivial G ∧ ∀ (H : Subgroup G), H.Normal → H = ⊥ ∨ H = ⊤

class IsSimpleAddGroup (A : Type u_2) [AddGroup A] extends Nontrivial A :

An AddGroup is simple when it has exactly two normal AddSubgroups.

exists_pair_ne : ∃ (x : A) (y : A), x ≠ y
eq_bot_or_eq_top_of_normal (H : AddSubgroup A) : H.Normal → H = ⊥ ∨ H = ⊤
Any normal additive subgroup is either ⊥ or ⊤

Instances

theorem isSimpleAddGroup_iff (A : Type u_2) [AddGroup A] :

IsSimpleAddGroup A ↔ Nontrivial A ∧ ∀ (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤

theorem Subgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [Group G] [IsSimpleGroup G] {H : Subgroup G} (Hn : H.Normal) :

H = ⊥ ∨ H = ⊤

theorem AddSubgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] {H : AddSubgroup G} (Hn : H.Normal) :

H = ⊥ ∨ H = ⊤

theorem Subgroup.isSimpleGroup_iff {G : Type u_1} [Group G] {H : Subgroup G} :

IsSimpleGroup ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H

theorem AddSubgroup.isSimpleAddGroup_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :

IsSimpleAddGroup ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.addSubgroupOf H).Normal → H' = ⊥ ∨ H' = H

instance IsSimpleGroup.instIsSimpleOrderSubgroup {C : Type u_3} [CommGroup C] [IsSimpleGroup C] :

IsSimpleOrder (Subgroup C)

instance IsSimpleAddGroup.instIsSimpleOrderAddSubgroup {C : Type u_3} [AddCommGroup C] [IsSimpleAddGroup C] :

IsSimpleOrder (AddSubgroup C)

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

IsSimpleGroup H

theorem IsSimpleAddGroup.isSimpleAddGroup_of_surjective {G : Type u_1} [AddGroup G] {H : Type u_3} [AddGroup H] [IsSimpleAddGroup G] [Nontrivial H] (f : G →+ H) (hf : Function.Surjective ⇑f) :

IsSimpleAddGroup H

theorem MulEquiv.isSimpleGroup {G : Type u_1} [Group G] {H : Type u_3} [Group H] [IsSimpleGroup H] (e : G ≃* H) :

IsSimpleGroup G

theorem AddEquiv.isSimpleAddGroup {G : Type u_1} [AddGroup G] {H : Type u_3} [AddGroup H] [IsSimpleAddGroup H] (e : G ≃+ H) :

IsSimpleAddGroup G

theorem MulEquiv.isSimpleGroup_congr {G : Type u_1} [Group G] {H : Type u_3} [Group H] (e : G ≃* H) :

IsSimpleGroup G ↔ IsSimpleGroup H

theorem AddEquiv.isSimpleAddGroup_congr {G : Type u_1} [AddGroup G] {H : Type u_3} [AddGroup H] (e : G ≃+ H) :

IsSimpleAddGroup G ↔ IsSimpleAddGroup H