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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-09-04 06:36:42 -04:00
parent 158c33e8d3
commit 128e75879e
9 changed files with 20 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
View file

@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
import HepLean.AnomalyCancellation.MSSMNu.Basic
import HepLean.AnomalyCancellation.MSSMNu.Y3
import HepLean.AnomalyCancellation.MSSMNu.B3
import Mathlib.Tactic.LinearCombination'
/-!
# The line through B₃ and Y₃
@ -78,10 +77,9 @@ lemma doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
have h3 := hLin 3
simp only [Fin.isValue, Fin.sum_univ_three, Prod.mk_zero_zero, LinearMap.coe_mk, AddHom.coe_mk,
Prod.mk_one_one] at h1 h2 h3
linear_combination (norm := ring_nf) -(12 * h2) + 9 * h1 + 3 * h3
linear_combination (norm := ring_nf) -(12 * h2) + 9 * h1 + 3 * h3
simp only [Fin.isValue, Prod.mk_zero_zero, Prod.mk_one_one, add_add_sub_cancel, add_neg_cancel]
lemma lineY₃B₃_doublePoint (R : MSSMACC.LinSols) (a b : ℚ) :
cubeTriLin (lineY₃B₃ a b).val (lineY₃B₃ a b).val R.val = 0 := by
change cubeTriLin (a • Y₃.val + b • B₃.val) (a • Y₃.val + b • B₃.val) R.val = 0

1
HepLean/AnomalyCancellation/MSSMNu/Y3.lean
View file

@ -77,5 +77,4 @@ lemma doublePoint_Y₃_Y₃ (R : MSSMACC.LinSols) :
linear_combination (norm := ring_nf) 6 * h3
simp only [Fin.isValue, Prod.mk_zero_zero, Prod.mk_one_one, add_add_sub_cancel, add_neg_cancel]
end MSSMACC

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

@ -203,7 +203,6 @@ def toGL : LorentzGroup d →* GL (Fin 1 ⊕ Fin d) ℝ where
map_mul' _ _ :=
(GeneralLinearGroup.ext_iff _ _).mpr fun _ => congrFun rfl
lemma toGL_injective : Function.Injective (@toGL d) := by
refine fun A B h => Subtype.eq ?_
rw [@Units.ext_iff] at h

5
HepLean/SpaceTime/LorentzGroup/Proper.lean
View file

@ -32,7 +32,6 @@ lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
local notation "ℤ₂" => Multiplicative (ZMod 2)
instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
instance : DiscreteTopology ℤ₂ := by
@ -98,14 +97,14 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
simp only [toMul_zero]
· rw [h2, (detContinuous_eq_zero Λ').mpr h2]
erw [Additive.toMul.apply_eq_iff_eq]
change (0 : Fin 2) = (1 : Fin 2) ↔ _
change (0 : Fin 2) = (1 : Fin 2) ↔ _
simp only [Fin.isValue, zero_ne_one, false_iff]
linarith
· rw [h1, (detContinuous_eq_zero Λ).mpr h1]
cases' det_eq_one_or_neg_one Λ' with h2 h2
· rw [h2, (detContinuous_eq_one Λ').mpr h2]
erw [Additive.toMul.apply_eq_iff_eq]
change (1 : Fin 2) = (0 : Fin 2) ↔ _
change (1 : Fin 2) = (0 : Fin 2) ↔ _
simp only [Fin.isValue, one_ne_zero, false_iff]
linarith
· rw [h2, (detContinuous_eq_zero Λ').mpr h2]

19
HepLean/SpaceTime/LorentzTensor/Basic.lean
View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.LinearAlgebra.DFinsupp
/-!
# Structure of Tensors
@ -54,7 +53,7 @@ def colorRel (μ ν : 𝓒.Color) : Prop := μ = ν ∨ μ = 𝓒.τ ν
instance : Decidable (colorRel 𝓒 μ ν) :=
Or.decidable
omit [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
omit [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
/-- An equivalence relation on colors which is true if the two colors are equal or are duals. -/
lemma colorRel_equivalence : Equivalence 𝓒.colorRel where
refl := by
@ -421,7 +420,7 @@ def elimPureTensor (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) : 𝓣.Pure
| Sum.inl x => p x
| Sum.inr x => q x
omit [Fintype X] [Fintype Y] in
omit [Fintype X] [Fintype Y] in
@[simp]
lemma elimPureTensor_update_right (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY)
(y : Y) (r : 𝓣.ColorModule (cY y)) : 𝓣.elimPureTensor p (Function.update q y r) =
@ -438,7 +437,7 @@ lemma elimPureTensor_update_right (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor
simp_all only
· rfl
omit [Fintype X] [Fintype Y] in
omit [Fintype X] [Fintype Y] in
@[simp]
lemma elimPureTensor_update_left (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY)
(x : X) (r : 𝓣.ColorModule (cX x)) : 𝓣.elimPureTensor (Function.update p x r) q =
@ -499,7 +498,7 @@ lemma inrPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (S
rfl
· rfl
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
@[simp]
lemma inlPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y)
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inr y))) :
@ -592,7 +591,7 @@ def tensoratorEquiv (c : X → 𝓣.Color) (d : Y → 𝓣.Color) :
simp [elimPureTensorMulLin]
rfl)
omit [Fintype X] [Fintype Y] in
omit [Fintype X] [Fintype Y] in
@[simp]
lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) :
(𝓣.tensoratorEquiv cX cY) ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) =
@ -601,7 +600,7 @@ lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor c
lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, PiTensorProduct.lift.tprod]
exact PiTensorProduct.lift.tprod q
omit [Fintype X] [Fintype Y] in
omit [Fintype X] [Fintype Y] in
@[simp]
lemma tensoratorEquiv_symm_tprod (f : 𝓣.PureTensor (Sum.elim cX cY)) :
(𝓣.tensoratorEquiv cX cY).symm ((PiTensorProduct.tprod R) f) =
@ -611,7 +610,7 @@ lemma tensoratorEquiv_symm_tprod (f : 𝓣.PureTensor (Sum.elim cX cY)) :
change (PiTensorProduct.lift 𝓣.domCoprod) ((PiTensorProduct.tprod R) f) = _
simp [domCoprod]
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
@[simp]
lemma tensoratorEquiv_mapIso (e' : Z ≃ Y) (e'' : W ≃ X)
(h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX) :
@ -630,7 +629,7 @@ lemma tensoratorEquiv_mapIso (e' : Z ≃ Y) (e'' : W ≃ X)
| Sum.inl x => rfl
| Sum.inr x => rfl
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
@[simp]
lemma tensoratorEquiv_mapIso_apply (e' : Z ≃ Y) (e'' : W ≃ X)
(h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX)
@ -644,7 +643,7 @@ lemma tensoratorEquiv_mapIso_apply (e' : Z ≃ Y) (e'' : W ≃ X)
· rw [tensoratorEquiv_mapIso]
rfl
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
lemma tensoratorEquiv_mapIso_tmul (e' : Z ≃ Y) (e'' : W ≃ X)
(h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX)
(x : 𝓣.Tensor cW) (y : 𝓣.Tensor cZ) :

4
HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Basic.lean
View file

@ -67,11 +67,11 @@ noncomputable def einsteinTensor (R : Type) [CommSemiring R] (n : ℕ) : TensorS
Fintype.linearCombination_apply, Pi.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero,
Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, lid_tmul, one_smul]
· intro x hi
simp [TensorStructure.contrMidAux, LinearEquiv.refl_toLinearMap,
simp only [TensorStructure.contrMidAux, LinearEquiv.refl_toLinearMap,
TensorStructure.contrLeftAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
assoc_tmul, map_tmul, LinearMap.id_coe, id_eq, assoc_symm_tmul, lift.tmul,
Fintype.linearCombination_apply, Pi.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero,
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, lid_tmul, ite_smul, one_smul, zero_smul]
Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, lid_tmul, ite_smul, one_smul, zero_smul]
rw [if_neg hi]
exact tmul_zero (Fin n → R) (Pi.single x 1)

2
HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
View file

@ -120,7 +120,7 @@ def id (I : Index X) : ℕ := I.2
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
lemma eq_iff_color_eq_and_id_eq (I J : Index X) : I = J ↔ I.toColor = J.toColor ∧ I.id = J.id := by
refine Iff.intro (fun h => Prod.mk.inj_iff.mp h) (fun h => ?_)
refine Iff.intro (fun h => Prod.mk.inj_iff.mp h) (fun h => ?_)
· cases I
cases J
simp [toColor, id] at h

4
HepLean/SpaceTime/LorentzTensor/IndexNotation/ColorIndexList/Append.lean
View file

@ -20,7 +20,7 @@ It is conditional on `AppendCond` being true, which we define.
namespace IndexNotation
namespace ColorIndexList
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color]
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color]
(l l2 : ColorIndexList 𝓒)
open IndexList TensorColor
@ -50,7 +50,7 @@ def append (h : AppendCond l l2) : ColorIndexList 𝓒 where
can be appended to form a `ColorIndexList`. -/
scoped[IndexNotation.ColorIndexList] notation l " ++["h"] " l2 => append l l2 h
omit [DecidableEq 𝓒.Color] in
omit [DecidableEq 𝓒.Color] in
@[simp]
lemma append_toIndexList (h : AppendCond l l2) :
(l ++[h] l2).toIndexList = l.toIndexList ++ l2.toIndexList := rfl

6
HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
View file

@ -107,7 +107,7 @@ lemma dual_eq_of_neq (h : DualMap c₁ c₂) {x : X} (h' : c₁ x ≠ c₂ x) :
simp_all only [ne_eq, false_or]
exact 𝓒.τ_involutive (c₂ x)
omit [Fintype X] [DecidableEq X] in
omit [Fintype X] [DecidableEq X] in
@[simp]
lemma split_dual (h : DualMap c₁ c₂) : c₁.partDual (split c₁ c₂) = c₂ := by
rw [partDual, Equiv.comp_symm_eq]
@ -118,7 +118,7 @@ lemma split_dual (h : DualMap c₁ c₂) : c₁.partDual (split c₁ c₂) = c
| Sum.inr x =>
exact x.2
omit [Fintype X] [DecidableEq X] in
omit [Fintype X] [DecidableEq X] in
@[simp]
lemma split_dual' (h : DualMap c₁ c₂) : c₂.partDual (split c₁ c₂) = c₁ := by
rw [partDual, Equiv.comp_symm_eq]
@ -281,7 +281,7 @@ def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by
rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
apply congrArg
simp
omit [Fintype X] [DecidableEq X]
omit [Fintype X] [DecidableEq X]
@[simp]
lemma dualizeAll_equivariant (g : G) : (𝓣.dualizeAll.toLinearMap) ∘ₗ (@rep R _ G _ 𝓣 _ X cX g)
= 𝓣.rep g ∘ₗ (𝓣.dualizeAll.toLinearMap) := by