Merge branch 'master' into Feynman_Diagrams

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
 

README.md

@@ -1,9 +1,9 @@
-# High Energy Physics in Lean
 
+![HepLean](./doc/HepLeanLogo_white.jpeg)
 [![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/)
 [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
 [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
-[![](https://img.shields.io/badge/Lean-v4.9.0_rc1-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc1)
+[![](https://img.shields.io/badge/Lean-v4.9.0_rc2-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0-rc1)
 
 A project to digitalize high energy physics.
 
@@ -12,7 +12,7 @@ A project to digitalize high energy physics.
 - Use Lean to create an exhaustive database of definitions, theorems, proofs, and calculations in high energy physics.
 - Make a library that is easy to use by the high energy physics community.
 - Keep the database up-to date with developments in MathLib4. 
-- Create gitHub workflows of relevance to the high energy physics community. 
+- Create GitHub workflows of relevance to the high energy physics community. 
 
 ## Areas of high energy physics with some coverage in HepLean
 

doc/index.markdown

@@ -1,7 +1,7 @@
 ---
 # Feel free to add content and custom Front Matter to this file.
 # To modify the layout, see https://jekyllrb.com/docs/themes/#overriding-theme-defaults
-
+# To view changes run: bundle exec jekyll serve
 layout: home
 ---
 [![](https://img.shields.io/badge/Documentation-blue)](https://heplean.github.io/HepLean/docs)
@@ -9,4 +9,3 @@ layout: home
 
 (This site is a work in progress. More to follow. Follow the links above to 
 the documentation page or GitHub.)
-