ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
theorem quotient_mk_mem_commutator_of_surjective_image_mem_commutator
{N K : Type u} [Group N] [Group K]
(f : N →* K) (hf : Function.Surjective f)
(U : Subgroup N) [U.Normal] (hkerU : f.ker ≤ U)
{n : N} (hn : f n ∈ commutator K) :
QuotientGroup.mk' U n ∈ commutator (N ⧸ U)A quotient-level commutator descent along a surjective homomorphism. If \(f: N \to K\) is onto, f n is in the ordinary commutator subgroup of K, and the kernel of f dies in the quotient \(N/U\), then the image of n in \(N/U\) is in the ordinary commutator subgroup.
Show proof
by
have hcomm_le :
commutator K ≤ (commutator N).map f := by
rw [_root_.map_commutator_eq]
have hrange : f.range = (⊤ : Subgroup K) := by
ext k
constructor
· intro hk
trivial
· intro _hk
rcases hf k with ⟨n, rfl⟩
exact ⟨n, rfl⟩
rw [hrange]
exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
rcases hcomm_le hn with ⟨c, hc, hcn⟩
have hdiff : n * c⁻¹ ∈ U := by
apply hkerU
change f (n * c⁻¹) = 1
rw [map_mul, map_inv, ← hcn, mul_inv_cancel]
have hquot :
QuotientGroup.mk' U n = QuotientGroup.mk' U c :=
(QuotientGroup.eq_iff_div_mem (N := U)).2 (by
simpa [div_eq_mul_inv] using hdiff)
have hcquot :
QuotientGroup.mk' U c ∈ commutator (N ⧸ U) := by
have hmap :
(commutator N).map (QuotientGroup.mk' U) ≤
commutator (N ⧸ U) := by
rw [_root_.map_commutator_eq]
exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
exact hmap ⟨c, hc, rfl⟩
simpa [hquot] using hcquotProof. 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. 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 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 mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass C G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))) :
x ∈ Subgroup.closedCommutator GMembership in the closed commutator subgroup of a pro-\(C\) group is detected on every open-normal quotient whose quotient lies in \(C\).
Show proof
by
let S := openNormalSubgroupInClassSystem C G
let e := openNormalSubgroupInClassMulEquivInverseLimit (C := C) (G := G) hForm hG
letI : Nonempty (OpenNormalSubgroupInClass C G) := openNormalSubgroupInClass_nonempty hG
letI : Nonempty (OrderDual (OpenNormalSubgroupInClass C G)) := inferInstance
letI : CompactSpace G := hG.compactSpace
letI : T2Space G := hG.t2Space
letI : TotallyDisconnectedSpace G := hG.totallyDisconnectedSpace
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Group (S.X U) := fun U => by
dsimp [S, openNormalSubgroupInClassSystem]
infer_instance
letI : InverseSystems.IsGroupSystem S := by
dsimp [S]
infer_instance
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Finite (S.X U) := fun U => by
dsimp [S, openNormalSubgroupInClassSystem]
exact hForm.finiteOnly (OrderDual.ofDual U).2
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), DiscreteTopology (S.X U) := fun U => by
dsimp [S, openNormalSubgroupInClassSystem]
exact QuotientGroup.discreteTopology
(openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), CompactSpace (S.X U) := fun _ => by
infer_instance
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), T2Space (S.X U) := fun _ => by
infer_instance
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G),
TotallyDisconnectedSpace (S.X U) := fun _ => by
infer_instance
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), IsTopologicalGroup (S.X U) :=
fun _ => by
infer_instance
letI : Group S.inverseLimit := by infer_instance
letI : IsTopologicalGroup S.inverseLimit := by infer_instance
have hlim : e x ∈ Subgroup.closedCommutator S.inverseLimit := by
rw [ProCGroups.Abelian.mem_closedCommutator_inverseLimit_iff
(S := S) (directed_openNormalSubgroupInClass (C := C) (G := G) hForm)]
intro U
have hproj :
S.projection U (e x) =
openNormalSubgroupInClassProj (C := C) (G := G) U x := by
simpa [S, e] using
openNormalSubgroupInClassMulEquivInverseLimit_projection
(C := C) (G := G) hForm hG U x
rw [hproj]
simpa [openNormalSubgroupInClassProj] using hx (OrderDual.ofDual U)
have hmap :
e x ∈
((Subgroup.closedCommutator G).map e.toMulEquiv.toMonoidHom :
Subgroup S.inverseLimit) := by
rw [Subgroup.closedCommutator_map_eq_of_equiv e]
exact hlim
rcases hmap with ⟨y, hy, hyx⟩
have hy_eq : y = x := by
exact e.toMulEquiv.injective hyx
simpa [hy_eq] using hyProof. 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. 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 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 density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G} :
x ∈ Subgroup.closedCommutator G ↔
∀ U : OpenNormalSubgroupInClass C G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))Closed-commutator membership in a pro-\(C\) group is equivalent to closed-commutator membership after every open-normal quotient whose quotient lies in \(C\).
Show proof
by
constructor
· intro hx U
exact Subgroup.closedCommutator_map_le (OpenNormalSubgroupInClass.quotientProj (C := C) U)
⟨x, hx, rfl⟩
· exact mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient hForm hGProof. 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. 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 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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass C G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
commutator (G ⧸ (U.1 : Subgroup G))) :
x ∈ Subgroup.closedCommutator GTo prove membership in the closed commutator subgroup of a pro-\(C\) group, it is enough to prove ordinary commutator membership in every finite open-normal quotient in \(C\). This is the finite-stage form used by Magnus-kernel arguments: each quotient stage is discrete, so its closed commutator is the ordinary algebraic commutator subgroup.
Show proof
mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient hForm hG
(by
intro U
simpa [Subgroup.closedCommutator_eq_commutator_of_discrete] using hx U)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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass C G,
∃ V : OpenNormalSubgroupInClass C G,
(V.1 : Subgroup G) ≤ (U.1 : Subgroup G) ∧
QuotientGroup.mk' (V.1 : Subgroup G) x ∈
commutator (G ⧸ (V.1 : Subgroup G))) :
x ∈ Subgroup.closedCommutator GCofinal finite-stage form of closed-commutator detection. It is enough to prove ordinary commutator membership after passing, below every open-normal quotient in \(C\), to some smaller open-normal quotient in \(C\).
Show proof
by
refine
mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
hForm hG ?_
intro U
rcases hx U with ⟨V, hVU, hxV⟩
let qVU : G ⧸ (V.1 : Subgroup G) →* G ⧸ (U.1 : Subgroup G) :=
QuotientGroup.map (V.1 : Subgroup G) (U.1 : Subgroup G)
(MonoidHom.id G) (by
intro g hg
exact hVU hg)
have hq :
qVU (QuotientGroup.mk' (V.1 : Subgroup G) x) =
QuotientGroup.mk' (U.1 : Subgroup G) x := by
simp only [QuotientGroup.mk'_apply, QuotientGroup.map_mk, MonoidHom.id_apply, qVU]
have hcomm_map :
(commutator (G ⧸ (V.1 : Subgroup G))).map qVU ≤
commutator (G ⧸ (U.1 : Subgroup G)) := by
rw [_root_.map_commutator_eq]
exact Subgroup.commutator_mono (by intro y hy; trivial) (by intro y hy; trivial)
have hxU :
qVU (QuotientGroup.mk' (V.1 : Subgroup G) x) ∈
commutator (G ⧸ (U.1 : Subgroup G)) :=
hcomm_map ⟨QuotientGroup.mk' (V.1 : Subgroup G) x, hxV, rfl⟩
simpa [hq] using hxUProof. 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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G} :
x ∈ Subgroup.closedCommutator G ↔
∀ U : OpenNormalSubgroupInClass C G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
commutator (G ⧸ (U.1 : Subgroup G))Closed-commutator membership in a pro-\(C\) group is equivalent to ordinary commutator membership after every finite open-normal quotient in \(C\).
Show proof
by
rw [mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient hForm hG]
constructor
· intro hx U
simpa [Subgroup.closedCommutator_eq_commutator_of_discrete] using hx U
· intro hx U
simpa [Subgroup.closedCommutator_eq_commutator_of_discrete] using hx UProof. 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. 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 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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
[hG : ProCGroup ProC G] {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))) :
x ∈ Subgroup.closedCommutator GMembership in the closed commutator subgroup of a pro-\(C\) group is detected on every open-normal quotient whose quotient lies in \(C\).
Show proof
IsProCGroup.mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient
(C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup hxProof. 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. 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 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 density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
[hG : ProCGroup ProC G] {x : G} :
x ∈ Subgroup.closedCommutator G ↔
∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))Closed-commutator membership in a pro-\(C\) group is equivalent to closed-commutator membership after every open-normal quotient whose quotient lies in \(C\).
Show proof
IsProCGroup.mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient
(C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroupProof. 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. 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 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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
[hG : ProCGroup ProC G] {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
commutator (G ⧸ (U.1 : Subgroup G))) :
x ∈ Subgroup.closedCommutator GFor bundled pro-\(C\) groups, ordinary commutator membership in every discrete finite quotient stage implies membership in the closed commutator subgroup.
Show proof
IsProCGroup.mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
(C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup hxProof. 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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
[hG : ProCGroup ProC G] {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
∃ V : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
(V.1 : Subgroup G) ≤ (U.1 : Subgroup G) ∧
QuotientGroup.mk' (V.1 : Subgroup G) x ∈
commutator (G ⧸ (V.1 : Subgroup G))) :
x ∈ Subgroup.closedCommutator GFor bundled pro-\(C\) groups, the cofinal finite-stage commutator criterion implies membership in the closed commutator subgroup.
Show proof
IsProCGroup.mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
(C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup hxProof. 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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
[hG : ProCGroup ProC G] {x : G} :
x ∈ Subgroup.closedCommutator G ↔
∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
QuotientGroup.mk' (U.1 : Subgroup G) x ∈
commutator (G ⧸ (U.1 : Subgroup G))For bundled pro-\(C\) groups, membership in the closed commutator subgroup is equivalent to ordinary commutator membership in every discrete finite quotient stage.
Show proof
IsProCGroup.mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator
(C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroupProof. 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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□