Continuous finite quotients of a topological group

A finite group Q occurs as a continuous finite quotient of a topological group G, written IsFiniteContinuousQuotient G Q, when Q is finite and some surjective homomorphism G →* Q has open kernel. The predicate is phrased through the kernel and not through a topology on Q: when G is a topological group (IsTopologicalGroup G), a homomorphism into a finite discrete group is continuous exactly when its kernel is open (MonoidHom.continuous_iff_isOpen_ker), so nothing is lost, and the predicate is manifestly invariant under isomorphism of Q. The continuous finite quotients of G are, up to isomorphism, the quotients G ⧸ U by its open normal subgroups of finite index; when G is compact with separately continuous multiplication (in particular a compact topological group) every open subgroup has finite index, so they are the quotients by all open normal subgroups.

The finite-quotient determinacy of topologically finitely generated profinite groups, the main consumer of this predicate, is in TauCeti.Topology.Algebra.Group.Profinite.FiniteQuotients.

Main definitions

• TauCeti.IsFiniteContinuousQuotient: Q occurs as a continuous finite quotient of G.

Main results

• TauCeti.isFiniteContinuousQuotient_iff_exists_openNormalSubgroup: the continuous finite quotients of G are the quotients by its open normal subgroups of finite index, up to isomorphism.
• TauCeti.isFiniteContinuousQuotient_iff_exists_continuous: for a finite discrete Q and a topological group G, the predicate is the existence of a continuous surjection G →* Q.
• TauCeti.isFiniteContinuousQuotient_congr_left, TauCeti.isFiniteContinuousQuotient_congr_right: the predicate depends only on the topological isomorphism class of G and on the isomorphism class of Q.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 3.2.

def TauCeti.IsFiniteContinuousQuotient (G : Type u) [Group G] [TopologicalSpace G] (Q : Type v) [Group Q] : Prop

Q occurs as a continuous finite quotient of the topological group G: Q is finite and some surjective homomorphism G →* Q has open kernel. The group Q carries no topology; when G is a topological group (IsTopologicalGroup G) and Q carries the discrete topology, an open kernel is the same as continuity (isFiniteContinuousQuotient_iff_exists_continuous). Finiteness is part of the predicate because an open kernel alone does not force it: a discrete group is a quotient of itself with open kernel. When G is compact with separately continuous multiplication (in particular a compact topological group) every open subgroup has finite index, so there finiteness is automatic (OpenNormalSubgroup.isFiniteContinuousQuotient).

Equations

• TauCeti.IsFiniteContinuousQuotient G Q = (Finite Q ∧ ∃ (f : G →* Q), Function.Surjective ⇑f ∧ IsOpen ↑f.ker)

theorem TauCeti.isFiniteContinuousQuotient_iff {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] : IsFiniteContinuousQuotient G Q ↔ Finite Q ∧ ∃ (f : G →* Q), Function.Surjective ⇑f ∧ IsOpen ↑f.ker

A group Q is a continuous finite quotient of G exactly when it is finite and there is a surjective homomorphism G →* Q with open kernel.

theorem OpenNormalSubgroup.isFiniteContinuousQuotient {G : Type u} [Group G] [TopologicalSpace G] (U : OpenNormalSubgroup G) [(↑U.toOpenSubgroup).FiniteIndex] : TauCeti.IsFiniteContinuousQuotient G (G ⧸ ↑U.toOpenSubgroup)

The quotient of G by an open normal subgroup of finite index is a continuous finite quotient of G. When G is compact with separately continuous multiplication (in particular a compact topological group) every open subgroup has finite index (OpenSubgroup.finiteIndex_toSubgroup), so the finite-index instance is then found automatically.

theorem TauCeti.IsFiniteContinuousQuotient.finite {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] (h : IsFiniteContinuousQuotient G Q) : Finite Q

A continuous finite quotient is finite.

theorem TauCeti.isFiniteContinuousQuotient_iff_exists_continuous {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] [IsTopologicalGroup G] [Finite Q] [TopologicalSpace Q] [DiscreteTopology Q] : IsFiniteContinuousQuotient G Q ↔ ∃ (f : G →* Q), Function.Surjective ⇑f ∧ Continuous ⇑f

For a topological group G and a finite group Q carrying the discrete topology, occurring as a continuous finite quotient is the existence of a continuous surjective homomorphism onto Q.

theorem TauCeti.IsFiniteContinuousQuotient.comp {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] {G' : Type u_1} [Group G'] [TopologicalSpace G'] (h : IsFiniteContinuousQuotient G Q) {φ : G' →* G} (hφ : Continuous ⇑φ) (hsurj : Function.Surjective ⇑φ) : IsFiniteContinuousQuotient G' Q

If G is a continuous surjective image of G', then every continuous finite quotient of G is also a continuous finite quotient of G'.

theorem TauCeti.IsFiniteContinuousQuotient.of_mulEquiv {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] {Q' : Type u_1} [Group Q'] (h : IsFiniteContinuousQuotient G Q) (e : Q ≃* Q') : IsFiniteContinuousQuotient G Q'

Occurring as a continuous finite quotient is transported along an isomorphism of the quotient.

theorem TauCeti.isFiniteContinuousQuotient_congr_left {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] {G' : Type u_1} [Group G'] [TopologicalSpace G'] (e : G ≃ₜ* G') : IsFiniteContinuousQuotient G Q ↔ IsFiniteContinuousQuotient G' Q

Occurring as a continuous finite quotient depends only on the topological isomorphism class of the group.

theorem TauCeti.isFiniteContinuousQuotient_congr_right {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] {Q' : Type u_1} [Group Q'] (e : Q ≃* Q') : IsFiniteContinuousQuotient G Q ↔ IsFiniteContinuousQuotient G Q'

Occurring as a continuous finite quotient depends only on the isomorphism class of the quotient.

theorem TauCeti.isFiniteContinuousQuotient_iff_exists_openNormalSubgroup {G : Type u} [Group G] [TopologicalSpace G] {Q : Type v} [Group Q] : IsFiniteContinuousQuotient G Q ↔ ∃ (U : OpenNormalSubgroup G), (↑U.toOpenSubgroup).FiniteIndex ∧ Nonempty (G ⧸ ↑U.toOpenSubgroup ≃* Q)

The continuous finite quotients of G are, up to isomorphism, exactly the quotients of G by its open normal subgroups of finite index.