diff --git a/HepLean.lean b/HepLean.lean index 429a466..4934ff8 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -68,6 +68,7 @@ import HepLean.SpaceTime.LorentzGroup.Orthochronous import HepLean.SpaceTime.LorentzGroup.Proper import HepLean.SpaceTime.LorentzGroup.Rotations import HepLean.SpaceTime.Metric +import HepLean.SpaceTime.SL2C.Basic import HepLean.StandardModel.Basic import HepLean.StandardModel.HiggsBoson.Basic import HepLean.StandardModel.HiggsBoson.TargetSpace diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean index 411e2fd..83fa2dd 100644 --- a/HepLean/AnomalyCancellation/SM/Basic.lean +++ b/HepLean/AnomalyCancellation/SM/Basic.lean @@ -52,7 +52,7 @@ lemma charges_eq_toSpecies_eq (S T : (SMCharges n).charges) : exact fun a i => congrArg (⇑(toSpecies i)) a intro h apply toSpeciesEquiv.injective - exact (Set.eqOn_univ (toSpeciesEquiv S) (toSpeciesEquiv T)).mp fun ⦃x⦄ a => h x + exact (Set.eqOn_univ (toSpeciesEquiv S) (toSpeciesEquiv T)).mp fun ⦃x⦄ _ => h x lemma toSMSpecies_toSpecies_inv (i : Fin 5) (f : (Fin 5 → Fin n → ℚ) ) : (toSpecies i) (toSpeciesEquiv.symm f) = f i := by diff --git a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean index 56bab80..c510829 100644 --- a/HepLean/SpaceTime/AsSelfAdjointMatrix.lean +++ b/HepLean/SpaceTime/AsSelfAdjointMatrix.lean @@ -45,19 +45,17 @@ noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2 /-- The linear equivalence between the vector-space `spaceTime` and self-adjoint 2×2-complex matrices. -/ -noncomputable def spaceTimeToHerm : spaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where +noncomputable def toSelfAdjointMatrix : spaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where toFun := toSelfAdjointMatrix' invFun := fromSelfAdjointMatrix' left_inv x := by - simp only [fromSelfAdjointMatrix', one_div, Fin.isValue, toSelfAdjointMatrix'_coe, of_apply, - cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons, - head_fin_const, add_add_sub_cancel, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, - I_im, mul_one, sub_self, add_zero, add_im, mul_im, zero_add, add_sub_sub_cancel, - half_add_self] - funext i - fin_cases i <;> field_simp - rfl - rfl + simp only [fromSelfAdjointMatrix', one_div, toSelfAdjointMatrix'_coe, of_apply, cons_val', + cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_cons, head_fin_const, + add_add_sub_cancel, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, + sub_self, add_zero, add_im, mul_im, zero_add, add_sub_sub_cancel, half_add_self] + field_simp [spaceTime] + ext1 x + fin_cases x <;> rfl right_inv x := by simp only [toSelfAdjointMatrix', toMatrix, fromSelfAdjointMatrix', one_div, Fin.isValue, add_re, sub_re, cons_val_zero, ofReal_mul, ofReal_inv, ofReal_ofNat, ofReal_add, cons_val_three, @@ -73,19 +71,22 @@ noncomputable def spaceTimeToHerm : spaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (F rfl exact conj_eq_iff_re.mp (congrArg (fun M => M 1 1) $ selfAdjoint.mem_iff.mp x.2 ) map_add' x y := by - simp only [toSelfAdjointMatrix', toMatrix, Fin.isValue, add_apply, ofReal_add, - AddSubmonoid.mk_add_mk, of_add_of, add_cons, head_cons, tail_cons, empty_add_empty, - Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq] - ext i j - fin_cases i <;> fin_cases j <;> - field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal, add_apply] - <;> ring + ext i j : 2 + simp only [toSelfAdjointMatrix'_coe, add_apply, ofReal_add, of_apply, cons_val', empty_val', + cons_val_fin_one, AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, Matrix.add_apply] + fin_cases i <;> fin_cases j <;> simp <;> ring map_smul' r x := by + ext i j : 2 simp only [toSelfAdjointMatrix', toMatrix, Fin.isValue, smul_apply, ofReal_mul, RingHom.id_apply] - ext i j fin_cases i <;> fin_cases j <;> field_simp [fromSelfAdjointMatrix', toMatrix, conj_ofReal, smul_apply] <;> ring +lemma det_eq_ηLin (x : spaceTime) : det (toSelfAdjointMatrix x).1 = ηLin x x := by + simp [toSelfAdjointMatrix, ηLin_expand] + ring_nf + simp only [Fin.isValue, I_sq, mul_neg, mul_one] + ring + end spaceTime diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean index c0b9a5f..0acc3ae 100644 --- a/HepLean/SpaceTime/LorentzGroup/Basic.lean +++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean @@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith -/ import HepLean.SpaceTime.Metric import HepLean.SpaceTime.FourVelocity +import HepLean.SpaceTime.AsSelfAdjointMatrix import Mathlib.GroupTheory.SpecificGroups.KleinFour import Mathlib.Geometry.Manifold.Algebra.LieGroup import Mathlib.Analysis.Matrix @@ -45,6 +46,30 @@ namespace PreservesηLin variable (Λ : Matrix (Fin 4) (Fin 4) ℝ) +lemma iff_norm : PreservesηLin Λ ↔ + ∀ (x : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ x) = ηLin x x := by + refine Iff.intro (fun h x => h x x) (fun h x y => ?_) + have hp := h (x + y) + have hn := h (x - y) + rw [mulVec_add] at hp + rw [mulVec_sub] at hn + simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn + rw [ηLin_symm (Λ *ᵥ y) (Λ *ᵥ x), ηLin_symm y x] at hp hn + linear_combination hp / 4 + -1 * hn / 4 + +lemma iff_det_selfAdjoint : PreservesηLin Λ ↔ + ∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)), + det ((toSelfAdjointMatrix ∘ toLin stdBasis stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1 + = det x.1 := by + rw [iff_norm] + apply Iff.intro + intro h x + have h1 := congrArg ofReal $ h (toSelfAdjointMatrix.symm x) + simpa [← det_eq_ηLin] using h1 + intro h x + have h1 := h (toSelfAdjointMatrix x) + simpa [det_eq_ηLin] using h1 + lemma iff_on_right : PreservesηLin Λ ↔ ∀ (x y : spaceTime), ηLin x ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by apply Iff.intro @@ -74,14 +99,13 @@ lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, ← mul_assoc, transpose_one] at h1 rw [iff_matrix' Λ.transpose, ← h1] - rw [← mul_assoc, ← mul_assoc] - exact Matrix.mul_assoc (Λᵀ * η) Λᵀᵀ η + noncomm_ring intro h have h1 := congrArg transpose ((iff_matrix Λ.transpose).mp h) rw [transpose_mul, transpose_mul, transpose_mul, η_transpose, ← mul_assoc, transpose_one, transpose_transpose] at h1 rw [iff_matrix', ← h1] - repeat rw [← mul_assoc] + noncomm_ring /-- The lift of a matrix which preserves `ηLin` to an invertible matrix. -/ def liftGL {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : GL (Fin 4) ℝ := diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean index 931ad56..33ae0c7 100644 --- a/HepLean/SpaceTime/Metric.lean +++ b/HepLean/SpaceTime/Metric.lean @@ -182,9 +182,7 @@ lemma ηLin_expand (x y : spaceTime) : ηLin x y = x 0 * y 0 - x 1 * y 1 - x 2 * lemma ηLin_expand_self (x : spaceTime) : ηLin x x = x 0 ^ 2 - ‖x.space‖ ^ 2 := by rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three, ηLin_expand] - simp only [Fin.isValue, space, cons_val_zero, RCLike.inner_apply, conj_trivial, cons_val_one, - head_cons, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons] - ring + noncomm_ring lemma time_elm_sq_of_ηLin (x : spaceTime) : x 0 ^ 2 = ηLin x x + ‖x.space‖ ^ 2 := by rw [ηLin_expand_self] @@ -197,9 +195,7 @@ lemma ηLin_leq_time_sq (x : spaceTime) : ηLin x x ≤ x 0 ^ 2 := by lemma ηLin_space_inner_product (x y : spaceTime) : ηLin x y = x 0 * y 0 - ⟪x.space, y.space⟫_ℝ := by rw [ηLin_expand, @PiLp.inner_apply, Fin.sum_univ_three] - simp only [Fin.isValue, space, cons_val_zero, RCLike.inner_apply, conj_trivial, cons_val_one, - head_cons, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons] - ring + noncomm_ring lemma ηLin_ge_abs_inner_product (x y : spaceTime) : x 0 * y 0 - ‖⟪x.space, y.space⟫_ℝ‖ ≤ (ηLin x y) := by diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean new file mode 100644 index 0000000..ab47a3a --- /dev/null +++ b/HepLean/SpaceTime/SL2C/Basic.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.LorentzGroup.Basic +import Mathlib.RepresentationTheory.Basic +/-! +# The group SL(2, ℂ) and it's relation to the Lorentz group + +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 + +open Matrix +open MatrixGroups +open Complex + +namespace SL2C + +open spaceTime + +noncomputable section + +/-- 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!] +def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) : + selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) →ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where + toFun A := ⟨M.1 * A.1 * Matrix.conjTranspose M, + by + noncomm_ring [selfAdjoint.mem_iff, star_eq_conjTranspose, + conjTranspose_mul, conjTranspose_conjTranspose, + (star_eq_conjTranspose A.1).symm.trans $ selfAdjoint.mem_iff.mp A.2]⟩ + map_add' A B := by + noncomm_ring [AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, AddSubmonoid.mk_add_mk, + Subtype.mk.injEq] + map_smul' r A := by + noncomm_ring [selfAdjoint.val_smul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, + RingHom.id_apply] + +/-- The representation of `SL(2, ℂ)` on `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` given by + `M A ↦ M * A * Mᴴ`. -/ +@[simps!] +def repSelfAdjointMatrix : Representation ℝ SL(2, ℂ) $ selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where + toFun := toLinearMapSelfAdjointMatrix + map_one' := by + noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_one, one_mul, + conjTranspose_one, mul_one, Subtype.coe_eta] + map_mul' M N := by + ext x i j : 3 + noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_mul, mul_assoc, + conjTranspose_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply] + +/-- The representation of `SL(2, ℂ)` on `spaceTime` obtained from `toSelfAdjointMatrix` and + `repSelfAdjointMatrix`. -/ +def repSpaceTime : Representation ℝ SL(2, ℂ) spaceTime where + toFun M := toSelfAdjointMatrix.symm.comp ((repSelfAdjointMatrix M).comp + toSelfAdjointMatrix.toLinearMap) + map_one' := by + ext + simp + map_mul' M N := by + ext x : 3 + simp + +/-- Given an element `M ∈ SL(2, ℂ)` the corresponding element of the Lorentz group. -/ +@[simps!] +def toLorentzGroupElem (M : SL(2, ℂ)) : 𝓛 := + ⟨LinearMap.toMatrix stdBasis stdBasis (repSpaceTime M) , + by simp [repSpaceTime, PreservesηLin.iff_det_selfAdjoint]⟩ + +/-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/ +@[simps!] +def toLorentzGroup : SL(2, ℂ) →* 𝓛 where + toFun := toLorentzGroupElem + map_one' := by + simp only [toLorentzGroupElem, _root_.map_one, LinearMap.toMatrix_one] + rfl + map_mul' M N := by + apply Subtype.eq + simp only [toLorentzGroupElem, _root_.map_mul, LinearMap.toMatrix_mul, + lorentzGroupIsGroup_mul_coe] + +end +end SL2C + +end spaceTime diff --git a/README.md b/README.md index e682d0a..f37e81a 100644 --- a/README.md +++ b/README.md @@ -14,6 +14,15 @@ A project to digitalize high energy physics. - Keep the database up-to date with developments in MathLib4. - Create gitHub workflows of relevance to the high energy physics community. +## Areas of high energy physics currently covered + + +[![](https://img.shields.io/badge/The_CKM_Matrix-blue)](https://heplean.github.io/HepLean/HepLean/FlavorPhysics/CKMMatrix/Basic.html) +[![](https://img.shields.io/badge/Higgs_Field-blue)](https://heplean.github.io/HepLean/HepLean/StandardModel/HiggsBoson/Basic.html) +[![](https://img.shields.io/badge/2HDM-blue)](https://heplean.github.io/HepLean/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html) +[![](https://img.shields.io/badge/Lorentz_Group-blue)](https://heplean.github.io/HepLean/HepLean/SpaceTime/LorentzGroup/Basic.html) +[![](https://img.shields.io/badge/Anomaly_Cancellation-blue)](https://heplean.github.io/HepLean/HepLean/AnomalyCancellation/Basic.html) + ## Where to learn more - Read the associated paper: