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

Tags #

subgroup, subgroups

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

    Any normal subgroup is either ⊥ or ⊤

Instances
    source
    theorem IsSimpleGroup.eq_bot_or_eq_top_of_normal {G : Type u_1} :
    ∀ {inst : Group G} [self : IsSimpleGroup G] (H : Subgroup G), H.Normal → H = ⊥ ∨ H = ⊤

    Any normal subgroup is either ⊥ or ⊤

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

      Any normal additive subgroup is either ⊥ or ⊤

    Instances
      source
      theorem IsSimpleAddGroup.eq_bot_or_eq_top_of_normal {A : Type u_2} :
      ∀ {inst : AddGroup A} [self : IsSimpleAddGroup A] (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤

      Any normal additive subgroup is either ⊥ or ⊤

      source
      theorem AddSubgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] {H : AddSubgroup G} (Hn : H.Normal) :
      H = ⊥ ∨ H = ⊤
      source
      theorem Subgroup.Normal.eq_bot_or_eq_top {G : Type u_1} [Group G] [IsSimpleGroup G] {H : Subgroup G} (Hn : H.Normal) :
      H = ⊥ ∨ H = ⊤
      source
      instance IsSimpleAddGroup.instIsSimpleOrderAddSubgroup {C : Type u_3} [AddCommGroup C] [IsSimpleAddGroup C] :
      IsSimpleOrder (AddSubgroup C)
      Equations
      • ⋯ = ⋯
      source
      instance IsSimpleGroup.instIsSimpleOrderSubgroup {C : Type u_3} [CommGroup C] [IsSimpleGroup C] :
      IsSimpleOrder (Subgroup C)
      Equations
      • ⋯ = ⋯
      source
      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
      source
      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