ProCGroups.Profinite.MathlibBridge
This module studies mathlib bridge for pro cgroups. Every bundled profinite group is profinite in the working unbundled sense. Bundle an unbundled profinite group as the standard library's ProfiniteGrp.
import
- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
- ProCGroups.Profinite.Basic
theorem of_profiniteGrp (G : ProfiniteGrp) : IsProfiniteGroup GEvery bundled profinite group is profinite in the working unbundled sense.
Show proof
by
letI : CompactSpace G := by infer_instance
letI : T2Space G := by infer_instance
letI : TotallyDisconnectedSpace G := by infer_instance
exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩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. 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. 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. 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 pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□noncomputable def toProfiniteGrp (hG : IsProfiniteGroup G) : ProfiniteGrp.{u} := by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
exact ProfiniteGrp.of GBundle an unbundled profinite group as the standard library's ProfiniteGrp.
@[simp] theorem coe_toProfiniteGrp (hG : IsProfiniteGroup G) :
(IsProfiniteGroup.toProfiniteGrp (G := G) hG : Type u) = GThe bundled profinite group has the same underlying type as the original profinite group.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
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. 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. 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. 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 pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem ofContinuousMulEquiv {H : Type v} [Group H] [TopologicalSpace H]
[IsTopologicalGroup H] (hG : IsProfiniteGroup G) (e : G ≃ₜ* H) :
IsProfiniteGroup HA continuous multiplicative equivalence transports profiniteness of the underlying topological group.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
let PG : ProfiniteGrp := ProfiniteGrp.of G
simpa using of_profiniteGrp (G := ProfiniteGrp.ofContinuousMulEquiv (G := PG) e)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. 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. 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. 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.
□