From b0c5ed894fa57a6d13402350f780e534fa3fee25 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Sun, 10 Nov 2024 06:57:41 +0000 Subject: [PATCH] refactor: Lint --- HepLean.lean | 1 + HepLean/Lorentz/Group/Basic.lean | 2 -- HepLean/Lorentz/Group/Boosts.lean | 2 +- HepLean/Lorentz/RealVector/Basic.lean | 3 --- HepLean/Lorentz/RealVector/Contraction.lean | 3 +-- HepLean/Lorentz/RealVector/Modules.lean | 8 ++++++++ HepLean/Lorentz/RealVector/NormOne.lean | 6 +++--- HepLean/Lorentz/SL2C/Basic.lean | 2 ++ 8 files changed, 16 insertions(+), 11 deletions(-) diff --git a/HepLean.lean b/HepLean.lean index f45f00b..a8aaa9c 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -95,6 +95,7 @@ import HepLean.Lorentz.PauliMatrices.SelfAdjoint import HepLean.Lorentz.RealVector.Basic import HepLean.Lorentz.RealVector.Contraction import HepLean.Lorentz.RealVector.Modules +import HepLean.Lorentz.RealVector.NormOne import HepLean.Lorentz.SL2C.Basic import HepLean.Lorentz.Weyl.Basic import HepLean.Lorentz.Weyl.Contraction diff --git a/HepLean/Lorentz/Group/Basic.lean b/HepLean/Lorentz/Group/Basic.lean index d2b1017..1ee45f7 100644 --- a/HepLean/Lorentz/Group/Basic.lean +++ b/HepLean/Lorentz/Group/Basic.lean @@ -123,7 +123,6 @@ instance (M : LorentzGroup d) : Invertible M.1 where rw [← coe_inv] exact (mem_iff_self_mul_dual.mp M.2) -@[simp] lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by trans Subtype.val (Λ⁻¹ * Λ) · rw [← coe_inv] @@ -131,7 +130,6 @@ lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by · rw [inv_mul_cancel Λ] rfl -@[simp] lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := by trans Subtype.val (Λ * Λ⁻¹) · rw [← coe_inv] diff --git a/HepLean/Lorentz/Group/Boosts.lean b/HepLean/Lorentz/Group/Boosts.lean index 7f8c407..6e6df8f 100644 --- a/HepLean/Lorentz/Group/Boosts.lean +++ b/HepLean/Lorentz/Group/Boosts.lean @@ -145,7 +145,7 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) : rw [contrContrContractField.matrix_apply_stdBasis (Λ := toMatrix u v) μ ν, toMatrix_mulVec] simp only [genBoost, genBoostAux₁, genBoostAux₂, smul_add, neg_smul, LinearMap.add_apply, LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, contrContrContractField.basis_left, - map_add, map_smul, map_neg, toField_apply, mul_eq_mul_left_iff] + map_add, map_smul, map_neg, mul_eq_mul_left_iff] ring_nf simp only [Pi.add_apply, Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse, diff --git a/HepLean/Lorentz/RealVector/Basic.lean b/HepLean/Lorentz/RealVector/Basic.lean index 862729c..e44fb6a 100644 --- a/HepLean/Lorentz/RealVector/Basic.lean +++ b/HepLean/Lorentz/RealVector/Basic.lean @@ -61,9 +61,6 @@ def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoMod.rep open CategoryTheory.MonoidalCategory -def toField (d : ℕ) : (𝟙_ (Rep ℝ ↑(LorentzGroup d))) →ₗ[ℝ] ℝ := LinearMap.id - -lemma toField_apply {d : ℕ} (a : 𝟙_ (Rep ℝ ↑(LorentzGroup d))) : toField d a = a := rfl /-! ## Isomorphism between contravariant and covariant Lorentz vectors diff --git a/HepLean/Lorentz/RealVector/Contraction.lean b/HepLean/Lorentz/RealVector/Contraction.lean index 3ccec4b..00029df 100644 --- a/HepLean/Lorentz/RealVector/Contraction.lean +++ b/HepLean/Lorentz/RealVector/Contraction.lean @@ -200,7 +200,7 @@ lemma action_tmul (g : LorentzGroup d) : ⟪(Contr d).ρ g x, (Contr d).ρ g y rfl lemma as_sum : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) - - ∑ i, x.val (Sum.inr i) * y.val (Sum.inr i) := by + ∑ i, x.val (Sum.inr i) * y.val (Sum.inr i) := by rw [contrContrContract_hom_tmul] simp only [dotProduct, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Sum.elim_inl, @@ -214,7 +214,6 @@ lemma as_sum_toSpace : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) - rw [as_sum] rfl -@[simp] lemma stdBasis_inl {d : ℕ} : ⟪@ContrMod.stdBasis d (Sum.inl 0), ContrMod.stdBasis (Sum.inl 0)⟫ₘ = (1 : ℝ) := by rw [as_sum] diff --git a/HepLean/Lorentz/RealVector/Modules.lean b/HepLean/Lorentz/RealVector/Modules.lean index 8da6e39..fbd8735 100644 --- a/HepLean/Lorentz/RealVector/Modules.lean +++ b/HepLean/Lorentz/RealVector/Modules.lean @@ -136,9 +136,11 @@ lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis -/ +/-- Multiplication of a matrix with a vector in `ContrMod`. -/ abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : ContrMod d := Matrix.toLinAlgEquiv stdBasis M v +/-- Multiplication of a matrix with a vector in `ContrMod`. -/ scoped[Lorentz] infixr:73 " *ᵥ " => ContrMod.mulVec @[simp] @@ -173,6 +175,8 @@ lemma mulVec_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : (Not the Minkowski norm, but the norm of a vector in `ContrℝModule d`.) -/ +/-- A `NormedAddCommGroup` structure on `ContrMod`. This is not an instance, as we + don't want it to be applied always. -/ def norm : NormedAddCommGroup (ContrMod d) where norm v := ‖v.val‖₊ dist_self x := Pi.normedAddCommGroup.dist_self x.val @@ -180,6 +184,8 @@ def norm : NormedAddCommGroup (ContrMod d) where dist_comm x y := Pi.normedAddCommGroup.dist_comm x.val y.val eq_of_dist_eq_zero {x y} := fun h => ext (MetricSpace.eq_of_dist_eq_zero h) +/-- The underlying space part of a `ContrMod` formed by removing the first element. + A better name for this might be `tail`. -/ def toSpace (v : ContrMod d) : EuclideanSpace ℝ (Fin d) := v.val ∘ Sum.inr /-! @@ -368,9 +374,11 @@ lemma stdBasis_decomp (v : CoMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i : -/ +/-- Multiplication of a matrix with a vector in `CoMod`. -/ abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) : CoMod d := Matrix.toLinAlgEquiv stdBasis M v +/-- Multiplication of a matrix with a vector in `CoMod`. -/ scoped[Lorentz] infixr:73 " *ᵥ " => CoMod.mulVec @[simp] diff --git a/HepLean/Lorentz/RealVector/NormOne.lean b/HepLean/Lorentz/RealVector/NormOne.lean index 4e49c25..c95e28b 100644 --- a/HepLean/Lorentz/RealVector/NormOne.lean +++ b/HepLean/Lorentz/RealVector/NormOne.lean @@ -208,7 +208,7 @@ lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ Fu simp [neg, neg_tmul, tmul_neg] lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) : - ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by + ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg] have h1 := metric_reflect_mem_mem h ((not_mem_iff_neg w).mp hw) apply le_of_le_of_eq h1 ?_ @@ -248,8 +248,8 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur | Sum.inr i => t * u.1.1.toSpace i}, by rw [NormOne.mem_iff, contrContrContractField.as_sum_toSpace] - simp only [ContrMod.toSpace, Function.comp_apply, PiLp.inner_apply, RCLike.inner_apply, map_mul, - conj_trivial] + simp only [ContrMod.toSpace, Function.comp_apply, PiLp.inner_apply, RCLike.inner_apply, + map_mul, conj_trivial] rw [Real.mul_self_sqrt, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply] · simp only [Function.comp_apply, RCLike.inner_apply, conj_trivial] refine Eq.symm (eq_sub_of_add_eq (congrArg (HAdd.hAdd _) ?_)) diff --git a/HepLean/Lorentz/SL2C/Basic.lean b/HepLean/Lorentz/SL2C/Basic.lean index 5a7991e..28852e2 100644 --- a/HepLean/Lorentz/SL2C/Basic.lean +++ b/HepLean/Lorentz/SL2C/Basic.lean @@ -76,6 +76,8 @@ lemma toLinearMapSelfAdjointMatrix_det (M : SL(2, ℂ)) (A : selfAdjoint (Matrix selfAdjoint.mem_iff, det_conjTranspose, det_mul, det_one, RingHom.id_apply] simp only [SpecialLinearGroup.det_coe, one_mul, star_one, mul_one] +/-- 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) map_one' := by