ProCGroups.ProC.MaximalQuotients.ResidualCore
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
import
- Mathlib.Topology.Algebra.Group.Quotient
- ProCGroups.ProC.GroupPredicate
structure ProCQuotientKernel
(ProC : ProCGroupPredicate)
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
toSubgroup : Subgroup G
normal : toSubgroup.Normal
quotient_isProC : letI := normal; ProC (G := G ⧸ toSubgroup)Bundled closed normal kernels whose quotient is pro-\(C\).
noncomputable def proCResidualCore
(ProC : ProCGroupPredicate)
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subgroup G :=
sInf (Set.range fun N : ProCQuotientKernel ProC G => N.toSubgroup)The residual core \(R_C(G)\), defined as the intersection of all normal kernels with pro-\(C\) quotient.
theorem proCResidualCore_normal
(ProC : ProCGroupPredicate)
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
(proCResidualCore ProC G).NormalThe residual core is a normal subgroup.
Show proof
by
change
(sInf (Set.range fun N : ProCQuotientKernel ProC G => N.toSubgroup)).Normal
simpa [proCResidualCore, sInf_range] using
(Subgroup.normal_iInf_normal
(a := fun N : ProCQuotientKernel ProC G => N.toSubgroup)
(norm := fun N => N.normal))Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□structure IsSubgroupClosedProC (ProC : ProCGroupPredicate) : Prop where
of_injective :
∀ {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(f : G →* H), Continuous f → Function.Injective f →
ProC (G := H) → ProC (G := G)A pro-\(C\) predicate is subgroup-closed: an injective continuous homomorphism into a pro-\(C\) group makes the source pro-\(C\).
structure IsClosedUnderExtensionsWithAbelianKernel (ProC : ProCGroupPredicate) : Prop where
of_extension :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(A : Subgroup G), [A.Normal] → CommGroup ↥A →
ProC (G := ↥A) → ProC (G := G ⧸ A) → ProC (G := G)Closure under extensions with abelian kernel.