From 885c3ae204f8ff78c8e00dee4f6a0f13fed96b7a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 11 Nov 2024 05:54:31 +0000 Subject: [PATCH 1/3] refactor: Remove hypothesis of FLT three --- .../AnomalyCancellation/SM/NoGrav/One/Lemmas.lean | 9 +++++---- .../SM/NoGrav/One/LinearParameterization.lean | 15 +++++++-------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean index f4f96c7..38c4965 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith import HepLean.AnomalyCancellation.SM.Basic import HepLean.AnomalyCancellation.SM.NoGrav.Basic import HepLean.AnomalyCancellation.SM.NoGrav.One.LinearParameterization +import Mathlib.NumberTheory.FLT.Three /-! # Lemmas for 1 family SM Accs @@ -47,12 +48,12 @@ lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) : simp_all linear_combination 3 * h2 -lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0) - (FLTThree : FermatLastTheoremWith ℚ 3) : +lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0) : accGrav S.val = 0 := by have hE := E_zero_iff_Q_zero.mpr.mt hQ let S' := linearParametersQENeqZero.bijection.symm ⟨S.1.1, And.intro hQ hE⟩ have hC := cubeSol S + have FLTThree := fermatLastTheoremFor_iff_rat.mp fermatLastTheoremThree have hS' := congrArg (fun S => S.val.val) (linearParametersQENeqZero.bijection.right_inv ⟨S.1.1, And.intro hQ hE⟩) change _ = S.val at hS' @@ -60,11 +61,11 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0 exact S'.grav_of_cubic hC FLTThree /-- Any solution to the ACCs without gravity satisfies the gravitational ACC. -/ -theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWith ℚ 3) : +theorem accGravSatisfied {S : (SMNoGrav 1).Sols} : accGrav S.val = 0 := by by_cases hQ : Q S.val (0 : Fin 1)= 0 · exact accGrav_Q_zero hQ - · exact accGrav_Q_neq_zero hQ FLTThree + · exact accGrav_Q_neq_zero hQ end One end SMNoGrav diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean index 536e25b..5b00d24 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean @@ -9,6 +9,7 @@ import Mathlib.Tactic.FieldSimp import Mathlib.Tactic.Linarith import Mathlib.NumberTheory.FLT.Basic import Mathlib.Algebra.QuadraticDiscriminant +import Mathlib.NumberTheory.FLT.Three /-! # Parameterizations for solutions to the linear ACCs for 1 family @@ -279,14 +280,14 @@ lemma cubic (S : linearParametersQENeqZero) : simp_all exact add_eq_zero_iff_eq_neg -lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) - (FLTThree : FermatLastTheoremWith ℚ 3) : +lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) : S.v = 0 ∨ S.w = 0 := by rw [S.cubic] at h have h1 : (-1)^3 = (-1 : ℚ) := by rfl rw [← h1] at h by_contra hn rw [not_or] at hn + have FLTThree := fermatLastTheoremFor_iff_rat.mp fermatLastTheoremThree have h2 := FLTThree S.v S.w (-1) hn.1 hn.2 (Ne.symm (ne_of_beq_false (by rfl))) exact h2 h @@ -326,10 +327,9 @@ lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.v simp_all 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) : +lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) : (S.v = -1 ∧ S.w = 0) ∨ (S.v = 0 ∧ S.w = -1) := by - have h' := cubic_v_or_w_zero S h FLTThree + have h' := cubic_v_or_w_zero S h cases' h' with hx hx · simpa [hx] using cubic_v_zero S h hx · simpa [hx] using cube_w_zero S h hx @@ -345,11 +345,10 @@ lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔ · rw [h] 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) : +lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) : accGrav (bijection S).1.val = 0 := by rw [grav] - have h' := cube_w_v S h FLTThree + have h' := cube_w_v S h cases' h' with h h · rw [h.1, h.2] exact Rat.add_zero (-1) From a8243f4e79f38e9b9ad4f5342bad0fe4ad2c8add Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 11 Nov 2024 07:02:33 +0000 Subject: [PATCH 2/3] feat: Some properties of SL(2,C) and Lorentz --- HepLean/Lorentz/PauliMatrices/AsTensor.lean | 2 +- HepLean/Lorentz/SL2C/Basic.lean | 149 ++++++++++++++++---- 2 files changed, 126 insertions(+), 25 deletions(-) diff --git a/HepLean/Lorentz/PauliMatrices/AsTensor.lean b/HepLean/Lorentz/PauliMatrices/AsTensor.lean index c77bbac..ac0103f 100644 --- a/HepLean/Lorentz/PauliMatrices/AsTensor.lean +++ b/HepLean/Lorentz/PauliMatrices/AsTensor.lean @@ -137,7 +137,7 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ _ = ∑ x, ((∑ i, (SL2C.toLorentzGroup M).1 i x • (complexContrBasis i)) ⊗ₜ[ℂ] ∑ j, leftRightToMatrix.symm ((SL2C.toLorentzGroup M⁻¹).1 x j • (σSA j))) := by refine Finset.sum_congr rfl (fun x _ => ?_) - rw [SL2CRep_ρ_basis, SL2C.toLinearMapSelfAdjointMatrix_σSA] + rw [SL2CRep_ρ_basis, toSelfAdjointMap_σSA] simp only [Action.instMonoidalCategory_tensorObj_V, SL2C.toLorentzGroup_apply_coe, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, map_inv, lorentzGroupIsGroup_inv, AddSubgroup.coe_add, diff --git a/HepLean/Lorentz/SL2C/Basic.lean b/HepLean/Lorentz/SL2C/Basic.lean index 28852e2..15bdbe0 100644 --- a/HepLean/Lorentz/SL2C/Basic.lean +++ b/HepLean/Lorentz/SL2C/Basic.lean @@ -55,7 +55,7 @@ we can define a representation a representation of `SL(2, ℂ)` on spacetime. /-- Given an element `M ∈ SL(2, ℂ)` the linear map from `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` to itself defined by `A ↦ M * A * Mᴴ`. -/ @[simps!] -def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) : +def toSelfAdjointMap (M : SL(2, ℂ)) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) →ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where toFun A := ⟨M.1 * A.1 * Matrix.conjTranspose M, by @@ -70,18 +70,67 @@ def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) : noncomm_ring [selfAdjoint.val_smul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, RingHom.id_apply] -lemma toLinearMapSelfAdjointMatrix_det (M : SL(2, ℂ)) (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : - det ((toLinearMapSelfAdjointMatrix M) A).1 = det A.1 := by - simp only [LinearMap.coe_mk, AddHom.coe_mk, toLinearMapSelfAdjointMatrix, det_mul, +lemma toSelfAdjointMap_apply_det (M : SL(2, ℂ)) (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) : + det ((toSelfAdjointMap M) A).1 = det A.1 := by + simp only [LinearMap.coe_mk, AddHom.coe_mk, toSelfAdjointMap, det_mul, selfAdjoint.mem_iff, det_conjTranspose, det_mul, det_one, RingHom.id_apply] simp only [SpecialLinearGroup.det_coe, one_mul, star_one, mul_one] +lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) : + toSelfAdjointMap M (PauliMatrix.σSAL (Sum.inl 0)) = + ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) • + PauliMatrix.σSAL (Sum.inl 0) + + (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + + (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) • PauliMatrix.σSAL (Sum.inr 0) + + ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im + - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) • PauliMatrix.σSAL (Sum.inr 1) + + ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) • + PauliMatrix.σSAL (Sum.inr 2) := by + simp only [toSelfAdjointMap, PauliMatrix.σSAL, Fin.isValue, Basis.coe_mk, PauliMatrix.σSAL', + PauliMatrix.σ0, LinearMap.coe_mk, AddHom.coe_mk, norm_eq_abs, neg_add_rev, PauliMatrix.σ1, + neg_of, neg_cons, neg_zero, neg_empty, neg_mul, PauliMatrix.σ2, neg_neg, PauliMatrix.σ3] + ext1 + simp only [Fin.isValue, AddSubgroup.coe_add, selfAdjoint.val_smul, smul_of, smul_cons, real_smul, + ofReal_div, ofReal_add, ofReal_pow, ofReal_ofNat, mul_one, smul_zero, smul_empty, smul_neg, + ofReal_neg, ofReal_mul, neg_add_rev, neg_neg, of_add_of, add_cons, head_cons, add_zero, + tail_cons, zero_add, empty_add_empty, ofReal_sub] + conv => lhs; erw [← eta_fin_two 1, mul_one] + conv => lhs; lhs; rw [eta_fin_two M.1] + conv => lhs; rhs; rw [eta_fin_two M.1ᴴ] + simp + rw [mul_conj', mul_conj', mul_conj', mul_conj'] + ext x y + match x, y with + | 0, 0 => + simp + ring_nf + | 0, 1 => + simp + ring_nf + rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)] + simp [- re_add_im] + ring_nf + simp + ring + | 1, 0 => + simp + ring_nf + rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)] + simp [- re_add_im] + ring_nf + simp + ring + | 1, 1 => + simp + ring_nf + + /-- The monoid homomorphisms from `SL(2, ℂ)` to matrices indexed by `Fin 1 ⊕ Fin 3` formed by the action `M A Mᴴ`. -/ def toMatrix : SL(2, ℂ) →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ where - toFun M := LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL (toLinearMapSelfAdjointMatrix M) + toFun M := LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL (toSelfAdjointMap M) map_one' := by - simp only [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_one, one_mul, conjTranspose_one, + simp only [toSelfAdjointMap, SpecialLinearGroup.coe_one, one_mul, conjTranspose_one, mul_one, Subtype.coe_eta] erw [LinearMap.toMatrix_one] map_mul' M N := by @@ -89,14 +138,14 @@ def toMatrix : SL(2, ℂ) →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ wh rw [← LinearMap.toMatrix_mul] apply congrArg ext1 x - simp only [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_mul, conjTranspose_mul, + simp only [toSelfAdjointMap, SpecialLinearGroup.coe_mul, conjTranspose_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply, Subtype.mk.injEq] noncomm_ring open Lorentz in lemma toMatrix_apply_contrMod (M : SL(2, ℂ)) (v : ContrMod 3) : (toMatrix M) *ᵥ v = ContrMod.toSelfAdjoint.symm - ((toLinearMapSelfAdjointMatrix M) (ContrMod.toSelfAdjoint v)) := by + ((toSelfAdjointMap M) (ContrMod.toSelfAdjoint v)) := by simp only [ContrMod.mulVec, toMatrix, MonoidHom.coe_mk, OneHom.coe_mk] obtain ⟨a, ha⟩ := ContrMod.toSelfAdjoint.symm.surjective v subst ha @@ -104,7 +153,7 @@ lemma toMatrix_apply_contrMod (M : SL(2, ℂ)) (v : ContrMod 3) : simp only [ContrMod.toSelfAdjoint, LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.trans_apply] change ContrMod.toFin1dℝEquiv.symm - ((((LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL) (toLinearMapSelfAdjointMatrix M))) + ((((LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL) (toSelfAdjointMap M))) *ᵥ (((Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)) (PauliMatrix.σSAL.repr a)))) = _ apply congrArg erw [LinearMap.toMatrix_mulVec_repr] @@ -117,7 +166,7 @@ lemma toMatrix_mem_lorentzGroup (M : SL(2, ℂ)) : toMatrix M ∈ LorentzGroup 3 rw [Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint] rw [toMatrix_apply_contrMod] rw [LinearEquiv.apply_symm_apply] - rw [toLinearMapSelfAdjointMatrix_det] + rw [toSelfAdjointMap_apply_det] rw [Lorentz.contrContrContractField.same_eq_det_toSelfAdjoint] /-- The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`. -/ @@ -133,28 +182,27 @@ def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where lemma toLorentzGroup_eq_σSAL (M : SL(2, ℂ)) : toLorentzGroup M = LinearMap.toMatrix - PauliMatrix.σSAL PauliMatrix.σSAL (toLinearMapSelfAdjointMatrix M) := by + PauliMatrix.σSAL PauliMatrix.σSAL (toSelfAdjointMap M) := by rfl -lemma toLinearMapSelfAdjointMatrix_basis (i : Fin 1 ⊕ Fin 3) : - toLinearMapSelfAdjointMatrix M (PauliMatrix.σSAL i) = - ∑ j, (toLorentzGroup M).1 j i • - PauliMatrix.σSAL j := by +lemma toSelfAdjointMap_basis (i : Fin 1 ⊕ Fin 3) : + toSelfAdjointMap M (PauliMatrix.σSAL i) = + ∑ j, (toLorentzGroup M).1 j i • PauliMatrix.σSAL j := by rw [toLorentzGroup_eq_σSAL] simp only [LinearMap.toMatrix_apply, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton] nth_rewrite 1 [← (Basis.sum_repr PauliMatrix.σSAL - ((toLinearMapSelfAdjointMatrix M) (PauliMatrix.σSAL i)))] + ((toSelfAdjointMap M) (PauliMatrix.σSAL i)))] rfl -lemma toLinearMapSelfAdjointMatrix_σSA (i : Fin 1 ⊕ Fin 3) : - toLinearMapSelfAdjointMatrix M (PauliMatrix.σSA i) = +lemma toSelfAdjointMap_σSA (i : Fin 1 ⊕ Fin 3) : + toSelfAdjointMap M (PauliMatrix.σSA i) = ∑ j, (toLorentzGroup M⁻¹).1 i j • PauliMatrix.σSA j := by have h1 : (toLorentzGroup M⁻¹).1 = minkowskiMatrix.dual (toLorentzGroup M).1 := by simp simp only [h1] rw [PauliMatrix.σSA_minkowskiMetric_σSAL, _root_.map_smul] - rw [toLinearMapSelfAdjointMatrix_basis] + rw [toSelfAdjointMap_basis] rw [Finset.smul_sum] apply congrArg funext j @@ -163,6 +211,63 @@ lemma toLinearMapSelfAdjointMatrix_σSA (i : Fin 1 ⊕ Fin 3) : apply congrArg exact Eq.symm (minkowskiMatrix.dual_apply_minkowskiMatrix ((toLorentzGroup M).1) i j) +/-- The first column of the Lorentz matrix formed from an element of `SL(2, ℂ)`. -/ +lemma toLorentzGroup_fst_col (M : SL(2, ℂ)) : + (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = fun μ => + match μ with + | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) + | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + + (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) + | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im + - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) + | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) := by + let k : Fin 1 ⊕ Fin 3 → ℝ := fun μ => + match μ with + | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) + | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + + (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) + | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im + - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) + | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) + change (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = k + have h1 : toSelfAdjointMap M (PauliMatrix.σSAL (Sum.inl 0)) = ∑ μ, k μ • PauliMatrix.σSAL μ := by + simp [Fin.sum_univ_three] + rw [toSelfAdjointMap_apply_σSAL_inl] + abel + rw [toSelfAdjointMap_basis] at h1 + have h1x := sub_eq_zero_of_eq h1 + rw [← Finset.sum_sub_distrib] at h1x + funext μ + refine sub_eq_zero.mp ?_ + refine Fintype.linearIndependent_iff.mp PauliMatrix.σSAL.linearIndependent + (fun x => ((toLorentzGroup M).1 x (Sum.inl 0) - k x)) ?_ μ + rw [← h1x] + congr + funext x + exact sub_smul ((toLorentzGroup M).1 x (Sum.inl 0)) (k x) (PauliMatrix.σSAL x) + +/-- The first element of the image of `SL(2, ℂ)` in the Lorentz group. -/ +lemma toLorentzGroup_inl_inl (M : SL(2, ℂ)) : + (toLorentzGroup M).1 (Sum.inl 0) (Sum.inl 0) = + ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) := by + change (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) (Sum.inl 0) = _ + rw [toLorentzGroup_fst_col] + +/-- The image of `SL(2, ℂ)` in the Lorentz group is orthochronous. -/ +lemma toLorentzGroup_isOrthochronous (M : SL(2, ℂ)) : + LorentzGroup.IsOrthochronous (toLorentzGroup M) := by + rw [LorentzGroup.IsOrthochronous] + rw [toLorentzGroup_inl_inl] + apply div_nonneg + · apply add_nonneg + · apply add_nonneg + · apply add_nonneg + · exact sq_nonneg _ + · exact sq_nonneg _ + · exact sq_nonneg _ + · exact sq_nonneg _ + · exact zero_le_two + /-! ## Homomorphism to the restricted Lorentz group @@ -176,13 +281,9 @@ informal_lemma toLorentzGroup_det_one where math :≈ "The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one." deps :≈ [``toLorentzGroup] -informal_lemma toLorentzGroup_inl_inl_nonneg where - math :≈ "The time coponent of the image of `SL(2, ℂ)` in the Lorentz group is non-negative." - deps :≈ [``toLorentzGroup] - informal_lemma toRestrictedLorentzGroup where math :≈ "The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group." - deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_inl_inl_nonneg, + deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_isOrthochronous, ``LorentzGroup.Restricted] /-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/ From 081955c993f8e675b94b15e4d2b4c5c0587b2474 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 11 Nov 2024 07:22:36 +0000 Subject: [PATCH 3/3] refactor: Lint --- .../SM/NoGrav/One/Lemmas.lean | 3 +- HepLean/Lorentz/PauliMatrices/AsTensor.lean | 4 +- HepLean/Lorentz/RealVector/Modules.lean | 2 - HepLean/Lorentz/RealVector/NormOne.lean | 14 +++---- HepLean/Lorentz/SL2C/Basic.lean | 37 ++++++++++++------- HepLean/Lorentz/Weyl/Two.lean | 9 ++--- 6 files changed, 35 insertions(+), 34 deletions(-) diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean index 38c4965..b17a946 100644 --- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean +++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean @@ -53,12 +53,11 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0 have hE := E_zero_iff_Q_zero.mpr.mt hQ let S' := linearParametersQENeqZero.bijection.symm ⟨S.1.1, And.intro hQ hE⟩ have hC := cubeSol S - have FLTThree := fermatLastTheoremFor_iff_rat.mp fermatLastTheoremThree have hS' := congrArg (fun S => S.val.val) (linearParametersQENeqZero.bijection.right_inv ⟨S.1.1, And.intro hQ hE⟩) change _ = S.val at hS' rw [← hS'] at hC ⊢ - exact S'.grav_of_cubic hC FLTThree + exact S'.grav_of_cubic hC /-- Any solution to the ACCs without gravity satisfies the gravitational ACC. -/ theorem accGravSatisfied {S : (SMNoGrav 1).Sols} : diff --git a/HepLean/Lorentz/PauliMatrices/AsTensor.lean b/HepLean/Lorentz/PauliMatrices/AsTensor.lean index ac0103f..e256f1a 100644 --- a/HepLean/Lorentz/PauliMatrices/AsTensor.lean +++ b/HepLean/Lorentz/PauliMatrices/AsTensor.lean @@ -130,14 +130,14 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ map_sum, map_tmul] symm calc _ = ∑ x, ((complexContr.ρ M) (complexContrBasis x) ⊗ₜ[ℂ] - leftRightToMatrix.symm (SL2C.toLinearMapSelfAdjointMatrix M (σSA x))) := by + leftRightToMatrix.symm (SL2C.toSelfAdjointMap M (σSA x))) := by refine Finset.sum_congr rfl (fun x _ => ?_) rw [← leftRightToMatrix_ρ_symm_selfAdjoint] rfl _ = ∑ x, ((∑ i, (SL2C.toLorentzGroup M).1 i x • (complexContrBasis i)) ⊗ₜ[ℂ] ∑ j, leftRightToMatrix.symm ((SL2C.toLorentzGroup M⁻¹).1 x j • (σSA j))) := by refine Finset.sum_congr rfl (fun x _ => ?_) - rw [SL2CRep_ρ_basis, toSelfAdjointMap_σSA] + rw [SL2CRep_ρ_basis, SL2C.toSelfAdjointMap_σSA] simp only [Action.instMonoidalCategory_tensorObj_V, SL2C.toLorentzGroup_apply_coe, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, map_inv, lorentzGroupIsGroup_inv, AddSubgroup.coe_add, diff --git a/HepLean/Lorentz/RealVector/Modules.lean b/HepLean/Lorentz/RealVector/Modules.lean index 4e15b39..55af355 100644 --- a/HepLean/Lorentz/RealVector/Modules.lean +++ b/HepLean/Lorentz/RealVector/Modules.lean @@ -278,11 +278,9 @@ lemma toSelfAdjoint_symm_basis (i : Fin 1 ⊕ Fin 3) : ## Topology -/ - instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced ContrMod.toFin1dℝEquiv (Pi.topologicalSpace) - lemma toFin1dℝEquiv_isInducing : IsInducing (@ContrMod.toFin1dℝEquiv d) := by exact { eq_induced := rfl } diff --git a/HepLean/Lorentz/RealVector/NormOne.lean b/HepLean/Lorentz/RealVector/NormOne.lean index c95e28b..f8f0f32 100644 --- a/HepLean/Lorentz/RealVector/NormOne.lean +++ b/HepLean/Lorentz/RealVector/NormOne.lean @@ -22,7 +22,7 @@ variable {d : ℕ} /-- The set of Lorentz vectors with norm 1. -/ def NormOne (d : ℕ) : Set (Contr d) := fun v => ⟪v, v⟫ₘ = (1 : ℝ) -noncomputable section +noncomputable section namespace NormOne @@ -68,7 +68,7 @@ lemma _root_.LorentzGroup.inl_inl_mul (Λ Λ' : LorentzGroup d) : (Λ * Λ').1 ( ⟪(LorentzGroup.toNormOne (LorentzGroup.transpose Λ)).1, (Contr d).ρ LorentzGroup.parity (LorentzGroup.toNormOne Λ').1⟫ₘ := by rw [contrContrContractField.right_parity] - simp only [Fin.isValue, lorentzGroupIsGroup_mul_coe, Matrix.mul_apply, Fintype.sum_sum_type, + simp only [Fin.isValue, lorentzGroupIsGroup_mul_coe, Matrix.mul_apply, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, LorentzGroup.transpose, PiLp.inner_apply, Function.comp_apply, RCLike.inner_apply, conj_trivial] @@ -80,7 +80,7 @@ lemma _root_.LorentzGroup.inl_inl_mul (Λ Λ' : LorentzGroup d) : (Λ * Λ').1 ( rw [LorentzGroup.toNormOne_inr, LorentzGroup.toNormOne_inr] rfl -lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2 := by +lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2 := by rw [contrContrContractField.inl_sq_eq, v.2] congr rw [← real_inner_self_eq_norm_sq] @@ -99,14 +99,14 @@ lemma inl_le_neg_one_or_one_le_inl : v.val.val (Sum.inl 0) ≤ -1 ∨ 1 ≤ v.va lemma norm_space_le_abs_inl : ‖v.1.toSpace‖ < |v.val.val (Sum.inl 0)| := by rw [(abs_norm _).symm, ← @sq_lt_sq, inl_sq] - change ‖ContrMod.toSpace v.val‖ ^ 2 < 1 + ‖ContrMod.toSpace v.val‖ ^ 2 + change ‖ContrMod.toSpace v.val‖ ^ 2 < 1 + ‖ContrMod.toSpace v.val‖ ^ 2 exact lt_one_add (‖(v.1).toSpace‖ ^ 2) lemma norm_space_leq_abs_inl : ‖v.1.toSpace‖ ≤ |v.val.val (Sum.inl 0)| := le_of_lt (norm_space_le_abs_inl v) lemma inl_abs_sub_space_norm : - 0 ≤ |v.val.val (Sum.inl 0)| * |w.val.val (Sum.inl 0)| - ‖v.1.toSpace‖ * ‖w.1.toSpace‖ := by + 0 ≤ |v.val.val (Sum.inl 0)| * |w.val.val (Sum.inl 0)| - ‖v.1.toSpace‖ * ‖w.1.toSpace‖ := by apply sub_nonneg.mpr apply mul_le_mul (norm_space_leq_abs_inl v) (norm_space_leq_abs_inl w) ?_ ?_ · exact norm_nonneg _ @@ -148,7 +148,6 @@ lemma mem_iff_parity_mem : v ∈ FuturePointing d ↔ ⟨(Contr d).ρ LorentzGro change _ ↔ 0 < (minkowskiMatrix.mulVec v.val.val) (Sum.inl 0) simp only [Fin.isValue, minkowskiMatrix.mulVec_inl_0] - lemma not_mem_iff_inl_le_zero : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) ≤ 0 := by rw [mem_iff] simp @@ -173,7 +172,7 @@ lemma not_mem_iff_neg : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d := variable (f f' : FuturePointing d) -lemma inl_nonneg : 0 ≤ f.val.val.val (Sum.inl 0):= le_of_lt f.2 +lemma inl_nonneg : 0 ≤ f.val.val.val (Sum.inl 0) := le_of_lt f.2 lemma abs_inl : |f.val.val.val (Sum.inl 0)| = f.val.val.val (Sum.inl 0) := abs_of_nonneg (inl_nonneg f) @@ -231,7 +230,6 @@ namespace FuturePointing ## Topology -/ - /-- The `FuturePointing d` which has all space components zero. -/ @[simps!] noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨ContrMod.stdBasis (Sum.inl 0), by diff --git a/HepLean/Lorentz/SL2C/Basic.lean b/HepLean/Lorentz/SL2C/Basic.lean index 15bdbe0..5fc0b9f 100644 --- a/HepLean/Lorentz/SL2C/Basic.lean +++ b/HepLean/Lorentz/SL2C/Basic.lean @@ -83,7 +83,7 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) : (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) • PauliMatrix.σSAL (Sum.inr 0) + ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im - - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) • PauliMatrix.σSAL (Sum.inr 1) + - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) • PauliMatrix.σSAL (Sum.inr 1) + ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) • PauliMatrix.σSAL (Sum.inr 2) := by simp only [toSelfAdjointMap, PauliMatrix.σSAL, Fin.isValue, Basis.coe_mk, PauliMatrix.σSAL', @@ -97,34 +97,43 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) : conv => lhs; erw [← eta_fin_two 1, mul_one] conv => lhs; lhs; rw [eta_fin_two M.1] conv => lhs; rhs; rw [eta_fin_two M.1ᴴ] - simp + simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def, cons_mul, Nat.succ_eq_add_one, + Nat.reduceAdd, vecMul_cons, head_cons, smul_cons, smul_eq_mul, smul_empty, tail_cons, + empty_vecMul, add_zero, add_cons, empty_add_empty, empty_mul, Equiv.symm_apply_apply, + EmbeddingLike.apply_eq_iff_eq] rw [mul_conj', mul_conj', mul_conj', mul_conj'] ext x y match x, y with | 0, 0 => - simp + simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_zero, empty_val', cons_val_fin_one] ring_nf | 0, 1 => - simp + simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_one, head_cons, empty_val', + cons_val_fin_one, cons_val_zero] ring_nf rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)] - simp [- re_add_im] + simp only [Fin.isValue, map_add, conj_ofReal, _root_.map_mul, conj_I, mul_neg, add_re, + ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self, add_zero, add_im, + mul_im, zero_add] ring_nf - simp + simp only [Fin.isValue, I_sq, mul_neg, mul_one, neg_mul, neg_neg, one_mul, sub_neg_eq_add] ring | 1, 0 => - simp + simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_zero, empty_val', cons_val_fin_one, + cons_val_one, head_fin_const] ring_nf rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)] - simp [- re_add_im] + simp only [Fin.isValue, map_add, conj_ofReal, _root_.map_mul, conj_I, mul_neg, add_re, + ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self, add_zero, add_im, + mul_im, zero_add] ring_nf - simp + simp only [Fin.isValue, I_sq, mul_neg, mul_one, neg_mul, neg_neg, one_mul, sub_neg_eq_add] ring | 1, 1 => - simp + simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_one, head_cons, empty_val', + cons_val_fin_one, head_fin_const] ring_nf - /-- The monoid homomorphisms from `SL(2, ℂ)` to matrices indexed by `Fin 1 ⊕ Fin 3` formed by the action `M A Mᴴ`. -/ def toMatrix : SL(2, ℂ) →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ where @@ -216,15 +225,15 @@ lemma toLorentzGroup_fst_col (M : SL(2, ℂ)) : (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = fun μ => match μ with | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) - | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + + | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) := by - let k : Fin 1 ⊕ Fin 3 → ℝ := fun μ => + let k : Fin 1 ⊕ Fin 3 → ℝ := fun μ => match μ with | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) - | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + + | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im + (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) diff --git a/HepLean/Lorentz/Weyl/Two.lean b/HepLean/Lorentz/Weyl/Two.lean index 9c04010..b6ee63e 100644 --- a/HepLean/Lorentz/Weyl/Two.lean +++ b/HepLean/Lorentz/Weyl/Two.lean @@ -718,12 +718,10 @@ open Lorentz lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ) (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) : TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M) (altLeftAltRightToMatrix.symm v) = - altLeftAltRightToMatrix.symm - (SL2C.toLinearMapSelfAdjointMatrix (M.transpose⁻¹) ⟨v, hv⟩) := by + altLeftAltRightToMatrix.symm (SL2C.toSelfAdjointMap (M.transpose⁻¹) ⟨v, hv⟩) := by rw [altLeftAltRightToMatrix_ρ_symm] apply congrArg - simp only [MonoidHom.coe_mk, OneHom.coe_mk, - SL2C.toLinearMapSelfAdjointMatrix_apply_coe, SpecialLinearGroup.coe_inv, + simp only [SL2C.toSelfAdjointMap_apply_coe, SpecialLinearGroup.coe_inv, SpecialLinearGroup.coe_transpose] congr · rw [SL2C.inverse_coe] @@ -737,8 +735,7 @@ lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) lemma leftRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ) (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) : TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M) (leftRightToMatrix.symm v) = - leftRightToMatrix.symm - (SL2C.toLinearMapSelfAdjointMatrix M ⟨v, hv⟩) := by + leftRightToMatrix.symm (SL2C.toSelfAdjointMap M ⟨v, hv⟩) := by rw [leftRightToMatrix_ρ_symm] rfl