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 : Prop

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), Subgroup.Normal H → H = ⊥ ∨ H = ⊤

  Any normal subgroup is either ⊥ or ⊤

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

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), AddSubgroup.Normal H → H = ⊥ ∨ H = ⊤

  Any normal additive subgroup is either ⊥ or ⊤

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

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

instance IsSimpleAddGroup.instIsSimpleOrderAddSubgroupToAddGroupToLEToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeAddSubgroupToBoundedOrder {C : Type u_3} [AddCommGroup C] [IsSimpleAddGroup C] : IsSimpleOrder (AddSubgroup C)

Equations

• ⋯ = ⋯

instance IsSimpleGroup.instIsSimpleOrderSubgroupToGroupToLEToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeSubgroupToBoundedOrder {C : Type u_3} [CommGroup C] [IsSimpleGroup C] : IsSimpleOrder (Subgroup C)

Equations

• ⋯ = ⋯

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 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