ProCGroups.ProC.OpenNormalSubgroups.Separation
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
theorem mem_closed_iff_forall_openNormal_quotient
{G : Type u} [Group G] [TopologicalSpace G]
(hG : IsProfiniteGroup G) {S : Set G} (hSclosed : IsClosed S) {x : G} :
x ∈ S ↔
∀ U : OpenNormalSubgroup G,
∃ y ∈ S, QuotientGroup.mk' (U : Subgroup G) y =
QuotientGroup.mk' (U : Subgroup G) xMembership in a closed subset of a profinite group can be tested on all open-normal quotients.
Show proof
by
letI : IsTopologicalGroup G := hG.isTopologicalGroup
letI : CompactSpace G := hG.compactSpace
letI : T2Space G := hG.t2Space
letI : TotallyDisconnectedSpace G := hG.totallyDisconnectedSpace
constructor
· intro hx U
exact ⟨x, hx, rfl⟩
· intro hx
by_contra hxS
let A : Set G := (fun y : G => y⁻¹ * x) '' S
have hAclosed : IsClosed A := by
exact (hSclosed.isCompact.image (continuous_inv.mul continuous_const)).isClosed
have h1A : (1 : G) ∉ A := by
rintro ⟨y, hyS, hyx⟩
have hxy : x = y := by
have h := congrArg (fun z : G => y * z) hyx
simpa [mul_assoc] using h
exact hxS (by simpa [hxy] using hyS)
have hAcomplOpen : IsOpen (Aᶜ) := hAclosed.isOpen_compl
have h1Acompl : (1 : G) ∈ Aᶜ := h1A
rcases ProC.exists_openNormalSubgroup_sub_open_nhds_of_one
(G := G) hAcomplOpen h1Acompl with ⟨U, hUA⟩
rcases hx U with ⟨y, hyS, hyquot⟩
have hyU : y⁻¹ * x ∈ (U : Subgroup G) :=
QuotientGroup.eq.1 hyquot
have hyA : y⁻¹ * x ∈ A := ⟨y, hyS, rfl⟩
exact hUA hyU hyAProof. 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. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. 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.
□theorem eq_of_forall_quotientProj_eq (hG : IsProfiniteGroup G) {x y : G}
(hxy : ∀ U : OpenNormalSubgroup G, quotientProj U x = quotientProj U y) :
x = yTwo open normal subgroups are equal if all their quotient projections agree.
Show proof
by
by_contra hne
have hdiff : x⁻¹ * y ≠ 1 := by
intro h
exact hne (inv_mul_eq_one.mp h)
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
let W : Set G := ({x⁻¹ * y} : Set G)ᶜ
have hW : IsOpen W := by
simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
have h1W : (1 : G) ∈ W := by
simpa [W] using hdiff.symm
rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
have hmem : x⁻¹ * y ∈ (U : Subgroup G) := by
exact QuotientGroup.eq.1 (hxy U)
exact hdiff <| by
have hxW : x⁻¹ * y ∈ W := hUW hmem
simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxWProof. 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. 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 mem_sup_of_quotient_mk_mem_map
{Q : Type u} [TopologicalSpace Q] [Group Q]
(H : Subgroup Q) (U : OpenNormalSubgroup Q)
{y : Q}
(hy :
QuotientGroup.mk' (U : Subgroup Q) y ∈
H.map (QuotientGroup.mk' (U : Subgroup Q))) :
y ∈ H ⊔ (U : Subgroup Q)If the image of y modulo an open normal subgroup lies in the image of H, then y lies in H \(\sqcup\) U.
Show proof
by
rcases hy with ⟨h, hh, hhy⟩
have hU : h⁻¹ * y ∈ (U : Subgroup Q) := by
have hq : QuotientGroup.mk' (U : Subgroup Q) (h⁻¹ * y) = 1 := by
calc
QuotientGroup.mk' (U : Subgroup Q) (h⁻¹ * y)
= (QuotientGroup.mk' (U : Subgroup Q) h)⁻¹ *
QuotientGroup.mk' (U : Subgroup Q) y := by
simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_mul,
QuotientGroup.mk_inv]
_ = (QuotientGroup.mk' (U : Subgroup Q) h)⁻¹ *
QuotientGroup.mk' (U : Subgroup Q) h := by rw [← hhy]
_ = 1 := by simp only [QuotientGroup.mk'_apply, inv_mul_cancel]
exact (QuotientGroup.eq_one_iff (N := (U : Subgroup Q)) (h⁻¹ * y)).1 hq
exact
(Subgroup.mem_sup_of_normal_right (s := H) (t := (U : Subgroup Q))).2
⟨h, hh, h⁻¹ * y, hU, by simp only [mul_inv_cancel_left]⟩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. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. 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 mem_closedSubgroup_of_forall_openNormal_sup
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
[CompactSpace Q] [TotallyDisconnectedSpace Q]
(H : ClosedSubgroup Q) {y : Q}
(hy : ∀ U : OpenNormalSubgroup Q,
y ∈ (H : Subgroup Q) ⊔ (U : Subgroup Q)) :
y ∈ (H : Subgroup Q)Closed-subgroup membership can be checked after adjoining every open normal subgroup.
Show proof
by
have hEq := closedSubgroup_eq_sInf_open (G := Q) H
rw [hEq]
rw [Subgroup.mem_sInf]
intro K hK
let Kopen : OpenSubgroup Q := ⟨K, hK.1⟩
let U : OpenNormalSubgroup Q := OpenNormalSubgroup.normalCore Kopen
have hyU := hy U
have hsup_le : (H : Subgroup Q) ⊔ (U : Subgroup Q) ≤ K := by
refine sup_le hK.2 ?_
exact OpenNormalSubgroup.normalCore_le Kopen
exact hsup_le hyUProof. 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\). Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. 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.
□def openNormalSubgroup_inf
{Q : Type u} [TopologicalSpace Q] [Group Q]
(U V : OpenNormalSubgroup Q) : OpenNormalSubgroup Q where
toOpenSubgroup :=
{ toSubgroup := (U : Subgroup Q) ⊓ (V : Subgroup Q)
isOpen' :=
(ProCGroups.openNormalSubgroup_isOpen (G := Q) U).inter
(ProCGroups.openNormalSubgroup_isOpen (G := Q) V) }
isNormal' := by
change ((U : Subgroup Q) ⊓ (V : Subgroup Q)).Normal
infer_instanceThe intersection of two open normal subgroups is open and normal.
theorem exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
[CompactSpace Q] [TotallyDisconnectedSpace Q]
(H : ClosedSubgroup Q) {x : Q} (hx : x ∉ (H : Subgroup Q))
(U : OpenNormalSubgroup Q) :
∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
x ∉ (H : Subgroup Q) ⊔ (W : Subgroup Q)Cofinal separation from a closed subgroup by open normal subgroups.
Show proof
by
classical
have hEq := closedSubgroup_eq_sInf_open (G := Q) H
have hxInf :
x ∉ sInf {N : Subgroup Q | IsOpen (N : Set Q) ∧ (H : Subgroup Q) ≤ N} := by
simpa [← hEq] using hx
rw [Subgroup.mem_sInf] at hxInf
push_neg at hxInf
rcases hxInf with ⟨N, hN, hxN⟩
let Nopen : OpenSubgroup Q := ⟨N, hN.1⟩
let Ncore : OpenNormalSubgroup Q := OpenNormalSubgroup.normalCore Nopen
let W : OpenNormalSubgroup Q := openNormalSubgroup_inf Ncore U
refine ⟨W, ?_, ?_⟩
· intro y hy
exact hy.2
· intro hxSup
have hsup_le_N : (H : Subgroup Q) ⊔ (W : Subgroup Q) ≤ N := by
refine sup_le hN.2 ?_
intro y hy
exact OpenNormalSubgroup.normalCore_le Nopen hy.1
exact hxN (hsup_le_N hxSup)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\). Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. 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.
□def openNormalSubgroup_sup_normal
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(K : Subgroup Q) [K.Normal] (U : OpenNormalSubgroup Q) :
OpenNormalSubgroup Q where
toOpenSubgroup :=
{ toSubgroup := K ⊔ (U : Subgroup Q)
isOpen' :=
Subgroup.isOpen_of_openSubgroup (K ⊔ (U : Subgroup Q))
(show (U : Subgroup Q) ≤ K ⊔ (U : Subgroup Q) from le_sup_right) }
isNormal' := by
change (K ⊔ (U : Subgroup Q)).Normal
infer_instanceThe open normal subgroup K \(\sqcup\) U, where K is normal and U is open normal.
theorem cofinal_openNormal_cyclic_containment_of_finite_lift
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
[CompactSpace Q] [TotallyDisconnectedSpace Q]
(x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
(hnotK : x ^ n ∉ K)
(hfinite : ∀ W : OpenNormalSubgroup Q,
x ^ n ∉ K ⊔ (W : Subgroup Q) →
let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
QuotientGroup.mk' (V : Subgroup Q) y ∈
((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
ClosedSubgroup Q) :
Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
∀ U : OpenNormalSubgroup Q,
∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
let V : OpenNormalSubgroup QShow proof
openNormalSubgroup_sup_normal K W
∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
QuotientGroup.mk' (V : Subgroup Q) y ∈
((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
ClosedSubgroup Q) :
Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q)) := by
intro U
let Kclosed : ClosedSubgroup Q := ⟨K, hKclosed⟩
rcases
exists_openNormalSubgroup_le_not_mem_sup_closedSubgroup
(H := Kclosed) hnotK U with
⟨W, hWU, hnotW⟩
refine ⟨W, hWU, ?_⟩
change x ^ n ∉ K ⊔ (W : Subgroup Q) at hnotW
exact hfinite W hnotWProof. 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 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 centralizerOf_zpow_le_cyclic_join_closedNormal_of_cofinal_openNormal_image
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
[CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q]
(x : Q) (n : ℤ) (K : Subgroup Q) [K.Normal] (hKclosed : IsClosed (K : Set Q))
(himage : ∀ U : OpenNormalSubgroup Q,
∃ W : OpenNormalSubgroup Q, (W : Subgroup Q) ≤ (U : Subgroup Q) ∧
let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
∀ y : Q, y ∈ ProCGroups.GroupTheory.centralizerOf (x ^ n) →
QuotientGroup.mk' (V : Subgroup Q) y ∈
((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
ClosedSubgroup Q) :
Subgroup Q).map (QuotientGroup.mk' (V : Subgroup Q))) :
ProCGroups.GroupTheory.centralizerOf (x ^ n) ≤
((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
ClosedSubgroup Q) :
Subgroup Q) ⊔ KCofinal image criterion for bounding a centralizer by a cyclic subgroup joined with a closed normal subgroup.
Show proof
by
let L : Subgroup Q :=
((ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q) :
ClosedSubgroup Q) : Subgroup Q)
let H : ClosedSubgroup Q :=
⟨L ⊔ K,
Subgroup.isClosed_sup_of_normal L K
(ProCGroups.Generation.closedSubgroupGenerated (G := Q) ({x} : Set Q)).isClosed'
hKclosed⟩
intro y hy
apply mem_closedSubgroup_of_forall_openNormal_sup H
intro U
rcases himage U with ⟨W, hWU, hWimage⟩
let V : OpenNormalSubgroup Q := openNormalSubgroup_sup_normal K W
have hyVL :
QuotientGroup.mk' (V : Subgroup Q) y ∈
L.map (QuotientGroup.mk' (V : Subgroup Q)) := by
simpa [L, V] using hWimage y hy
have hySupV : y ∈ L ⊔ (V : Subgroup Q) :=
mem_sup_of_quotient_mk_mem_map L V hyVL
have hle : L ⊔ (V : Subgroup Q) ≤ (H : Subgroup Q) ⊔ (U : Subgroup Q) := by
change L ⊔ (K ⊔ (W : Subgroup Q)) ≤ (L ⊔ K) ⊔ (U : Subgroup Q)
refine sup_le ?_ ?_
· exact (show L ≤ L ⊔ K from le_sup_left).trans le_sup_left
· refine sup_le ?_ ?_
· exact (show K ≤ L ⊔ K from le_sup_right).trans le_sup_left
· exact hWU.trans le_sup_right
exact hle hySupVProof. 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\). 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.
□theorem continuousMonoidHom_ext_openNormalQuotients
{A : Type u} [Group A] [TopologicalSpace A]
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(hH : IsProfiniteGroup H) {φ ψ : A →ₜ* H}
(h : ∀ U : OpenNormalSubgroup H,
(OpenNormalSubgroup.quotientProj U).comp φ =
(OpenNormalSubgroup.quotientProj U).comp ψ) :
φ = ψContinuous homomorphisms into a profinite group are equal if they agree after every open-normal finite quotient of the target.
Show proof
by
ext x
exact OpenNormalSubgroup.eq_of_forall_quotientProj_eq (G := H) hH
(fun U => by
have hU := congrArg (fun f : A →ₜ* H ⧸ (U : Subgroup H) => f x) (h U)
simpa using hU)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.
□