From fd28b269a9bedb2fb58eda468bbd38e46acb1e0d Mon Sep 17 00:00:00 2001
From: zjj <j.jj@jj.j>
Date: Thu, 15 Aug 2024 18:53:25 +0100
Subject: [PATCH] closed subgroup

---
 BrauerGroup/Profinite/Basic.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/BrauerGroup/Profinite/Basic.lean b/BrauerGroup/Profinite/Basic.lean
index 9ccee77..1d5c780 100644
--- 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)