Pro-C groups and the pro-C completion

Let C be a class of finite groups, in the sense of TauCeti.FiniteGroupClass. A topological group is pro-C when each of its quotients by an open normal subgroup is a finite group in C. The C-kernel proCKernel C G is the intersection of the open normal subgroups whose quotient lies in C, and the pro-C completion is proCCompletion C G = G ⧸ proCKernel C G. For profinite G this is the universal pro-C group receiving a continuous homomorphism from G.

For a compact group, every open subgroup containing the C-kernel contains an open normal subgroup whose quotient lies in C; consequently the completion is pro-C. The completion is characterized by its universal property for continuous homomorphisms from G to profinite pro-C groups.

For the class of finite p-groups, proCKernel_finiteGroupClassP_eq_proPKernel identifies the C-kernel with the pro-p kernel, and proCCompletion.equivMaximalProPQuotient gives the corresponding topological isomorphism of completions.

Membership is transported through Shrink, so the class, the groups, and the continuous homomorphisms between them may live in independent universes.

Main definitions

• TauCeti.IsProC: every quotient by an open normal subgroup is a finite group in the class.
• TauCeti.proCKernel: the intersection of the open normal subgroups with quotient in the class.
• TauCeti.proCCompletion: the quotient G ⧸ proCKernel C G.
• TauCeti.proCCompletion.mk: the canonical quotient homomorphism.
• TauCeti.proCCompletion.map: the functorial action on continuous homomorphisms.
• TauCeti.proCCompletion.lift: the canonical factorisation of a continuous homomorphism to a profinite pro-C group.

Main results

• TauCeti.IsProC.of_surjective, TauCeti.IsProC.quotient: the pro-C property passes to continuous surjective images and to quotients.
• TauCeti.isClosed_proCKernel: the C-kernel is closed, so the completion is profinite again.
• TauCeti.exists_openNormalSubgroup_memFinite_le: an open subgroup containing the C-kernel contains a member of the defining family.
• TauCeti.isProC_proCCompletion: the pro-C completion is pro-C.
• TauCeti.existsUnique_continuousMonoidHom_proCCompletion: a continuous homomorphism from G to a profinite pro-C group factors uniquely and continuously through the completion.
• TauCeti.proCKernel_eq_bot_iff: G is pro-C exactly when its C-kernel is trivial; with TauCeti.proCKernel_proCCompletion_eq_bot this is idempotence of the completion.
• TauCeti.proCKernel_finiteGroupClassP_eq_proPKernel: for the class of finite p-groups the C-kernel is the pro-p kernel.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 2.1 and 3.2.
• The compactness and universal-property development is adapted from TauCeti.Topology.Algebra.Group.Profinite.MaximalProP.

def TauCeti.IsProC (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] : Prop

A topological group is pro-C when every quotient by an open normal subgroup is a finite group in the class C. For a profinite group these quotients are exactly its continuous finite quotients.

Equations

• TauCeti.IsProC C G = ∀ (U : OpenNormalSubgroup G), C.MemFinite (G ⧸ ↑U.toOpenSubgroup)

def TauCeti.proCKernel (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] : Subgroup G

The C-kernel of a topological group G: the intersection of the open normal subgroups of G whose quotient lies in C. For profinite G it is the kernel of the universal continuous homomorphism from G to a pro-C group.

Equations

• TauCeti.proCKernel C G = ⨅ (U : { U : OpenNormalSubgroup G // C.MemFinite (G ⧸ ↑U.toOpenSubgroup) }), ↑(↑U).toOpenSubgroup

instance TauCeti.proCKernel_normal (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] : (proCKernel C G).Normal

The C-kernel is a normal subgroup.

@[reducible, inline]

abbrev TauCeti.proCCompletion (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] : Type v

The pro-C completion G ⧸ proCKernel C G.

Equations

• TauCeti.proCCompletion C G = (G ⧸ TauCeti.proCKernel C G)

@[reducible, inline]

abbrev TauCeti.proCCompletion.mk (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] : G →* proCCompletion C G

The canonical homomorphism from G to its pro-C completion.

Equations

• TauCeti.proCCompletion.mk C G = QuotientGroup.mk' (TauCeti.proCKernel C G)

@[simp]

theorem TauCeti.proCCompletion.mk_apply (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] (x : G) : (mk C G) x = ↑x

The canonical quotient homomorphism sends an element to its quotient class.

theorem TauCeti.proCCompletion.mk_surjective (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] : Function.Surjective ⇑(mk C G)

The canonical homomorphism to the pro-C completion is surjective.

theorem TauCeti.proCCompletion.continuous_mk (C : FiniteGroupClass) (G : Type v) [Group G] [TopologicalSpace G] : Continuous ⇑(mk C G)

The canonical homomorphism to the pro-C completion is continuous.

theorem TauCeti.isProC_iff {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] : IsProC C G ↔ ∀ (U : OpenNormalSubgroup G), C.MemFinite (G ⧸ ↑U.toOpenSubgroup)

A group is pro-C exactly when its quotients by open normal subgroups lie in C.

theorem TauCeti.IsProC.of_surjective {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (hG : IsProC C G) (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : IsProC C H

A continuous surjective image of a pro-C group is pro-C.

theorem TauCeti.IsProC.quotient {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] (hG : IsProC C G) (N : Subgroup G) [N.Normal] : IsProC C (G ⧸ N)

A quotient of a pro-C group by a normal subgroup is pro-C. No closedness hypothesis is needed: closedness controls whether the quotient is Hausdorff, not whether its finite quotients lie in C.

theorem TauCeti.mem_proCKernel_iff {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {x : G} : x ∈ proCKernel C G ↔ ∀ (U : OpenNormalSubgroup G), C.MemFinite (G ⧸ ↑U.toOpenSubgroup) → x ∈ ↑U.toOpenSubgroup

Membership in the C-kernel, unfolded over the defining family.

theorem TauCeti.proCKernel_le {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {U : OpenNormalSubgroup G} (hU : C.MemFinite (G ⧸ ↑U.toOpenSubgroup)) : proCKernel C G ≤ ↑U.toOpenSubgroup

The C-kernel is contained in every open normal subgroup whose quotient lies in C.

instance TauCeti.isClosed_proCKernel {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed ↑(proCKernel C G)

The C-kernel is closed, so its quotient is profinite when G is profinite.

Trivial completions

theorem TauCeti.proCKernel_eq_top_iff {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] : proCKernel C G = ⊤ ↔ ∀ (U : OpenNormalSubgroup G), C.MemFinite (G ⧸ ↑U.toOpenSubgroup) → ↑U.toOpenSubgroup = ⊤

The C-kernel is the whole group exactly when every open normal subgroup with quotient in C is the whole group. Equivalently, G has no nontrivial continuous quotient in C.

theorem TauCeti.proCCompletion.subsingleton_iff {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] : Subsingleton (proCCompletion C G) ↔ proCKernel C G = ⊤

The pro-C completion is trivial exactly when the C-kernel is the whole group.

Functoriality

theorem TauCeti.proCKernel_le_comap {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : proCKernel C G ≤ Subgroup.comap f (proCKernel C H)

A continuous homomorphism carries the C-kernel into the C-kernel.

theorem TauCeti.map_proCKernel_le {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : Subgroup.map f (proCKernel C G) ≤ proCKernel C H

The image of the C-kernel under a continuous homomorphism lies in the C-kernel of the target.

theorem TauCeti.map_proCKernel_eq {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) : Subgroup.map e.toMonoidHom (proCKernel C G) = proCKernel C H

Continuous multiplicative equivalences identify the C-kernels of their source and target. In particular, the C-kernel is characteristic under continuous automorphisms.

def TauCeti.proCCompletion.map {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : proCCompletion C G →* proCCompletion C H

The map induced on pro-C completions by a continuous homomorphism.

Equations

• TauCeti.proCCompletion.map f hf = QuotientGroup.map (TauCeti.proCKernel C G) (TauCeti.proCKernel C H) f ⋯

@[simp]

theorem TauCeti.proCCompletion.map_mk {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (x : G) : (map f hf) ↑x = (mk C H) (f x)

The induced map on pro-C completions is computed on classes by f.

theorem TauCeti.proCCompletion.continuous_map {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) : Continuous ⇑(map f hf)

The induced map on pro-C completions is continuous.

@[simp]

theorem TauCeti.proCCompletion.map_id {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] : map (MonoidHom.id G) ⋯ = MonoidHom.id (proCCompletion C G)

Functoriality: the identity induces the identity.

@[simp]

theorem TauCeti.proCCompletion.map_comp {C : FiniteGroupClass} {G : Type v} {H : Type w} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] {K : Type x} [Group K] [TopologicalSpace K] (f : G →* H) (hf : Continuous ⇑f) (g : H →* K) (hg : Continuous ⇑g) : map (g.comp f) ⋯ = (map g hg).comp (map f hf)

Functoriality: the induced maps compose.

The compactness step

theorem TauCeti.exists_openNormalSubgroup_memFinite_le {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Subgroup G} (hM : IsOpen ↑M) (hKM : proCKernel C G ≤ M) : ∃ (U : OpenNormalSubgroup G), C.MemFinite (G ⧸ ↑U.toOpenSubgroup) ∧ ↑U.toOpenSubgroup ≤ M

An open subgroup containing the C-kernel contains an open normal subgroup whose quotient lies in C.

theorem TauCeti.memFinite_quotient_of_proCKernel_le {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {U : OpenNormalSubgroup G} (hU : proCKernel C G ≤ ↑U.toOpenSubgroup) : C.MemFinite (G ⧸ ↑U.toOpenSubgroup)

An open normal subgroup containing the C-kernel has its quotient in C.

theorem TauCeti.proCKernel_le_iff_memFinite_quotient {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {U : OpenNormalSubgroup G} : proCKernel C G ≤ ↑U.toOpenSubgroup ↔ C.MemFinite (G ⧸ ↑U.toOpenSubgroup)

For an open normal subgroup of a compact group, containing the C-kernel is the same as having its quotient in C.

theorem TauCeti.isProC_proCCompletion {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : IsProC C (proCCompletion C G)

The pro-C completion is pro-C.

The universal property

theorem TauCeti.proCKernel_le_ker {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) : proCKernel C G ≤ f.ker

A continuous homomorphism to a profinite pro-C group kills the C-kernel.

def TauCeti.proCCompletion.lift {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) : proCCompletion C G →* P

The canonical factorisation of a continuous homomorphism to a profinite pro-C group through the pro-C completion.

Equations

• TauCeti.proCCompletion.lift hP f hf = QuotientGroup.lift (TauCeti.proCKernel C G) f ⋯

@[simp]

theorem TauCeti.proCCompletion.lift_mk {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) (x : G) : (lift hP f hf) ↑x = f x

The factorisation through the pro-C completion computes as f on classes.

@[simp]

theorem TauCeti.proCCompletion.lift_comp_mk {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) : (lift hP f hf).comp (mk C G) = f

The factorisation through the pro-C completion recovers f.

theorem TauCeti.proCCompletion.continuous_lift {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) : Continuous ⇑(lift hP f hf)

The factorisation through the pro-C completion is continuous.

theorem TauCeti.proCCompletion.lift_unique {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) {g : proCCompletion C G →* P} (hg : ∀ (x : G), g ((mk C G) x) = f x) : g = lift hP f hf

The factorisation through the pro-C completion is the only homomorphism restricting to f along the quotient map.

theorem TauCeti.proCCompletion.lift_comp_map {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] {G' : Type x} [Group G'] [TopologicalSpace G'] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) (u : G' →* G) (hu : Continuous ⇑u) : (lift hP f hf).comp (map u hu) = lift hP (f.comp u) ⋯

Naturality in the source: the factorisation of f ∘ u is the factorisation of f precomposed with the map induced by u.

theorem TauCeti.proCCompletion.comp_lift {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] {Q : Type x} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [TotallyDisconnectedSpace Q] (hP : IsProC C P) (hQ : IsProC C Q) (f : G →* P) (hf : Continuous ⇑f) (v : P →* Q) (hv : Continuous ⇑v) : v.comp (lift hP f hf) = lift hQ (v.comp f) ⋯

Naturality in the target: postcomposing the factorisation of f with a continuous homomorphism of profinite pro-C groups gives the factorisation of the composite.

theorem TauCeti.existsUnique_continuousMonoidHom_proCCompletion {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] {P : Type w} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProC C P) (f : G →* P) (hf : Continuous ⇑f) : ∃! g : proCCompletion C G →* P, Continuous ⇑g ∧ ∀ (x : G), g ((proCCompletion.mk C G) x) = f x

The universal property of the pro-C completion. A continuous homomorphism to a profinite pro-C group factors uniquely and continuously through the canonical quotient map.

Pro-C groups and idempotence

theorem TauCeti.proCKernel_eq_bot_iff {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : proCKernel C G = ⊥ ↔ IsProC C G

A profinite group is pro-C exactly when its C-kernel is trivial.

theorem TauCeti.IsProC.proCKernel_eq_bot {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProC C G) : proCKernel C G = ⊥

The C-kernel of a profinite pro-C group is trivial.

def TauCeti.proCCompletion.equivOfIsProC {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProC C G) : proCCompletion C G ≃ₜ* G

The canonical continuous multiplicative equivalence from the pro-C completion of a profinite pro-C group to the group itself.

Equations

• TauCeti.proCCompletion.equivOfIsProC hG = { toMulEquiv := (QuotientGroup.quotientMulEquivOfEq ⋯).trans QuotientGroup.quotientBot, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.proCCompletion.equivOfIsProC_mk {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProC C G) (x : G) : (equivOfIsProC hG) ↑x = x

The canonical equivalence from a pro-C group's completion sends each class to its representative.

theorem TauCeti.proCKernel_proCCompletion_eq_bot {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : proCKernel C (proCCompletion C G) = ⊥

Idempotence. The C-kernel of a pro-C completion is trivial.

def TauCeti.proCCompletion.idempotentEquiv {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : proCCompletion C (proCCompletion C G) ≃ₜ* proCCompletion C G

Idempotence. Applying the pro-C completion twice gives a group canonically continuously equivalent to applying it once.

Equations

• TauCeti.proCCompletion.idempotentEquiv = TauCeti.proCCompletion.equivOfIsProC ⋯

@[simp]

theorem TauCeti.proCCompletion.idempotentEquiv_mk {C : FiniteGroupClass} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : proCCompletion C G) : idempotentEquiv ↑x = x

The idempotence equivalence sends each class to its representative.

Distinguished classes of finite groups

theorem TauCeti.isProC_finiteGroupClassP_iff {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} : IsProC (finiteGroupClassP p) G ↔ IsProP p G

For the class of finite p-groups, being pro-C is being pro-p.

theorem TauCeti.proCKernel_finiteGroupClassP_eq_proPKernel {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} : proCKernel (finiteGroupClassP p) G = proPKernel p G

The C-kernel of the class of finite p-groups is the pro-p kernel. The two subgroups are cut out by different index sets: the pro-p kernel by the open normal subgroups with p-group quotient, the C-kernel by those whose quotient is in addition recorded as finite, which for a compact group is automatic.

def TauCeti.proCCompletion.equivMaximalProPQuotient (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] : proCCompletion (finiteGroupClassP p) G ≃ₜ* maximalProPQuotient p G

The pro-C completion at the class of finite p-groups is the maximal pro-p quotient.

Equations

• TauCeti.proCCompletion.equivMaximalProPQuotient p G = { toMulEquiv := QuotientGroup.quotientMulEquivOfEq ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.proCCompletion.equivMaximalProPQuotient_mk {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} (x : G) : (equivMaximalProPQuotient p G) ↑x = ↑x

The comparison with the maximal pro-p quotient sends a class to the class of the same element.

theorem TauCeti.proCKernel_finiteGroupClassTrivial_eq_top {G : Type v} [Group G] [TopologicalSpace G] : proCKernel finiteGroupClassTrivial G = ⊤

The C-kernel for the class of trivial finite groups is the whole group.

theorem TauCeti.proCCompletion.subsingleton_finiteGroupClassTrivial {G : Type v} [Group G] [TopologicalSpace G] : Subsingleton (proCCompletion finiteGroupClassTrivial G)

The completion for the class of trivial finite groups is trivial.

theorem TauCeti.proCKernel_finiteGroupClassAll_eq_bot {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : proCKernel finiteGroupClassAll G = ⊥

Every profinite group is pro-C for the class of all finite groups, so its C-kernel is trivial. Its pro-C completion is then the group itself, by TauCeti.proCCompletion.equivOfIsProC.