refactor: Golfing
This commit is contained in:
jstoobysmith
parent
fbda420da9
commit
d7b6cf7246
13 changed files with 73 additions and 117 deletions
|
|
@ -43,19 +43,16 @@ def toSpeciesEquiv : (SMCharges n).charges ≃ (Fin 5 → Fin n → ℚ) :=
|
|||
@[simps!]
|
||||
def toSpecies (i : Fin 5) : (SMCharges n).charges →ₗ[ℚ] (SMSpecies n).charges where
|
||||
toFun S := toSpeciesEquiv S i
|
||||
map_add' _ _ := by aesop
|
||||
map_smul' _ _ := by aesop
|
||||
map_add' _ _ := by rfl
|
||||
map_smul' _ _ := by rfl
|
||||
|
||||
lemma charges_eq_toSpecies_eq (S T : (SMCharges n).charges) :
|
||||
S = T ↔ ∀ i, toSpecies i S = toSpecies i T := by
|
||||
apply Iff.intro
|
||||
intro h
|
||||
rw [h]
|
||||
simp only [forall_const]
|
||||
exact fun a i => congrArg (⇑(toSpecies i)) a
|
||||
intro h
|
||||
apply toSpeciesEquiv.injective
|
||||
funext i
|
||||
exact h i
|
||||
exact (Set.eqOn_univ (toSpeciesEquiv S) (toSpeciesEquiv T)).mp fun ⦃x⦄ a => h x
|
||||
|
||||
lemma toSMSpecies_toSpecies_inv (i : Fin 5) (f : (Fin 5 → Fin n → ℚ) ) :
|
||||
(toSpecies i) (toSpeciesEquiv.symm f) = f i := by
|
||||
|
|
@ -142,8 +139,7 @@ lemma accSU2_ext {S T : (SMCharges n).charges}
|
|||
AddHom.coe_mk]
|
||||
repeat erw [Finset.sum_add_distrib]
|
||||
repeat erw [← Finset.mul_sum]
|
||||
repeat erw [hj]
|
||||
rfl
|
||||
exact Mathlib.Tactic.LinearCombination.add_pf (congrArg (HMul.hMul 3) (hj 0)) (hj 3)
|
||||
|
||||
/-- The `SU(3)` anomaly equations. -/
|
||||
@[simp]
|
||||
|
|
|
|||
|
|
@ -107,7 +107,7 @@ lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
|
|||
rw [h1] at hc
|
||||
simp at hc
|
||||
cases' hc with hc hc
|
||||
have h2 := (add_eq_zero_iff' (by nlinarith) (by nlinarith)).mp hc
|
||||
have h2 := (add_eq_zero_iff' (by nlinarith) (sq_nonneg S.Y)).mp hc
|
||||
simp at h2
|
||||
exact h2.1
|
||||
exact hc
|
||||
|
|
@ -120,8 +120,6 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
|
|||
SMCharges.E S.val (0 : Fin 1)⟩
|
||||
left_inv S := by
|
||||
apply linearParameters.ext
|
||||
simp only [Fin.isValue, toSpecies_apply]
|
||||
repeat erw [speciesVal]
|
||||
rfl
|
||||
repeat erw [speciesVal]
|
||||
simp only [Fin.isValue]
|
||||
|
|
@ -243,7 +241,7 @@ def bijectionLinearParameters :
|
|||
have hvw := S.hvw
|
||||
have hQ := S.hx
|
||||
apply linearParametersQENeqZero.ext
|
||||
simp only [tolinearParametersQNeqZero_x, toLinearParameters_coe_Q']
|
||||
rfl
|
||||
field_simp
|
||||
ring
|
||||
simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
|
||||
|
|
@ -255,7 +253,7 @@ def bijectionLinearParameters :
|
|||
have hQ := S.2.1
|
||||
have hE := S.2.2
|
||||
apply linearParameters.ext
|
||||
simp only [ne_eq, toLinearParameters_coe_Q', tolinearParametersQNeqZero_x]
|
||||
rfl
|
||||
field_simp
|
||||
ring_nf
|
||||
field_simp [hQ, hE]
|
||||
|
|
@ -283,7 +281,7 @@ lemma cubic (S : linearParametersQENeqZero) :
|
|||
ring
|
||||
rw [h1]
|
||||
simp_all
|
||||
rw [add_eq_zero_iff_eq_neg]
|
||||
exact add_eq_zero_iff_eq_neg
|
||||
|
||||
|
||||
lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
|
||||
|
|
@ -294,8 +292,8 @@ lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection
|
|||
rw [← h1] at h
|
||||
by_contra hn
|
||||
simp [not_or] at hn
|
||||
have h2 := FLTThree S.v S.w (-1) hn.1 hn.2 (by simp)
|
||||
simp_all
|
||||
have h2 := FLTThree S.v S.w (-1) hn.1 hn.2 (Ne.symm (ne_of_beq_false (by rfl)))
|
||||
exact h2 h
|
||||
|
||||
lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
|
||||
(hv : S.v = 0 ) : S.w = -1 := by
|
||||
|
|
@ -303,8 +301,7 @@ lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.
|
|||
simp at h
|
||||
have h' : (S.w + 1) * (1 * S.w * S.w + (-1) * S.w + 1) = 0 := by
|
||||
ring_nf
|
||||
rw [add_comm]
|
||||
exact add_eq_zero_iff_eq_neg.mpr h
|
||||
exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))
|
||||
have h'' : (1 * S.w * S.w + (-1) * S.w + 1) ≠ 0 := by
|
||||
refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.w
|
||||
intro s
|
||||
|
|
@ -314,7 +311,7 @@ lemma cubic_v_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.
|
|||
simp [discrim]
|
||||
nlinarith
|
||||
simp_all
|
||||
linear_combination h'
|
||||
exact eq_neg_of_add_eq_zero_left h'
|
||||
|
||||
lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
|
||||
(hw : S.w = 0 ) : S.v = -1 := by
|
||||
|
|
@ -322,8 +319,7 @@ lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.v
|
|||
simp at h
|
||||
have h' : (S.v + 1) * (1 * S.v * S.v + (-1) * S.v + 1) = 0 := by
|
||||
ring_nf
|
||||
rw [add_comm]
|
||||
exact add_eq_zero_iff_eq_neg.mpr h
|
||||
exact add_eq_zero_iff_neg_eq.mpr (id (Eq.symm h))
|
||||
have h'' : (1 * S.v * S.v + (-1) * S.v + 1) ≠ 0 := by
|
||||
refine quadratic_ne_zero_of_discrim_ne_sq ?_ S.v
|
||||
intro s
|
||||
|
|
@ -333,7 +329,7 @@ lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.v
|
|||
simp [discrim]
|
||||
nlinarith
|
||||
simp_all
|
||||
linear_combination h'
|
||||
exact eq_neg_of_add_eq_zero_left h'
|
||||
|
||||
lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
|
||||
(FLTThree : FermatLastTheoremWith ℚ 3) :
|
||||
|
|
@ -356,7 +352,7 @@ lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔
|
|||
linear_combination -1 * h / 6
|
||||
intro h
|
||||
rw [h]
|
||||
ring
|
||||
exact Eq.symm (mul_neg_one (6 * S.x))
|
||||
|
||||
lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
|
||||
(FLTThree : FermatLastTheoremWith ℚ 3) :
|
||||
|
|
@ -365,9 +361,9 @@ lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1
|
|||
have h' := cube_w_v S h FLTThree
|
||||
cases' h' with h h
|
||||
rw [h.1, h.2]
|
||||
simp only [add_zero]
|
||||
exact Rat.add_zero (-1)
|
||||
rw [h.1, h.2]
|
||||
simp
|
||||
exact Rat.zero_add (-1)
|
||||
|
||||
end linearParametersQENeqZero
|
||||
|
||||
|
|
|
|||
|
|
@ -38,19 +38,8 @@ instance : Group (permGroup n) := Pi.group
|
|||
@[simps!]
|
||||
def chargeMap (f : permGroup n) : (SMCharges n).charges →ₗ[ℚ] (SMCharges n).charges where
|
||||
toFun S := toSpeciesEquiv.symm (fun i => toSpecies i S ∘ f i )
|
||||
map_add' S T := by
|
||||
simp only
|
||||
rw [charges_eq_toSpecies_eq]
|
||||
intro i
|
||||
rw [(toSpecies i).map_add]
|
||||
rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
|
||||
rfl
|
||||
map_smul' a S := by
|
||||
simp only
|
||||
rw [charges_eq_toSpecies_eq]
|
||||
intro i
|
||||
rw [(toSpecies i).map_smul, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
|
||||
rfl
|
||||
map_add' _ _ := rfl
|
||||
map_smul' _ _ := rfl
|
||||
|
||||
/-- The representation of `(permGroup n)` acting on the vector space of charges. -/
|
||||
@[simp]
|
||||
|
|
@ -81,10 +70,10 @@ lemma repCharges_toSpecies (f : permGroup n) (S : (SMCharges n).charges) (j : Fi
|
|||
lemma toSpecies_sum_invariant (m : ℕ) (f : permGroup n) (S : (SMCharges n).charges) (j : Fin 5) :
|
||||
∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
|
||||
∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
|
||||
erw [repCharges_toSpecies]
|
||||
change ∑ i : Fin n, ((fun a => a ^ m) ∘ _) (⇑(f⁻¹ _) i) = ∑ i : Fin n, ((fun a => a ^ m) ∘ _) i
|
||||
refine Equiv.Perm.sum_comp _ _ _ ?_
|
||||
simp only [permGroup, Fin.isValue, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ]
|
||||
rw [repCharges_toSpecies]
|
||||
exact Fintype.sum_equiv (f⁻¹ j) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) x)
|
||||
(fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl)
|
||||
|
||||
|
||||
|
||||
lemma accGrav_invariant (f : permGroup n) (S : (SMCharges n).charges) :
|
||||
|
|
@ -116,7 +105,6 @@ lemma accQuad_invariant (f : permGroup n) (S : (SMCharges n).charges) :
|
|||
|
||||
lemma accCube_invariant (f : permGroup n) (S : (SMCharges n).charges) :
|
||||
accCube (repCharges f S) = accCube S :=
|
||||
accCube_ext
|
||||
(by simpa using toSpecies_sum_invariant 3 f S)
|
||||
accCube_ext (fun j => toSpecies_sum_invariant 3 f S j)
|
||||
|
||||
end SM
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ lemma toMatrix_isSelfAdjoint (x : spaceTime) : IsSelfAdjoint x.toMatrix := by
|
|||
intro i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [toMatrix, conj_ofReal]
|
||||
ring
|
||||
rfl
|
||||
|
||||
/-- A self-adjoint matrix formed from a space-time point. -/
|
||||
@[simps!]
|
||||
|
|
@ -69,9 +69,7 @@ noncomputable def spaceTimeToHerm : spaceTime ≃ₗ[ℝ] selfAdjoint (Matrix (F
|
|||
exact conj_eq_iff_re.mp (congrArg (fun M => M 0 0) $ selfAdjoint.mem_iff.mp x.2 )
|
||||
have h01 := congrArg (fun M => M 0 1) $ selfAdjoint.mem_iff.mp x.2
|
||||
simp only [Fin.isValue, star_apply, RCLike.star_def] at h01
|
||||
rw [← h01]
|
||||
rw [RCLike.conj_eq_re_sub_im]
|
||||
simp only [Fin.isValue, RCLike.re_to_complex, RCLike.im_to_complex, RCLike.I_to_complex]
|
||||
rw [← h01, RCLike.conj_eq_re_sub_im]
|
||||
rfl
|
||||
exact conj_eq_iff_re.mp (congrArg (fun M => M 1 1) $ selfAdjoint.mem_iff.mp x.2 )
|
||||
map_add' x y := by
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ lemma stdBasis_mulVec (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
|
|||
simp only [↓reduceIte, mul_one]
|
||||
intro x h
|
||||
rw [stdBasis_apply, if_neg (Ne.symm h)]
|
||||
simp
|
||||
exact CommMonoidWithZero.mul_zero (Λ ν x)
|
||||
|
||||
lemma explicit (x : spaceTime) : x = ![x 0, x 1, x 2, x 3] := by
|
||||
funext i
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ lemma zero_abs_ge_one (v : PreFourVelocity) : 1 ≤ |v.1 0| := by
|
|||
|
||||
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]
|
||||
exact lt_one_add (‖(v.1).space‖ ^ 2)
|
||||
|
||||
lemma zero_abs_ge_norm_space (v : PreFourVelocity) : ‖v.1.space‖ ≤ |v.1 0| :=
|
||||
le_of_lt (zero_abs_gt_norm_space v)
|
||||
|
|
@ -80,8 +80,7 @@ lemma IsFourVelocity_abs_zero {v : PreFourVelocity} (hv : IsFourVelocity v) :
|
|||
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
|
||||
exact fun a => le_of_lt a
|
||||
intro h
|
||||
have h1 := (zero_nonpos_iff v).mp h
|
||||
linarith
|
||||
|
|
@ -91,7 +90,7 @@ lemma not_IsFourVelocity_iff_neg {v : PreFourVelocity} : ¬ IsFourVelocity v ↔
|
|||
rw [not_IsFourVelocity_iff, IsFourVelocity]
|
||||
simp only [Fin.isValue, neg]
|
||||
change _ ↔ 0 ≤ - v.1 0
|
||||
simp
|
||||
exact Iff.symm neg_nonneg
|
||||
|
||||
lemma zero_abs_mul_sub_norm_space (v v' : PreFourVelocity) :
|
||||
0 ≤ |v.1 0| * |v'.1 0| - ‖v.1.space‖ * ‖v'.1.space‖ := by
|
||||
|
|
@ -125,7 +124,7 @@ lemma euclid_norm_not_IsFourVelocity_not_IsFourVelocity {v v' : PreFourVelocity}
|
|||
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]
|
||||
rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, 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]
|
||||
|
|
@ -211,9 +210,9 @@ noncomputable def pathFromZero (u : FourVelocity) : Path zero u where
|
|||
lemma isPathConnected_FourVelocity : IsPathConnected (@Set.univ FourVelocity) := by
|
||||
use zero
|
||||
apply And.intro trivial ?_
|
||||
intro y _
|
||||
intro y a
|
||||
use pathFromZero y
|
||||
simp only [Set.mem_univ, implies_true]
|
||||
exact fun _ => a
|
||||
|
||||
lemma η_pos (u v : FourVelocity) : 0 < ηLin u v := by
|
||||
refine lt_of_lt_of_le ?_ (ηLin_ge_sub_norm u v)
|
||||
|
|
|
|||
|
|
@ -59,9 +59,7 @@ lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 4) (Fin 4) ℝ}
|
|||
simpa [Nat.reduceAdd, reindexLieEquiv_symm, reindexLieEquiv_apply,
|
||||
LieAlgebra.Orthogonal.so', mem_skewAdjointMatricesLieSubalgebra,
|
||||
mem_skewAdjointMatricesSubmodule, IsSkewAdjoint, IsAdjointPair, mul_neg] using h1
|
||||
· change (reindexLieEquiv finSumFinEquiv) _ = _
|
||||
simp only [Nat.reduceAdd, reindexLieEquiv_symm, reindexLieEquiv_apply, reindex_apply,
|
||||
Equiv.symm_symm, submatrix_submatrix, Equiv.self_comp_symm, submatrix_id_id]
|
||||
· exact LieEquiv.apply_symm_apply (reindexLieEquiv finSumFinEquiv) _
|
||||
|
||||
|
||||
lemma mem_iff {A : Matrix (Fin 4) (Fin 4) ℝ} : A ∈ lorentzAlgebra ↔ Aᵀ * η = - η * A :=
|
||||
|
|
|
|||
|
|
@ -139,10 +139,9 @@ instance : Module.Finite ℝ lorentzAlgebra :=
|
|||
/-- The Lorentz algebra is 6-dimensional. -/
|
||||
theorem finrank_eq_six : FiniteDimensional.finrank ℝ lorentzAlgebra = 6 := by
|
||||
have h := Module.mk_finrank_eq_card_basis σBasis
|
||||
simp_all
|
||||
simp [FiniteDimensional.finrank]
|
||||
rw [h]
|
||||
simp only [Cardinal.toNat_ofNat]
|
||||
simp only [finrank_eq_rank, Cardinal.mk_fintype, Fintype.card_fin, Nat.cast_ofNat] at h
|
||||
exact FiniteDimensional.finrank_eq_of_rank_eq h
|
||||
|
||||
|
||||
end lorentzAlgebra
|
||||
|
||||
|
|
|
|||
|
|
@ -48,13 +48,11 @@ variable (Λ : Matrix (Fin 4) (Fin 4) ℝ)
|
|||
lemma iff_on_right : PreservesηLin Λ ↔
|
||||
∀ (x y : spaceTime), ηLin x ((η * Λᵀ * η * Λ) *ᵥ y) = ηLin x y := by
|
||||
apply Iff.intro
|
||||
intro h
|
||||
intro x y
|
||||
intro h x y
|
||||
have h1 := h x y
|
||||
rw [ηLin_mulVec_left, mulVec_mulVec] at h1
|
||||
exact h1
|
||||
intro h
|
||||
intro x y
|
||||
intro h x y
|
||||
rw [ηLin_mulVec_left, mulVec_mulVec]
|
||||
exact h x y
|
||||
|
||||
|
|
@ -62,16 +60,12 @@ lemma iff_matrix : PreservesηLin Λ ↔ η * Λᵀ * η * Λ = 1 := by
|
|||
rw [iff_on_right, η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]
|
||||
· exact fun a x y => Eq.symm (Real.ext_cauchy (congrArg Real.cauchy (a x y)))
|
||||
|
||||
lemma iff_matrix' : PreservesηLin Λ ↔ Λ * (η * Λᵀ * η) = 1 := by
|
||||
rw [iff_matrix]
|
||||
apply Iff.intro
|
||||
intro h
|
||||
exact mul_eq_one_comm.mp h
|
||||
intro h
|
||||
exact mul_eq_one_comm.mp h
|
||||
exact mul_eq_one_comm
|
||||
|
||||
|
||||
lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by
|
||||
apply Iff.intro
|
||||
|
|
@ -80,7 +74,8 @@ lemma iff_transpose : PreservesηLin Λ ↔ PreservesηLin Λᵀ := by
|
|||
rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
|
||||
← mul_assoc, transpose_one] at h1
|
||||
rw [iff_matrix' Λ.transpose, ← h1]
|
||||
repeat rw [← mul_assoc]
|
||||
rw [← mul_assoc, ← mul_assoc]
|
||||
exact Matrix.mul_assoc (Λᵀ * η) Λᵀᵀ η
|
||||
intro h
|
||||
have h1 := congrArg transpose ((iff_matrix Λ.transpose).mp h)
|
||||
rw [transpose_mul, transpose_mul, transpose_mul, η_transpose,
|
||||
|
|
@ -157,7 +152,7 @@ lemma toGL_injective : Function.Injective toGL := by
|
|||
intro A B h
|
||||
apply Subtype.eq
|
||||
rw [@Units.ext_iff] at h
|
||||
simpa using h
|
||||
exact h
|
||||
|
||||
/-- The homomorphism from the Lorentz Group into the monoid of matrices times the opposite of
|
||||
the monoid of matrices. -/
|
||||
|
|
@ -201,21 +196,8 @@ lemma toGL_embedding : Embedding toGL.toFun where
|
|||
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
|
||||
exact exists_exists_and_eq_and
|
||||
|
||||
|
||||
instance : TopologicalGroup 𝓛 := Inducing.topologicalGroup toGL toGL_embedding.toInducing
|
||||
|
||||
|
|
|
|||
|
|
@ -68,6 +68,10 @@ def genBoost (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime :=
|
|||
|
||||
namespace genBoost
|
||||
|
||||
/--
|
||||
This lemma states that for a given four-velocity `u`, the general boost
|
||||
transformation `genBoost u u` is equal to the identity linear map `LinearMap.id`.
|
||||
-/
|
||||
lemma self (u : FourVelocity) : genBoost u u = LinearMap.id := by
|
||||
ext x
|
||||
simp [genBoost]
|
||||
|
|
|
|||
|
|
@ -44,16 +44,13 @@ def fstCol (Λ : lorentzGroup) : PreFourVelocity := ⟨Λ.1 *ᵥ stdBasis 0, by
|
|||
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⟩
|
||||
exact h00⟩
|
||||
|
||||
/-- A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative. -/
|
||||
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.liftGL,
|
||||
transpose_transpose, transpose_apply]
|
||||
IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by rfl
|
||||
|
||||
lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
|
||||
IsOrthochronous Λ ↔ IsFourVelocity (fstCol Λ) := by
|
||||
|
|
@ -61,9 +58,8 @@ lemma IsOrthochronous_iff_fstCol_IsFourVelocity (Λ : lorentzGroup) :
|
|||
rw [stdBasis_mulVec]
|
||||
|
||||
/-- 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' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'⟩
|
||||
def mapZeroZeroComp : C(lorentzGroup, ℝ) := ⟨fun Λ => Λ.1 0 0,
|
||||
Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) 0 0⟩
|
||||
|
||||
/-- An auxillary function used in the definition of `orthchroMapReal`. -/
|
||||
def stepFunction : ℝ → ℝ := fun t =>
|
||||
|
|
@ -77,9 +73,9 @@ lemma stepFunction_continuous : Continuous stepFunction := by
|
|||
rw [ha]
|
||||
simp [neg_lt_self_iff, zero_lt_one, ↓reduceIte]
|
||||
have h1 : ¬ (1 : ℝ) ≤ 0 := by simp
|
||||
rw [if_neg h1]
|
||||
exact Eq.symm (if_neg h1)
|
||||
rw [Set.Ici_def, @frontier_Ici, @Set.mem_singleton_iff] at ha
|
||||
simp [ha]
|
||||
exact id (Eq.symm ha)
|
||||
|
||||
/-- The continuous map from `lorentzGroup` to `ℝ` wh
|
||||
taking Orthochronous elements to `1` and non-orthochronous to `-1`. -/
|
||||
|
|
@ -174,25 +170,22 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬
|
|||
/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
|
||||
def orthchroRep : lorentzGroup →* ℤ₂ where
|
||||
toFun := orthchroMap
|
||||
map_one' := by
|
||||
have h1 : IsOrthochronous 1 := by simp [IsOrthochronous]
|
||||
rw [orthchroMap_IsOrthochronous h1]
|
||||
map_one' := orthchroMap_IsOrthochronous (by simp [IsOrthochronous])
|
||||
map_mul' Λ Λ' := by
|
||||
simp only
|
||||
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 only [mul_one]
|
||||
rfl
|
||||
rw [orthchroMap_IsOrthochronous h, orthchroMap_not_IsOrthochronous h',
|
||||
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_othchron_not_othchron h h')]
|
||||
simp only [Nat.reduceAdd, one_mul]
|
||||
rfl
|
||||
rw [orthchroMap_not_IsOrthochronous h, orthchroMap_IsOrthochronous h',
|
||||
orthchroMap_not_IsOrthochronous (mul_not_othchron_of_not_othchron_othchron h h')]
|
||||
simp only [Nat.reduceAdd, mul_one]
|
||||
rfl
|
||||
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
|
||||
|
||||
end lorentzGroup
|
||||
|
|
|
|||
|
|
@ -41,7 +41,8 @@ instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk
|
|||
/-- 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))
|
||||
toFun x := if x = ⟨1, Set.mem_insert_of_mem (-1) rfl⟩
|
||||
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
|
||||
|
|
@ -118,7 +119,7 @@ instance : DecidablePred IsProper := by
|
|||
apply Real.decidableEq
|
||||
|
||||
lemma IsProper_iff (Λ : lorentzGroup) : IsProper Λ ↔ detRep Λ = 1 := by
|
||||
rw [show 1 = detRep 1 by simp]
|
||||
rw [show 1 = detRep 1 from Eq.symm (MonoidHom.map_one detRep)]
|
||||
rw [detRep_apply, detRep_apply, detContinuous_eq_iff_det_eq]
|
||||
simp only [IsProper, lorentzGroupIsGroup_one_coe, det_one]
|
||||
|
||||
|
|
|
|||
|
|
@ -8,6 +8,7 @@ import Mathlib.Analysis.InnerProductSpace.Adjoint
|
|||
import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
|
||||
import Mathlib.Algebra.Lie.Classical
|
||||
import Mathlib.Algebra.Lie.TensorProduct
|
||||
import Mathlib.Tactic.RewriteSearch
|
||||
/-!
|
||||
# Spacetime Metric
|
||||
|
||||
|
|
@ -56,11 +57,12 @@ lemma η_block : η = Matrix.reindex finSumFinEquiv finSumFinEquiv (
|
|||
rw [η]
|
||||
congr
|
||||
simp [LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
rw [← @fromBlocks_diagonal]
|
||||
rw [← fromBlocks_diagonal]
|
||||
refine fromBlocks_inj.mpr ?_
|
||||
simp only [diagonal_one, true_and]
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;> simp
|
||||
rw [← diagonal_neg]
|
||||
rfl
|
||||
|
||||
lemma η_reindex : (Matrix.reindex finSumFinEquiv finSumFinEquiv).symm η =
|
||||
LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ :=
|
||||
|
|
@ -89,8 +91,7 @@ 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)
|
||||
exact Eq.symm (η_off_diagonal fun a => h (id (Eq.symm a)))
|
||||
|
||||
@[simp]
|
||||
lemma η_transpose : η.transpose = η := by
|
||||
|
|
@ -128,7 +129,7 @@ lemma η_mul (Λ : Matrix (Fin 4) (Fin 4) ℝ) (μ ρ : Fin 4) :
|
|||
|
||||
lemma mul_η (Λ : Matrix (Fin 4) (Fin 4) ℝ) (μ ρ : Fin 4) :
|
||||
[Λ * η]^[μ]_[ρ] = [Λ]^[μ]_[ρ] * [η]^[ρ]_[ρ] := by
|
||||
rw [η_as_diagonal, @mul_diagonal, diagonal_apply_eq ![1, -1, -1, -1] ρ]
|
||||
rw [η_as_diagonal, @mul_diagonal, diagonal_apply_eq ![1, -1, -1, -1] ρ]
|
||||
|
||||
lemma η_mul_self (μ ν : Fin 4) : η^[ν]_[μ] * η_[ν]_[ν] = η_[μ]_[ν] := by
|
||||
fin_cases μ <;> fin_cases ν <;> simp [ηUpDown]
|
||||
|
|
@ -229,9 +230,10 @@ lemma ηLin_η_stdBasis (μ ν : Fin 4) : ηLin (stdBasis μ) (stdBasis ν) = η
|
|||
subst h
|
||||
simp
|
||||
· rw [stdBasis_not_eq, η_off_diagonal h]
|
||||
simp only [mul_zero]
|
||||
exact CommMonoidWithZero.mul_zero η_[μ]_[μ]
|
||||
exact fun a ↦ h (id a.symm)
|
||||
|
||||
set_option maxHeartbeats 0
|
||||
lemma ηLin_mulVec_left (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
|
||||
ηLin (Λ *ᵥ x) y = ηLin x ((η * Λᵀ * η) *ᵥ y) := by
|
||||
simp [ηLin, LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue