From 710e4f7b22f38782c5cb0aac246687fdb39338d6 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Sat, 15 Jun 2024 17:08:08 -0400
Subject: [PATCH] docs: Improve some documentation

---
 HepLean/SpaceTime/AsSelfAdjointMatrix.lean |  6 ++--
 HepLean/SpaceTime/LorentzGroup/Basic.lean  | 31 ++++++++++++++++--
 HepLean/SpaceTime/SL2C/Basic.lean          | 38 +++++++++++++++++++---
 3 files changed, 67 insertions(+), 8 deletions(-)

diff --git a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
index c510829..a7673b8 100644
--- a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean
@@ -10,8 +10,10 @@ import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 /-!
 # Spacetime as a self-adjoint matrix
 
-The main result of this file is a linear equivalence `spaceTimeToHerm` between the vector space
-of space-time points and the vector space of 2×2-complex self-adjoint matrices.
+There is a linear equivalence between the vector space of space-time points
+and the vector space of 2×2-complex self-adjoint matrices.
+
+In this file we define this linear equivalence in `toSelfAdjointMatrix`.
 
 -/
 namespace spaceTime
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 0acc3ae..cd76b6f 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -37,6 +37,14 @@ open Matrix
 open Complex
 open ComplexConjugate
 
+/-!
+## Matrices which preserve `ηLin`
+
+We start studying the properties of matrices which preserve `ηLin`.
+These matrices form the Lorentz group, which we will define in the next section at `lorentzGroup`.
+
+-/
+
 /-- We say a matrix `Λ` preserves `ηLin` if for all `x` and `y`,
   `ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y`.  -/
 def PreservesηLin (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Prop :=
@@ -125,6 +133,14 @@ lemma η : PreservesηLin η := by
 
 end PreservesηLin
 
+/-!
+## The Lorentz group
+
+We define the Lorentz group as the set of matrices which preserve `ηLin`.
+We show that the Lorentz group is indeed a group.
+
+-/
+
 /-- The Lorentz group is the subset of matrices which preserve ηLin. -/
 def lorentzGroup : Type := {Λ : Matrix (Fin 4) (Fin 4) ℝ // PreservesηLin Λ}
 
@@ -160,6 +176,19 @@ lemma coe_inv (A : 𝓛) : (A⁻¹).1 = A.1⁻¹:= by
   refine (inv_eq_left_inv ?h).symm
   exact (PreservesηLin.iff_matrix A.1).mp A.2
 
+/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
+def transpose (Λ : lorentzGroup) : lorentzGroup := ⟨Λ.1ᵀ, (PreservesηLin.iff_transpose Λ.1).mp Λ.2⟩
+
+/-!
+
+## Lorentz group as a topological group
+
+We now show that the Lorentz group is a topological group.
+We do this by showing that the natrual map from the Lorentz group to `GL (Fin 4) ℝ` is an
+embedding.
+
+-/
+
 /-- The homomorphism of the Lorentz group into `GL (Fin 4) ℝ`. -/
 def toGL : 𝓛 →* GL (Fin 4) ℝ where
   toFun A := ⟨A.1, (A⁻¹).1, mul_eq_one_comm.mpr $ (PreservesηLin.iff_matrix A.1).mp A.2,
@@ -225,8 +254,6 @@ lemma toGL_embedding : Embedding toGL.toFun where
 
 instance : TopologicalGroup 𝓛 := Inducing.topologicalGroup toGL toGL_embedding.toInducing
 
-/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
-def transpose (Λ : lorentzGroup) : lorentzGroup := ⟨Λ.1ᵀ, (PreservesηLin.iff_transpose Λ.1).mp Λ.2⟩
 
 
 end lorentzGroup
diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean
index ab47a3a..6ab1399 100644
--- a/HepLean/SpaceTime/SL2C/Basic.lean
+++ b/HepLean/SpaceTime/SL2C/Basic.lean
@@ -10,10 +10,6 @@ import Mathlib.RepresentationTheory.Basic
 
 The aim of this file is to give the relationship between `SL(2, ℂ)` and the Lorentz group.
 
-## TODO
-
-This file is a working progress.
-
 -/
 namespace spaceTime
 
@@ -27,6 +23,15 @@ open spaceTime
 
 noncomputable section
 
+/-!
+
+## Representation of SL(2, ℂ) on spacetime
+
+Through the correspondence between spacetime and self-adjoint matrices,
+we can define a representation a representation of `SL(2, ℂ)` on spacetime.
+
+-/
+
 /-- Given an element  `M ∈ SL(2, ℂ)` the linear map from `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` to
  itself defined by  `A ↦ M * A * Mᴴ`. -/
 @[simps!]
@@ -69,6 +74,16 @@ def repSpaceTime : Representation ℝ SL(2, ℂ) spaceTime where
     ext x : 3
     simp
 
+/-!
+
+## Homomorphism to the Lorentz group
+
+There is a group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
+The purpose of this section is to define this homomorphism.
+In the next section we will restrict this homomorphism to the restricted Lorentz group.
+
+-/
+
 /-- Given an element `M ∈ SL(2, ℂ)` the corresponding element of the Lorentz group. -/
 @[simps!]
 def toLorentzGroupElem (M : SL(2, ℂ)) : 𝓛 :=
@@ -87,6 +102,21 @@ def toLorentzGroup : SL(2, ℂ) →* 𝓛 where
     simp only [toLorentzGroupElem, _root_.map_mul, LinearMap.toMatrix_mul,
       lorentzGroupIsGroup_mul_coe]
 
+/-!
+
+## Homomorphism to the restricted Lorentz group
+
+The homomorphism `toLorentzGroup` restricts to a homomorphism to the restricted Lorentz group.
+In this section we will define this homomorphism.
+
+### TODO
+
+Complete this section.
+
+-/
+
+
+
 end
 end SL2C