From 026ed8b85e7a3c83656d9de99ef81bf41ac20e9e Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 21 May 2024 06:21:51 -0400
Subject: [PATCH] feat: Add instance of SO(3) as topological group

---
 HepLean/GroupTheory/SO3/Basic.lean            |  8 ++----
 HepLean/SpaceTime/LorentzGroup/Rotations.lean | 28 +++++++++++++++++++
 2 files changed, 30 insertions(+), 6 deletions(-)
 create mode 100644 HepLean/SpaceTime/LorentzGroup/Rotations.lean

diff --git a/HepLean/GroupTheory/SO3/Basic.lean b/HepLean/GroupTheory/SO3/Basic.lean
index 0330885..60d513d 100644
--- a/HepLean/GroupTheory/SO3/Basic.lean
+++ b/HepLean/GroupTheory/SO3/Basic.lean
@@ -45,7 +45,6 @@ scoped[GroupTheory] notation (name := SO3_notation) "SO(3)" => SO3
 /-- SO3 has the subtype topology. -/
 instance : TopologicalSpace SO3 := instTopologicalSpaceSubtype
 
-
 namespace SO3
 
 @[simp]
@@ -139,11 +138,8 @@ def embeddingGL : Embedding toGL.toFun where
       apply And.intro (isOpen_induced hU1)
       exact hU2
 
-
-
-
-
-
+instance : TopologicalGroup SO(3) :=
+  Inducing.topologicalGroup toGL embeddingGL.toInducing
 
 
 
diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
new file mode 100644
index 0000000..befb0c3
--- /dev/null
+++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzGroup.Orthochronous
+import HepLean.SpaceTime.LorentzGroup.Proper
+import HepLean.GroupTheory.SO3.Basic
+import Mathlib.GroupTheory.SpecificGroups.KleinFour
+import Mathlib.Topology.Constructions
+/-!
+# Rotations
+
+-/
+noncomputable section
+namespace spaceTime
+
+namespace lorentzGroup
+open GroupTheory
+
+
+
+
+end lorentzGroup
+
+
+end spaceTime
+end