ProCGroups.ProC.Subgroups.Closed
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
theorem of_closedSubgroup
(hIso : FiniteGroupClass.IsomClosed C)
(hSub : FiniteGroupClass.SubgroupClosed C)
(_hQuot : FiniteGroupClass.QuotientClosed C)
(hG : IsProCGroup C G) (H : ClosedSubgroup G) :
IsProCGroup C ↥(H : Subgroup G)A closed subgroup of a pro-\(C\) group is pro-\(C\).
Show proof
by
refine ⟨IsProfiniteGroup.of_closedSubgroup (G := G) hG.isProfinite H, ?_⟩
intro W hW h1W
letI : CompactSpace G := IsProCGroup.compactSpace hG
letI : T2Space G := IsProCGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
have hW_nhds : W ∈ 𝓝 (1 : H) := hW.mem_nhds h1W
rcases (mem_nhds_subtype (H : Set G) (1 : H) W).1 hW_nhds with
⟨W₀, hW₀_nhds, hW₀W⟩
rcases mem_nhds_iff.mp hW₀_nhds with ⟨W', hW'W₀, hW'open, h1W'⟩
rcases hG.hasOpenNormalBasisInClass W' hW'open h1W' with
⟨V, hVW', hCV⟩
let VH : OpenNormalSubgroup H :=
OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V
have hVHW : (((VH : Subgroup H) : Set H)) ⊆ W := by
intro x hx
exact hW₀W <| by
change x.1 ∈ W₀
exact hW'W₀ (hVW' hx)
let ψ : H →* G ⧸ (V : Subgroup G) :=
(QuotientGroup.mk' (V : Subgroup G)).comp ((H : Subgroup G).subtype)
have hRange : C ψ.range := hSub ψ.range hCV
have hKerEq : (VH : Subgroup H) = ψ.ker := by
ext x
constructor
· intro hx
simpa [MonoidHom.mem_ker, ψ] using
(QuotientGroup.eq_one_iff (N := (V : Subgroup G)) x.1).2 hx
· intro hx
exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) x.1).1
(by simpa [MonoidHom.mem_ker, ψ] using hx)
have hQuotVH : C (H ⧸ (VH : Subgroup H)) := by
let e1 : H ⧸ (VH : Subgroup H) ≃* H ⧸ ψ.ker :=
QuotientGroup.quotientMulEquivOfEq hKerEq
exact hIso
⟨(e1.trans (QuotientGroup.quotientKerEquivRange ψ)).symm⟩
hRange
exact ⟨VH, hVHW, hQuotVH⟩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 of_isClosed_subgroup
(hIso : FiniteGroupClass.IsomClosed C)
(hSub : FiniteGroupClass.SubgroupClosed C)
(hQuot : FiniteGroupClass.QuotientClosed C)
(hG : IsProCGroup C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :
IsProCGroup C HA closed ordinary subgroup of a pro-\(C\) group is pro-\(C\) with the induced topology.
Show proof
by
exact ProCGroups.of_isClosed_subgroup_of_closedSubgroup
(G := G) (P := fun H => IsProCGroup C ↥H)
(of_closedSubgroup (C := C) hIso hSub hQuot hG) H hHProof. 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. 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.
□theorem of_closedSubgroup_of_fullFormation
(hC : FiniteGroupClass.FullFormation C)
(hG : IsProCGroup C G) (H : ClosedSubgroup G) :
IsProCGroup C ↥(H : Subgroup G)Closed-subgroup permanence for pro-\(C\) groups from a full formation package.
Show proof
of_closedSubgroup hC.isomClosed hC.subgroupClosed hC.quotientClosed hG HProof. 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. 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.
□theorem of_isClosed_subgroup_of_fullFormation
(hC : FiniteGroupClass.FullFormation C)
(hG : IsProCGroup C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :
IsProCGroup C HClosed-subgroup permanence in ordinary subgroup form from a full formation package.
Show proof
of_isClosed_subgroup hC.isomClosed hC.subgroupClosed hC.quotientClosed hG H hHProof. 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. 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.
□theorem range
(hIso : FiniteGroupClass.IsomClosed C)
(hQuot : FiniteGroupClass.QuotientClosed C)
(hG : IsProCGroup C G)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
(f : G →ₜ* H) :
IsProCGroup C f.toMonoidHom.rangeThe range of a continuous homomorphism from a pro-\(C\) group to a Hausdorff topological group is again pro-\(C\), with the induced subtype topology.
Show proof
by
letI : CompactSpace G := hG.compactSpace
let K : Subgroup G := f.toMonoidHom.ker
have hKclosed : IsClosed (K : Set G) := by
dsimp [K]
exact f.isClosed_ker
letI : K.Normal := by
dsimp [K]
infer_instance
have hQuotG : IsProCGroup C (G ⧸ K) :=
quotient_closedNormalSubgroup (C := C) hIso hQuot hG K hKclosed
have e : (G ⧸ K) ≃ₜ* f.toMonoidHom.range := by
simpa [K] using ContinuousMonoidHom.quotientKerContinuousMulEquivRange f
exact IsProCGroup.ofContinuousMulEquiv (C := C) (G := G ⧸ K) hIso hQuot hQuotG eProof. 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. 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. 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. 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.
□theorem of_closedSubgroup
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients]
[hG : ProCGroup ProC G] (H : ClosedSubgroup G) :
ProCGroup ProC ↥(H : Subgroup G)A closed subgroup of a pro-\(C\) group, bundled as a closed subgroup, is again a pro-\(C\) group.
Show proof
ProCGroup.of_isProCGroup ProC ↥(H : Subgroup G)
(IsProCGroup.of_closedSubgroup
ProC.finiteQuotientIsomClosed
ProC.finiteQuotientHereditary.subgroupClosed
ProC.finiteQuotientQuotientClosed
hG.isProCGroup H)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. 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.
□theorem of_isClosed_subgroup
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients]
[hG : ProCGroup ProC G] (H : Subgroup G) (hH : IsClosed (H : Set G)) :
ProCGroup ProC HA closed subgroup of a pro-\(C\) group is again a pro-\(C\) group. The finite quotient input is the standard Melnikov-formation package together with hereditary subgroup closure.
Show proof
ProCGroup.of_isProCGroup ProC H
(IsProCGroup.of_isClosed_subgroup
ProC.finiteQuotientIsomClosed
ProC.finiteQuotientHereditary.subgroupClosed
ProC.finiteQuotientQuotientClosed
hG.isProCGroup H hH)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. 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.
□theorem quotient_closedNormalSubgroup
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
[hG : ProCGroup ProC G] (K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
ProCGroup ProC (G ⧸ K)If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by a closed normal subgroup is again pro-\(C\). The proof reconstructs \(G/K\) as the inverse limit of the finite quotients \(G/U\) over the open normal subgroups \(U\) containing \(K\), and then applies the inverse-limit permanence theorem.
Show proof
ProCGroup.of_isProCGroup ProC (G ⧸ K)
(ProCGroups.ProC.quotient_closedNormalSubgroup
ProC.finiteQuotientIsomClosed
ProC.finiteQuotientQuotientClosed
hG.isProCGroup K hK)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. 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.
□theorem range
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
[ProC.DeterminedByFiniteQuotients]
[hG : ProCGroup ProC G]
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
(f : G →ₜ* H) :
ProCGroup ProC f.toMonoidHom.rangeThe range of a continuous homomorphism from a pro-\(C\) group to a Hausdorff topological group is again a pro-\(C\) group, with the induced subtype topology.
Show proof
ProCGroup.of_isProCGroup ProC f.toMonoidHom.range
(IsProCGroup.range
ProC.finiteQuotientIsomClosed
ProC.finiteQuotientQuotientClosed
hG.isProCGroup f)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. 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. 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. 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.
□theorem of_surjective
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
[ProC.DeterminedByFiniteQuotients]
[hG : ProCGroup ProC G]
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
(f : G →ₜ* H) (hf : Function.Surjective f) :
ProCGroup ProC HA Hausdorff continuous quotient of a pro-\(C\) group is again a pro-\(C\) group.
Show proof
by
let R : Subgroup H := f.toMonoidHom.range
have hR : ProCGroup ProC R := range (ProC := ProC) (G := G) f
letI : ProCGroup ProC R := hR
have hcompactR : CompactSpace R := hR.isProCGroup.compactSpace
letI : CompactSpace R := hcompactR
let e : R ≃ₜ* H :=
ContinuousMulEquiv.ofBijectiveCompactToT2 (Subgroup.subtype R)
continuous_subtype_val
⟨by
intro x y hxy
exact Subtype.ext hxy,
by
intro h
rcases hf h with ⟨g, rfl⟩
exact ⟨⟨f g, ⟨g, rfl⟩⟩, rfl⟩⟩
exact ProCGroup.ofContinuousMulEquiv (G := R) ProC eProof. 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. 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. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□theorem extension
(hIso : FiniteGroupClass.IsomClosed C)
(hQuot : FiniteGroupClass.QuotientClosed C)
(hExt : FiniteGroupClass.ExtensionClosed C)
(hE : IsProfiniteGroup E)
(K : Subgroup E) [K.Normal]
(hK : IsProCGroup C K) (hQ : IsProCGroup C (E ⧸ K)) :
IsProCGroup C EExtension permanence for pro-\(C\) groups. We assume E is already profinite; the pro-\(C\) conclusion is then obtained by checking each open-normal finite quotient of E. Extensions of pro-\(C\) groups remain pro-\(C\) once the ambient group is known to be profinite.
Show proof
by
refine IsProCGroup.of_allOpenNormalQuotients (C := C) hE ?_
intro U
letI : CompactSpace E := IsProfiniteGroup.compactSpace hE
letI : T2Space E := IsProfiniteGroup.t2Space hE
letI : CompactSpace (E ⧸ K) := IsProfiniteGroup.compactSpace hQ.isProfinite
letI : T2Space (E ⧸ K) := IsProfiniteGroup.t2Space hQ.isProfinite
letI : CompactSpace K := IsProfiniteGroup.compactSpace hK.isProfinite
letI : T2Space K := IsProfiniteGroup.t2Space hK.isProfinite
let M : Subgroup E := K ⊔ (U : Subgroup E)
let Wsub : Subgroup (E ⧸ K) := Subgroup.map (QuotientGroup.mk' K) M
have hWclosed : IsClosed (Wsub : Set (E ⧸ K)) := by
have hMclosed : IsClosed (M : Set E) := by
have hMopen : IsOpen (M : Set E) := by
exact Subgroup.isOpen_of_openSubgroup M (show (U : Subgroup E) ≤ M from le_sup_right)
exact Subgroup.isClosed_of_isOpen M hMopen
have hMcompact : IsCompact (M : Set E) := hMclosed.isCompact
have hcont : Continuous (QuotientGroup.mk' K : E → E ⧸ K) := continuous_quotient_mk'
have himage : IsCompact ((QuotientGroup.mk' K) '' (M : Set E)) := hMcompact.image hcont
have hEq : (QuotientGroup.mk' K) '' (M : Set E) = (Wsub : Set (E ⧸ K)) := by
ext x
simp only [QuotientGroup.mk'_apply, mem_image, SetLike.mem_coe, Subgroup.coe_map, M, Wsub]
rw [← hEq]
exact himage.isClosed
have hWfinite : Finite ((E ⧸ K) ⧸ Wsub) := by
have hMopen : IsOpen (M : Set E) := by
exact Subgroup.isOpen_of_openSubgroup M (show (U : Subgroup E) ≤ M from le_sup_right)
have hMfinite : Finite (E ⧸ M) :=
(subgroup_isOpen_iff_isClosed_finite_quotient (G := E) (U := M)).1 hMopen |>.2
let e : (E ⧸ K) ⧸ Wsub ≃* E ⧸ M := by
simpa [Wsub, M, Subgroup.map_sup] using
(QuotientGroup.quotientQuotientEquivQuotient K M (show K ≤ M from le_sup_left))
exact Finite.of_injective e e.injective
have hWopen : IsOpen (Wsub : Set (E ⧸ K)) :=
(subgroup_isOpen_iff_isClosed_finite_quotient (G := E ⧸ K) (U := Wsub)).2
⟨hWclosed, hWfinite⟩
letI : Wsub.Normal := by
dsimp [Wsub, M]
have hMnormal : M.Normal := by infer_instance
exact Subgroup.Normal.map hMnormal (QuotientGroup.mk' K) (QuotientGroup.mk'_surjective K)
let W : OpenNormalSubgroup (E ⧸ K) :=
{ toOpenSubgroup := ⟨Wsub, hWopen⟩
isNormal' := inferInstance }
have hQuotM : C (E ⧸ M) := by
let e : (E ⧸ K) ⧸ (W : Subgroup (E ⧸ K)) ≃* E ⧸ M := by
simpa [W, Wsub, M, Subgroup.map_sup] using
(QuotientGroup.quotientQuotientEquivQuotient K M (show K ≤ M from le_sup_left))
exact hIso ⟨e⟩
(IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hIso hQuot hQ W)
let KU : OpenNormalSubgroup K :=
OpenNormalSubgroup.comap (K.subtype) continuous_subtype_val U
let ψ : K →* E ⧸ (U : Subgroup E) :=
(QuotientGroup.mk' (U : Subgroup E)).comp K.subtype
have hKerEq : (KU : Subgroup K) = ψ.ker := by
ext x
constructor
· intro hx
simpa [MonoidHom.mem_ker, KU, ψ] using
(QuotientGroup.eq_one_iff (N := (U : Subgroup E)) x.1).2 hx
· intro hx
exact (QuotientGroup.eq_one_iff (N := (U : Subgroup E)) x.1).1
(by simpa [MonoidHom.mem_ker, KU, ψ] using hx)
have hKernelC : C ψ.range := by
have hQuotKU : C (K ⧸ (KU : Subgroup K)) :=
IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hIso hQuot hK KU
let e1 : K ⧸ (KU : Subgroup K) ≃* K ⧸ ψ.ker :=
QuotientGroup.quotientMulEquivOfEq hKerEq
exact hIso ⟨e1.trans (QuotientGroup.quotientKerEquivRange ψ)⟩ hQuotKU
let L : Subgroup (E ⧸ (U : Subgroup E)) := Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) K
have hRangeEq : ψ.range = L := by
ext x
simp only [MonoidHom.mem_range, MonoidHom.coe_comp, QuotientGroup.coe_mk', Subgroup.coe_subtype,
Function.comp_apply, Subtype.exists, exists_prop, Subgroup.mem_map, QuotientGroup.mk'_apply, ψ, L]
have hLC : C L := by
exact hIso ⟨MulEquiv.subgroupCongr hRangeEq⟩ hKernelC
have hMapUbot : Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) (U : Subgroup E) = ⊥ := by
ext x
constructor
· intro hx
rcases (Subgroup.mem_map).1 hx with ⟨u, hu, hux⟩
rw [Subgroup.mem_bot]
have hu1 : QuotientGroup.mk' (U : Subgroup E) u = 1 :=
(QuotientGroup.eq_one_iff (N := (U : Subgroup E)) u).2 hu
exact hux.symm.trans hu1
· intro hx
rcases Subgroup.mem_bot.1 hx with rfl
exact ⟨1, U.one_mem, by simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]⟩
have hMapM : Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M = L := by
calc
Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M
= Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) K ⊔
Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) (U : Subgroup E) := by
simp only [Subgroup.map_sup, QuotientGroup.map_mk'_self, bot_le, sup_of_le_left, M]
_ = L ⊔ ⊥ := by simp only [hMapUbot, bot_le, sup_of_le_left, L]
_ = L := by simp only [bot_le, sup_of_le_left]
have hQuotL : C ((E ⧸ (U : Subgroup E)) ⧸ L) := by
let e0 : (E ⧸ (U : Subgroup E)) ⧸ L ≃* (E ⧸ (U : Subgroup E)) ⧸
Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M :=
QuotientGroup.quotientMulEquivOfEq hMapM.symm
let e1 : (E ⧸ (U : Subgroup E)) ⧸
Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M ≃* E ⧸ M :=
QuotientGroup.quotientQuotientEquivQuotient (U : Subgroup E) M
(show (U : Subgroup E) ≤ M from le_sup_right)
exact hIso ⟨(e0.trans e1).symm⟩ hQuotM
letI : L.Normal := by
dsimp [L]
exact Subgroup.Normal.map inferInstance (QuotientGroup.mk' (U : Subgroup E))
(QuotientGroup.mk'_surjective (U : Subgroup E))
exact hExt L hLC hQuotLProof. 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. 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. 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. 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.
□