ProCGroups.Topologies.OpenSubgroup
This module studies open subgroup for pro cgroups. The \(\top\) open subgroup is canonically equivalent to the ambient topological group. The open-subgroup comparison equivalence evaluates on representatives.
import
- Mathlib.Topology.Algebra.OpenSubgroup
- Mathlib.Topology.Algebra.ContinuousMonoidHom
noncomputable def topContinuousMulEquiv
(G : Type u) [TopologicalSpace G] [Group G] :
↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ* G :=
{ toMulEquiv :=
{ toFun := fun x => x.1
invFun := fun x => ⟨x, by simp only [toSubgroup_top, Subgroup.mem_top]⟩
left_inv := by
intro x
ext
rfl
right_inv := by
intro x
rfl
map_mul' := by
intro x y
rfl }
continuous_toFun := continuous_subtype_val
continuous_invFun := by
exact Continuous.subtype_mk continuous_id (by intro x; simp only [toSubgroup_top, id_eq, Subgroup.mem_top]) }The \(\top\) open subgroup is canonically equivalent to the ambient topological group.
@[simp] theorem topContinuousMulEquiv_apply
(G : Type u) [TopologicalSpace G] [Group G]
(x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :
topContinuousMulEquiv G x = x.1The open-subgroup comparison equivalence evaluates on representatives.
Show proof
rflProof. 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. 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. 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.
□@[simp] theorem topContinuousMulEquiv_symm_apply
(G : Type u) [TopologicalSpace G] [Group G] (x : G) :
(topContinuousMulEquiv G).symm x = ⟨x, by simp only [toSubgroup_top, Subgroup.mem_top]⟩The inverse comparison equivalence is evaluated by the same coordinate data, read in the opposite direction.
Show proof
rflProof. 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. 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. 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.
□