ProCGroups.NormalSubgroups.SimpleQuotients.Compactness
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.
theorem maximal_open_normal_intersections_compactness_step
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
(K : Subgroup G) [K.Normal] (hKclosed : IsClosed (K : Set G))
(๐ : Set (Subgroup G))
(hMclosed : โ M โ ๐, IsClosed (M : Set G))
(hfinite :
โ S : Set (Subgroup G), S.Finite โ S โ ๐ โ sInf S โ K = โค) :
sInf ๐ โ K = โคCompactness step: if the closed normal subgroups satisfying \(M \sqcup K = \top\) are already stable under finite intersections, then they are stable under arbitrary intersections.
Show proof
by
rw [eq_top_iff]
intro g _
by_cases h๐ : ๐.Nonempty
ยท rcases h๐ with โจMโ, hMโโฉ
let coset : Set G := {x | gโปยน * x โ K}
let I := {M : Subgroup G // M โ ๐}
let F : I โ Set G := fun i => (i.1 : Set G) โฉ coset
have hcosetClosed : IsClosed coset := by
simpa [coset] using hKclosed.preimage (continuous_mul_left gโปยน)
have hclosed : โ i : I, IsClosed (F i) := by
intro i
exact (hMclosed i.1 i.2).inter hcosetClosed
have hfiniteNonempty : โ s : Finset I, (โ i โ s, F i).Nonempty := by
intro s
let S : Set (Subgroup G) := (fun i : I => i.1) '' (s : Set _)
have hSfinite : S.Finite := s.finite_toSet.image _
have hSsub : S โ ๐ := by
rintro M โจi, _hi, rflโฉ
exact i.2
have htop : sInf S โ K = โค := hfinite S hSfinite hSsub
have hgmem : g โ sInf S โ K := by
rw [htop]
exact Subgroup.mem_top g
rcases (Subgroup.mem_sup_of_normal_right (s := sInf S) (t := K) (x := g)).1 hgmem with
โจl, hlS, k, hk, hlkโฉ
refine โจl, ?_โฉ
simp only [Set.mem_iInter]
intro i hi
constructor
ยท exact (Subgroup.mem_sInf.mp hlS) i.1 โจi, hi, rflโฉ
ยท have hg : g = l * k := hlk.symm
have : gโปยน * l = kโปยน := by
rw [hg]
simp only [mul_inv_rev, mul_assoc, inv_mul_cancel, mul_one]
change gโปยน * l โ K
rw [this]
exact K.inv_mem hk
rcases CompactSpace.iInter_nonempty (t := F) hclosed hfiniteNonempty with โจx, hxโฉ
have hxall : โ i : I, x โ F i := by
simpa [F] using hx
have hxL : x โ sInf ๐ := by
rw [Subgroup.mem_sInf]
intro M hM
exact (hxall โจM, hMโฉ).1
have hxK : gโปยน * x โ K := (hxall โจMโ, hMโโฉ).2
have hxmem : x * (gโปยน * x)โปยน โ sInf ๐ โ K :=
Subgroup.mul_mem_sup hxL (K.inv_mem hxK)
simpa [mul_assoc] using hxmem
ยท have h๐_empty : ๐ = โ
:= Set.not_nonempty_iff_eq_empty.mp h๐
have htop : sInf ๐ = โค := by
rw [h๐_empty, sInf_empty]
simp only [htop, le_top, sup_of_le_left, Subgroup.mem_top]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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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.
โกtheorem maximal_open_normal_intersections_nonabelian_simple
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
(K : Subgroup G) [K.Normal] [IsSimpleGroup (G โงธ K)]
(hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G โงธ K))
(hKclosed : IsClosed (K : Set G))
(๐ : Set (Subgroup G))
(hMnormal : โ M โ ๐, M.Normal)
(hMclosed : โ M โ ๐, IsClosed (M : Set G))
(hMtop : โ M โ ๐, M โ K = โค) :
sInf ๐ โ K = โคMaximal open normal subgroups with a fixed nonabelian simple quotient are closed under arbitrary intersections.
Show proof
maximal_open_normal_intersections_compactness_step K hKclosed ๐ hMclosed
(fun _S hSfinite hSsub =>
finite_sInf_sup_eq_top_of_noncomm_simple_quotient K hquotNoncomm hSfinite
(fun M hM => hMnormal M (hSsub hM))
(fun M hM => hMtop M (hSsub hM)))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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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.
โก