DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Major refactor of Lorentz group

Browse source
This commit is contained in:
jstoobysmith 2024-05-17 15:10:35 -04:00
parent 89e940a029
commit 7ebd2af7a5
6 changed files with 563 additions and 931 deletions
Download patch file Download diff file Expand all files Collapse all files

242
HepLean/SpaceTime/FourVelocity.lean Normal file
View file

@ -0,0 +1,242 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.Metric
/-!
# Four velocity
We define
- `PreFourVelocity` : as a space-time element with norm 1.
- `FourVelocity` : as a space-time element with norm 1 and future pointing.
-/
open spaceTime
@[simp]
def PreFourVelocity : Set spaceTime :=
fun x => ηLin x x = 1
instance : TopologicalSpace PreFourVelocity := by
exact instTopologicalSpaceSubtype
namespace PreFourVelocity
lemma mem_PreFourVelocity_iff {x : spaceTime} : x ∈ PreFourVelocity ↔ ηLin x x = 1 := by
rfl
def neg (v : PreFourVelocity) : PreFourVelocity := ⟨-v, by
rw [mem_PreFourVelocity_iff]
simp only [map_neg, LinearMap.neg_apply, neg_neg]
exact v.2 ⟩
lemma zero_sq (v : PreFourVelocity) : v.1 0 ^ 2 = 1 + ‖v.1.space‖ ^ 2 := by
rw [time_elm_sq_of_ηLin, v.2]
lemma zero_abs_ge_one (v : PreFourVelocity) : 1 ≤ |v.1 0| := by
have h1 := ηLin_leq_time_sq v.1
rw [v.2] at h1
exact (one_le_sq_iff_one_le_abs _).mp h1
lemma zero_abs_gt_norm_space (v : PreFourVelocity) : ‖v.1.space‖ < |v.1 0| := by
rw [(abs_norm _).symm, ← @sq_lt_sq, zero_sq]
simp only [space, Fin.isValue, lt_add_iff_pos_left, zero_lt_one]
lemma zero_abs_ge_norm_space (v : PreFourVelocity) : ‖v.1.space‖ ≤ |v.1 0| :=
le_of_lt (zero_abs_gt_norm_space v)
lemma zero_le_minus_one_or_ge_one (v : PreFourVelocity) : v.1 0 ≤ -1 ∨ 1 ≤ v.1 0 :=
le_abs'.mp (zero_abs_ge_one v)
lemma zero_nonpos_iff (v : PreFourVelocity) : v.1 0 ≤ 0 ↔ v.1 0 ≤ - 1 := by
apply Iff.intro
· intro h
cases' zero_le_minus_one_or_ge_one v with h1 h1
exact h1
linarith
· intro h
linarith
lemma zero_nonneg_iff (v : PreFourVelocity) : 0 ≤ v.1 0 ↔ 1 ≤ v.1 0 := by
apply Iff.intro
· intro h
cases' zero_le_minus_one_or_ge_one v with h1 h1
linarith
exact h1
· intro h
linarith
def IsFourVelocity (v : PreFourVelocity) : Prop := 0 ≤ v.1 0
lemma IsFourVelocity_abs_zero {v : PreFourVelocity} (hv : IsFourVelocity v) :
|v.1 0| = v.1 0 := abs_of_nonneg hv
lemma not_IsFourVelocity_iff (v : PreFourVelocity) : ¬ IsFourVelocity v ↔ v.1 0 ≤ 0 := by
rw [IsFourVelocity, not_le]
apply Iff.intro
intro h
exact le_of_lt h
intro h
have h1 := (zero_nonpos_iff v).mp h
linarith
lemma not_IsFourVelocity_iff_neg {v : PreFourVelocity} : ¬ IsFourVelocity v ↔
IsFourVelocity (neg v):= by
rw [not_IsFourVelocity_iff, IsFourVelocity]
simp only [Fin.isValue, neg]
change _ ↔ 0 ≤ - v.1 0
simp
lemma zero_abs_mul_sub_norm_space (v v' : PreFourVelocity) :
0 ≤ |v.1 0| * |v'.1 0| - ‖v.1.space‖ * ‖v'.1.space‖ := by
apply sub_nonneg.mpr
apply mul_le_mul (zero_abs_ge_norm_space v) (zero_abs_ge_norm_space v') ?_ ?_
exact norm_nonneg v'.1.space
exact abs_nonneg (v.1 0)
lemma euclid_norm_IsFourVelocity_IsFourVelocity {v v' : PreFourVelocity}
(h : IsFourVelocity v) (h' : IsFourVelocity v') :
0 ≤ (v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ := by
apply le_trans (zero_abs_mul_sub_norm_space v v')
rw [IsFourVelocity_abs_zero h, IsFourVelocity_abs_zero h', sub_eq_add_neg]
apply (add_le_add_iff_left _).mpr
rw [@neg_le]
apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (v'.1).space⟫_ℝ|) ?_
exact abs_real_inner_le_norm (v.1).space (v'.1).space
lemma euclid_norm_not_IsFourVelocity_not_IsFourVelocity {v v' : PreFourVelocity}
(h : ¬ IsFourVelocity v) (h' : ¬ IsFourVelocity v') :
0 ≤ (v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ := by
have h1 := euclid_norm_IsFourVelocity_IsFourVelocity (not_IsFourVelocity_iff_neg.mp h)
(not_IsFourVelocity_iff_neg.mp h')
apply le_of_le_of_eq h1 ?_
simp [neg, Fin.sum_univ_three, neg]
repeat rw [show (- v.1) _ = - v.1 _ from rfl]
repeat rw [show (- v'.1) _ = - v'.1 _ from rfl]
ring
lemma euclid_norm_IsFourVelocity_not_IsFourVelocity {v v' : PreFourVelocity}
(h : IsFourVelocity v) (h' : ¬ IsFourVelocity v') :
(v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ ≤ 0 := by
rw [show (0 : ℝ) = - 0 by simp, le_neg]
have h1 := euclid_norm_IsFourVelocity_IsFourVelocity h (not_IsFourVelocity_iff_neg.mp h')
apply le_of_le_of_eq h1 ?_
simp [neg, Fin.sum_univ_three, neg]
repeat rw [show (- v'.1) _ = - v'.1 _ from rfl]
ring
lemma euclid_norm_not_IsFourVelocity_IsFourVelocity {v v' : PreFourVelocity}
(h : ¬ IsFourVelocity v) (h' : IsFourVelocity v') :
(v.1 0) * (v'.1 0) + ⟪v.1.space, v'.1.space⟫_ℝ ≤ 0 := by
rw [show (0 : ℝ) = - 0 by simp, le_neg]
have h1 := euclid_norm_IsFourVelocity_IsFourVelocity h' (not_IsFourVelocity_iff_neg.mp h)
apply le_of_le_of_eq h1 ?_
simp [neg, Fin.sum_univ_three, neg]
repeat rw [show (- v.1) _ = - v.1 _ from rfl]
ring
end PreFourVelocity
def FourVelocity : Set PreFourVelocity :=
fun x => PreFourVelocity.IsFourVelocity x
instance : TopologicalSpace FourVelocity := instTopologicalSpaceSubtype
namespace FourVelocity
open PreFourVelocity
lemma mem_FourVelocity_iff {x : PreFourVelocity} : x ∈ FourVelocity ↔ 0 ≤ x.1 0 := by
rfl
lemma time_comp (x : FourVelocity) : x.1.1 0 = √(1 + ‖x.1.1.space‖ ^ 2) := by
symm
rw [Real.sqrt_eq_cases]
refine Or.inl (And.intro ?_ x.2)
rw [← PreFourVelocity.zero_sq x.1, sq]
def zero : FourVelocity := ⟨⟨![1, 0, 0, 0], by
rw [mem_PreFourVelocity_iff, ηLin_expand]; simp⟩, by
rw [mem_FourVelocity_iff]; simp⟩
noncomputable def pathFromZero (u : FourVelocity) : Path zero u where
toFun t := ⟨
⟨![√(1 + t ^ 2 * ‖u.1.1.space‖ ^ 2), t * u.1.1 1, t * u.1.1 2, t * u.1.1 3],
by
rw [mem_PreFourVelocity_iff, ηLin_expand]
simp only [space, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
Matrix.cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, Matrix.tail_cons,
Matrix.cons_val_three]
rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
simp only [Fin.isValue, Matrix.cons_val_zero, RCLike.inner_apply, conj_trivial,
Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two, Nat.succ_eq_add_one,
Nat.reduceAdd, Matrix.tail_cons]
ring
refine Right.add_nonneg (zero_le_one' ℝ) $
mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩,
by
rw [mem_FourVelocity_iff]
exact Real.sqrt_nonneg _⟩
continuous_toFun := by
refine Continuous.subtype_mk ?_ _
refine Continuous.subtype_mk ?_ _
apply (continuous_pi_iff).mpr
intro i
fin_cases i
<;> continuity
source' := by
simp
rfl
target' := by
simp
refine SetCoe.ext ?_
refine SetCoe.ext ?_
funext i
fin_cases i
simp
exact (time_comp _).symm
all_goals rfl
lemma isPathConnected_FourVelocity : IsPathConnected (@Set.univ FourVelocity) := by
use zero
apply And.intro trivial ?_
intro y _
use pathFromZero y
simp only [Set.mem_univ, implies_true]
lemma η_pos (u v : FourVelocity) : 0 < ηLin u v := by
refine lt_of_lt_of_le ?_ (ηLin_ge_sub_norm u v)
apply sub_pos.mpr
refine mul_lt_mul_of_nonneg_of_pos ?_ ?_ ?_ ?_
simpa [IsFourVelocity_abs_zero u.2] using zero_abs_gt_norm_space u.1
simpa [IsFourVelocity_abs_zero v.2] using zero_abs_ge_norm_space v.1
exact norm_nonneg u.1.1.space
have h2 := (mem_FourVelocity_iff).mp v.2
rw [zero_nonneg_iff] at h2
linarith
lemma one_plus_ne_zero (u v : FourVelocity) : 1 + ηLin u v ≠ 0 := by
linarith [η_pos u v]
lemma η_continuous (u : spaceTime) : Continuous (fun (a : FourVelocity) => ηLin u a) := by
simp only [ηLin_expand]
refine Continuous.add ?_ ?_
refine Continuous.add ?_ ?_
refine Continuous.add ?_ ?_
refine Continuous.comp' (continuous_mul_left _) ?_
apply (continuous_pi_iff).mp
exact Isometry.continuous fun x1 => congrFun rfl
all_goals apply Continuous.neg
all_goals apply Continuous.comp' (continuous_mul_left _)
all_goals apply (continuous_pi_iff).mp
all_goals exact Isometry.continuous fun x1 => congrFun rfl
end FourVelocity

501
HepLean/SpaceTime/LorentzGroup.lean
View file

@ -1,501 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.Metric
import Mathlib.GroupTheory.SpecificGroups.KleinFour
/-!
# The Lorentz Group
We define the Lorentz group.
## TODO
- Show that the Lorentz is a Lie group.
- Prove that the restricted Lorentz group is equivalent to the connected component of the
identity.
- Define the continuous maps from `ℝ³` to `restrictedLorentzGroup` defining boosts.
## References
- http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
- A proof that the restricted Lorentz group is connected can be found at:
https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
The proof involves the introduction of boosts.
-/
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 preserve_ηLin_iff' (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
(∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔
∀ (x y : spaceTime), ηLin (x) ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by
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 preserve_ηLin_iff'' (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
(∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔
η * Λᵀ * η * Λ = 1 := by
rw [preserve_ηLin_iff', ηLin_matrix_eq_identity_iff (η * Λᵀ * η * Λ)]
apply Iff.intro
· simp_all [ηLin, implies_true, iff_true, one_mulVec]
· simp_all only [ηLin, LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply,
mulVec_mulVec, implies_true]
lemma preserve_ηLin_iff''' (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
(∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔
Λ * (η * Λᵀ * η) = 1 := by
rw [preserve_ηLin_iff'']
apply Iff.intro
intro h
exact mul_eq_one_comm.mp h
intro h
exact mul_eq_one_comm.mp h
lemma preserve_ηLin_iff_transpose (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
(∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) ↔
(∀ (x y : spaceTime), ηLin (Λᵀ *ᵥ x) (Λᵀ *ᵥ y) = ηLin x y) := by
apply Iff.intro
intro h
have h1 := congrArg transpose ((preserve_ηLin_iff'' Λ).mp h)
rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
← mul_assoc, transpose_one] at h1
rw [preserve_ηLin_iff''' Λ.transpose, ← h1]
repeat rw [← mul_assoc]
intro h
have h1 := congrArg transpose ((preserve_ηLin_iff'' Λ.transpose).mp h)
rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
← mul_assoc, transpose_one, transpose_transpose] at h1
rw [preserve_ηLin_iff''', ← h1]
repeat rw [← mul_assoc]
def preserveηLinGLnLift {Λ : Matrix (Fin 4) (Fin 4) ℝ}
(h : ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) : GL (Fin 4) ℝ :=
⟨Λ, η * Λᵀ * η ,(preserve_ηLin_iff''' Λ).mp h , (preserve_ηLin_iff'' Λ).mp h⟩
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]
exact preserve_ηLin_iff' Λ.1
lemma mem_lorentzGroup_iff'' (Λ : GL (Fin 4) ℝ) :
Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η * Λ.1 = 1 := by
rw [mem_lorentzGroup_iff]
exact preserve_ηLin_iff'' Λ
lemma mem_lorentzGroup_iff''' (Λ : GL (Fin 4) ℝ) :
Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η = Λ⁻¹ := by
rw [mem_lorentzGroup_iff'']
exact Units.mul_eq_one_iff_eq_inv
def preserveηLinLorentzLift {Λ : Matrix (Fin 4) (Fin 4) ℝ}
(h : ∀ (x y : spaceTime), ηLin (Λ *ᵥ x) (Λ *ᵥ y) = ηLin x y) : lorentzGroup :=
⟨preserveηLinGLnLift h, (mem_lorentzGroup_iff (preserveηLinGLnLift h)).mpr h⟩
-- TODO: Simplify using preserveηLinLorentzLift.
lemma mem_lorentzGroup_iff_transpose (Λ : GL (Fin 4) ℝ) :
Λ ∈ lorentzGroup ↔ ⟨transpose Λ, (transpose Λ)⁻¹, by
rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ).symm]
rw [show ((Λ)⁻¹).1 * Λ.1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.inv_mul_eq_one]]
rw [@transpose_eq_one], by
rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ).symm]
rw [show Λ.1 * ((Λ)⁻¹).1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.mul_inv_eq_one]]
rw [@transpose_eq_one]⟩ ∈ lorentzGroup := by
rw [mem_lorentzGroup_iff''', mem_lorentzGroup_iff''']
simp only [coe_units_inv, transpose_transpose, Units.inv_mk]
apply Iff.intro
intro h
have h1 := congrArg transpose h
rw [transpose_mul, transpose_mul, transpose_transpose, η_transpose, ← mul_assoc] at h1
rw [h1]
exact transpose_nonsing_inv _
intro h
have h1 := congrArg transpose h
rw [transpose_mul, transpose_mul, η_transpose, ← mul_assoc] at h1
rw [h1, transpose_nonsing_inv, transpose_transpose]
/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
def lorentzGroupTranspose (Λ : lorentzGroup) : lorentzGroup :=
⟨⟨transpose Λ.1, (transpose Λ.1)⁻¹, by
rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ.1).symm]
rw [show ((Λ.1)⁻¹).1 * Λ.1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.inv_mul_eq_one]]
rw [@transpose_eq_one], by
rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ.1).symm]
rw [show Λ.1.1 * ((Λ.1)⁻¹).1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.mul_inv_eq_one]]
rw [@transpose_eq_one]⟩,
(mem_lorentzGroup_iff_transpose Λ.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
/-- The Lorentz Group is a closed subset of `GL (Fin 4) ℝ`. -/
theorem lorentzGroup_isClosed : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by
rw [lorentzGroup_kernal]
exact continuous_iff_isClosed.mp lorentzMap_continuous {1} isClosed_singleton
namespace lorentzGroup
lemma det_eq_one_or_neg_one (Λ : 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))
local notation "ℤ₂" => Multiplicative (ZMod 2)
instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
/-- A group homomorphism from `lorentzGroup` to `ℤ₂` taking a matrix to
0 if it's determinant is 1 and 1 if its determinant is -1.-/
@[simps!]
def detRep : lorentzGroup →* ℤ₂ where
toFun Λ := if Λ.1.1.det = 1 then (Additive.toMul 0) else Additive.toMul (1 : ZMod 2)
map_one' := by
simp
map_mul' := by
intro Λ1 Λ2
simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero,
mul_ite, mul_one, ite_mul, one_mul]
cases' (det_eq_one_or_neg_one Λ1) with h1 h1
<;> cases' (det_eq_one_or_neg_one Λ2) with h2 h2
<;> simp [h1, h2]
rfl
/-- A Lorentz Matrix is proper if its determinant is 1. -/
def IsProper (Λ : lorentzGroup) : Prop := Λ.1.1.det = 1
instance : DecidablePred IsProper := by
intro Λ
apply Real.decidableEq
lemma IsProper_iff (Λ : lorentzGroup) :
IsProper Λ ↔ detRep Λ = Additive.toMul 0 := by
apply Iff.intro
intro h
erw [detRep_apply, if_pos h]
simp only [toMul_zero]
intro h
by_cases h1 : IsProper Λ
exact h1
erw [detRep_apply, if_neg h1] at h
contradiction
section Orthochronous
/-- The space-like part of the first row of of a Lorentz matrix. -/
@[simp]
def fstRowToEuclid (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 0 i.succ
/-- The space-like part of the first column of of a Lorentz matrix. -/
@[simp]
def fstColToEuclid (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 i.succ 0
lemma fst_col_normalized (Λ : lorentzGroup) :
(Λ.1 0 0) ^ 2 - (Λ.1 1 0) ^ 2 - (Λ.1 2 0) ^ 2 - (Λ.1 3 0) ^ 2 = 1 := by
have h00 := congrFun (congrFun ((mem_lorentzGroup_iff'' Λ).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
simp only [η, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two,
Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00
rw [← h00]
ring
lemma fst_row_normalized (Λ : lorentzGroup) :
(Λ.1 0 0) ^ 2 - (Λ.1 0 1) ^ 2 - (Λ.1 0 2) ^ 2 - (Λ.1 0 3) ^ 2 = 1 := by
simpa using fst_col_normalized (lorentzGroupTranspose Λ)
lemma zero_zero_sq_col (Λ : lorentzGroup) :
(Λ.1 0 0) ^ 2 = 1 + (Λ.1 1 0) ^ 2 + (Λ.1 2 0) ^ 2 + (Λ.1 3 0) ^ 2 := by
rw [← fst_col_normalized Λ]
ring
lemma zero_zero_sq_row (Λ : lorentzGroup) :
(Λ.1 0 0) ^ 2 = 1 + (Λ.1 0 1) ^ 2 + (Λ.1 0 2) ^ 2 + (Λ.1 0 3) ^ 2 := by
rw [← fst_row_normalized Λ]
ring
lemma zero_zero_sq_col' (Λ : lorentzGroup) :
(Λ.1 0 0) ^ 2 = 1 + ‖fstColToEuclid Λ‖ ^ 2 := by
rw [zero_zero_sq_col, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
simp only [Fin.isValue, fstColToEuclid, Fin.succ_zero_eq_one, RCLike.inner_apply, conj_trivial,
Fin.succ_one_eq_two]
rw [show (Fin.succ 2) = 3 by rfl]
ring_nf
lemma zero_zero_sq_row' (Λ : lorentzGroup) :
(Λ.1 0 0) ^ 2 = 1 + ‖fstRowToEuclid Λ‖ ^ 2 := by
rw [zero_zero_sq_row, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
simp only [Fin.isValue, fstRowToEuclid, Fin.succ_zero_eq_one, RCLike.inner_apply, conj_trivial,
Fin.succ_one_eq_two]
rw [show (Fin.succ 2) = 3 by rfl]
ring_nf
lemma norm_col_leq_abs_zero_zero (Λ : lorentzGroup) : ‖fstColToEuclid Λ‖ ≤ |Λ.1 0 0| := by
rw [(abs_norm (fstColToEuclid Λ)).symm, ← @sq_le_sq, zero_zero_sq_col']
simp only [le_add_iff_nonneg_left, zero_le_one]
lemma norm_row_leq_abs_zero_zero (Λ : lorentzGroup) : ‖fstRowToEuclid Λ‖ ≤ |Λ.1 0 0| := by
rw [(abs_norm (fstRowToEuclid Λ)).symm, ← @sq_le_sq, zero_zero_sq_row']
simp only [le_add_iff_nonneg_left, zero_le_one]
lemma zero_zero_sq_ge_one (Λ : lorentzGroup) : 1 ≤ (Λ.1 0 0) ^ 2 := by
rw [zero_zero_sq_col Λ]
refine le_add_of_le_of_nonneg ?_ (sq_nonneg _)
refine le_add_of_le_of_nonneg ?_ (sq_nonneg _)
refine le_add_of_le_of_nonneg (le_refl 1) (sq_nonneg _)
lemma abs_zero_zero_ge_one (Λ : lorentzGroup) : 1 ≤ |Λ.1 0 0| :=
(one_le_sq_iff_one_le_abs _).mp (zero_zero_sq_ge_one Λ)
lemma zero_zero_le_minus_one_or_ge_one (Λ : lorentzGroup) : (Λ.1 0 0) ≤ - 1 ∨ 1 ≤ (Λ.1 0 0) :=
le_abs'.mp (abs_zero_zero_ge_one Λ)
lemma zero_zero_nonpos_iff (Λ : lorentzGroup) : (Λ.1 0 0) ≤ 0 ↔ (Λ.1 0 0) ≤ - 1 := by
apply Iff.intro
· intro h
cases' zero_zero_le_minus_one_or_ge_one Λ with h1 h1
exact h1
linarith
· intro h
linarith
lemma zero_zero_nonneg_iff (Λ : lorentzGroup) : 0 ≤ (Λ.1 0 0) ↔ 1 ≤ (Λ.1 0 0) := by
apply Iff.intro
· intro h
cases' zero_zero_le_minus_one_or_ge_one Λ with h1 h1
linarith
exact h1
· intro h
linarith
/-- An element of the lorentz group is orthochronous if its time-time element is non-negative. -/
@[simp]
def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0
instance : Decidable (IsOrthochronous Λ) :=
Real.decidableLE 0 (Λ.1 0 0)
lemma not_IsOrthochronous_iff (Λ : lorentzGroup) : ¬ IsOrthochronous Λ ↔ Λ.1 0 0 ≤ 0 := by
rw [IsOrthochronous, not_le]
apply Iff.intro
intro h
exact le_of_lt h
intro h
have h1 := (zero_zero_nonpos_iff Λ).mp h
linarith
lemma IsOrthochronous_abs_zero_zero {Λ : lorentzGroup} (h : IsOrthochronous Λ) :
|Λ.1 0 0| = Λ.1 0 0 :=
abs_eq_self.mpr h
lemma not_IsOrthochronous_abs_zero_zero {Λ : lorentzGroup} (h : ¬ IsOrthochronous Λ) :
Λ.1 0 0 = - |Λ.1 0 0| := by
refine neg_eq_iff_eq_neg.mp (abs_eq_neg_self.mpr ?_).symm
simp only [IsOrthochronous, Fin.isValue, not_le] at h
exact le_of_lt h
lemma schwartz_identity_fst_row_col (Λ Λ' : lorentzGroup) :
‖⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ‖ ≤ ‖fstRowToEuclid Λ‖ * ‖fstColToEuclid Λ'‖ :=
norm_inner_le_norm (fstRowToEuclid Λ) (fstColToEuclid Λ')
lemma zero_zero_mul (Λ Λ' : lorentzGroup) :
(Λ * Λ').1 0 0 = (Λ.1 0 0) * (Λ'.1 0 0) + ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ := by
rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four]
rw [@PiLp.inner_apply, Fin.sum_univ_three]
simp
rw [show (Fin.succ 2) = 3 by rfl]
ring_nf
example (a b c : ℝ ) (h : a - b ≤ a + c) : - b ≤ c := by
exact (add_le_add_iff_left a).mp h
lemma zero_zero_mul_sub_row_col (Λ Λ' : lorentzGroup) :
0 ≤ |Λ.1 0 0| * |Λ'.1 0 0| - ‖fstRowToEuclid Λ‖ * ‖fstColToEuclid Λ'‖ :=
sub_nonneg.mpr (mul_le_mul (norm_row_leq_abs_zero_zero Λ) (norm_col_leq_abs_zero_zero Λ')
(norm_nonneg (fstColToEuclid Λ')) (abs_nonneg (Λ.1 0 0)))
lemma orthchro_mul_orthchro {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
(h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
apply le_trans (zero_zero_mul_sub_row_col Λ Λ')
have h1 := zero_zero_mul Λ Λ'
rw [← IsOrthochronous_abs_zero_zero h, ← IsOrthochronous_abs_zero_zero h'] at h1
refine le_trans
(?_ : _ ≤ |Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|)) ?_
· erw [add_le_add_iff_left]
simp only [neg_mul, neg_neg, neg_le]
exact schwartz_identity_fst_row_col Λ Λ'
· rw [h1, add_le_add_iff_left]
exact neg_abs_le ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
lemma not_orthchro_mul_not_orthchro {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ)
(h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
apply le_trans (zero_zero_mul_sub_row_col Λ Λ')
refine le_trans
(?_ : _ ≤ |Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|)) ?_
· erw [add_le_add_iff_left]
simp only [neg_mul, neg_neg, neg_le]
exact schwartz_identity_fst_row_col Λ Λ'
· rw [zero_zero_mul Λ Λ', not_IsOrthochronous_abs_zero_zero h,
not_IsOrthochronous_abs_zero_zero h']
simp only [Fin.isValue, abs_neg, _root_.abs_abs, conj_trivial, mul_neg, neg_mul, neg_neg,
add_le_add_iff_left]
exact neg_abs_le ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
lemma orthchro_mul_not_orthchro {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
(h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
rw [not_IsOrthochronous_iff]
refine le_trans
(?_ : _ ≤ - (|Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|))) ?_
· rw [zero_zero_mul Λ Λ', ← IsOrthochronous_abs_zero_zero h,
not_IsOrthochronous_abs_zero_zero h']
simp only [Fin.isValue, mul_neg, _root_.abs_abs, abs_neg, neg_add_rev, neg_neg,
le_add_neg_iff_add_le, neg_add_cancel_comm]
exact le_abs_self ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
· apply le_trans ?_ (neg_nonpos_of_nonneg (zero_zero_mul_sub_row_col Λ Λ'))
simp only [Fin.isValue, neg_add_rev, neg_neg, neg_sub, add_neg_le_iff_le_add, sub_add_cancel]
exact schwartz_identity_fst_row_col _ _
lemma not_orthchro_mul_orthchro {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ)
(h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
rw [not_IsOrthochronous_iff]
refine le_trans
(?_ : _ ≤ - (|Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|))) ?_
· rw [zero_zero_mul Λ Λ', ← IsOrthochronous_abs_zero_zero h',
not_IsOrthochronous_abs_zero_zero h]
simp only [Fin.isValue, neg_mul, PiLp.inner_apply, fstRowToEuclid, fstColToEuclid,
RCLike.inner_apply, conj_trivial, abs_neg, _root_.abs_abs, neg_add_rev, neg_neg,
le_add_neg_iff_add_le, neg_add_cancel_comm]
exact le_abs_self ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
· apply le_trans ?_ (neg_nonpos_of_nonneg (zero_zero_mul_sub_row_col Λ Λ'))
simp only [Fin.isValue, neg_add_rev, neg_neg, neg_sub, add_neg_le_iff_le_add, sub_add_cancel]
exact schwartz_identity_fst_row_col _ _
/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernal consists of precisely the
orthochronous elements. -/
@[simps!]
def orthochronousRep : lorentzGroup →* ℤ₂ where
toFun Λ := if IsOrthochronous Λ then (Additive.toMul 0) else Additive.toMul (1 : ZMod 2)
map_one' := by
simp
map_mul' := by
intro Λ1 Λ2
simp only [toMul_zero, mul_ite, mul_one, ite_mul, one_mul]
cases' (em (IsOrthochronous Λ1)) with h h
<;> cases' (em (IsOrthochronous Λ2)) with h' h'
rw [if_pos (orthchro_mul_orthchro h h'), if_pos h, if_pos h']
rw [if_neg (orthchro_mul_not_orthchro h h'), if_neg h', if_pos h]
rw [if_neg (not_orthchro_mul_orthchro h h'), if_pos h', if_neg h]
rw [if_pos (not_orthchro_mul_not_orthchro h h'), if_neg h', if_neg h]
rfl
lemma IsOrthochronous_iff (Λ : lorentzGroup) :
IsOrthochronous Λ ↔ orthochronousRep Λ = Additive.toMul 0 := by
apply Iff.intro
intro h
erw [orthochronousRep_apply, if_pos h]
simp only [toMul_zero]
intro h
by_cases h1 : IsOrthochronous Λ
exact h1
erw [orthochronousRep_apply, if_neg h1] at h
contradiction
end Orthochronous
end lorentzGroup
open lorentzGroup in
/-- The restricted lorentz group consists of those elements of the `lorentzGroup` which are
proper and orthochronous. -/
def restrictedLorentzGroup : Subgroup (lorentzGroup) where
carrier := {Λ | IsProper Λ ∧ IsOrthochronous Λ}
mul_mem' {Λa Λb} := by
intro ha hb
apply And.intro
rw [IsProper_iff, detRep.map_mul, (IsProper_iff Λa).mp ha.1, (IsProper_iff Λb).mp hb.1]
simp only [toMul_zero, mul_one]
rw [IsOrthochronous_iff, orthochronousRep.map_mul, (IsOrthochronous_iff Λa).mp ha.2,
(IsOrthochronous_iff Λb).mp hb.2]
simp
one_mem' := by
simp only [IsOrthochronous, Fin.isValue, Set.mem_setOf_eq, OneMemClass.coe_one, Units.val_one,
one_apply_eq, zero_le_one, and_true]
rw [IsProper_iff, detRep.map_one]
simp
inv_mem' {Λ} := by
intro h
apply And.intro
rw [IsProper_iff, detRep.map_inv, (IsProper_iff Λ).mp h.1]
simp only [toMul_zero, inv_one]
rw [IsOrthochronous_iff, orthochronousRep.map_inv, (IsOrthochronous_iff Λ).mp h.2]
simp
/-- The restricted lorentz group is a topological group. -/
instance : TopologicalGroup restrictedLorentzGroup :=
Subgroup.instTopologicalGroupSubtypeMem restrictedLorentzGroup
end spaceTime
end

59
HepLean/SpaceTime/LorentzGroup/Basic.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.Metric
import HepLean.SpaceTime.FourVelocity
import Mathlib.GroupTheory.SpecificGroups.KleinFour
/-!
# The Lorentz Group
@ -112,7 +113,7 @@ def lorentzGroup : Subgroup (GL (Fin 4) ℝ) where
instance : TopologicalGroup lorentzGroup :=
Subgroup.instTopologicalGroupSubtypeMem lorentzGroup
@[simps!]
def PreservesηLin.liftLor {Λ : Matrix (Fin 4) (Fin 4) ℝ} (h : PreservesηLin Λ) :
lorentzGroup := ⟨liftGL h, h⟩
@ -143,62 +144,6 @@ theorem isClosed_of_GL4 : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by
rw [kernalMap_kernal_eq_lorentzGroup]
exact continuous_iff_isClosed.mp kernalMap.2 {1} isClosed_singleton
section Relations
/-- The first column of a lorentz matrix. -/
@[simp]
def fstCol (Λ : lorentzGroup) : spaceTime := fun i => Λ.1 i 0
lemma ηLin_fstCol (Λ : lorentzGroup) : ηLin (fstCol Λ) (fstCol Λ) = 1 := by
rw [ηLin_expand]
have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp ((mem_iff Λ.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
simp only [η, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two,
Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00
rw [← h00]
simp only [fstCol, Fin.isValue]
ring
lemma zero_component (x : { x : spaceTime // ηLin x x = 1}) :
x.1 0 ^ 2 = 1 + ‖x.1.space‖ ^ 2 := by
sorry
/-- The space-like part of the first row of of a Lorentz matrix. -/
@[simp]
def fstSpaceRow (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 0 i.succ
/-- The space-like part of the first column of of a Lorentz matrix. -/
@[simp]
def fstSpaceCol (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 i.succ 0
lemma fstSpaceRow_transpose (Λ : lorentzGroup) : fstSpaceRow (transpose Λ) = fstSpaceCol Λ := by
rfl
lemma fstSpaceCol_transpose (Λ : lorentzGroup) : fstSpaceCol (transpose Λ) = fstSpaceRow Λ := by
rfl
lemma fst_col_normalized (Λ : lorentzGroup) :
(Λ.1 0 0) ^ 2 - ‖fstSpaceCol Λ‖ ^ 2 = 1 := by
rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
simp
rw [show Fin.succ 2 = 3 by rfl]
have h00 := congrFun (congrFun ((PreservesηLin.iff_matrix Λ.1).mp ((mem_iff Λ.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
simp only [η, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two,
Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00
rw [← h00]
ring
lemma fst_row_normalized
end Relations
end lorentzGroup
end spaceTime

170
HepLean/SpaceTime/LorentzGroup/Boosts.lean Normal file
View file

@ -0,0 +1,170 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzGroup.Orthochronous
import Mathlib.GroupTheory.SpecificGroups.KleinFour
import Mathlib.Topology.Constructions
/-!
# Boosts
This file defines those Lorentz which are boosts.
We first define generalised boosts, which are restricted lorentz transforamations taking
a four velocity `u` to a four velcoity `v`.
A boost is the speical case of a generalised boost when `u = stdBasis 0`.
## TODO
- Show that generalised boosts are in the restircted Lorentz group.
- Define boosts.
## References
- The main argument follows: Guillem Cobos, The Lorentz Group, 2015:
https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
-/
noncomputable section
namespace spaceTime
namespace lorentzGroup
open FourVelocity
def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
toFun x := (2 * ηLin x u) • v.1.1
map_add' x y := by
simp only [map_add, LinearMap.add_apply]
rw [mul_add, add_smul]
map_smul' c x := by
simp only [LinearMapClass.map_smul, LinearMap.smul_apply, smul_eq_mul,
RingHom.id_apply]
rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul]
def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where
toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v)
map_add' x y := by
simp only
rw [ηLin.map_add, div_eq_mul_one_div]
rw [show (ηLin x + ηLin y) (↑u + ↑v) = ηLin x (u+v) + ηLin y (u+v) from rfl]
rw [add_mul, neg_add, add_smul, ← div_eq_mul_one_div, ← div_eq_mul_one_div]
map_smul' c x := by
simp only
rw [ηLin.map_smul]
rw [show (c • ηLin x) (↑u + ↑v) = c * ηLin x (u+v) from rfl]
rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
rfl
def genBoost (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime :=
LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v
namespace genBoost
lemma self (u : FourVelocity) : genBoost u u = LinearMap.id := by
ext x
simp [genBoost]
rw [add_assoc]
rw [@add_right_eq_self]
rw [@add_eq_zero_iff_eq_neg]
rw [genBoostAux₁, genBoostAux₂]
simp only [LinearMap.coe_mk, AddHom.coe_mk, map_add, smul_add, neg_smul, neg_add_rev, neg_neg]
rw [← add_smul]
apply congr
apply congrArg
repeat rw [u.1.2]
field_simp
ring
rfl
def toMatrix (u v : FourVelocity) : Matrix (Fin 4) (Fin 4) ℝ :=
LinearMap.toMatrix stdBasis stdBasis (genBoost u v)
lemma toMatrix_mulVec (u v : FourVelocity) (x : spaceTime) :
(toMatrix u v).mulVec x = genBoost u v x :=
LinearMap.toMatrix_mulVec_repr stdBasis stdBasis (genBoost u v) x
lemma toMatrix_apply (u v : FourVelocity) (i j : Fin 4) :
(toMatrix u v) i j =
η i i * (ηLin (stdBasis i) (stdBasis j) + 2 * ηLin (stdBasis j) u * ηLin (stdBasis i) v -
ηLin (stdBasis i) (u + v) * ηLin (stdBasis j) (u + v) / (1 + ηLin u v)) := by
rw [ηLin_matrix_stdBasis' j i (toMatrix u v), toMatrix_mulVec]
simp only [genBoost, genBoostAux₁, genBoostAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply,
LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, smul_eq_mul,
map_neg, mul_eq_mul_left_iff]
apply Or.inl
ring
lemma toMatrix_continuous (u : FourVelocity) : Continuous (toMatrix u) := by
refine continuous_matrix ?_
intro i j
simp only [toMatrix_apply]
refine Continuous.comp' (continuous_mul_left (η i i)) ?hf
refine Continuous.sub ?_ ?_
refine Continuous.comp' (continuous_add_left ((ηLin (stdBasis i)) (stdBasis j))) ?_
refine Continuous.comp' (continuous_mul_left (2 * (ηLin (stdBasis j)) ↑u)) ?_
exact η_continuous _
refine Continuous.mul ?_ ?_
refine Continuous.mul ?_ ?_
simp only [(ηLin _).map_add]
refine Continuous.comp' ?_ ?_
exact continuous_add_left ((ηLin (stdBasis i)) ↑u)
exact η_continuous _
simp only [(ηLin _).map_add]
refine Continuous.comp' ?_ ?_
exact continuous_add_left _
exact η_continuous _
refine Continuous.inv₀ ?_ ?_
refine Continuous.comp' (continuous_add_left 1) ?_
exact η_continuous _
exact fun x => one_plus_ne_zero u x
lemma toMatrix_PreservesηLin (u v : FourVelocity) : PreservesηLin (toMatrix u v) := by
intro x y
rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂]
have h1 : (1 + (ηLin ↑u) ↑v) ≠ 0 := one_plus_ne_zero u v
simp only [map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_coe,
id_eq, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, map_neg, LinearMap.smul_apply,
smul_eq_mul, LinearMap.neg_apply]
field_simp
rw [u.1.2, v.1.2, ηLin_symm v u, ηLin_symm u y, ηLin_symm v y]
ring
def toLorentz (u v : FourVelocity) : lorentzGroup :=
PreservesηLin.liftLor (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 ?_ ?_)
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
obtain ⟨f, _⟩ := isPathConnected_FourVelocity.joinedIn u trivial v trivial
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 ?_
simp [PreservesηLin.liftGL, toMatrix, self u]
· simp
end genBoost
end lorentzGroup
end spaceTime
end

293
HepLean/SpaceTime/LorentzGroup/Connectedness.lean
View file

@ -1,293 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzGroup
import Mathlib.GroupTheory.SpecificGroups.KleinFour
import Mathlib.Topology.Constructions
/-!
# Connectedness of the restricted Lorentz group
In this file we provide a proof that the restricted Lorentz group is connected.
## References
- The main argument follows: Guillem Cobos, The Lorentz Group, 2015:
https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
-/
noncomputable section
namespace spaceTime
def stepFunction : ℝ → ℝ := fun t =>
if t < -1 then -1 else
if t < 1 then t else 1
lemma stepFunction_continuous : Continuous stepFunction := by
apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_id continuous_const)
all_goals
intro a ha
rw [@Set.Iio_def, @frontier_Iio, @Set.mem_singleton_iff] at ha
rw [ha]
simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte]
def lorentzDet (Λ : lorentzGroup) : ({-1, 1} : Set ℝ) :=
⟨Λ.1.1.det, by
simp
exact Or.symm (lorentzGroup.det_eq_one_or_neg_one _)⟩
lemma lorentzDet_continuous : Continuous lorentzDet := by
refine Continuous.subtype_mk ?_ fun x => lorentzDet.proof_1 x
exact Continuous.matrix_det $
Continuous.comp' Units.continuous_val continuous_subtype_val
instance set_discrete : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite
lemma lorentzDet_eq_if_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') :
Λ.1.1.det = Λ'.1.1.det := by
obtain ⟨f, hf, hf2⟩ := h
have h1 : Joined (lorentzDet Λ) (lorentzDet Λ') :=
⟨ContinuousMap.comp ⟨lorentzDet, lorentzDet_continuous⟩ f, congrArg lorentzDet hf,
congrArg lorentzDet hf2⟩
obtain ⟨g, hg1, hg2⟩ := h1
have h2 := (@IsPreconnected.subsingleton ({-1, 1} : Set ℝ) _ _ _ (isPreconnected_range g.2))
(Set.mem_range_self 0) (Set.mem_range_self 1)
rw [hg1, hg2] at h2
simpa [lorentzDet] using h2
lemma det_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
Λ.1.1.det = Λ'.1.1.det := by
obtain ⟨s, hs, hΛ'⟩ := h
let f : ContinuousMap s ({-1, 1} : Set ℝ) :=
ContinuousMap.restrict s ⟨lorentzDet, lorentzDet_continuous⟩
haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1
have hf := (@IsPreconnected.subsingleton ({-1, 1} : Set ℝ) _ _ _ (isPreconnected_range f.2))
(Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩)
simpa [lorentzDet, f] using hf
lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.1.det :=
det_on_connected_component $ pathComponent_subset_component _ h
namespace restrictedLorentzGroup
/-- The set of spacetime points such that the time element is positive, and which are
normalised to 1. -/
def P : Set (spaceTime) := {x | x 0 > 0 ∧ ηLin x x = 1}
lemma P_time_comp (x : P) : x.1 0 = √(1 + ‖x.1.space‖ ^ 2) := by
symm
rw [Real.sqrt_eq_cases]
apply Or.inl
refine And.intro ?_ (le_of_lt x.2.1)
rw [← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
simp only [Fin.isValue, space, Matrix.cons_val_zero, RCLike.inner_apply, conj_trivial,
Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd,
Matrix.tail_cons]
have h1 := x.2.2
rw [ηLin_expand] at h1
linear_combination h1
def oneInP : P := ⟨![1, 0, 0, 0], by simp, by
rw [ηLin_expand]
simp⟩
def pathToOneInP (u : P) : Path oneInP u where
toFun t := ⟨![√(1 + t ^ 2 * ‖u.1.space‖ ^ 2), t * u.1 1, t * u.1 2, t * u.1 3],
by
simp
refine Right.add_pos_of_pos_of_nonneg (Real.zero_lt_one) $
mul_nonneg (sq_nonneg _) (sq_nonneg _)
, by
rw [ηLin_expand]
simp
rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
simp
ring
refine Right.add_nonneg (zero_le_one' ℝ) $
mul_nonneg (sq_nonneg _) (sq_nonneg _) ⟩
continuous_toFun := by
refine Continuous.subtype_mk ?_ _
apply (continuous_pi_iff).mpr
intro i
fin_cases i
<;> continuity
source' := by
simp
rfl
target' := by
simp
refine SetCoe.ext ?_
funext i
fin_cases i
simp
exact (P_time_comp u).symm
all_goals rfl
/-- P is a topological space with the subset topology. -/
instance : TopologicalSpace P := instTopologicalSpaceSubtype
lemma P_path_connected : IsPathConnected (@Set.univ P) := by
use oneInP
apply And.intro trivial ?_
intro y _
use pathToOneInP y
simp only [Set.mem_univ, implies_true]
lemma P_abs_space_lt_time_comp (x : P) : ‖x.1.space‖ < x.1 0 := by
rw [P_time_comp, Real.lt_sqrt]
exact lt_one_add (‖(x.1).space‖ ^ 2)
exact norm_nonneg (x.1).space
lemma η_P_P_pos (u v : P) : 0 < ηLin u v :=
lt_of_lt_of_le (sub_pos.mpr (mul_lt_mul_of_nonneg_of_pos
(P_abs_space_lt_time_comp u) ((P_abs_space_lt_time_comp v).le)
(norm_nonneg (u.1).space) v.2.1)) (ηLin_ge_sub_norm u v)
lemma η_P_continuous (u : spaceTime) : Continuous (fun (a : P) => ηLin u a) := by
simp only [ηLin_expand]
refine Continuous.add ?_ ?_
refine Continuous.add ?_ ?_
refine Continuous.add ?_ ?_
refine Continuous.comp' (continuous_mul_left _) ?_
apply (continuous_pi_iff).mp
exact continuous_subtype_val
all_goals apply Continuous.neg
all_goals apply Continuous.comp' (continuous_mul_left _)
all_goals apply (continuous_pi_iff).mp
all_goals exact continuous_subtype_val
lemma one_plus_η_P_P (u v : P) : 1 + ηLin u v ≠ 0 := by
linarith [η_P_P_pos u v]
def φAux₁ (u v : P) : spaceTime →ₗ[ℝ] spaceTime where
toFun x := (2 * ηLin x u) • v
map_add' x y := by
simp only [map_add, LinearMap.add_apply]
rw [mul_add, add_smul]
map_smul' c x := by
simp only [LinearMapClass.map_smul, LinearMap.smul_apply, smul_eq_mul,
RingHom.id_apply]
rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul]
def φAux₂ (u v : P) : spaceTime →ₗ[ℝ] spaceTime where
toFun x := - (ηLin x (u + v) / (1 + ηLin u v)) • (u + v)
map_add' x y := by
simp only
rw [ηLin.map_add, div_eq_mul_one_div]
rw [show (ηLin x + ηLin y) (↑u + ↑v) = ηLin x (u+v) + ηLin y (u+v) from rfl]
rw [add_mul, neg_add, add_smul, ← div_eq_mul_one_div, ← div_eq_mul_one_div]
map_smul' c x := by
simp only
rw [ηLin.map_smul]
rw [show (c • ηLin x) (↑u + ↑v) = c * ηLin x (u+v) from rfl]
rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
rfl
def φ (u v : P) : spaceTime →ₗ[ℝ] spaceTime := LinearMap.id + φAux₁ u v + φAux₂ u v
lemma φ_u_u_eq_id (u : P) : φ u u = LinearMap.id := by
ext x
simp [φ]
rw [add_assoc]
rw [@add_right_eq_self]
rw [@add_eq_zero_iff_eq_neg]
rw [φAux₁, φAux₂]
simp only [LinearMap.coe_mk, AddHom.coe_mk, map_add, smul_add, neg_smul, neg_add_rev, neg_neg]
rw [← add_smul]
apply congr
apply congrArg
repeat rw [u.2.2]
field_simp
ring
rfl
def φMat (u v : P) : Matrix (Fin 4) (Fin 4) ℝ := LinearMap.toMatrix stdBasis stdBasis (φ u v)
lemma φMat_mulVec (u v : P) (x : spaceTime) : (φMat u v).mulVec x = φ u v x :=
LinearMap.toMatrix_mulVec_repr stdBasis stdBasis (φ u v) x
lemma φMat_element (u v : P) (i j : Fin 4) : (φMat u v) i j =
η i i * (ηLin (stdBasis i) (stdBasis j) + 2 * ηLin (stdBasis j) u * ηLin (stdBasis i) v -
ηLin (stdBasis i) (u + v) * ηLin (stdBasis j) (u + v) / (1 + ηLin u v)) := by
rw [ηLin_matrix_stdBasis' j i (φMat u v), φMat_mulVec]
simp only [φ, φAux₁, φAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_apply,
LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, smul_eq_mul, map_neg,
mul_eq_mul_left_iff]
apply Or.inl
ring
lemma φMat_continuous (u : P) : Continuous (φMat u) := by
refine continuous_matrix ?_
intro i j
simp only [φMat_element]
refine Continuous.comp' (continuous_mul_left (η i i)) ?hf
refine Continuous.sub ?_ ?_
refine Continuous.comp' (continuous_add_left ((ηLin (stdBasis i)) (stdBasis j))) ?_
refine Continuous.comp' (continuous_mul_left (2 * (ηLin (stdBasis j)) ↑u)) ?_
exact η_P_continuous _
refine Continuous.mul ?_ ?_
refine Continuous.mul ?_ ?_
simp only [(ηLin _).map_add]
refine Continuous.comp' ?_ ?_
exact continuous_add_left ((ηLin (stdBasis i)) ↑u)
exact η_P_continuous _
simp only [(ηLin _).map_add]
refine Continuous.comp' ?_ ?_
exact continuous_add_left _
exact η_P_continuous _
refine Continuous.inv₀ ?_ ?_
refine Continuous.comp' (continuous_add_left 1) ?_
exact η_P_continuous _
exact fun x => one_plus_η_P_P u x
lemma φMat_in_lorentz (u v : P) (x y : spaceTime) :
ηLin ((φMat u v).mulVec x) ((φMat u v).mulVec y) = ηLin x y := by
rw [φMat_mulVec, φMat_mulVec, φ, φAux₁, φAux₂]
have h1 : (1 + (ηLin ↑u) ↑v) ≠ 0 := one_plus_η_P_P u v
simp only [map_add, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_coe,
id_eq, LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul, map_neg, LinearMap.smul_apply,
smul_eq_mul, LinearMap.neg_apply]
field_simp
simp only [v.2.2, mul_one, u.2.2]
rw [ηLin_symm v u, ηLin_symm u y, ηLin_symm v y]
ring
def φLor (u v : P) : lorentzGroup :=
preserveηLinLorentzLift (φMat_in_lorentz u v)
lemma φLor_continuous (u : P) : Continuous (φLor u) := by
refine Continuous.subtype_mk ?_ fun x => (preserveηLinLorentzLift (φMat_in_lorentz u x)).2
refine Units.continuous_iff.mpr (And.intro ?_ ?_)
exact φMat_continuous u
change Continuous fun x => (η * (φMat u x).transpose * η)
refine Continuous.matrix_mul ?_ continuous_const
refine Continuous.matrix_mul continuous_const ?_
exact Continuous.matrix_transpose (φMat_continuous u)
lemma φLor_joined_to_identity (u v : P) : Joined 1 (φLor u v) := by
obtain ⟨f, _⟩ := P_path_connected.joinedIn u trivial v trivial
use ContinuousMap.comp ⟨φLor u, φLor_continuous u⟩ f
· simp only [ContinuousMap.toFun_eq_coe, ContinuousMap.comp_apply, ContinuousMap.coe_coe,
Path.source, ContinuousMap.coe_mk]
rw [@Subtype.ext_iff, φLor, preserveηLinLorentzLift]
refine Units.val_eq_one.mp ?_
simp [preserveηLinGLnLift, φMat, φ_u_u_eq_id u ]
· simp
end restrictedLorentzGroup
end spaceTime
end

229
HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
View file

@ -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.FourVelocity
import HepLean.SpaceTime.LorentzGroup.Proper
import Mathlib.GroupTheory.SpecificGroups.KleinFour
/-!
@ -11,6 +12,10 @@ import Mathlib.GroupTheory.SpecificGroups.KleinFour
We define the give a series of lemmas related to the orthochronous property of lorentz
matrices.
## TODO
- Prove topological properties.
-/
@ -24,100 +29,164 @@ open Complex
open ComplexConjugate
namespace lorentzGroup
open PreFourVelocity
/-- 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
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)))
/-- The first column of a lorentz matrix as a `PreFourVelocity`. -/
@[simp]
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
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
simp only [η, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
vecCons_const, one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two,
Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00
rw [← h00]
ring⟩
def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0
lemma IsOrthochronous_iff_transpose (Λ : lorentzGroup) :
IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by
simp [IsOrthochronous]
simp [transpose]
lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
IsOrthochronous Λ ↔ IsFourVelocity (fstCol Λ) := by
simp [IsOrthochronous, IsFourVelocity]
rw [stdBasis_mulVec]
def mapZeroZeroComp : C(lorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0, by
refine Continuous.matrix_elem ?_ 0 0
refine Continuous.comp' Units.continuous_val continuous_subtype_val⟩
def stepFunction : ℝ → ℝ := fun t =>
if t ≤ -1 then -1 else
if 1 ≤ t then 1 else t
lemma stepFunction_continuous : Continuous stepFunction := by
apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_const continuous_id)
<;> intro a ha
rw [@Set.Iic_def, @frontier_Iic, @Set.mem_singleton_iff] at ha
rw [ha]
simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte]
have h1 : ¬ (1 : ℝ) ≤ 0 := by simp
rw [if_neg h1]
rw [Set.Ici_def, @frontier_Ici, @Set.mem_singleton_iff] at ha
simp [ha]
def orthchroMapReal : C(lorentzGroup, ℝ) := ContinuousMap.comp
⟨stepFunction, stepFunction_continuous⟩ mapZeroZeroComp
lemma orthchroMapReal_on_IsOrthochronous {Λ : lorentzGroup} (h : IsOrthochronous Λ) :
orthchroMapReal Λ = 1 := by
rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h
simp only [IsFourVelocity] at h
rw [zero_nonneg_iff] at h
simp [stdBasis_mulVec] at h
have h1 : ¬ Λ.1 0 0 ≤ (-1 : ℝ) := by linarith
change stepFunction (Λ.1 0 0) = 1
rw [stepFunction, if_neg h1, if_pos h]
lemma orthchroMapReal_on_not_IsOrthochronous {Λ : lorentzGroup} (h : ¬ IsOrthochronous Λ) :
orthchroMapReal Λ = - 1 := by
rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h
rw [not_IsFourVelocity_iff, zero_nonpos_iff] at h
simp only [fstCol, Fin.isValue, stdBasis_mulVec] at h
change stepFunction (Λ.1 0 0) = - 1
rw [stepFunction, if_pos h]
lemma orthchroMapReal_minus_one_or_one (Λ : lorentzGroup) :
orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := by
by_cases h : IsOrthochronous Λ
apply Or.inr $ orthchroMapReal_on_IsOrthochronous h
apply Or.inl $ orthchroMapReal_on_not_IsOrthochronous h
local notation "ℤ₂" => Multiplicative (ZMod 2)
instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
def orthchroMap : C(lorentzGroup, ℤ₂) :=
ContinuousMap.comp coeForℤ₂ {
toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
continuous_toFun := Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _}
instance : DiscreteTopology ℤ₂ := by
exact forall_open_iff_discrete.mp fun _ => trivial
lemma orthchroMap_IsOrthochronous {Λ : lorentzGroup} (h : IsOrthochronous Λ) :
orthchroMap Λ = 1 := by
simp [orthchroMap, orthchroMapReal_on_IsOrthochronous h]
instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk
lemma orthchroMap_not_IsOrthochronous {Λ : lorentzGroup} (h : ¬ IsOrthochronous Λ) :
orthchroMap Λ = Additive.toMul (1 : ZMod 2) := by
simp [orthchroMap, orthchroMapReal_on_not_IsOrthochronous h]
rfl
/-- A continuous function from `({-1, 1} : Set ℝ)` to `ℤ₂`. -/
@[simps!]
def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where
toFun x := if x = ⟨1, by simp⟩ then (Additive.toMul 0) else (Additive.toMul (1 : ZMod 2))
continuous_toFun := by
haveI : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite
exact continuous_of_discreteTopology
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]
ring
/-- The continuous map taking a lorentz matrix to its determinant. -/
def detContinuous : C(lorentzGroup, ℤ₂) :=
ContinuousMap.comp coeForℤ₂ {
toFun := fun Λ => ⟨Λ.1.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}
lemma mul_othchron_of_othchron_othchron {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
(h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
rw [IsOrthochronous_iff_transpose] at h
rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
rw [IsOrthochronous, zero_zero_mul]
exact euclid_norm_IsFourVelocity_IsFourVelocity h h'
lemma detContinuous_eq_iff_det_eq (Λ Λ' : lorentzGroup) :
detContinuous Λ = detContinuous Λ' ↔ Λ.1.1.det = Λ'.1.1.det := by
apply Iff.intro
intro h
simp [detContinuous] at h
cases' det_eq_one_or_neg_one Λ with h1 h1
<;> cases' det_eq_one_or_neg_one Λ' with h2 h2
<;> simp_all [h1, h2, h]
rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h
change (0 : Fin 2) = (1 : Fin 2) at h
simp only [Fin.isValue, zero_ne_one] at h
nth_rewrite 2 [← toMul_zero] at h
rw [@Equiv.apply_eq_iff_eq] at h
change (1 : Fin 2) = (0 : Fin 2) at h
simp [Fin.isValue, zero_ne_one] at h
intro h
simp [detContinuous, h]
lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ)
(h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
rw [IsOrthochronous_iff_transpose] at h
rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
rw [IsOrthochronous, zero_zero_mul]
exact euclid_norm_not_IsFourVelocity_not_IsFourVelocity h h'
lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
(h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
rw [IsOrthochronous_iff_transpose] at h
rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
rw [IsOrthochronous_iff_fstCol_IsFourVelocity, not_IsFourVelocity_iff]
simp [stdBasis_mulVec]
change (Λ * Λ').1 0 0 ≤ _
rw [zero_zero_mul]
exact euclid_norm_IsFourVelocity_not_IsFourVelocity h h'
/-- The representation taking a lorentz matrix to its determinant. -/
@[simps!]
def detRep : lorentzGroup →* ℤ₂ where
toFun Λ := detContinuous Λ
lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ)
(h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
rw [IsOrthochronous_iff_transpose] at h
rw [IsOrthochronous_iff_fstCol_IsFourVelocity] at h h'
rw [IsOrthochronous_iff_fstCol_IsFourVelocity, not_IsFourVelocity_iff]
simp [stdBasis_mulVec]
change (Λ * Λ').1 0 0 ≤ _
rw [zero_zero_mul]
exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
def orthchroRep : lorentzGroup →* ℤ₂ where
toFun := orthchroMap
map_one' := by
simp [detContinuous]
map_mul' := by
intro Λ1 Λ2
simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero,
mul_ite, mul_one, ite_mul, one_mul]
cases' (det_eq_one_or_neg_one Λ1) with h1 h1
<;> cases' (det_eq_one_or_neg_one Λ2) with h2 h2
<;> simp [h1, h2, detContinuous]
have h1 : IsOrthochronous 1 := by simp [IsOrthochronous]
rw [orthchroMap_IsOrthochronous h1]
map_mul' Λ Λ' := by
simp
by_cases h : IsOrthochronous Λ
<;> by_cases h' : IsOrthochronous Λ'
rw [orthchroMap_IsOrthochronous h, orthchroMap_IsOrthochronous h',
orthchroMap_IsOrthochronous (mul_othchron_of_othchron_othchron h h')]
simp
rw [orthchroMap_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_othchron_not_othchron h h')]
simp
rw [orthchroMap_not_IsOrthochronous h, orthchroMap_IsOrthochronous h',
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_not_othchron_othchron h h')]
simp
rw [orthchroMap_not_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
orthchroMap_IsOrthochronous (mul_othchron_of_not_othchron_not_othchron h h')]
simp only [Nat.reduceAdd]
rfl
lemma detRep_continuous : Continuous detRep := detContinuous.2
lemma det_on_connected_component {Λ Λ' : lorentzGroup} (h : Λ' ∈ connectedComponent Λ) :
Λ.1.1.det = Λ'.1.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
simpa [f, detContinuous_eq_iff_det_eq] using
(@IsPreconnected.subsingleton ℤ₂ _ _ _ (isPreconnected_range f.2))
(Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩)
lemma det_of_joined {Λ Λ' : lorentzGroup} (h : Joined Λ Λ') : Λ.1.1.det = Λ'.1.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
instance : DecidablePred IsProper := by
intro Λ
apply Real.decidableEq
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]
end lorentzGroup
end spaceTime