closed subgroup

Whysoserioushah · Aug 15, 2024 · fd28b26 · fd28b26
1 parent d8ab250
commit fd28b26
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/BrauerGroup/Profinite/Basic.lean b/BrauerGroup/Profinite/Basic.lean
@@ -63,6 +63,8 @@ instance : CoeSort ProfiniteGrp (Type u) where
 
 instance (G : ProfiniteGrp) : Group G := G.group
 
+instance (G : ProfiniteGrp) : TopologicalGroup G := G.topologicalGroup
+
 def of (G : Type u) [Group G] [TopologicalSpace G] [TopologicalGroup G]
     [CompactSpace G] [TotallyDisconnectedSpace G] : ProfiniteGrp where
   toCompHaus :=
@@ -134,6 +136,14 @@ def ofFiniteGrp (G : FiniteGrp) : ProfiniteGrp :=
   letI : TopologicalGroup G := {}
   of G
 
+def ofClosedSubgroup {G : ProfiniteGrp}
+    (H : Subgroup G) (hH : IsClosed (H : Set G)) : ProfiniteGrp :=
+  letI : CompactSpace H := ClosedEmbedding.compactSpace (f := H.subtype)
+    { induced := rfl
+      inj := H.subtype_injective
+      isClosed_range := by simpa }
+  of H
+
 section
 
 variable {J : Type v} [Category J] (F : J ⥤ FiniteGrp)