Module

Algebraic.lean

Nyll.ProCGroups.NormalSubgroups.SimpleQuotients.Algebraic

3 declarations indexed from sourceView source ↗

Module documentation

Algebraic properties of simple quotients

This module translates simplicity of G ⧸ K into a dichotomy for normal subgroups above K and derives the intersection property needed for noncommutative simple quotients.

Imports1

Nyll.ProCGroups.NormalSubgroups.Framework

Imported by2

theorem

normal_subgroup_eq_kernel_or_top_of_simple_quotient

L24 ↗

ProCGroups.NormalSubgroups.normal_subgroup_eq_kernel_or_top_of_simple_quotient

Documentation

If \(G/K\) is simple, every normal subgroup of \(G\) containing \(K\) is either \(K\) or all of \(G\). This is the correspondence theorem form of the simple-quotient dichotomy.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.NormalSubgroups
universe u

Lean source · statement

theorem normal_subgroup_eq_kernel_or_top_of_simple_quotient
    {G : Type u} [Group G] (K L : Subgroup G) [K.Normal] (hL : L.Normal)
    [IsSimpleGroup (G ⧸ K)] (hKL : K ≤ L) :
    L = K ∨ L = ⊤

theorem

inf_sup_eq_top_of_simple_quotient_dichotomy

L52 ↗

ProCGroups.NormalSubgroups.inf_sup_eq_top_of_simple_quotient_dichotomy

Documentation

If subgroups above \(K\) satisfy the two-point dichotomy induced by a simple noncommutative quotient, then two normal subgroups whose products with \(K\) equal \(G\) retain that property after intersection.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.NormalSubgroups
universe u

Lean source · statement

theorem inf_sup_eq_top_of_simple_quotient_dichotomy
    {G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
    (hsimple : ∀ L : Subgroup G, L.Normal → K ≤ L → L = K ∨ L = ⊤)
    (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
    (hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
    M ⊓ N ⊔ K = ⊤

theorem

inf_sup_eq_top_of_noncomm_simple_quotient

L92 ↗

ProCGroups.NormalSubgroups.inf_sup_eq_top_of_noncomm_simple_quotient

Documentation

Algebraic core with the simple quotient written directly.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.NormalSubgroups
universe u

Lean source · statement

theorem inf_sup_eq_top_of_noncomm_simple_quotient
    {G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
    [IsSimpleGroup (G ⧸ K)]
    (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
    (hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
    M ⊓ N ⊔ K = ⊤

Module documentation

Algebraic properties of simple quotients

Declarations

normal_subgroup_eq_kernel_or_top_of_simple_quotient

inf_sup_eq_top_of_simple_quotient_dichotomy

inf_sup_eq_top_of_noncomm_simple_quotient