docs: Improve some documentation

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

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

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