NYLL
Module

FiniteIntersections.lean

Nyll.ProCGroups.NormalSubgroups.SimpleQuotients.FiniteIntersections
2 declarations indexed from sourceView source ↗

Module documentation

Finite intersections above a simple-quotient kernel

This module proves normality of indexed intersections and shows that finite intersections retain the full-product property with the kernel of a noncommutative simple quotient.

Imports1
Imported by2

Declarations

theorem

sInf_normal_of_forall_normal

L24 ↗
ProCGroups.NormalSubgroups.sInf_normal_of_forall_normal
Documentation

An arbitrary infimum of normal subgroups is normal, when normality is known for every subgroup in the indexing set.

Source context 2 commands

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

namespace ProCGroups.NormalSubgroups
universe u
Lean source · statement
theorem sInf_normal_of_forall_normal
    {G : Type u} [Group G] {S : Set (Subgroup G)}
    (hSnormal : ∀ M ∈ S, M.Normal) :
    (sInf S).Normal
theorem

finite_sInf_sup_eq_top_of_noncomm_simple_quotient

L35 ↗
ProCGroups.NormalSubgroups.finite_sInf_sup_eq_top_of_noncomm_simple_quotient
Documentation

Finite-intersection step: in a noncommutative simple quotient, any finite intersection of normal subgroups whose product with K is all of G still has product \(\top\) with K.

Source context 2 commands

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

namespace ProCGroups.NormalSubgroups
universe u
Lean source · statement
theorem finite_sInf_sup_eq_top_of_noncomm_simple_quotient
    {G : Type u} [Group G] (K : Subgroup G) [K.Normal]
    [IsSimpleGroup (G ⧸ K)]
    (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
    {S : Set (Subgroup G)} (hSfinite : S.Finite)
    (hSnormal : ∀ M ∈ S, M.Normal)
    (hStop : ∀ M ∈ S, M ⊔ K = ⊤) :
    sInf S ⊔ K = ⊤

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.