From 7020263053f9d96398aaa860dc7b31460214b0b0 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 14 May 2024 08:25:03 -0400 Subject: [PATCH] refactor: Move spacetime --- HepLean.lean | 4 + HepLean/SpaceTime/Basic.lean | 88 +++++++ .../CliffordAlgebra.lean | 16 +- HepLean/SpaceTime/LorentzGroup.lean | 100 +++++++ HepLean/SpaceTime/Metric.lean | 176 +++++++++++++ HepLean/StandardModel/Basic.lean | 247 +----------------- HepLean/StandardModel/HiggsBoson/Basic.lean | 5 +- 7 files changed, 385 insertions(+), 251 deletions(-) create mode 100644 HepLean/SpaceTime/Basic.lean rename HepLean/{StandardModel => SpaceTime}/CliffordAlgebra.lean (71%) create mode 100644 HepLean/SpaceTime/LorentzGroup.lean create mode 100644 HepLean/SpaceTime/Metric.lean diff --git a/HepLean.lean b/HepLean.lean index 14e922d..6c336db 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -54,6 +54,10 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations import HepLean.FlavorPhysics.CKMMatrix.Rows import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters +import HepLean.SpaceTime.Basic +import HepLean.SpaceTime.CliffordAlgebra +import HepLean.SpaceTime.LorentzGroup +import HepLean.SpaceTime.Metric import HepLean.StandardModel.Basic import HepLean.StandardModel.HiggsBoson.Basic import HepLean.StandardModel.HiggsBoson.TargetSpace diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean new file mode 100644 index 0000000..193138e --- /dev/null +++ b/HepLean/SpaceTime/Basic.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import Mathlib.Data.Complex.Exponential +import Mathlib.Geometry.Manifold.VectorBundle.Basic +/-! +# Space time + +This file introduce 4d Minkowski spacetime. + +-/ + +noncomputable section + +/-- The space-time -/ +def spaceTime : Type := Fin 4 → ℝ + +/-- Give spacetime the structure of an additive commutative monoid. -/ +instance : AddCommMonoid spaceTime := Pi.addCommMonoid + + +/-- Give spacetime the structure of a module over the reals. -/ +instance : Module ℝ spaceTime := Pi.module _ _ _ + +instance euclideanNormedAddCommGroup : NormedAddCommGroup spaceTime := Pi.normedAddCommGroup + +instance euclideanNormedSpace : NormedSpace ℝ spaceTime := Pi.normedSpace + + +namespace spaceTime + +open Manifold +open Matrix +open Complex +open ComplexConjugate + + +/-- The structure of a smooth manifold on spacetime. -/ +def asSmoothManifold : ModelWithCorners ℝ spaceTime spaceTime := 𝓘(ℝ, spaceTime) + +/-- The standard basis for spacetime. -/ +def stdBasis : Basis (Fin 4) ℝ spaceTime := Pi.basisFun ℝ (Fin 4) + +lemma stdBasis_apply (μ ν : Fin 4) : stdBasis μ ν = if μ = ν then 1 else 0 := by + erw [stdBasis, Pi.basisFun_apply, LinearMap.stdBasis_apply'] + +lemma stdBasis_not_eq {μ ν : Fin 4} (h : μ ≠ ν) : stdBasis μ ν = 0 := by + rw [stdBasis_apply] + exact if_neg h + +lemma stdBasis_0 : stdBasis 0 = ![1, 0, 0, 0] := by + funext i + fin_cases i + <;> simp [stdBasis_apply] + +lemma stdBasis_1 : stdBasis 1 = ![0, 1, 0, 0] := by + funext i + fin_cases i + <;> simp [stdBasis_apply] + +lemma stdBasis_2 : stdBasis 2 = ![0, 0, 1, 0] := by + funext i + fin_cases i + <;> simp [stdBasis_apply] + +lemma stdBasis_3 : stdBasis 3 = ![0, 0, 0, 1] := by + funext i + fin_cases i + <;> simp [stdBasis_apply] + +lemma stdBasis_mulVec (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + (Λ *ᵥ stdBasis μ) ν = Λ ν μ := by + rw [mulVec, dotProduct, Fintype.sum_eq_single μ, stdBasis_apply] + simp + intro x h + rw [stdBasis_apply, if_neg (Ne.symm h)] + simp + +lemma explicit (x : spaceTime) : x = ![x 0, x 1, x 2, x 3] := by + funext i + fin_cases i <;> rfl + + +end spaceTime + +end diff --git a/HepLean/StandardModel/CliffordAlgebra.lean b/HepLean/SpaceTime/CliffordAlgebra.lean similarity index 71% rename from HepLean/StandardModel/CliffordAlgebra.lean rename to HepLean/SpaceTime/CliffordAlgebra.lean index f49de3b..39dad9b 100644 --- a/HepLean/StandardModel/CliffordAlgebra.lean +++ b/HepLean/SpaceTime/CliffordAlgebra.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import HepLean.StandardModel.Basic +import HepLean.SpaceTime.Metric /-! # The Clifford Algebra @@ -16,41 +16,49 @@ This file defines the Gamma matrices. - Include relations for gamma matrices. -/ -namespace StandardModel +namespace spaceTime open Complex noncomputable section diracRepresentation +/-- The γ⁰ gamma matrix in the Dirac representation. -/ def γ0 : Matrix (Fin 4) (Fin 4) ℂ := ![![1, 0, 0, 0], ![0, 1, 0, 0], ![0, 0, -1, 0], ![0, 0, 0, -1]] +/-- The γ¹ gamma matrix in the Dirac representation. -/ def γ1 : Matrix (Fin 4) (Fin 4) ℂ := ![![0, 0, 0, 1], ![0, 0, 1, 0], ![0, -1, 0, 0], ![-1, 0, 0, 0]] +/-- The γ² gamma matrix in the Dirac representation. -/ def γ2 : Matrix (Fin 4) (Fin 4) ℂ := ![![0, 0, 0, - I], ![0, 0, I, 0], ![0, I, 0, 0], ![-I, 0, 0, 0]] +/-- The γ³ gamma matrix in the Dirac representation. -/ def γ3 : Matrix (Fin 4) (Fin 4) ℂ := ![![0, 0, 1, 0], ![0, 0, 0, -1], ![-1, 0, 0, 0], ![0, 1, 0, 0]] +/-- The γ⁵ gamma matrix in the Dirac representation. -/ def γ5 : Matrix (Fin 4) (Fin 4) ℂ := I • (γ0 * γ1 * γ2 * γ3) +/-- The γ gamma matrices in the Dirac representation. -/ @[simp] def γ : Fin 4 → Matrix (Fin 4) (Fin 4) ℂ := ![γ0, γ1, γ2, γ3] - namespace γ open spaceTime variable (μ ν : Fin 4) +/-- The subset of `Matrix (Fin 4) (Fin 4) ℂ` formed by the gamma matrices in the Dirac +representation. -/ @[simp] def γSet : Set (Matrix (Fin 4) (Fin 4) ℂ) := {γ i | i : Fin 4} lemma γ_in_γSet (μ : Fin 4) : γ μ ∈ γSet := by simp [γSet] +/-- The algebra generated by the gamma matrices in the Dirac representation. -/ def diracAlgebra : Subalgebra ℝ (Matrix (Fin 4) (Fin 4) ℂ) := Algebra.adjoin ℝ γSet @@ -63,4 +71,4 @@ lemma γ_in_diracAlgebra (μ : Fin 4) : γ μ ∈ diracAlgebra := end γ end diracRepresentation -end StandardModel +end spaceTime diff --git a/HepLean/SpaceTime/LorentzGroup.lean b/HepLean/SpaceTime/LorentzGroup.lean new file mode 100644 index 0000000..1fc8c66 --- /dev/null +++ b/HepLean/SpaceTime/LorentzGroup.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.Metric +/-! +# The Lorentz Group + +We define the Lorentz group, and show it is a closed subgroup General Linear Group. + +## TODO + +- Show that the Lorentz is a Lie group. +- Define the proper Lorentz group. +- Define the restricted Lorentz group, and prove it is connected. + +-/ + +noncomputable section + +namespace spaceTime + +open Manifold +open Matrix +open Complex +open ComplexConjugate + +/-- The Lorentz group as a subgroup of the general linear group over the reals. -/ +def lorentzGroup : Subgroup (GeneralLinearGroup (Fin 4) ℝ) where + carrier := {Λ | ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y} + mul_mem' {a b} := by + intros ha hb x y + simp only [Units.val_mul, mulVec_mulVec] + rw [← mulVec_mulVec, ← mulVec_mulVec, ha, hb] + one_mem' := by + intros x y + simp + inv_mem' {a} := by + intros ha x y + simp only [coe_units_inv, ← ha ((a.1⁻¹) *ᵥ x) ((a.1⁻¹) *ᵥ y), mulVec_mulVec] + have hx : (a.1 * (a.1)⁻¹) = 1 := by + simp only [@Units.mul_eq_one_iff_inv_eq, coe_units_inv] + simp [hx] + +/-- The Lorentz group is a topological group with the subset topology. -/ +instance : TopologicalGroup lorentzGroup := + Subgroup.instTopologicalGroupSubtypeMem lorentzGroup + +lemma mem_lorentzGroup_iff (Λ : GeneralLinearGroup (Fin 4) ℝ) : + Λ ∈ lorentzGroup ↔ ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y := by + rfl + +lemma mem_lorentzGroup_iff' (Λ : GeneralLinearGroup (Fin 4) ℝ) : + Λ ∈ lorentzGroup ↔ ∀ (x y : spaceTime), ηLin (x) ((η * Λ.1ᵀ * η * Λ.1) *ᵥ y) = ηLin x y := by + rw [mem_lorentzGroup_iff] + apply Iff.intro + intro h + intro x y + have h1 := h x y + rw [ηLin_mulVec_left, mulVec_mulVec] at h1 + exact h1 + intro h + intro x y + rw [ηLin_mulVec_left, mulVec_mulVec] + exact h x y + +lemma mem_lorentzGroup_iff'' (Λ : GL (Fin 4) ℝ) : + Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η * Λ.1 = 1 := by + rw [mem_lorentzGroup_iff', ηLin_matrix_eq_identity_iff (η * Λ.1ᵀ * η * Λ.1)] + apply Iff.intro + · simp_all only [ηLin_apply_apply, implies_true, iff_true, one_mulVec] + · simp_all only [ηLin_apply_apply, mulVec_mulVec, implies_true] + +lemma det_lorentzGroup (Λ : lorentzGroup) : Λ.1.1.det = 1 ∨ Λ.1.1.det = -1 := by + simpa [← sq, det_one, det_mul, det_mul, det_mul, det_transpose, det_η] using + (congrArg det ((mem_lorentzGroup_iff'' Λ.1).mp Λ.2)) + +/-- A continous map from `GL (Fin 4) ℝ` to `Matrix (Fin 4) (Fin 4) ℝ` for which the Lorentz +group is the kernal. -/ +def lorentzMap (Λ : GL (Fin 4) ℝ) : Matrix (Fin 4) (Fin 4) ℝ := η * Λ.1ᵀ * η * Λ.1 + +lemma lorentzMap_continuous : Continuous lorentzMap := by + apply Continuous.mul _ Units.continuous_val + apply Continuous.mul _ continuous_const + exact Continuous.mul continuous_const (Continuous.matrix_transpose (Units.continuous_val)) + +lemma lorentzGroup_kernal : lorentzGroup = lorentzMap ⁻¹' {1} := by + ext Λ + erw [mem_lorentzGroup_iff'' Λ] + rfl + +theorem lorentzGroup_isClosed : IsClosed (lorentzGroup : Set (GeneralLinearGroup (Fin 4) ℝ)) := by + rw [lorentzGroup_kernal] + exact continuous_iff_isClosed.mp lorentzMap_continuous {1} isClosed_singleton + + +end spaceTime + +end diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean new file mode 100644 index 0000000..b7d97ce --- /dev/null +++ b/HepLean/SpaceTime/Metric.lean @@ -0,0 +1,176 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import HepLean.SpaceTime.Basic +import Mathlib.Analysis.InnerProductSpace.Adjoint +import Mathlib.LinearAlgebra.CliffordAlgebra.Basic +/-! +# Spacetime Metric + +This file introduces the metric on spacetime in the (+, -, -, -) signature. + +-/ + +noncomputable section + +namespace spaceTime + +open Manifold +open Matrix +open Complex +open ComplexConjugate + +/-- The metric as a `4×4` real matrix. -/ +def η : Matrix (Fin 4) (Fin 4) ℝ := + ![![1, 0, 0, 0], ![0, -1, 0, 0], ![0, 0, -1, 0], ![0, 0, 0, -1]] + +lemma η_off_diagonal {μ ν : Fin 4} (h : μ ≠ ν) : η μ ν = 0 := by + fin_cases μ <;> + fin_cases ν <;> + simp_all [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, + Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, + Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, + vecHead, vecTail, Function.comp_apply] + +lemma η_symmetric (μ ν : Fin 4) : η μ ν = η ν μ := by + by_cases h : μ = ν + rw [h] + rw [η_off_diagonal h] + refine (η_off_diagonal ?_).symm + exact fun a => h (id a.symm) + +lemma η_transpose : η.transpose = η := by + funext μ ν + rw [transpose_apply, η_symmetric] + +lemma det_η : η.det = - 1 := by + simp only [η, det_succ_row_zero, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val', + empty_val', cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, + cons_val_one, head_cons, submatrix_submatrix, Function.comp_apply, Fin.succ_one_eq_two, + cons_val_two, tail_cons, det_unique, Fin.default_eq_zero, cons_val_succ, head_fin_const, + Fin.sum_univ_succ, Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove, Finset.univ_unique, + Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, neg_mul, Fin.succ_succAbove_zero, + Finset.sum_neg_distrib, Finset.sum_singleton, Fin.succ_succAbove_one, even_two, Even.neg_pow, + one_pow, mul_one, mul_neg, neg_neg, mul_zero, neg_zero, add_zero, zero_mul, + Finset.sum_const_zero] + + +lemma η_sq : η * η = 1 := by + funext μ ν + rw [mul_apply, Fin.sum_univ_four] + fin_cases μ <;> fin_cases ν <;> + simp [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, + Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, + Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, + vecHead, vecTail, Function.comp_apply] + + + +lemma η_mulVec (x : spaceTime) : η *ᵥ x = ![x 0, -x 1, -x 2, -x 3] := by + rw [explicit x] + rw [η] + funext i + rw [mulVec, dotProduct, Fin.sum_univ_four] + fin_cases i <;> + simp [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, + Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, + Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, + vecHead, vecTail, Function.comp_apply] + +/-- Given a point in spaceTime `x` the linear map `y → x ⬝ᵥ (η *ᵥ y)`. -/ +@[simps!] +def linearMapForSpaceTime (x : spaceTime) : spaceTime →ₗ[ℝ] ℝ where + toFun y := x ⬝ᵥ (η *ᵥ y) + map_add' y z := by + simp only + rw [mulVec_add, dotProduct_add] + map_smul' c y := by + simp only + rw [mulVec_smul, dotProduct_smul] + rfl + +/-- The metric as a bilinear map from `spaceTime` to `ℝ`. -/ +@[simps!] +def ηLin : LinearMap.BilinForm ℝ spaceTime where + toFun x := linearMapForSpaceTime x + map_add' x y := by + apply LinearMap.ext + intro z + simp only [linearMapForSpaceTime_apply, LinearMap.add_apply] + rw [add_dotProduct] + map_smul' c x := by + apply LinearMap.ext + intro z + simp only [linearMapForSpaceTime_apply, RingHom.id_apply, LinearMap.smul_apply, smul_eq_mul] + rw [smul_dotProduct] + rfl + +lemma ηLin_expand (x y : spaceTime) : ηLin x y = x 0 * y 0 - x 1 * y 1 - x 2 * y 2 - x 3 * y 3 := by + rw [ηLin] + simp only [LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply, Fin.isValue] + erw [η_mulVec] + nth_rewrite 1 [explicit x] + simp only [dotProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.sum_univ_four, + cons_val_zero, cons_val_one, head_cons, mul_neg, cons_val_two, tail_cons, cons_val_three] + ring + +lemma ηLin_symm (x y : spaceTime) : ηLin x y = ηLin y x := by + rw [ηLin_expand, ηLin_expand] + ring + +lemma ηLin_stdBasis_apply (μ : Fin 4) (x : spaceTime) : ηLin (stdBasis μ) x = η μ μ * x μ := by + rw [ηLin_expand] + fin_cases μ + <;> simp [stdBasis_0, stdBasis_1, stdBasis_2, stdBasis_3, η] + + +lemma ηLin_η_stdBasis (μ ν : Fin 4) : ηLin (stdBasis μ) (stdBasis ν) = η μ ν := by + rw [ηLin_stdBasis_apply] + by_cases h : μ = ν + rw [stdBasis_apply] + subst h + simp + rw [stdBasis_not_eq, η_off_diagonal h] + simp + exact fun a => h (id a.symm) + +lemma ηLin_mulVec_left (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + ηLin (Λ *ᵥ x) y = ηLin x ((η * Λᵀ * η) *ᵥ y) := by + simp only [ηLin_apply_apply, mulVec_mulVec] + rw [(vecMul_transpose Λ x).symm, ← dotProduct_mulVec, mulVec_mulVec] + rw [← mul_assoc, ← mul_assoc, η_sq, one_mul] + +lemma ηLin_mulVec_right (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + ηLin x (Λ *ᵥ y) = ηLin ((η * Λᵀ * η) *ᵥ x) y := by + rw [ηLin_symm, ηLin_symm ((η * Λᵀ * η) *ᵥ x) _ ] + exact ηLin_mulVec_left y x Λ + +lemma ηLin_matrix_stdBasis (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + ηLin (stdBasis ν) (Λ *ᵥ stdBasis μ) = η ν ν * Λ ν μ := by + rw [ηLin_stdBasis_apply, stdBasis_mulVec] + +lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) : + Λ = 1 ↔ ∀ (x y : spaceTime), ηLin x y = ηLin x (Λ *ᵥ y) := by + apply Iff.intro + intro h + subst h + simp + intro h + funext μ ν + have h1 := h (stdBasis μ) (stdBasis ν) + rw [ηLin_matrix_stdBasis, ηLin_η_stdBasis] at h1 + fin_cases μ <;> fin_cases ν <;> + simp_all [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, + Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, + Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, + vecHead, vecTail, Function.comp_apply] + +/-- The metric as a quadratic form on `spaceTime`. -/ +def quadraticForm : QuadraticForm ℝ spaceTime := ηLin.toQuadraticForm + + +end spaceTime + +end diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean index 27df917..9533e2e 100644 --- a/HepLean/StandardModel/Basic.lean +++ b/HepLean/StandardModel/Basic.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ +import HepLean.SpaceTime.Basic import Mathlib.Data.Complex.Exponential import Mathlib.Geometry.Manifold.VectorBundle.Basic import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection @@ -11,6 +12,7 @@ import Mathlib.RepresentationTheory.Basic import Mathlib.LinearAlgebra.Matrix.ToLin import Mathlib.Analysis.InnerProductSpace.Adjoint import Mathlib.LinearAlgebra.CliffordAlgebra.Basic +import Mathlib.Analysis.NormedSpace.MatrixExponential /-! # The Standard Model @@ -30,251 +32,6 @@ open Matrix open Complex open ComplexConjugate -noncomputable section spaceTime - -/-- The space-time -/ -def spaceTime : Type := Fin 4 → ℝ - -/-- Give spacetime the structure of an additive commutative monoid. -/ -instance : AddCommMonoid spaceTime := Pi.addCommMonoid - -/-- Give spacetime the structure of a module over the reals. -/ -instance : Module ℝ spaceTime := Pi.module _ _ _ - -instance euclideanNormedAddCommGroup : NormedAddCommGroup spaceTime := Pi.normedAddCommGroup - -instance euclideanNormedSpace : NormedSpace ℝ spaceTime := Pi.normedSpace - - -namespace spaceTime - -def asSmoothManifold : ModelWithCorners ℝ spaceTime spaceTime := 𝓘(ℝ, spaceTime) - -def stdBasis : Basis (Fin 4) ℝ spaceTime := Pi.basisFun ℝ (Fin 4) - -lemma stdBasis_apply (μ ν : Fin 4) : stdBasis μ ν = if μ = ν then 1 else 0 := by - erw [stdBasis, Pi.basisFun_apply, LinearMap.stdBasis_apply'] - -lemma stdBasis_not_eq {μ ν : Fin 4} (h : μ ≠ ν) : stdBasis μ ν = 0 := by - rw [stdBasis_apply] - exact if_neg h - -lemma stdBasis_0 : stdBasis 0 = ![1, 0, 0, 0] := by - funext i - fin_cases i - <;> simp [stdBasis_apply] - -lemma stdBasis_1 : stdBasis 1 = ![0, 1, 0, 0] := by - funext i - fin_cases i - <;> simp [stdBasis_apply] - -lemma stdBasis_2 : stdBasis 2 = ![0, 0, 1, 0] := by - funext i - fin_cases i - <;> simp [stdBasis_apply] - -lemma stdBasis_3 : stdBasis 3 = ![0, 0, 0, 1] := by - funext i - fin_cases i - <;> simp [stdBasis_apply] - -lemma stdBasis_mulVec (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - (Λ *ᵥ stdBasis μ) ν = Λ ν μ := by - rw [mulVec, dotProduct, Fintype.sum_eq_single μ, stdBasis_apply] - simp - intro x h - rw [stdBasis_apply, if_neg (Ne.symm h)] - simp - - - -lemma explicit (x : spaceTime) : x = ![x 0, x 1, x 2, x 3] := by - funext i - fin_cases i <;> rfl - - - -def η : Matrix (Fin 4) (Fin 4) ℝ := - ![![1, 0, 0, 0], ![0, -1, 0, 0], ![0, 0, -1, 0], ![0, 0, 0, -1]] - -lemma η_off_diagonal {μ ν : Fin 4} (h : μ ≠ ν) : η μ ν = 0 := by - fin_cases μ <;> - fin_cases ν <;> - simp_all [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, - Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, - Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, - vecHead, vecTail, Function.comp_apply] - -lemma η_symmetric (μ ν : Fin 4) : η μ ν = η ν μ := by - by_cases h : μ = ν - rw [h] - rw [η_off_diagonal h] - refine (η_off_diagonal ?_).symm - exact fun a => h (id a.symm) - -lemma η_transpose : η.transpose = η := by - funext μ ν - rw [transpose_apply, η_symmetric] - -lemma η_sq : η * η = 1 := by - funext μ ν - rw [mul_apply, Fin.sum_univ_four] - fin_cases μ <;> fin_cases ν <;> - simp [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, - Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, - Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, - vecHead, vecTail, Function.comp_apply] - - - -lemma η_mulVec (x : spaceTime) : η *ᵥ x = ![x 0, -x 1, -x 2, -x 3] := by - rw [explicit x] - rw [η] - funext i - rw [mulVec, dotProduct, Fin.sum_univ_four] - fin_cases i <;> - simp [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, - Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, - Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, - vecHead, vecTail, Function.comp_apply] - -@[simps!] -def linearMapForSpaceTime (x : spaceTime) : spaceTime →ₗ[ℝ] ℝ where - toFun y := x ⬝ᵥ (η *ᵥ y) - map_add' y z := by - simp only - rw [mulVec_add, dotProduct_add] - map_smul' c y := by - simp only - rw [mulVec_smul, dotProduct_smul] - rfl - -@[simps!] -def ηLin : LinearMap.BilinForm ℝ spaceTime where - toFun x := linearMapForSpaceTime x - map_add' x y := by - apply LinearMap.ext - intro z - simp only [linearMapForSpaceTime_apply, LinearMap.add_apply] - rw [add_dotProduct] - map_smul' c x := by - apply LinearMap.ext - intro z - simp only [linearMapForSpaceTime_apply, RingHom.id_apply, LinearMap.smul_apply, smul_eq_mul] - rw [smul_dotProduct] - rfl - -lemma ηLin_expand (x y : spaceTime) : ηLin x y = x 0 * y 0 - x 1 * y 1 - x 2 * y 2 - x 3 * y 3 := by - rw [ηLin] - simp only [LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply, Fin.isValue] - erw [η_mulVec] - nth_rewrite 1 [explicit x] - simp only [dotProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.sum_univ_four, - cons_val_zero, cons_val_one, head_cons, mul_neg, cons_val_two, tail_cons, cons_val_three] - ring - -lemma ηLin_symm (x y : spaceTime) : ηLin x y = ηLin y x := by - rw [ηLin_expand, ηLin_expand] - ring - -lemma ηLin_stdBasis_apply (μ : Fin 4) (x : spaceTime) : ηLin (stdBasis μ) x = η μ μ * x μ := by - rw [ηLin_expand] - fin_cases μ - <;> simp [stdBasis_0, stdBasis_1, stdBasis_2, stdBasis_3, η] - - -lemma ηLin_η_stdBasis (μ ν : Fin 4) : ηLin (stdBasis μ) (stdBasis ν) = η μ ν := by - rw [ηLin_stdBasis_apply] - by_cases h : μ = ν - rw [stdBasis_apply] - subst h - simp - rw [stdBasis_not_eq, η_off_diagonal h] - simp - exact fun a => h (id a.symm) - -lemma ηLin_mulVec_left (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - ηLin (Λ *ᵥ x) y = ηLin x ((η * Λᵀ * η) *ᵥ y) := by - simp only [ηLin_apply_apply, mulVec_mulVec] - rw [(vecMul_transpose Λ x).symm, ← dotProduct_mulVec, mulVec_mulVec] - rw [← mul_assoc, ← mul_assoc, η_sq, one_mul] - -lemma ηLin_mulVec_right (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - ηLin x (Λ *ᵥ y) = ηLin ((η * Λᵀ * η) *ᵥ x) y := by - rw [ηLin_symm, ηLin_symm ((η * Λᵀ * η) *ᵥ x) _ ] - exact ηLin_mulVec_left y x Λ - -lemma ηLin_matrix_stdBasis (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - ηLin (stdBasis ν) (Λ *ᵥ stdBasis μ) = η ν ν * Λ ν μ := by - rw [ηLin_stdBasis_apply, stdBasis_mulVec] - -lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) : - Λ = 1 ↔ ∀ (x y : spaceTime), ηLin x y = ηLin x (Λ *ᵥ y) := by - apply Iff.intro - intro h - subst h - simp - intro h - funext μ ν - have h1 := h (stdBasis μ) (stdBasis ν) - rw [ηLin_matrix_stdBasis, ηLin_η_stdBasis] at h1 - fin_cases μ <;> fin_cases ν <;> - simp_all [η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one, - Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons, - Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one, - vecHead, vecTail, Function.comp_apply] - - -def quadraticForm : QuadraticForm ℝ spaceTime := ηLin.toQuadraticForm - -def lorentzGroup : Subgroup (GeneralLinearGroup (Fin 4) ℝ) where - carrier := {Λ | ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y} - mul_mem' {a b} := by - intros ha hb x y - simp only [Units.val_mul, mulVec_mulVec] - rw [← mulVec_mulVec, ← mulVec_mulVec, ha, hb] - one_mem' := by - intros x y - simp - inv_mem' {a} := by - intros ha x y - simp only [coe_units_inv, ← ha ((a.1⁻¹) *ᵥ x) ((a.1⁻¹) *ᵥ y), mulVec_mulVec] - have hx : (a.1 * (a.1)⁻¹) = 1 := by - simp only [@Units.mul_eq_one_iff_inv_eq, coe_units_inv] - simp [hx] - - -lemma mem_lorentzGroup_iff (Λ : GeneralLinearGroup (Fin 4) ℝ) : - Λ ∈ lorentzGroup ↔ ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y := by - rfl - -lemma mem_lorentzGroup_iff' (Λ : GeneralLinearGroup (Fin 4) ℝ) : - Λ ∈ lorentzGroup ↔ ∀ (x y : spaceTime), ηLin (x) ((η * Λ.1ᵀ * η * Λ.1) *ᵥ y) = ηLin x y := by - rw [mem_lorentzGroup_iff] - apply Iff.intro - intro h - intro x y - have h1 := h x y - rw [ηLin_mulVec_left, mulVec_mulVec] at h1 - exact h1 - intro h - intro x y - rw [ηLin_mulVec_left, mulVec_mulVec] - exact h x y - -lemma mem_lorentzGroup_iff'' (Λ : GeneralLinearGroup (Fin 4) ℝ) : - Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η * Λ.1 = 1 := by - rw [mem_lorentzGroup_iff', ηLin_matrix_eq_identity_iff (η * Λ.1ᵀ * η * Λ.1)] - apply Iff.intro - · simp_all only [ηLin_apply_apply, implies_true, iff_true, one_mulVec] - · simp_all only [ηLin_apply_apply, mulVec_mulVec, implies_true] - -abbrev cliffordAlgebra := CliffordAlgebra quadraticForm - -end spaceTime - -end spaceTime /-- The global gauge group of the standard model. TODO: Generalize to quotient. -/ abbrev gaugeGroup : Type := diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean index b44b047..da76073 100644 --- a/HepLean/StandardModel/HiggsBoson/Basic.lean +++ b/HepLean/StandardModel/HiggsBoson/Basic.lean @@ -34,15 +34,16 @@ open Manifold open Matrix open Complex open ComplexConjugate +open spaceTime /-- The trivial vector bundle 𝓡² × ℂ². (TODO: Make associated bundle.) -/ abbrev higgsBundle := Bundle.Trivial spaceTime higgsVec -instance : SmoothVectorBundle higgsVec higgsBundle (𝓡 4) := +instance : SmoothVectorBundle higgsVec higgsBundle spaceTime.asSmoothManifold := Bundle.Trivial.smoothVectorBundle higgsVec 𝓘(ℝ, spaceTime) /-- A higgs field is a smooth section of the higgs bundle. -/ -abbrev higgsField : Type := SmoothSection (𝓡 4) higgsVec higgsBundle +abbrev higgsField : Type := SmoothSection spaceTime.asSmoothManifold higgsVec higgsBundle instance : NormedAddCommGroup (Fin 2 → ℂ) := by exact Pi.normedAddCommGroup