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-11-09 18:12:05 +00:00
parent e963be5ef8
commit d058f41689
11 changed files with 38 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/Lorentz/ComplexVector/Basic.lean
View file

@ -138,7 +138,7 @@ lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
change _ = ContrMod.toFin1dℝ ((SL2C.toLorentzGroup M) *ᵥ v)
simp only [SL2C.toLorentzGroup_apply_coe, ContrMod.mulVec_toFin1dℝ]
/-! TODO: Rename.-/
/-! TODO: Rename. -/
lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
(complexContr.ρ M) (complexContrBasis i) =
∑ j, (SL2C.toLorentzGroup M).1 j i •
@ -150,6 +150,6 @@ lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
simp only [LinearMap.map_smulₛₗ, ofRealHom_eq_coe, coe_smul]
rw [complexContrBasis_of_real]
/-! TODO: Include relation to real Lorentz vectors.-/
/-! TODO: Include relation to real Lorentz vectors. -/
end Lorentz
end

3
HepLean/Lorentz/Group/Basic.lean
View file

@ -85,7 +85,6 @@ lemma dual_mem (h : Λ ∈ LorentzGroup d) : dual Λ ∈ LorentzGroup d := by
rw [mem_iff_dual_mul_self, dual_dual]
exact mem_iff_self_mul_dual.mp h
end LorentzGroup
/-!
@ -187,7 +186,7 @@ lemma comm_minkowskiMatrix : Λ.1 * minkowskiMatrix = minkowskiMatrix * (transpo
rw [h1]
simp
lemma minkowskiMatrix_comm : minkowskiMatrix * Λ.1 = (transpose Λ⁻¹).1 * minkowskiMatrix := by
lemma minkowskiMatrix_comm : minkowskiMatrix * Λ.1 = (transpose Λ⁻¹).1 * minkowskiMatrix := by
conv_rhs => rw [← @transpose_mul_minkowskiMatrix_mul_self d Λ]
rw [← transpose_inv, coe_inv, transpose_val]
rw [← mul_assoc, ← mul_assoc]

28
HepLean/Lorentz/Group/Boosts.lean
View file

@ -39,7 +39,7 @@ def genBoostAux₁ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d
map_add' x y := by
simp [map_add, LinearMap.add_apply, tmul_add, add_tmul, mul_add, add_smul]
map_smul' c x := by
simp only [ Action.instMonoidalCategory_tensorObj_V,
simp only [Action.instMonoidalCategory_tensorObj_V,
Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
smul_tmul, tmul_smul, map_smul, smul_eq_mul, RingHom.id_apply]
@ -74,7 +74,7 @@ lemma genBoostAux₂_self (u : FuturePointing d) : genBoostAux₂ u u = - genBoo
congr 1
rw [u.1.2]
conv => lhs; lhs; rhs; rhs; change 1
rw [show 1 + (1 : ℝ) = (2 : ℝ ) by ring]
rw [show 1 + (1 : ℝ) = (2 : ℝ) by ring]
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
IsUnit.div_mul_cancel]
rw [← (two_smul ℝ u.val.val)]
@ -137,15 +137,15 @@ lemma toMatrix_mulVec (u v : FuturePointing d) (x : Contr d) :
open minkowskiMatrix in
@[simp]
lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
(toMatrix u v) μ ν = η μ μ * (toField d ⟪ContrMod.stdBasis μ, ContrMod.stdBasis ν⟫ₘ + 2 *
toField d ⟪ContrMod.stdBasis ν, u.val.val⟫ₘ * toField d ⟪ContrMod.stdBasis μ, v.val.val⟫ₘ
- toField d ⟪ContrMod.stdBasis μ, u.val.val + v.val.val⟫ₘ *
toField d ⟪ContrMod.stdBasis ν, u.val.val + v.val.val⟫ₘ /
(1 + toField d ⟪u.val.val, v.val.val⟫ₘ)) := by
(toMatrix u v) μ ν = η μ μ * (⟪ContrMod.stdBasis μ, ContrMod.stdBasis ν⟫ₘ + 2 *
⟪ContrMod.stdBasis ν, u.val.val⟫ₘ * ⟪ContrMod.stdBasis μ, v.val.val⟫ₘ
- ⟪ContrMod.stdBasis μ, u.val.val + v.val.val⟫ₘ *
⟪ContrMod.stdBasis ν, u.val.val + v.val.val⟫ₘ /
(1 + ⟪u.val.val, v.val.val⟫ₘ)) := by
rw [contrContrContractField.matrix_apply_stdBasis (Λ := 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, contrContrContractField.basis_left, map_smul, smul_eq_mul, map_neg,
mul_eq_mul_left_iff, toField_apply]
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]
ring_nf
simp only [Pi.add_apply, Action.instMonoidalCategory_tensorObj_V,
Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
@ -186,9 +186,9 @@ lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ Lor
rw [LorentzGroup.mem_iff_invariant]
intro x y
rw [toMatrix_mulVec, toMatrix_mulVec]
have h1 : (((1 + ⟪u.1.1, v.1.1⟫ₘ)) * (1 + ⟪u.1.1, v.1.1⟫ₘ)) •
(contrContrContractField ((genBoost u v) y ⊗ₜ[ℝ] (genBoost u v) x))
= (((1 + ⟪u.1.1, v.1.1⟫ₘ)) * (1 + ⟪u.1.1, v.1.1⟫ₘ)) • ⟪y, x⟫ₘ := by
have h1 : (((1 + ⟪u.1.1, v.1.1⟫ₘ)) * (1 + ⟪u.1.1, v.1.1⟫ₘ)) •
(contrContrContractField ((genBoost u v) y ⊗ₜ[ℝ] (genBoost u v) x))
= (((1 + ⟪u.1.1, v.1.1⟫ₘ)) * (1 + ⟪u.1.1, v.1.1⟫ₘ)) • ⟪y, x⟫ₘ := by
conv_lhs =>
erw [← map_smul]
rw [← smul_smul]
@ -200,7 +200,7 @@ lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ Lor
contrContrContractField.symm u.1.1 x]
simp only [smul_eq_mul]
ring
have hn (a : ℝ ) {b c : ℝ} (h : a ≠ 0) (hab : a * b = a * c ) : b = c := by
have hn (a : ℝ) {b c : ℝ} (h : a ≠ 0) (hab : a * b = a * c) : b = c := by
simp_all only [smul_eq_mul, ne_eq, mul_eq_mul_left_iff, or_false]
refine hn _ ?_ h1
simpa using (FuturePointing.one_add_metric_non_zero u v)

2
HepLean/Lorentz/Group/Orthochronous.lean
View file

@ -86,7 +86,7 @@ lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochron
lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
orthchroMapReal Λ = - 1 := by
rw [not_orthochronous_iff_le_neg_one] at h
change stepFunction (_)= - 1
change stepFunction _ = - 1
rw [stepFunction, if_pos]
exact h

2
HepLean/Lorentz/MinkowskiMatrix.lean
View file

@ -10,7 +10,6 @@ import Mathlib.Algebra.Lie.Classical
# The Minkowski matrix
-/
open Matrix
@ -98,7 +97,6 @@ lemma mulVec_inr_i (v : (Fin 1 ⊕ Fin d) → ℝ) (i : Fin d) :
simp only [mulVec, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal]
simp only [diagonal_dotProduct, Sum.elim_inr, neg_mul, one_mul]
variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
/-- The dual of a matrix with respect to the Minkowski metric. -/

2
HepLean/Lorentz/PauliMatrices/Basic.lean
View file

@ -19,7 +19,7 @@ open Complex
open Matrix
/-- The zeroth Pauli-matrix as a `2 x 2` complex matrix.
That is the matrix `!![1, 0; 0, 1]`. -/
That is the matrix `!![1, 0; 0, 1]`. -/
def σ0 : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, 1]
/-- The first Pauli-matrix as a `2 x 2` complex matrix.

2
HepLean/Lorentz/RealVector/Basic.lean
View file

@ -49,7 +49,7 @@ lemma continuous_contr {T : Type} [TopologicalSpace T] (f : T → Contr d)
exact continuous_induced_rng.mpr h
lemma contr_continuous {T : Type} [TopologicalSpace T] (f : Contr d → T)
(h : Continuous (f ∘ (@ContrMod.toFin1dℝEquiv d).symm)): Continuous f := by
(h : Continuous (f ∘ (@ContrMod.toFin1dℝEquiv d).symm)) : Continuous f := by
let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
toFin1dℝEquiv_isInducing
rw [← Homeomorph.comp_continuous_iff' x.symm]

30
HepLean/Lorentz/RealVector/Contraction.lean
View file

@ -78,7 +78,7 @@ def coModContrModBi (d : ℕ) : CoMod d →ₗ[ℝ] ContrMod d →ₗ[ℝ] ℝ w
def contrCoContract : Contr d ⊗ Co d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) where
hom := TensorProduct.lift (contrModCoModBi d)
comm M := TensorProduct.ext' fun ψ φ => by
change (M.1 *ᵥ ψ.toFin1dℝ) ⬝ᵥ ((LorentzGroup.transpose M⁻¹).1 *ᵥ φ.toFin1dℝ) = _
change (M.1 *ᵥ ψ.toFin1dℝ) ⬝ᵥ ((LorentzGroup.transpose M⁻¹).1 *ᵥ φ.toFin1dℝ) = _
rw [dotProduct_mulVec, LorentzGroup.transpose_val,
vecMul_transpose, mulVec_mulVec, LorentzGroup.coe_inv, inv_mul_of_invertible M.1]
simp only [one_mulVec, CategoryTheory.Equivalence.symm_inverse,
@ -101,7 +101,7 @@ lemma contrCoContract_hom_tmul (ψ : Contr d) (φ : Co d) : ⟪ψ, φ⟫ₘ = ψ
def coContrContract : Co d ⊗ Contr d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)) where
hom := TensorProduct.lift (coModContrModBi d)
comm M := TensorProduct.ext' fun ψ φ => by
change ((LorentzGroup.transpose M⁻¹).1 *ᵥ ψ.toFin1dℝ) ⬝ᵥ (M.1 *ᵥ φ.toFin1dℝ) = _
change ((LorentzGroup.transpose M⁻¹).1 *ᵥ ψ.toFin1dℝ) ⬝ᵥ (M.1 *ᵥ φ.toFin1dℝ) = _
rw [dotProduct_mulVec, LorentzGroup.transpose_val, mulVec_transpose, vecMul_vecMul,
LorentzGroup.coe_inv, inv_mul_of_invertible M.1]
simp only [vecMul_one, CategoryTheory.Equivalence.symm_inverse,
@ -143,7 +143,7 @@ def contrContrContract : Contr d ⊗ Contr d ⟶ 𝟙_ (Rep ℝ (LorentzGroup d)
/-- The linear map from Contr d ⊗ Contr d to ℝ induced by the homomorphism
`Contr.toCo` and the contraction `contrCoContract`. -/
def contrContrContractField : (Contr d).V ⊗[ℝ] (Contr d).V →ₗ[ℝ] ℝ :=
def contrContrContractField : (Contr d).V ⊗[ℝ] (Contr d).V →ₗ[ℝ] ℝ :=
contrContrContract.hom
/-- Notation for `contrContrContractField` acting on a tmul. -/
@ -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,
@ -244,7 +244,7 @@ lemma dual_mulVec_right : ⟪x, dual Λ *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ :=
lemma dual_mulVec_left : ⟪dual Λ *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by
rw [symm, dual_mulVec_right, symm]
lemma right_parity : ⟪x, (Contr d).ρ LorentzGroup.parity y⟫ₘ = ∑ i, x.val i * y.val i := by
lemma right_parity : ⟪x, (Contr d).ρ LorentzGroup.parity y⟫ₘ = ∑ i, x.val i * y.val i := by
rw [as_sum]
simp only [Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, Fintype.sum_sum_type,
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
@ -258,7 +258,7 @@ lemma right_parity : ⟪x, (Contr d).ρ LorentzGroup.parity y⟫ₘ = ∑ i, x.
exact mul_eq_mul_left_iff.mp rfl
· congr
funext i
change - (x.val (Sum.inr i) * ((η *ᵥ y.toFin1dℝ) (Sum.inr i))) = _
change - (x.val (Sum.inr i) * ((η *ᵥ y.toFin1dℝ) (Sum.inr i))) = _
simp only [mulVec_inr_i, mul_neg, neg_neg, mul_eq_mul_left_iff]
exact mul_eq_mul_left_iff.mp rfl
@ -338,7 +338,7 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
rw [ContrMod.mulVec_sub, tmul_sub, sub_tmul, sub_tmul, tmul_sub, sub_tmul, sub_tmul] at hn
simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn
let e : 𝟙_ (Rep ℝ ↑(LorentzGroup d)) ≃ₗ[ℝ] ℝ :=
let e : 𝟙_ (Rep ℝ ↑(LorentzGroup d)) ≃ₗ[ℝ] ℝ :=
LinearEquiv.refl ℝ (CoeSort.coe (𝟙_ (Rep ℝ ↑(LorentzGroup d))))
apply e.injective
have hp' := e.injective.eq_iff.mpr hp
@ -346,7 +346,7 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, map_add, map_sub] at hp' hn'
linear_combination (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn'
linear_combination (norm := ring_nf) (1 / 4) * hp' + (-1/ 4) * hn'
rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x]
simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
@ -373,19 +373,17 @@ lemma le_inl_sq (v : Contr d) : ⟪v, v⟫ₘ ≤ v.val (Sum.inl 0) ^ 2 := by
refine Fintype.sum_nonneg ?hf
exact fun i => pow_two_nonneg (v.val (Sum.inr i))
lemma ge_abs_inner_product (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
lemma ge_abs_inner_product (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
‖⟪v.toSpace, w.toSpace⟫_ℝ‖ ≤ ⟪v, w⟫ₘ := by
rw [as_sum_toSpace, sub_le_sub_iff_left]
exact Real.le_norm_self ⟪v.toSpace, w.toSpace⟫_ℝ
lemma ge_sub_norm (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
lemma ge_sub_norm (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
‖v.toSpace‖ * ‖w.toSpace‖ ≤ ⟪v, w⟫ₘ := by
apply le_trans _ (ge_abs_inner_product v w)
rw [sub_le_sub_iff_left]
exact norm_inner_le_norm v.toSpace w.toSpace
/-!
# The Minkowski metric and the standard basis
@ -413,7 +411,6 @@ lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) :
rw [basis_left, ContrMod.mulVec_toFin1dℝ]
simp [basis_left, mulVec, dotProduct, ContrMod.stdBasis_apply, ContrMod.toFin1dℝ_eq_val]
lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪ContrMod.stdBasis μ, ContrMod.stdBasis ν⟫ₘ = η μ ν := by
trans ⟪ContrMod.stdBasis μ, 1 *ᵥ ContrMod.stdBasis ν⟫ₘ
· rw [ContrMod.one_mulVec]
@ -424,10 +421,9 @@ lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪ContrMod.stdBasis μ, ContrMod.std
· simp only [Action.instMonoidalCategory_tensorUnit_V, ne_eq, h, not_false_eq_true, one_apply_ne,
mul_zero, off_diag_zero]
lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d) :
Λ ν μ = η ν ν * ⟪ ContrMod.stdBasis ν, Λ *ᵥ ContrMod.stdBasis μ⟫ₘ := by
rw [on_basis_mulVec, ← mul_assoc]
Λ ν μ = η ν ν * ⟪ ContrMod.stdBasis ν, Λ *ᵥ ContrMod.stdBasis μ⟫ₘ := by
rw [on_basis_mulVec, ← mul_assoc]
simp [η_apply_mul_η_apply_diag ν]
/-!
@ -437,7 +433,7 @@ lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d) :
-/
lemma same_eq_det_toSelfAdjoint (x : ContrMod 3) :
⟪x, x⟫ₘ = det (ContrMod.toSelfAdjoint x).1 := by
⟪x, x⟫ₘ = det (ContrMod.toSelfAdjoint x).1 := by
rw [ContrMod.toSelfAdjoint_apply_coe]
simp only [Fin.isValue, as_sum_toSpace,
PiLp.inner_apply, Function.comp_apply, RCLike.inner_apply, conj_trivial, Fin.sum_univ_three,

8
HepLean/Lorentz/RealVector/Modules.lean
View file

@ -86,7 +86,6 @@ lemma toFin1dℝ_eq_val (ψ : ContrMod d) : ψ.toFin1dℝ = ψ.val := by rfl
@[simps!]
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) := Basis.ofEquivFun toFin1dℝEquiv
@[simp]
lemma stdBasis_toFin1dℝEquiv_apply_same (μ : Fin 1 ⊕ Fin d) :
toFin1dℝEquiv (stdBasis μ) μ = 1 := by
@ -121,7 +120,7 @@ lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ =
/-- Decomposition of a contrvariant Lorentz vector into the standard basis. -/
lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
apply toFin1dℝEquiv.injective
simp only [map_sum, _root_.map_smul]
simp only [map_sum, _root_.map_smul]
funext μ
rw [Fintype.sum_apply μ fun c => toFin1dℝEquiv v c • toFin1dℝEquiv (stdBasis c)]
change _ = ∑ x : Fin 1 ⊕ Fin d, toFin1dℝEquiv v x • (toFin1dℝEquiv (stdBasis x) μ)
@ -189,7 +188,6 @@ def toSpace (v : ContrMod d) : EuclideanSpace ℝ (Fin d) := v.val ∘ Sum.inr
-/
/-- The representation of the Lorentz group acting on `ContrℝModule d`. -/
def rep : Representation ℝ (LorentzGroup d) (ContrMod d) where
toFun g := Matrix.toLinAlgEquiv stdBasis g
@ -237,7 +235,6 @@ lemma toSelfAdjoint_apply_coe (x : ContrMod 3) : (toSelfAdjoint x).1 =
rw [toSelfAdjoint_apply]
rfl
lemma toSelfAdjoint_stdBasis (i : Fin 1 ⊕ Fin 3) :
toSelfAdjoint (stdBasis i) = PauliMatrix.σSAL i := by
rw [toSelfAdjoint_apply]
@ -352,11 +349,10 @@ lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ =
refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
/-- Decomposition of a covariant Lorentz vector into the standard basis. -/
lemma stdBasis_decomp (v : CoMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
apply toFin1dℝEquiv.injective
simp only [map_sum, _root_.map_smul]
simp only [map_sum, _root_.map_smul]
funext μ
rw [Fintype.sum_apply μ fun c => toFin1dℝEquiv v c • toFin1dℝEquiv (stdBasis c)]
change _ = ∑ x : Fin 1 ⊕ Fin d, toFin1dℝEquiv v x • (toFin1dℝEquiv (stdBasis x) μ)

5
HepLean/Lorentz/SL2C/Basic.lean
View file

@ -103,8 +103,8 @@ lemma toMatrix_apply_contrMod (M : SL(2, ℂ)) (v : ContrMod 3) :
rw [LinearEquiv.apply_symm_apply]
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)))
change ContrMod.toFin1dℝEquiv.symm
((((LinearMap.toMatrix PauliMatrix.σSAL PauliMatrix.σSAL) (toLinearMapSelfAdjointMatrix M)))
*ᵥ (((Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)) (PauliMatrix.σSAL.repr a)))) = _
apply congrArg
erw [LinearMap.toMatrix_mulVec_repr]
@ -131,7 +131,6 @@ def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
ext1
simp only [_root_.map_mul, lorentzGroupIsGroup_mul_coe]
lemma toLorentzGroup_eq_σSAL (M : SL(2, ℂ)) :
toLorentzGroup M = LinearMap.toMatrix
PauliMatrix.σSAL PauliMatrix.σSAL (toLinearMapSelfAdjointMatrix M) := by

2
HepLean/Lorentz/Weyl/Two.lean
View file

@ -722,7 +722,7 @@ lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2)
(SL2C.toLinearMapSelfAdjointMatrix (M.transpose⁻¹) ⟨v, hv⟩) := by
rw [altLeftAltRightToMatrix_ρ_symm]
apply congrArg
simp only [ MonoidHom.coe_mk, OneHom.coe_mk,
simp only [MonoidHom.coe_mk, OneHom.coe_mk,
SL2C.toLinearMapSelfAdjointMatrix_apply_coe, SpecialLinearGroup.coe_inv,
SpecialLinearGroup.coe_transpose]
congr