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

ink

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

• Any normal subgroup is either ⊥⊥ or ⊤⊤

  eq_bot_or_eq_top_of_normal : ∀ (H : Subgroup G), Subgroup.Normal H → H = ⊥ ∨ H = ⊤

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

ink

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

• Any normal additive subgroup is either ⊥⊥ or ⊤⊤

  eq_bot_or_eq_top_of_normal : ∀ (H : AddSubgroup A), AddSubgroup.Normal H → H = ⊥ ∨ H = ⊤

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

ink

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

ink

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

ink

def IsSimpleAddGroup.instIsSimpleOrderAddSubgroupToAddGroupToLEToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeAddSubgroupToBoundedOrder.proof_1 {C : Type u_1} [inst : AddCommGroup C] [inst : IsSimpleAddGroup C] : IsSimpleOrder (AddSubgroup C)

Equations

• (_ : IsSimpleOrder (AddSubgroup C)) = (_ : IsSimpleOrder (AddSubgroup C))

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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