ProCGroups.lean

1import ProCGroups.Abelian.TopologicalAbelianization

2import ProCGroups.Abelian.TopologicalAbelianizationFunctoriality

3import ProCGroups.Abelian.TopologicalAbelianizationLimits

4import ProCGroups.Categorical.AlgebraicPullbacks

5import ProCGroups.Categorical.ProfinitePullbacks

6import ProCGroups.Categorical.PullbackComparison

7import ProCGroups.Categorical.PushoutSquares

8import ProCGroups.Categorical.QuotientPullbackEquivalences

9import ProCGroups.FiniteGeneration.Basic

10import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

11import ProCGroups.FiniteGroups.AllFinite

12import ProCGroups.FiniteGroups.StandardClasses

13import ProCGroups.FiniteStepSolvableQuotients.AbelianActions.Faithful

14import ProCGroups.FiniteStepSolvableQuotients.AbelianActions.SlimnessAndTorsion

15import ProCGroups.FiniteStepSolvableQuotients.Abelianization

16import ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic

17import ProCGroups.FiniteStepSolvableQuotients.Commutators.ClosureFromFiniteQuotients

18import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients

19import ProCGroups.FiniteStepSolvableQuotients.Commutators.Width

20import ProCGroups.Generation.Basic

21import ProCGroups.Generation.Convergence

22import ProCGroups.Generation.GeneratorConvergingPairs

23import ProCGroups.Generation.QuotientCriteria

24import ProCGroups.Generation.QuotientGeneratorConvergingPairs

25import ProCGroups.Generation.WordProductsAndClosure

26import ProCGroups.GroupTheory.CentralizerNormalizerCommensurator

27import ProCGroups.GroupTheory.Conjugation

28import ProCGroups.GroupTheory.Subgroups

29import ProCGroups.InverseSystems.CategoryBridge

30import ProCGroups.InverseSystems.CountableModels

31import ProCGroups.InverseSystems.Exactness

32import ProCGroups.InverseSystems.FiniteStageFactorization

33import ProCGroups.InverseSystems.ProfiniteLimits

34import ProCGroups.InverseSystems.Quotients

35import ProCGroups.InverseSystems.StagewiseIso

36import ProCGroups.Order.Basic

37import ProCGroups.ProC.Category.Basic

38import ProCGroups.ProC.Category.Pullbacks

39import ProCGroups.ProC.Category.Pushouts

40import ProCGroups.ProC.GroupPredicate

41import ProCGroups.ProC.GroupPredicates.Basic

42import ProCGroups.ProC.GroupPredicates.Standard

43import ProCGroups.ProC.GroupPredicates.Abelian

44import ProCGroups.ProC.Kernels

45import ProCGroups.ProC.MaximalQuotients.Definitions

46import ProCGroups.ProC.MaximalQuotients.ResidualCore

47import ProCGroups.ProC.MaximalQuotients.UniversalProperty

48import ProCGroups.ProC.OpenNormalSubgroups.Basic

49import ProCGroups.ProC.OpenNormalSubgroups.CountableChains

50import ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies

51import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation

52import ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator

53import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup

54import ProCGroups.ProC.OpenNormalSubgroups.Separation

55import ProCGroups.ProC.Quotients.ClosedNormal

56import ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods

57import ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients

58import ProCGroups.ProC.Quotients.LeftQuotientMaps

59import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections

60import ProCGroups.ProC.Quotients.OpenSubgroupSections

61import ProCGroups.ProC.Subgroups.Products

62import ProCGroups.Profinite.Basic

63import ProCGroups.Profinite.MathlibBridge

65/-

66PUBLIC_PAGE_SNAPSHOT

67generated_at: 2026-05-27T09:47:29+09:00

68lean_source: lean4/ProCGroups.lean

69translation_root: data/translation

70purpose: identifies the local data snapshot used to build pages/

71placement: after imports, never before imports

72-/

73/-!

74# ProCGroups

76Lightweight public root for reusable profinite and pro-`C` group infrastructure.

78This root keeps the default import surface small: finite-group classes, pro-`C` predicates,

79profinite groups, open normal quotients, inverse systems, categorical pullbacks/pushouts,

80generation, finite generation, and finite-step solvable quotients.

82Advanced topics such as completions, free pro-`C` groups, free-product universal properties,

83presentations, local-weight theory, normal-subgroup structure, duality, Frattini theory, and

84wreath products are available from `ProCGroups.Advanced` or from their focused folder wrappers.

85-/