ProCGroups/ProC/MaximalQuotients/Definitions.lean

1import ProCGroups.ProC.GroupPredicate

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/ProCGroups/ProC/MaximalQuotients/Definitions.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Pro-C groups and open normal quotients

14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.

15-/

17open Set

19namespace ProCGroups.ProC

21universe u

23section

25variable {ProC : ProCGroupPredicate}

27/-- Maximal pro-`C` quotient groups via their universal property. -/

28structure IsMaximalProCQuotient

29 (ProC : ProCGroupPredicate)

30 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

31 {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]

32 (π : G →* Q) : Prop where

33 isProC : ProC (G := Q)

34 continuous_π : Continuous π

35 surjective_π : Function.Surjective π

36 existsUnique_lift :

37 ∀ {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H],

38 ProC (G := H) →

39 ∀ (φ : G →* H), Continuous φ →

40 ∃! φbar : Q →* H, Continuous φbar ∧ φbar.comp π = φ

42end

44end ProCGroups.ProC