ProCGroups/ProC/MaximalQuotients/ResidualCore.lean
1import Mathlib.Topology.Algebra.Group.Quotient
2import ProCGroups.ProC.GroupPredicate
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/ProC/MaximalQuotients/ResidualCore.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Pro-C groups and open normal quotients
15Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
16-/
18open Set
20namespace ProCGroups.ProC
22universe u
24section
26variable {ProC : ProCGroupPredicate}
28/-- Bundled closed normal kernels whose quotient is pro-`C`. -/
29structure ProCQuotientKernel
30 (ProC : ProCGroupPredicate)
31 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
32 toSubgroup : Subgroup G
33 normal : toSubgroup.Normal
34 quotient_isProC : letI := normal; ProC (G := G ⧸ toSubgroup)
36attribute [instance] ProCQuotientKernel.normal
38/-- The residual core `R_C(G)`, defined as the intersection of all normal kernels with
39pro-`C` quotient. -/
40noncomputable def proCResidualCore
41 (ProC : ProCGroupPredicate)
42 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subgroup G :=
43 sInf (Set.range fun N : ProCQuotientKernel ProC G => N.toSubgroup)
45/-- The residual core is a normal subgroup. -/
46@[instance]
47theorem proCResidualCore_normal
48 (ProC : ProCGroupPredicate)
49 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
50 (proCResidualCore ProC G).Normal := by
51 change
52 (sInf (Set.range fun N : ProCQuotientKernel ProC G => N.toSubgroup)).Normal
53 simpa [proCResidualCore, sInf_range] using
54 (Subgroup.normal_iInf_normal
55 (a := fun N : ProCQuotientKernel ProC G => N.toSubgroup)
56 (norm := fun N => N.normal))
57/-- Closure of the pro-`C` notion under injective continuous homomorphisms. -/
58structure IsSubgroupClosedProC (ProC : ProCGroupPredicate) : Prop where
60 ∀ {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
61 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
62 (f : G →* H), Continuous f → Function.Injective f →
63 ProC (G := H) → ProC (G := G)
65/-- Closure under extensions with abelian kernel . -/
66structure IsClosedUnderExtensionsWithAbelianKernel (ProC : ProCGroupPredicate) : Prop where
67 of_extension :
68 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
69 (A : Subgroup G), [A.Normal] → CommGroup ↥A →
70 ProC (G := ↥A) → ProC (G := G ⧸ A) → ProC (G := G)
72end
74end ProCGroups.ProC