ProCGroups/Profinite/MathlibBridge.lean

1import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

2import ProCGroups.Profinite.Basic

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/ProCGroups/Profinite/MathlibBridge.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

12/-!

13# Profinite group basics

15Basic profinite group predicates, finite quotient facts, and standard closure properties used throughout the pro-C library.

18namespace ProCGroups

20universe u v

24variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

26/-- Every bundled profinite group is profinite in the working unbundled sense. -/

27theorem of_profiniteGrp (G : ProfiniteGrp) : IsProfiniteGroup G := by

28 letI : CompactSpace G := by infer_instance

29 letI : T2Space G := by infer_instance

30 letI : TotallyDisconnectedSpace G := by infer_instance

31 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩

33/-- Bundle an unbundled profinite group as Mathlib's `ProfiniteGrp`. -/

34noncomputable def toProfiniteGrp (hG : IsProfiniteGroup G) : ProfiniteGrp.{u} := by

35 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

36 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG

37 exact ProfiniteGrp.of G

39/-- The bundled profinite group has the same underlying type as the original profinite group. -/

41 (IsProfiniteGroup.toProfiniteGrp (G := G) hG : Type u) = G := by

42 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

43 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG

44 rfl

46/-- Profiniteness transports across continuous multiplicative equivalences. -/

47theorem ofContinuousMulEquiv {H : Type v} [Group H] [TopologicalSpace H]

48 [IsTopologicalGroup H] (hG : IsProfiniteGroup G) (e : G ≃ₜ* H) :

50 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

51 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG

52 let PG : ProfiniteGrp := ProfiniteGrp.of G

53 simpa using of_profiniteGrp (G := ProfiniteGrp.ofContinuousMulEquiv (G := PG) e)

57end ProCGroups