Profinite groups: the finite-quotient limit description

The unbundled workhorse of profinite group theory, phrased for the type-class stack [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (with TotallyDisconnectedSpace G only where needed) so that consumers outside the ProfiniteGrp category can use them directly.

• The limit description: a family of cosets of the open normal subgroups of a compact totally disconnected group, compatible along the canonical quotient maps, is realized by a unique element of G (existsUnique_forall_mk_eq; Ribes and Zalesskii, Profinite Groups, Proposition 1.1.4). This is the unbundled counterpart of ProfiniteGrp.toLimit_surjective and ProfiniteGrp.toLimit_injective, which describe the same identification for the ProfiniteGrp category. The compactness input is IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed.
• Three companion forms of the same identification: a point of G is determined by its images in the finite quotients (eq_of_forall_mk_eq), a map into G is continuous as soon as all of its finite-quotient shadows are (continuous_iff_forall_continuous_mk), and a map into G has dense range exactly when it surjects onto every finite quotient (denseRange_iff_forall_surjective_mk).
• The same identification for homomorphisms: a family of homomorphisms H →* G ⧸ U compatible along the quotient maps is induced by a unique homomorphism H →* G (existsUnique_monoidHom_mk'_comp_eq).
• The same for subgroups: a family H of subgroups of the quotients G ⧸ U cuts out the closed subgroup limitSubgroup H of G (isClosed_limitSubgroup), and when H is compatible along the quotient maps and G is compact, its image in every G ⧸ U is exactly H U (map_mk'_limitSubgroup). Conversely a closed subgroup is cut out by its own images (limitSubgroup_map_mk'), so the two constructions are mutually inverse.
• Sequential reconstruction along a sequence N : ℕ → Subgroup G of closed subgroups of a compact group with trivial intersection: a coset sequence x k has a unique common representative if every representative of x (k + 1) also represents x k (existsUnique_forall_mk_eq_of_iInf_eq_bot). For decreasing N, this is the inverse-limit description. When the N k are normal and decreasing, a compatible sequence of homomorphisms into the quotients G ⧸ N k comes from a unique homomorphism into G (existsUnique_monoidHom_mk'_comp_eq_of_iInf_eq_bot); when they are normal, a map into G is continuous as soon as its composites with the quotient maps are (continuous_iff_forall_continuous_mk_of_iInf_eq_bot); and when they are open and decreasing they form a neighbourhood basis of 1 (hasAntitoneBasis_nhds_one_of_iInf_eq_bot). The lower p-series of a pro-p group is a decreasing sequence of closed normal subgroups with trivial intersection, and its terms are open when the group is topologically finitely generated.

theorem TauCeti.existsUnique_forall_mk_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : (U : OpenNormalSubgroup G) → G ⧸ ↑U.toOpenSubgroup) (hcompat : ∀ (U V : OpenNormalSubgroup G), ↑U.toOpenSubgroup ≤ ↑V.toOpenSubgroup → ∀ (g : G), (QuotientGroup.mk' ↑U.toOpenSubgroup) g = x U → (QuotientGroup.mk' ↑V.toOpenSubgroup) g = x V) : ∃! g : G, ∀ (U : OpenNormalSubgroup G), (QuotientGroup.mk' ↑U.toOpenSubgroup) g = x U

Limit description of a profinite group (unbundled). A family x of cosets of the open normal subgroups of a compact totally disconnected group G that is compatible along the canonical quotient maps is realized by a unique element of G: the natural map from G to the inverse limit of the quotients G ⧸ U over the open normal subgroups U is bijective. The bundled counterpart for the ProfiniteGrp category is ProfiniteGrp.toLimit_surjective together with ProfiniteGrp.toLimit_injective.

theorem TauCeti.eq_of_forall_mk_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x y : G} (h : ∀ (U : OpenNormalSubgroup G), ↑x = ↑y) : x = y

Two elements of a profinite group with the same class modulo every open normal subgroup are equal.

theorem TauCeti.continuous_iff_forall_continuous_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {X : Type u_2} [TopologicalSpace X] {f : X → G} : Continuous f ↔ ∀ (U : OpenNormalSubgroup G), Continuous fun (x : X) => ↑(f x)

A map into a profinite group is continuous exactly when all of its composites with the quotient maps onto the finite quotients are.

Only the quotients themselves are visible in the criterion, so continuity of a map built from the limit description can be checked one finite quotient at a time.

theorem TauCeti.denseRange_iff_forall_surjective_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {X : Type u_2} {f : X → G} : DenseRange f ↔ ∀ (U : OpenNormalSubgroup G), Function.Surjective fun (x : X) => ↑(f x)

A map into a profinite group has dense range exactly when its composite with the quotient map onto every finite quotient is surjective: the cosets of the open normal subgroups form a basis of the topology.

theorem TauCeti.existsUnique_monoidHom_mk'_comp_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type u_2} [MulOneClass H] (x : (N : OpenNormalSubgroup G) → H →* G ⧸ ↑N.toOpenSubgroup) (hx : ∀ ⦃N N' : OpenNormalSubgroup G⦄ (hle : N ≤ N'), (QuotientGroup.mapOfLE hle).comp (x N) = x N') : ∃! φ : H →* G, ∀ (N : OpenNormalSubgroup G), (QuotientGroup.mk' ↑N.toOpenSubgroup).comp φ = x N

Limit description of a profinite group, for homomorphisms. A family of homomorphisms x N : H →* G ⧸ N into the quotients of G by its open normal subgroups, compatible along the quotient maps G ⧸ N → G ⧸ N' for N ≤ N', is induced by a unique homomorphism H →* G. This is the universal property of G as the inverse limit of its finite quotients, for abstract homomorphisms out of a monoid H that carries no topology.

theorem TauCeti.existsUnique_monoidHom_mk'_comp_eq_of_forall_exists_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {ι : Type u_2} {N : ι → OpenNormalSubgroup G} (hcof : ∀ (U : OpenNormalSubgroup G), ∃ (i : ι), N i ≤ U) {H : Type u_3} [MulOneClass H] (x : (i : ι) → H →* G ⧸ ↑(N i).toOpenSubgroup) (hx : ∀ ⦃i j : ι⦄ (hle : N i ≤ N j), (QuotientGroup.mapOfLE hle).comp (x i) = x j) : ∃! φ : H →* G, ∀ (i : ι), (QuotientGroup.mk' ↑(N i).toOpenSubgroup).comp φ = x i

Limit description of a profinite group, for homomorphisms along a cofinal family. A family of homomorphisms x i : H →* G ⧸ N i into the quotients of G by open normal subgroups N i below every open normal subgroup of G, compatible along the quotient maps G ⧸ N i → G ⧸ N j for N i ≤ N j, is induced by a unique homomorphism H →* G: the cofinal family already computes the inverse limit of all the finite quotients.

def TauCeti.limitSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] (H : (U : OpenNormalSubgroup G) → Subgroup (G ⧸ ↑U.toOpenSubgroup)) : Subgroup G

The subgroup of G cut out by a family H of subgroups of its quotients G ⧸ U by open normal subgroups: the elements whose class modulo every U lies in H U. It is closed (isClosed_limitSubgroup), and when H is compatible along the quotient maps and G is compact, its image in every G ⧸ U is H U (map_mk'_limitSubgroup).

Equations

• TauCeti.limitSubgroup H = ⨅ (U : OpenNormalSubgroup G), Subgroup.comap (QuotientGroup.mk' ↑U.toOpenSubgroup) (H U)

@[simp]

theorem TauCeti.mem_limitSubgroup_iff {G : Type u_1} [Group G] [TopologicalSpace G] {H : (U : OpenNormalSubgroup G) → Subgroup (G ⧸ ↑U.toOpenSubgroup)} {g : G} : g ∈ limitSubgroup H ↔ ∀ (U : OpenNormalSubgroup G), ↑g ∈ H U

An element lies in limitSubgroup H exactly when its class modulo every U lies in H U.

theorem TauCeti.isClosed_limitSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : (U : OpenNormalSubgroup G) → Subgroup (G ⧸ ↑U.toOpenSubgroup)) : IsClosed ↑(limitSubgroup H)

The subgroup cut out by a family of subgroups of the quotients by open normal subgroups is closed.

theorem TauCeti.limitSubgroup_map_mk' {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (P : Subgroup G) (hP : IsClosed ↑P) : (limitSubgroup fun (U : OpenNormalSubgroup G) => Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) P) = P

A closed subgroup of a profinite group is cut out by the family of its images in the finite quotients. Together with map_mk'_limitSubgroup this identifies the closed subgroups of G with the compatible families of subgroups of the quotients G ⧸ U.

theorem TauCeti.map_mk'_limitSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {H : (U : OpenNormalSubgroup G) → Subgroup (G ⧸ ↑U.toOpenSubgroup)} [IsTopologicalGroup G] [CompactSpace G] (hH : ∀ ⦃U V : OpenNormalSubgroup G⦄ (hUV : U ≤ V), Subgroup.map (QuotientGroup.mapOfLE hUV) (H U) = H V) (U : OpenNormalSubgroup G) : Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) (limitSubgroup H) = H U

A family of subgroups of the quotients of a compact group by its open normal subgroups that is compatible along the quotient maps is the family of images of the subgroup it cuts out.

Sequential limit descriptions

The limit description of a profinite group runs over all of its open normal subgroups. When a sequence N : ℕ → Subgroup G of closed subgroups of a compact group G has trivial intersection, a coset sequence x k has a unique common representative if every representative of x (k + 1) also represents x k: the coset fibers are nested. For decreasing N, this is the inverse-limit description. When the N k are normal and decreasing, a compatible sequence of homomorphisms into the quotients G ⧸ N k is induced by a unique homomorphism into G; and when they are normal, continuity of a map into G can be tested one quotient at a time. When the N k are open and decreasing, they are a neighbourhood basis of 1. The lower p-series of a pro-p group is a decreasing sequence of closed normal subgroups with trivial intersection, and its terms are open when the group is topologically finitely generated.

theorem TauCeti.eq_of_forall_mk_eq_of_iInf_eq_bot {G : Type u_1} [Group G] {ι : Type u_2} {N : ι → Subgroup G} (hN : ⨅ (i : ι), N i = ⊥) {x y : G} (h : ∀ (i : ι), ↑x = ↑y) : x = y

Two elements of a group with the same class modulo every member of a family of subgroups with trivial intersection are equal.

theorem TauCeti.existsUnique_forall_mk_eq_of_iInf_eq_bot {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : ℕ → Subgroup G} [CompactSpace G] (hclosed : ∀ (k : ℕ), IsClosed ↑(N k)) (hN : ⨅ (k : ℕ), N k = ⊥) (x : (k : ℕ) → G ⧸ N k) (hcompat : ∀ (k : ℕ) (g : G), ↑g = x (k + 1) → ↑g = x k) : ∃! g : G, ∀ (k : ℕ), ↑g = x k

Sequential coset reconstruction in a compact group. Suppose the closed subgroups N k of a compact group G have trivial intersection, and let x k : G ⧸ N k. If every representative of x (k + 1) also represents x k, the coset fibers are nested and have a unique common representative in G. For decreasing N, this is the inverse-limit description of G using the coset spaces G ⧸ N k; normality is not required.

theorem TauCeti.existsUnique_monoidHom_mk'_comp_eq_of_iInf_eq_bot {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : ℕ → Subgroup G} [CompactSpace G] [∀ (k : ℕ), (N k).Normal] {H : Type u_2} [MulOneClass H] (hle : ∀ (k : ℕ), N (k + 1) ≤ N k) (hclosed : ∀ (k : ℕ), IsClosed ↑(N k)) (hN : ⨅ (k : ℕ), N k = ⊥) (x : (k : ℕ) → H →* G ⧸ N k) (hx : ∀ (k : ℕ), (QuotientGroup.mapOfLE ⋯).comp (x (k + 1)) = x k) : ∃! φ : H →* G, ∀ (k : ℕ), (QuotientGroup.mk' (N k)).comp φ = x k

Sequential limit description of a compact group, for homomorphisms. A sequence of homomorphisms x k : H →* G ⧸ N k into the quotients of a compact group G by a decreasing sequence of closed normal subgroups with trivial intersection, compatible along the quotient maps, is induced by a unique homomorphism H →* G.

theorem TauCeti.hasAntitoneBasis_nhds_one_of_iInf_eq_bot {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {N : ℕ → Subgroup G} [CompactSpace G] (hanti : Antitone N) (hopen : ∀ (k : ℕ), IsOpen ↑(N k)) (hN : ⨅ (k : ℕ), N k = ⊥) : (nhds 1).HasAntitoneBasis fun (k : ℕ) => ↑(N k)

A decreasing sequence of open subgroups with trivial intersection is a neighbourhood basis of 1 in a compact group.

theorem TauCeti.continuous_iff_forall_continuous_mk_of_iInf_eq_bot {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {ι : Type u_2} {N : ι → Subgroup G} [∀ (i : ι), (N i).Normal] (hclosed : ∀ (i : ι), IsClosed ↑(N i)) (hN : ⨅ (i : ι), N i = ⊥) {X : Type u_3} [TopologicalSpace X] {f : X → G} : Continuous f ↔ ∀ (i : ι), Continuous fun (x : X) => ↑(f x)

A map into a compact group G is continuous exactly when all of its composites with the quotient maps G → G ⧸ N i are, for any family of closed normal subgroups N i with trivial intersection: G embeds into the product of the Hausdorff quotients G ⧸ N i.