Refactor: Lint
This commit is contained in:
jstoobysmith
parent
7107ba8b80
commit
9305effe79
8 changed files with 192 additions and 96 deletions
|
|
@ -54,6 +54,7 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations
|
|||
import HepLean.FlavorPhysics.CKMMatrix.Rows
|
||||
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
|
||||
import HepLean.GroupTheory.SO3.Basic
|
||||
import HepLean.SpaceTime.Basic
|
||||
import HepLean.SpaceTime.CliffordAlgebra
|
||||
import HepLean.SpaceTime.FourVelocity
|
||||
|
|
@ -61,6 +62,7 @@ import HepLean.SpaceTime.LorentzGroup.Basic
|
|||
import HepLean.SpaceTime.LorentzGroup.Boosts
|
||||
import HepLean.SpaceTime.LorentzGroup.Orthochronous
|
||||
import HepLean.SpaceTime.LorentzGroup.Proper
|
||||
import HepLean.SpaceTime.LorentzGroup.Rotations
|
||||
import HepLean.SpaceTime.Metric
|
||||
import HepLean.StandardModel.Basic
|
||||
import HepLean.StandardModel.HiggsBoson.Basic
|
||||
|
|
|
|||
|
|
@ -11,8 +11,7 @@ import Mathlib.LinearAlgebra.EigenSpace.Basic
|
|||
import Mathlib.Analysis.InnerProductSpace.Basic
|
||||
import Mathlib.Analysis.InnerProductSpace.Adjoint
|
||||
/-!
|
||||
# the 3d special orthogonal group
|
||||
|
||||
# The group SO(3)
|
||||
|
||||
|
||||
-/
|
||||
|
|
@ -20,8 +19,10 @@ import Mathlib.Analysis.InnerProductSpace.Adjoint
|
|||
namespace GroupTheory
|
||||
open Matrix
|
||||
|
||||
/-- The group of `3×3` real matrices with determinant 1 and `A * Aᵀ = 1`. -/
|
||||
def SO3 : Type := {A : Matrix (Fin 3) (Fin 3) ℝ // A.det = 1 ∧ A * Aᵀ = 1}
|
||||
|
||||
@[simps mul_coe one_coe inv div]
|
||||
instance SO3Group : Group SO3 where
|
||||
mul A B := ⟨A.1 * B.1,
|
||||
by
|
||||
|
|
@ -43,6 +44,7 @@ instance SO3Group : Group SO3 where
|
|||
apply Subtype.eq
|
||||
exact mul_eq_one_comm.mpr A.2.2
|
||||
|
||||
/-- Notation for the group `SO3`. -/
|
||||
scoped[GroupTheory] notation (name := SO3_notation) "SO(3)" => SO3
|
||||
|
||||
/-- SO3 has the subtype topology. -/
|
||||
|
|
@ -50,19 +52,18 @@ instance : TopologicalSpace SO3 := instTopologicalSpaceSubtype
|
|||
|
||||
namespace SO3
|
||||
|
||||
@[simp]
|
||||
lemma coe_inv (A : SO3) : (A⁻¹).1 = A.1⁻¹:= by
|
||||
refine (inv_eq_left_inv ?h).symm
|
||||
exact mul_eq_one_comm.mpr A.2.2
|
||||
|
||||
@[simps!]
|
||||
def toGL : SO3 →* GL (Fin 3) ℝ where
|
||||
/-- The inclusion of `SO(3)` into `GL (Fin 3) ℝ`. -/
|
||||
def toGL : SO(3) →* GL (Fin 3) ℝ where
|
||||
toFun A := ⟨A.1, (A⁻¹).1, A.2.2, mul_eq_one_comm.mpr A.2.2⟩
|
||||
map_one' := by
|
||||
simp
|
||||
rfl
|
||||
map_mul' x y := by
|
||||
simp
|
||||
simp only [_root_.mul_inv_rev, coe_inv]
|
||||
ext
|
||||
rfl
|
||||
|
||||
|
|
@ -77,9 +78,8 @@ lemma toGL_injective : Function.Injective toGL := by
|
|||
rw [@Units.ext_iff] at h
|
||||
simpa using h
|
||||
|
||||
example : TopologicalSpace (GL (Fin 3) ℝ) := by
|
||||
exact Units.instTopologicalSpaceUnits
|
||||
|
||||
/-- The inclusion of `SO(3)` into the monoid of matrices times the opposite of
|
||||
the monoid of matrices. -/
|
||||
@[simps!]
|
||||
def toProd : SO(3) →* (Matrix (Fin 3) (Fin 3) ℝ) × (Matrix (Fin 3) (Fin 3) ℝ)ᵐᵒᵖ :=
|
||||
MonoidHom.comp (Units.embedProduct _) toGL
|
||||
|
|
@ -110,20 +110,22 @@ lemma toProd_continuous : Continuous toProd := by
|
|||
exact continuous_iff_le_induced.mpr fun U a => a
|
||||
|
||||
|
||||
def embeddingProd : Embedding toProd where
|
||||
/-- The embedding of `SO(3)` into the monoid of matrices times the opposite of
|
||||
the monoid of matrices. -/
|
||||
lemma toProd_embedding : Embedding toProd where
|
||||
inj := toProd_injective
|
||||
induced := by
|
||||
refine (inducing_iff ⇑toProd).mp ?_
|
||||
refine inducing_of_inducing_compose toProd_continuous continuous_fst ?hgf
|
||||
exact (inducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl
|
||||
|
||||
|
||||
def embeddingGL : Embedding toGL.toFun where
|
||||
/-- The embedding of `SO(3)` into `GL (Fin 3) ℝ`. -/
|
||||
lemma toGL_embedding : Embedding toGL.toFun where
|
||||
inj := toGL_injective
|
||||
induced := by
|
||||
refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
|
||||
intro s
|
||||
rw [TopologicalSpace.ext_iff.mp embeddingProd.induced s ]
|
||||
rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s ]
|
||||
rw [isOpen_induced_iff, isOpen_induced_iff]
|
||||
apply Iff.intro ?_ ?_
|
||||
· intro h
|
||||
|
|
@ -142,7 +144,7 @@ def embeddingGL : Embedding toGL.toFun where
|
|||
exact hU2
|
||||
|
||||
instance : TopologicalGroup SO(3) :=
|
||||
Inducing.topologicalGroup toGL embeddingGL.toInducing
|
||||
Inducing.topologicalGroup toGL toGL_embedding.toInducing
|
||||
|
||||
lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
|
||||
have h1 : det (A.1 - 1) = - det (A.1 - 1) :=
|
||||
|
|
@ -170,13 +172,14 @@ lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
|
|||
@[simp]
|
||||
lemma one_in_spectrum (A : SO(3)) : 1 ∈ spectrum ℝ (A.1) := by
|
||||
rw [spectrum.mem_iff]
|
||||
simp
|
||||
simp only [_root_.map_one]
|
||||
rw [Matrix.isUnit_iff_isUnit_det]
|
||||
simp
|
||||
|
||||
noncomputable section action
|
||||
open Module
|
||||
|
||||
/-- The endomorphism of `EuclideanSpace ℝ (Fin 3)` associated to a element of `SO(3)`. -/
|
||||
@[simps!]
|
||||
def toEnd (A : SO(3)) : End ℝ (EuclideanSpace ℝ (Fin 3)) :=
|
||||
Matrix.toLin (EuclideanSpace.basisFun (Fin 3) ℝ).toBasis
|
||||
|
|
|
|||
|
|
@ -90,62 +90,138 @@ lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by
|
|||
def liftGL {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) : GL (Fin 4) ℝ :=
|
||||
⟨Λ, η * Λᵀ * η , (iff_matrix' Λ).mp h , (iff_matrix Λ).mp h⟩
|
||||
|
||||
lemma mul {Λ Λ' : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) (h' : PreservesηLin Λ') :
|
||||
PreservesηLin (Λ * Λ') := by
|
||||
intro x y
|
||||
rw [← mulVec_mulVec, ← mulVec_mulVec, h, h']
|
||||
|
||||
lemma one : PreservesηLin 1 := by
|
||||
intro x y
|
||||
simp
|
||||
|
||||
lemma η : PreservesηLin η := by
|
||||
simp [iff_matrix, η_transpose, η_sq]
|
||||
|
||||
end PreservesηLin
|
||||
|
||||
/-- The Lorentz group as a subgroup of the general linear group over the reals. -/
|
||||
def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where
|
||||
carrier := {Λ | PreservesηLin Λ}
|
||||
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 the subset of matrices which preserve ηLin. -/
|
||||
def lorentzGroup : Type := {Λ : Matrix (Fin 4) (Fin 4) ℝ // PreservesηLin Λ}
|
||||
|
||||
/-- The Lorentz group is a topological group with the subset topology. -/
|
||||
instance : TopologicalGroup lorentzGroup :=
|
||||
Subgroup.instTopologicalGroupSubtypeMem lorentzGroup
|
||||
@[simps mul_coe one_coe inv div]
|
||||
instance lorentzGroupIsGroup : Group lorentzGroup where
|
||||
mul A B := ⟨A.1 * B.1, PreservesηLin.mul A.2 B.2⟩
|
||||
mul_assoc A B C := by
|
||||
apply Subtype.eq
|
||||
exact Matrix.mul_assoc A.1 B.1 C.1
|
||||
one := ⟨1, PreservesηLin.one⟩
|
||||
one_mul A := by
|
||||
apply Subtype.eq
|
||||
exact Matrix.one_mul A.1
|
||||
mul_one A := by
|
||||
apply Subtype.eq
|
||||
exact Matrix.mul_one A.1
|
||||
inv A := ⟨η * A.1ᵀ * η , PreservesηLin.mul (PreservesηLin.mul PreservesηLin.η
|
||||
((PreservesηLin.iff_transpose A.1).mp A.2)) PreservesηLin.η⟩
|
||||
mul_left_inv A := by
|
||||
apply Subtype.eq
|
||||
exact (PreservesηLin.iff_matrix A.1).mp A.2
|
||||
|
||||
/-- The lift of a matrix preserving `ηLin` to a Lorentz Group element. -/
|
||||
def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) :
|
||||
lorentzGroup := ⟨liftGL h, h⟩
|
||||
/-- Notation for the Lorentz group. -/
|
||||
scoped[spaceTime] notation (name := lorentzGroup_notation) "𝓛" => lorentzGroup
|
||||
|
||||
|
||||
/-- `lorentzGroup` has the subtype topology. -/
|
||||
instance : TopologicalSpace lorentzGroup := instTopologicalSpaceSubtype
|
||||
|
||||
namespace lorentzGroup
|
||||
|
||||
lemma mem_iff (Λ : GL (Fin 4) ℝ): Λ ∈ lorentzGroup ↔ PreservesηLin Λ := by
|
||||
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 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,
|
||||
(PreservesηLin.iff_matrix A.1).mp A.2⟩
|
||||
map_one' := by
|
||||
simp
|
||||
rfl
|
||||
map_mul' x y := by
|
||||
simp only [lorentzGroupIsGroup, _root_.mul_inv_rev, coe_inv]
|
||||
ext
|
||||
rfl
|
||||
|
||||
lemma toGL_injective : Function.Injective toGL := by
|
||||
intro A B h
|
||||
apply Subtype.eq
|
||||
rw [@Units.ext_iff] at h
|
||||
simpa using h
|
||||
|
||||
/-- The homomorphism from the Lorentz Group into the monoid of matrices times the opposite of
|
||||
the monoid of matrices. -/
|
||||
@[simps!]
|
||||
def toProd : 𝓛 →* (Matrix (Fin 4) (Fin 4) ℝ) × (Matrix (Fin 4) (Fin 4) ℝ)ᵐᵒᵖ :=
|
||||
MonoidHom.comp (Units.embedProduct _) toGL
|
||||
|
||||
lemma toProd_eq_transpose_η : toProd A = (A.1, ⟨η * A.1ᵀ * η⟩) := rfl
|
||||
|
||||
lemma toProd_injective : Function.Injective toProd := by
|
||||
intro A B h
|
||||
rw [toProd_eq_transpose_η, toProd_eq_transpose_η] at h
|
||||
rw [@Prod.mk.inj_iff] at h
|
||||
apply Subtype.eq
|
||||
exact h.1
|
||||
|
||||
lemma toProd_continuous : Continuous toProd := by
|
||||
change Continuous (fun A => (A.1, ⟨η * A.1ᵀ * η⟩))
|
||||
refine continuous_prod_mk.mpr (And.intro ?_ ?_)
|
||||
exact continuous_iff_le_induced.mpr fun U a => a
|
||||
refine Continuous.comp' ?_ ?_
|
||||
exact MulOpposite.continuous_op
|
||||
refine Continuous.matrix_mul (Continuous.matrix_mul continuous_const ?_) continuous_const
|
||||
refine Continuous.matrix_transpose ?_
|
||||
exact continuous_iff_le_induced.mpr fun U a => a
|
||||
|
||||
/-- The embedding from the Lorentz Group into the monoid of matrices times the opposite of
|
||||
the monoid of matrices. -/
|
||||
lemma toProd_embedding : Embedding toProd where
|
||||
inj := toProd_injective
|
||||
induced := by
|
||||
refine (inducing_iff ⇑toProd).mp ?_
|
||||
refine inducing_of_inducing_compose toProd_continuous continuous_fst ?hgf
|
||||
exact (inducing_iff (Prod.fst ∘ ⇑toProd)).mpr rfl
|
||||
|
||||
/-- The embedding from the Lorentz Group into `GL (Fin 4) ℝ`. -/
|
||||
lemma toGL_embedding : Embedding toGL.toFun where
|
||||
inj := toGL_injective
|
||||
induced := by
|
||||
refine ((fun {X} {t t'} => TopologicalSpace.ext_iff.mpr) ?_).symm
|
||||
intro s
|
||||
rw [TopologicalSpace.ext_iff.mp toProd_embedding.induced s ]
|
||||
rw [isOpen_induced_iff, isOpen_induced_iff]
|
||||
apply Iff.intro ?_ ?_
|
||||
· intro h
|
||||
obtain ⟨U, hU1, hU2⟩ := h
|
||||
rw [isOpen_induced_iff] at hU1
|
||||
obtain ⟨V, hV1, hV2⟩ := hU1
|
||||
use V
|
||||
simp [hV1]
|
||||
rw [← hU2, ← hV2]
|
||||
rfl
|
||||
· intro h
|
||||
obtain ⟨U, hU1, hU2⟩ := h
|
||||
let t := (Units.embedProduct _) ⁻¹' U
|
||||
use t
|
||||
apply And.intro (isOpen_induced hU1)
|
||||
exact hU2
|
||||
|
||||
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 :=
|
||||
PreservesηLin.liftLor ((PreservesηLin.iff_transpose Λ.1).mp Λ.2)
|
||||
def transpose (Λ : lorentzGroup) : lorentzGroup := ⟨Λ.1ᵀ, (PreservesηLin.iff_transpose Λ.1).mp Λ.2⟩
|
||||
|
||||
|
||||
/-- The continuous map from `GL (Fin 4) ℝ` to `Matrix (Fin 4) (Fin 4) ℝ` whose kernel is
|
||||
the Lorentz group. -/
|
||||
def kernelMap : C(GL (Fin 4) ℝ, Matrix (Fin 4) (Fin 4) ℝ) where
|
||||
toFun Λ := η * Λ.1ᵀ * η * Λ.1
|
||||
continuous_toFun := by
|
||||
apply Continuous.mul _ Units.continuous_val
|
||||
apply Continuous.mul _ continuous_const
|
||||
exact Continuous.mul continuous_const (Continuous.matrix_transpose (Units.continuous_val))
|
||||
|
||||
lemma kernelMap_kernel_eq_lorentzGroup : lorentzGroup = kernelMap ⁻¹' {1} := by
|
||||
ext Λ
|
||||
erw [mem_iff Λ, PreservesηLin.iff_matrix]
|
||||
rfl
|
||||
|
||||
/-- The Lorentz Group is a closed subset of `GL (Fin 4) ℝ`. -/
|
||||
theorem isClosed_of_GL4 : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by
|
||||
rw [kernelMap_kernel_eq_lorentzGroup]
|
||||
exact continuous_iff_isClosed.mp kernelMap.2 {1} isClosed_singleton
|
||||
|
||||
end lorentzGroup
|
||||
|
||||
|
||||
end spaceTime
|
||||
|
|
|
|||
|
|
@ -141,16 +141,12 @@ lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u
|
|||
|
||||
/-- A generalised boost as an element of the Lorentz Group. -/
|
||||
def toLorentz (u v : FourVelocity) : lorentzGroup :=
|
||||
PreservesηLin.liftLor (toMatrix_PreservesηLin u v)
|
||||
⟨toMatrix u v, toMatrix_PreservesηLin u v⟩
|
||||
|
||||
lemma toLorentz_continuous (u : FourVelocity) : Continuous (toLorentz u) := by
|
||||
refine Continuous.subtype_mk ?_ fun x => (PreservesηLin.liftLor (toMatrix_PreservesηLin u x)).2
|
||||
refine Units.continuous_iff.mpr (And.intro ?_ ?_)
|
||||
refine Continuous.subtype_mk ?_ (fun x => toMatrix_PreservesηLin u x)
|
||||
exact toMatrix_continuous u
|
||||
change Continuous fun x => (η * (toMatrix u x).transpose * η)
|
||||
refine Continuous.matrix_mul ?_ continuous_const
|
||||
refine Continuous.matrix_mul continuous_const ?_
|
||||
exact Continuous.matrix_transpose (toMatrix_continuous u)
|
||||
|
||||
|
||||
|
||||
lemma toLorentz_joined_to_1 (u v : FourVelocity) : Joined 1 (toLorentz u v) := by
|
||||
|
|
@ -158,8 +154,7 @@ lemma toLorentz_joined_to_1 (u v : FourVelocity) : Joined 1 (toLorentz u v) := b
|
|||
use ContinuousMap.comp ⟨toLorentz u, toLorentz_continuous u⟩ f
|
||||
· simp only [ContinuousMap.toFun_eq_coe, ContinuousMap.comp_apply, ContinuousMap.coe_coe,
|
||||
Path.source, ContinuousMap.coe_mk]
|
||||
rw [@Subtype.ext_iff, toLorentz, PreservesηLin.liftLor]
|
||||
refine Units.val_eq_one.mp ?_
|
||||
rw [@Subtype.ext_iff, toLorentz]
|
||||
simp [PreservesηLin.liftGL, toMatrix, self u]
|
||||
· simp
|
||||
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ open PreFourVelocity
|
|||
def fstCol (Λ : lorentzGroup) : PreFourVelocity := ⟨Λ.1 *ᵥ stdBasis 0, by
|
||||
rw [mem_PreFourVelocity_iff, ηLin_expand]
|
||||
simp only [Fin.isValue, stdBasis_mulVec]
|
||||
have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp ((mem_iff Λ.1).mp Λ.2)) 0) 0
|
||||
have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp Λ.2) 0) 0
|
||||
simp only [Fin.isValue, mul_apply, transpose_apply, Fin.sum_univ_four, ne_eq, zero_ne_one,
|
||||
not_false_eq_true, η_off_diagonal, zero_mul, add_zero, Fin.reduceEq, one_ne_zero, mul_zero,
|
||||
zero_add, one_apply_eq] at h00
|
||||
|
|
@ -51,7 +51,7 @@ def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0
|
|||
|
||||
lemma IsOrthochronous_iff_transpose (Λ : lorentzGroup) :
|
||||
IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by
|
||||
simp only [IsOrthochronous, Fin.isValue, transpose, PreservesηLin.liftLor, PreservesηLin.liftGL,
|
||||
simp only [IsOrthochronous, Fin.isValue, transpose, PreservesηLin.liftGL,
|
||||
transpose_transpose, transpose_apply]
|
||||
|
||||
lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
|
||||
|
|
@ -62,7 +62,7 @@ lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
|
|||
/-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
|
||||
def mapZeroZeroComp : C(lorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0, by
|
||||
refine Continuous.matrix_elem ?_ 0 0
|
||||
refine Continuous.comp' Units.continuous_val continuous_subtype_val⟩
|
||||
refine Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'⟩
|
||||
|
||||
/-- An auxillary function used in the definition of `orthchroMapReal`. -/
|
||||
def stepFunction : ℝ → ℝ := fun t =>
|
||||
|
|
@ -130,9 +130,10 @@ lemma orthchroMap_not_IsOrthochronous {Λ : lorentzGroup} (h : ¬ IsOrthochronou
|
|||
lemma zero_zero_mul (Λ Λ' : lorentzGroup) :
|
||||
(Λ * Λ').1 0 0 = (fstCol (transpose Λ)).1 0 * (fstCol Λ').1 0 +
|
||||
⟪(fstCol (transpose Λ)).1.space, (fstCol Λ').1.space⟫_ℝ := by
|
||||
rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four]
|
||||
rw [@PiLp.inner_apply, Fin.sum_univ_three]
|
||||
simp [transpose, stdBasis_mulVec, PreservesηLin.liftLor, PreservesηLin.liftGL]
|
||||
simp only [Fin.isValue, lorentzGroupIsGroup_mul_coe, mul_apply, Fin.sum_univ_four, fstCol,
|
||||
transpose, stdBasis_mulVec, transpose_apply, space, PiLp.inner_apply, Nat.succ_eq_add_one,
|
||||
Nat.reduceAdd, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three, cons_val_zero,
|
||||
cons_val_one, head_cons, cons_val_two, tail_cons]
|
||||
ring
|
||||
|
||||
lemma mul_othchron_of_othchron_othchron {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
|
||||
|
|
|
|||
|
|
@ -25,9 +25,9 @@ open ComplexConjugate
|
|||
namespace lorentzGroup
|
||||
|
||||
/-- The determinant of a member of the lorentz group is `1` or `-1`. -/
|
||||
lemma det_eq_one_or_neg_one (Λ : lorentzGroup) : Λ.1.1.det = 1 ∨ Λ.1.1.det = -1 := by
|
||||
lemma det_eq_one_or_neg_one (Λ : 𝓛) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
|
||||
simpa [← sq, det_one, det_mul, det_mul, det_mul, det_transpose, det_η] using
|
||||
(congrArg det ((PreservesηLin.iff_matrix' Λ.1).mp ((mem_iff Λ.1).mp Λ.2)))
|
||||
(congrArg det ((PreservesηLin.iff_matrix' Λ.1).mp Λ.2))
|
||||
|
||||
local notation "ℤ₂" => Multiplicative (ZMod 2)
|
||||
|
||||
|
|
@ -47,16 +47,17 @@ def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where
|
|||
exact continuous_of_discreteTopology
|
||||
|
||||
/-- The continuous map taking a lorentz matrix to its determinant. -/
|
||||
def detContinuous : C(lorentzGroup, ℤ₂) :=
|
||||
def detContinuous : C(𝓛, ℤ₂) :=
|
||||
ContinuousMap.comp coeForℤ₂ {
|
||||
toFun := fun Λ => ⟨Λ.1.1.det, Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩,
|
||||
toFun := fun Λ => ⟨Λ.1.det, Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩,
|
||||
continuous_toFun := by
|
||||
refine Continuous.subtype_mk ?_ _
|
||||
exact Continuous.matrix_det $
|
||||
Continuous.comp' Units.continuous_val continuous_subtype_val}
|
||||
apply Continuous.matrix_det $
|
||||
Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'
|
||||
}
|
||||
|
||||
lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) :
|
||||
detContinuous Λ = detContinuous Λ' ↔ Λ.1.1.det = Λ'.1.1.det := by
|
||||
detContinuous Λ = detContinuous Λ' ↔ Λ.1.det = Λ'.1.det := by
|
||||
apply Iff.intro
|
||||
intro h
|
||||
simp [detContinuous] at h
|
||||
|
|
@ -76,10 +77,10 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) :
|
|||
|
||||
/-- The representation taking a lorentz matrix to its determinant. -/
|
||||
@[simps!]
|
||||
def detRep : lorentzGroup →* ℤ₂ where
|
||||
def detRep : 𝓛 →* ℤ₂ where
|
||||
toFun Λ := detContinuous Λ
|
||||
map_one' := by
|
||||
simp [detContinuous]
|
||||
simp [detContinuous, lorentzGroupIsGroup]
|
||||
map_mul' := by
|
||||
intro Λ1 Λ2
|
||||
simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero,
|
||||
|
|
@ -92,7 +93,7 @@ def detRep : lorentzGroup →* ℤ₂ where
|
|||
lemma detRep_continuous : Continuous detRep := detContinuous.2
|
||||
|
||||
lemma det_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
|
||||
Λ.1.1.det = Λ'.1.1.det := by
|
||||
Λ.1.det = Λ'.1.det := by
|
||||
obtain ⟨s, hs, hΛ'⟩ := h
|
||||
let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuous
|
||||
haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1
|
||||
|
|
@ -105,12 +106,12 @@ lemma detRep_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connec
|
|||
simp [detRep_apply, detRep_apply, detContinuous]
|
||||
rw [det_on_connected_component h]
|
||||
|
||||
lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.1.det :=
|
||||
lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.det = Λ'.1.det :=
|
||||
det_on_connected_component $ pathComponent_subset_component _ h
|
||||
|
||||
/-- A Lorentz Matrix is proper if its determinant is 1. -/
|
||||
@[simp]
|
||||
def IsProper (Λ : lorentzGroup) : Prop := Λ.1.1.det = 1
|
||||
def IsProper (Λ : lorentzGroup) : Prop := Λ.1.det = 1
|
||||
|
||||
instance : DecidablePred IsProper := by
|
||||
intro Λ
|
||||
|
|
@ -119,7 +120,7 @@ instance : DecidablePred IsProper := by
|
|||
lemma IsProper_iff (Λ : lorentzGroup) : IsProper Λ ↔ detRep Λ = 1 := by
|
||||
rw [show 1 = detRep 1 by simp]
|
||||
rw [detRep_apply, detRep_apply, detContinuous_eq_iff_det_eq]
|
||||
simp only [IsProper, OneMemClass.coe_one, Units.val_one, det_one]
|
||||
simp only [IsProper, lorentzGroupIsGroup_one_coe, det_one]
|
||||
|
||||
lemma id_IsProper : IsProper 1 := by
|
||||
simp [IsProper]
|
||||
|
|
|
|||
|
|
@ -18,23 +18,40 @@ namespace spaceTime
|
|||
namespace lorentzGroup
|
||||
open GroupTheory
|
||||
|
||||
/-- Given a element of `SO(3)` the matrix corresponding to a space-time rotation. -/
|
||||
@[simp]
|
||||
def SO3ToMatrix (A : SO(3)) : Matrix (Fin 4) (Fin 4) ℝ :=
|
||||
Matrix.reindex finSumFinEquiv finSumFinEquiv (Matrix.fromBlocks 1 0 0 A.1)
|
||||
|
||||
@[simp]
|
||||
lemma SO3ToMatrix_det (A : SO(3)) : (SO3ToMatrix A).det = 1 := by
|
||||
simp only [SO3ToMatrix, Nat.reduceAdd, Matrix.reindex_apply, Matrix.det_submatrix_equiv_self,
|
||||
Matrix.det_fromBlocks_zero₂₁, Matrix.det_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Matrix.one_apply_eq, A.2, mul_one]
|
||||
|
||||
lemma SO3ToMatrix_lorentz (A : SO(3)) : η * (SO3ToMatrix A).transpose * η * SO3ToMatrix A = 1 := by
|
||||
lemma SO3ToMatrix_PreservesηLin (A : SO(3)) : PreservesηLin $ SO3ToMatrix A := by
|
||||
rw [PreservesηLin.iff_matrix]
|
||||
simp only [η_block, Nat.reduceAdd, Matrix.reindex_apply, SO3ToMatrix, Matrix.transpose_submatrix,
|
||||
Matrix.fromBlocks_transpose, Matrix.transpose_one, Matrix.transpose_zero,
|
||||
Matrix.submatrix_mul_equiv, Matrix.fromBlocks_multiply, mul_one, Matrix.mul_zero, add_zero,
|
||||
Matrix.zero_mul, Matrix.mul_one, neg_mul, one_mul, zero_add, Matrix.mul_neg, neg_zero, mul_neg,
|
||||
neg_neg, Matrix.mul_eq_one_comm.mpr A.2.2, Matrix.fromBlocks_one, Matrix.submatrix_one_equiv]
|
||||
|
||||
lemma SO3ToMatrix_injective : Function.Injective SO3ToMatrix := by
|
||||
intro A B h
|
||||
erw [Equiv.apply_eq_iff_eq] at h
|
||||
have h1 := congrArg Matrix.toBlocks₂₂ h
|
||||
rw [Matrix.toBlocks_fromBlocks₂₂, Matrix.toBlocks_fromBlocks₂₂] at h1
|
||||
apply Subtype.eq
|
||||
exact h1
|
||||
|
||||
/-- Given a element of `SO(3)` the element of the Lorentz group corresponding to a
|
||||
space-time rotation. -/
|
||||
def SO3ToLorentz : SO(3) →* 𝓛 where
|
||||
toFun A := ⟨SO3ToMatrix A, SO3ToMatrix_PreservesηLin A⟩
|
||||
map_one' := by
|
||||
apply Subtype.eq
|
||||
simp only [SO3ToMatrix, Nat.reduceAdd, Matrix.reindex_apply, lorentzGroupIsGroup_one_coe]
|
||||
erw [Matrix.fromBlocks_one]
|
||||
exact Matrix.submatrix_one_equiv finSumFinEquiv.symm
|
||||
map_mul' A B := by
|
||||
apply Subtype.eq
|
||||
simp [Matrix.fromBlocks_multiply]
|
||||
|
||||
|
||||
end lorentzGroup
|
||||
|
||||
|
|
|
|||
|
|
@ -73,7 +73,8 @@ lemma η_block : η = Matrix.reindex finSumFinEquiv finSumFinEquiv (
|
|||
fin_cases i <;> fin_cases j
|
||||
<;> simp_all only [Fin.zero_eta, reindex_apply, submatrix_apply]
|
||||
any_goals rfl
|
||||
all_goals simp [finSumFinEquiv, Fin.addCases, η, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one,
|
||||
all_goals simp [finSumFinEquiv, Fin.addCases, η, 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]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue