ProCGroups/NormalSubgroups/PointedSumsAndSimpleQuotients.lean
1import ProCGroups.NormalSubgroups.Framework
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/NormalSubgroups/PointedSumsAndSimpleQuotients.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Closed normal subgroups and simple quotients
14Develops normal-subgroup frameworks, maximal intersections, simple quotient ranks, compactness arguments, and algebraic comparison theorems.
15-/
17namespace ProCGroups.NormalSubgroups
19universe u
21/-- Input data recording a closed normal closure that is free of the expected stabilized rank. -/
22structure NormalClosureFreeInputData
23 (C : ProCGroups.FiniteGroupClass.{u})
24 (F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
25 (S : Set F) (m : Cardinal) : Type (u + 1) where
26 normalClosure : Subgroup F
27 isClosedNormalClosure : IsClosedNormalClosure S normalClosure
28 isFree : ProCGroups.FreeProC.IsFreeProCGroupOfClassRank C normalClosure (m ⊔ ℵ₀)
30end ProCGroups.NormalSubgroups