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 diff --git a/README.md b/README.md index 56922cd..710fe8a 100644 --- a/README.md +++ b/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 diff --git a/doc/HepLeanLogo_color.jpeg b/doc/HepLeanLogo_color.jpeg new file mode 100644 index 0000000..50be3ef Binary files /dev/null and b/doc/HepLeanLogo_color.jpeg differ diff --git a/doc/HepLeanLogo_white.jpeg b/doc/HepLeanLogo_white.jpeg new file mode 100644 index 0000000..9632abc Binary files /dev/null and b/doc/HepLeanLogo_white.jpeg differ diff --git a/doc/index.markdown b/doc/index.markdown index a3ea455..953cc70 100644 --- a/doc/index.markdown +++ b/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.) -