Source: ProCGroups.ProC.MaximalQuotients.ResidualCore
1import Mathlib.Topology.Algebra.Group.Quotient
2import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
4/-!
5# Closed kernels and the pro-\(C\) residual core
7`ProCQuotientKernel C G` bundles a closed normal subgroup together with an open-normal
8quotient-in-\(C\) basis on its quotient. The residual core is their intersection; closedness and
9normality therefore follow directly from the stored kernel data, without reconstructing separation
10axioms from the basis property.
11-/
13open Set
15namespace ProCGroups.ProC
17universe u
19/-- Bundled closed normal kernels whose quotient has an open-normal quotient-in-\(C\) basis. -/
20structure ProCQuotientKernel
21 (C : FiniteGroupClass)
22 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
23 extends ClosedSubgroup G where
24 /-- The underlying closed subgroup is normal in \(G\). -/
25 normal : toSubgroup.Normal
26 /-- The quotient by the kernel has an open-normal basis of finite quotients in \(C\). -/
27 quotient_hasOpenNormalBasisInClass : letI := normal; HasOpenNormalBasisInClass C (G ⧸ toSubgroup)
29attribute [instance] ProCQuotientKernel.normal
31/-- The residual core \(R_C(G)\), defined as the intersection of all closed normal kernels whose
32quotient has an open-normal quotient-in-\(C\) basis. -/
33noncomputable def proCResidualCore
34 (C : FiniteGroupClass)
35 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subgroup G :=
36 sInf (Set.range fun N : ProCQuotientKernel C G => N.toSubgroup)
38/-- The residual core is a normal subgroup. -/
39@[instance]
40theorem proCResidualCore_normal
41 (C : FiniteGroupClass)
42 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
43 (proCResidualCore C G).Normal := by
44 change
45 (sInf (Set.range fun N : ProCQuotientKernel C G => N.toSubgroup)).Normal
46 simpa [proCResidualCore, sInf_range] using
47 (Subgroup.normal_iInf_normal
48 (a := fun N : ProCQuotientKernel C G => N.toSubgroup)
49 (norm := fun N => N.normal))
51/-- The residual core is closed. -/
52theorem proCResidualCore_isClosed
53 (C : FiniteGroupClass)
54 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
55 IsClosed ((proCResidualCore C G : Subgroup G) : Set G) := by
56 rw [proCResidualCore, sInf_range]
57 simp only [Subgroup.coe_iInf]
58 exact isClosed_iInter fun N => N.isClosed'
59end ProCGroups.ProC