Merge pull request #192 from HEPLean/Weyl
feat: Contraction, metric and unit for Weyl fermions
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
1b050cdf2f
7 changed files with 1202 additions and 179 deletions
|
|
@ -91,7 +91,11 @@ import HepLean.SpaceTime.LorentzVector.NormOne
|
|||
import HepLean.SpaceTime.MinkowskiMetric
|
||||
import HepLean.SpaceTime.SL2C.Basic
|
||||
import HepLean.SpaceTime.WeylFermion.Basic
|
||||
import HepLean.SpaceTime.WeylFermion.Contraction
|
||||
import HepLean.SpaceTime.WeylFermion.Metric
|
||||
import HepLean.SpaceTime.WeylFermion.Modules
|
||||
import HepLean.SpaceTime.WeylFermion.Two
|
||||
import HepLean.SpaceTime.WeylFermion.Unit
|
||||
import HepLean.StandardModel.Basic
|
||||
import HepLean.StandardModel.HiggsBoson.Basic
|
||||
import HepLean.StandardModel.HiggsBoson.GaugeAction
|
||||
|
|
|
|||
|
|
@ -47,6 +47,18 @@ def leftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
|
|||
simp only [LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply, LinearEquiv.apply_symm_apply,
|
||||
mulVec_mulVec]}
|
||||
|
||||
/-- The standard basis on left-handed Weyl fermions. -/
|
||||
def leftBasis : Basis (Fin 2) ℂ leftHanded := Basis.ofEquivFun
|
||||
(Equiv.linearEquiv ℂ LeftHandedModule.toFin2ℂFun)
|
||||
|
||||
@[simp]
|
||||
lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
|
||||
(LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M) i j = M.1 i j := by
|
||||
rw [LinearMap.toMatrix_apply]
|
||||
simp only [leftBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
|
||||
change (M.1 *ᵥ (Pi.single j 1)) i = _
|
||||
simp only [mulVec_single, mul_one]
|
||||
|
||||
/-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
|
||||
M → (M⁻¹)ᵀ. In index notation corresponds to a Weyl fermion with indices ψ^a. -/
|
||||
def altLeftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
|
||||
|
|
@ -70,6 +82,18 @@ def altLeftHanded : Rep ℂ SL(2,ℂ) := Rep.of {
|
|||
rw [Matrix.mul_inv_rev]
|
||||
exact transpose_mul _ _}
|
||||
|
||||
/-- The standard basis on alt-left-handed Weyl fermions. -/
|
||||
def altLeftBasis : Basis (Fin 2) ℂ altLeftHanded := Basis.ofEquivFun
|
||||
(Equiv.linearEquiv ℂ AltLeftHandedModule.toFin2ℂFun)
|
||||
|
||||
@[simp]
|
||||
lemma altLeftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
|
||||
(LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M) i j = (M.1⁻¹)ᵀ i j := by
|
||||
rw [LinearMap.toMatrix_apply]
|
||||
simp only [altLeftBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
|
||||
change ((M.1⁻¹)ᵀ *ᵥ (Pi.single j 1)) i = _
|
||||
simp only [mulVec_single, transpose_apply, mul_one]
|
||||
|
||||
/-- The vector space ℂ^2 carrying the conjugate representation of SL(2,C).
|
||||
In index notation corresponds to a Weyl fermion with indices ψ_{dot a}. -/
|
||||
def rightHanded : Rep ℂ SL(2,ℂ) := Rep.of {
|
||||
|
|
@ -90,6 +114,18 @@ def rightHanded : Rep ℂ SL(2,ℂ) := Rep.of {
|
|||
simp only [SpecialLinearGroup.coe_mul, RCLike.star_def, Matrix.map_mul, LinearMap.coe_mk,
|
||||
AddHom.coe_mk, LinearMap.mul_apply, LinearEquiv.apply_symm_apply, mulVec_mulVec]}
|
||||
|
||||
/-- The standard basis on right-handed Weyl fermions. -/
|
||||
def rightBasis : Basis (Fin 2) ℂ rightHanded := Basis.ofEquivFun
|
||||
(Equiv.linearEquiv ℂ RightHandedModule.toFin2ℂFun)
|
||||
|
||||
@[simp]
|
||||
lemma rightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
|
||||
(LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M) i j = (M.1.map star) i j := by
|
||||
rw [LinearMap.toMatrix_apply]
|
||||
simp only [rightBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
|
||||
change (M.1.map star *ᵥ (Pi.single j 1)) i = _
|
||||
simp only [mulVec_single, transpose_apply, mul_one]
|
||||
|
||||
/-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
|
||||
M → (M⁻¹)^†.
|
||||
In index notation this corresponds to a Weyl fermion with index `ψ^{dot a}`. -/
|
||||
|
|
@ -114,6 +150,19 @@ def altRightHanded : Rep ℂ SL(2,ℂ) := Rep.of {
|
|||
rw [Matrix.mul_inv_rev]
|
||||
exact conjTranspose_mul _ _}
|
||||
|
||||
/-- The standard basis on alt-right-handed Weyl fermions. -/
|
||||
def altRightBasis : Basis (Fin 2) ℂ altRightHanded := Basis.ofEquivFun
|
||||
(Equiv.linearEquiv ℂ AltRightHandedModule.toFin2ℂFun)
|
||||
|
||||
@[simp]
|
||||
lemma altRightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
|
||||
(LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M) i j =
|
||||
((M.1⁻¹).conjTranspose) i j := by
|
||||
rw [LinearMap.toMatrix_apply]
|
||||
simp only [altRightBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
|
||||
change ((M.1⁻¹).conjTranspose *ᵥ (Pi.single j 1)) i = _
|
||||
simp only [mulVec_single, transpose_apply, mul_one]
|
||||
|
||||
/-!
|
||||
|
||||
## Equivalences between Weyl fermion vector spaces.
|
||||
|
|
@ -224,174 +273,6 @@ informal_lemma rightHandedWeylAltEquiv_equivariant where
|
|||
action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
|
||||
deps :≈ [``rightHandedWeylAltEquiv]
|
||||
|
||||
/-!
|
||||
|
||||
## Contraction of Weyl fermions.
|
||||
|
||||
-/
|
||||
open CategoryTheory.MonoidalCategory
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a left-handed Weyl fermion with a
|
||||
alt-left-handed Weyl fermion. -/
|
||||
def leftAltBi : leftHanded →ₗ[ℂ] altLeftHanded →ₗ[ℂ] ℂ where
|
||||
toFun ψ := {
|
||||
toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
|
||||
map_add' := by
|
||||
intro φ φ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r φ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' ψ ψ':= by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
|
||||
rw [add_dotProduct]
|
||||
map_smul' r ψ := by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [smul_dotProduct]
|
||||
rfl
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a alt-left-handed Weyl fermion with a
|
||||
left-handed Weyl fermion. -/
|
||||
def altLeftBi : altLeftHanded →ₗ[ℂ] leftHanded →ₗ[ℂ] ℂ where
|
||||
toFun ψ := {
|
||||
toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
|
||||
map_add' := by
|
||||
intro φ φ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r φ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' ψ ψ':= by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [map_add, add_dotProduct, vec2_dotProduct, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk, LinearMap.add_apply]
|
||||
map_smul' ψ ψ' := by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [_root_.map_smul, smul_dotProduct, vec2_dotProduct, Fin.isValue, smul_eq_mul,
|
||||
LinearMap.coe_mk, AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply]
|
||||
|
||||
/-- The linear map from leftHandedWeyl ⊗ altLeftHandedWeyl to ℂ given by
|
||||
summing over components of leftHandedWeyl and altLeftHandedWeyl in the
|
||||
standard basis (i.e. the dot product).
|
||||
Physically, the contraction of a left-handed Weyl fermion with a alt-left-handed Weyl fermion.
|
||||
In index notation this is ψ_a φ^a. -/
|
||||
def leftAltContraction : leftHanded ⊗ altLeftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift leftAltBi
|
||||
comm M := by
|
||||
apply TensorProduct.ext'
|
||||
intro ψ φ
|
||||
change (M.1 *ᵥ ψ.toFin2ℂ) ⬝ᵥ (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
|
||||
rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
|
||||
simp
|
||||
|
||||
lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
|
||||
leftAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
|
||||
rw [leftAltContraction]
|
||||
erw [TensorProduct.lift.tmul]
|
||||
rfl
|
||||
|
||||
/-- The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
|
||||
summing over components of altLeftHandedWeyl and leftHandedWeyl in the
|
||||
standard basis (i.e. the dot product).
|
||||
Physically, the contraction of a alt-left-handed Weyl fermion with a left-handed Weyl fermion.
|
||||
In index notation this is φ^a ψ_a. -/
|
||||
def altLeftContraction : altLeftHanded ⊗ leftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift altLeftBi
|
||||
comm M := by
|
||||
apply TensorProduct.ext'
|
||||
intro φ ψ
|
||||
change (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) ⬝ᵥ (M.1 *ᵥ ψ.toFin2ℂ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
|
||||
rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
|
||||
simp
|
||||
|
||||
lemma altLeftContraction_hom_tmul (φ : altLeftHanded) (ψ : leftHanded) :
|
||||
altLeftContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
|
||||
rw [altLeftContraction]
|
||||
erw [TensorProduct.lift.tmul]
|
||||
rfl
|
||||
|
||||
lemma leftAltContraction_apply_symm (ψ : leftHanded) (φ : altLeftHanded) :
|
||||
leftAltContraction.hom (ψ ⊗ₜ φ) = altLeftContraction.hom (φ ⊗ₜ ψ) := by
|
||||
rw [altLeftContraction_hom_tmul, leftAltContraction_hom_tmul]
|
||||
exact dotProduct_comm ψ.toFin2ℂ φ.toFin2ℂ
|
||||
|
||||
/-- A manifestation of the statement that `ψ ψ' = - ψ' ψ` where `ψ` and `ψ'`
|
||||
are `leftHandedWeyl`. -/
|
||||
lemma leftAltContraction_apply_leftHandedAltEquiv (ψ ψ' : leftHanded) :
|
||||
leftAltContraction.hom (ψ ⊗ₜ leftHandedAltEquiv.hom.hom ψ') =
|
||||
- leftAltContraction.hom (ψ' ⊗ₜ leftHandedAltEquiv.hom.hom ψ) := by
|
||||
rw [leftAltContraction_hom_tmul, leftAltContraction_hom_tmul,
|
||||
leftHandedAltEquiv_hom_hom_apply, leftHandedAltEquiv_hom_hom_apply]
|
||||
simp only [CategoryTheory.Monoidal.transportStruct_tensorUnit,
|
||||
CategoryTheory.Equivalence.symm_functor, Action.functorCategoryEquivalence_inverse,
|
||||
Action.FunctorCategoryEquivalence.inverse_obj_V, CategoryTheory.Monoidal.tensorUnit_obj,
|
||||
cons_mulVec, cons_dotProduct, zero_mul, one_mul, dotProduct_empty, add_zero, zero_add, neg_mul,
|
||||
empty_mulVec, LinearEquiv.apply_symm_apply, dotProduct_cons, mul_neg, neg_add_rev, neg_neg]
|
||||
ring
|
||||
|
||||
/-- A manifestation of the statement that `φ φ' = - φ' φ` where `φ` and `φ'` are
|
||||
`altLeftHandedWeyl`. -/
|
||||
lemma leftAltContraction_apply_leftHandedAltEquiv_inv (φ φ' : altLeftHanded) :
|
||||
leftAltContraction.hom (leftHandedAltEquiv.inv.hom φ ⊗ₜ φ') =
|
||||
- leftAltContraction.hom (leftHandedAltEquiv.inv.hom φ' ⊗ₜ φ) := by
|
||||
rw [leftAltContraction_hom_tmul, leftAltContraction_hom_tmul,
|
||||
leftHandedAltEquiv_inv_hom_apply, leftHandedAltEquiv_inv_hom_apply]
|
||||
simp only [CategoryTheory.Monoidal.transportStruct_tensorUnit,
|
||||
CategoryTheory.Equivalence.symm_functor, Action.functorCategoryEquivalence_inverse,
|
||||
Action.FunctorCategoryEquivalence.inverse_obj_V, CategoryTheory.Monoidal.tensorUnit_obj,
|
||||
cons_mulVec, cons_dotProduct, zero_mul, neg_mul, one_mul, dotProduct_empty, add_zero, zero_add,
|
||||
empty_mulVec, LinearEquiv.apply_symm_apply, neg_add_rev, neg_neg]
|
||||
ring
|
||||
|
||||
informal_lemma leftAltWeylContraction_symm_altLeftWeylContraction where
|
||||
math :≈ "The linear map altLeftWeylContraction is leftAltWeylContraction composed
|
||||
with the braiding of the tensor product."
|
||||
deps :≈ [``leftAltContraction, ``altLeftContraction]
|
||||
|
||||
informal_lemma altLeftWeylContraction_invariant where
|
||||
math :≈ "The contraction altLeftWeylContraction is invariant with respect to
|
||||
the action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl."
|
||||
deps :≈ [``altLeftContraction]
|
||||
|
||||
informal_definition rightAltWeylContraction where
|
||||
math :≈ "The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
|
||||
summing over components of rightHandedWeyl and altRightHandedWeyl in the
|
||||
standard basis (i.e. the dot product)."
|
||||
physics :≈ "The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
|
||||
In index notation this is ψ_{dot a} φ^{dot a}."
|
||||
deps :≈ [``rightHanded, ``altRightHanded]
|
||||
|
||||
informal_lemma rightAltWeylContraction_invariant where
|
||||
math :≈ "The contraction rightAltWeylContraction is invariant with respect to
|
||||
the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
|
||||
deps :≈ [``rightAltWeylContraction]
|
||||
|
||||
informal_definition altRightWeylContraction where
|
||||
math :≈ "The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
|
||||
summing over components of altRightHandedWeyl and rightHandedWeyl in the
|
||||
standard basis (i.e. the dot product)."
|
||||
physics :≈ "The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
|
||||
In index notation this is φ^{dot a} ψ_{dot a}."
|
||||
deps :≈ [``rightHanded, ``altRightHanded]
|
||||
|
||||
informal_lemma rightAltWeylContraction_symm_altRightWeylContraction where
|
||||
math :≈ "The linear map altRightWeylContraction is rightAltWeylContraction composed
|
||||
with the braiding of the tensor product."
|
||||
deps :≈ [``rightAltWeylContraction, ``altRightWeylContraction]
|
||||
|
||||
informal_lemma altRightWeylContraction_invariant where
|
||||
math :≈ "The contraction altRightWeylContraction is invariant with respect to
|
||||
the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
|
||||
deps :≈ [``altRightWeylContraction]
|
||||
|
||||
end
|
||||
|
||||
end Fermion
|
||||
|
|
|
|||
269
HepLean/SpaceTime/WeylFermion/Contraction.lean
Normal file
269
HepLean/SpaceTime/WeylFermion/Contraction.lean
Normal file
|
|
@ -0,0 +1,269 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.SpaceTime.WeylFermion.Basic
|
||||
/-!
|
||||
|
||||
# Contraction of Weyl fermions
|
||||
|
||||
We define the contraction of Weyl fermions.
|
||||
|
||||
-/
|
||||
|
||||
namespace Fermion
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
|
||||
/-!
|
||||
|
||||
## Contraction of Weyl fermions.
|
||||
|
||||
-/
|
||||
open CategoryTheory.MonoidalCategory
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a left-handed Weyl fermion with a
|
||||
alt-left-handed Weyl fermion. -/
|
||||
def leftAltBi : leftHanded →ₗ[ℂ] altLeftHanded →ₗ[ℂ] ℂ where
|
||||
toFun ψ := {
|
||||
toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
|
||||
map_add' := by
|
||||
intro φ φ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r φ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' ψ ψ':= by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
|
||||
rw [add_dotProduct]
|
||||
map_smul' r ψ := by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [smul_dotProduct]
|
||||
rfl
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a alt-left-handed Weyl fermion with a
|
||||
left-handed Weyl fermion. -/
|
||||
def altLeftBi : altLeftHanded →ₗ[ℂ] leftHanded →ₗ[ℂ] ℂ where
|
||||
toFun ψ := {
|
||||
toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
|
||||
map_add' := by
|
||||
intro φ φ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r φ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' ψ ψ':= by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [map_add, add_dotProduct, vec2_dotProduct, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk, LinearMap.add_apply]
|
||||
map_smul' ψ ψ' := by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [_root_.map_smul, smul_dotProduct, vec2_dotProduct, Fin.isValue, smul_eq_mul,
|
||||
LinearMap.coe_mk, AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply]
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a right-handed Weyl fermion with a
|
||||
alt-right-handed Weyl fermion. -/
|
||||
def rightAltBi : rightHanded →ₗ[ℂ] altRightHanded →ₗ[ℂ] ℂ where
|
||||
toFun ψ := {
|
||||
toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
|
||||
map_add' := by
|
||||
intro φ φ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r φ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' ψ ψ':= by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [map_add, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
|
||||
rw [add_dotProduct]
|
||||
map_smul' r ψ := by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [LinearEquiv.map_smul, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [smul_dotProduct]
|
||||
rfl
|
||||
|
||||
/-- The bi-linear map corresponding to contraction of a alt-right-handed Weyl fermion with a
|
||||
right-handed Weyl fermion. -/
|
||||
def altRightBi : altRightHanded →ₗ[ℂ] rightHanded →ₗ[ℂ] ℂ where
|
||||
toFun ψ := {
|
||||
toFun := fun φ => ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ,
|
||||
map_add' := by
|
||||
intro φ φ'
|
||||
simp only [map_add]
|
||||
rw [dotProduct_add]
|
||||
map_smul' := by
|
||||
intro r φ
|
||||
simp only [LinearEquiv.map_smul]
|
||||
rw [dotProduct_smul]
|
||||
rfl}
|
||||
map_add' ψ ψ':= by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [map_add, add_dotProduct, vec2_dotProduct, Fin.isValue, LinearMap.coe_mk,
|
||||
AddHom.coe_mk, LinearMap.add_apply]
|
||||
map_smul' ψ ψ' := by
|
||||
refine LinearMap.ext (fun φ => ?_)
|
||||
simp only [_root_.map_smul, smul_dotProduct, vec2_dotProduct, Fin.isValue, smul_eq_mul,
|
||||
LinearMap.coe_mk, AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply]
|
||||
|
||||
/-- The linear map from leftHandedWeyl ⊗ altLeftHandedWeyl to ℂ given by
|
||||
summing over components of leftHandedWeyl and altLeftHandedWeyl in the
|
||||
standard basis (i.e. the dot product).
|
||||
Physically, the contraction of a left-handed Weyl fermion with a alt-left-handed Weyl fermion.
|
||||
In index notation this is ψ_a φ^a. -/
|
||||
def leftAltContraction : leftHanded ⊗ altLeftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift leftAltBi
|
||||
comm M := TensorProduct.ext' fun ψ φ => by
|
||||
change (M.1 *ᵥ ψ.toFin2ℂ) ⬝ᵥ (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
|
||||
rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
|
||||
simp
|
||||
|
||||
lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
|
||||
leftAltContraction.hom (ψ ⊗ₜ φ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ := by
|
||||
rw [leftAltContraction]
|
||||
erw [TensorProduct.lift.tmul]
|
||||
rfl
|
||||
|
||||
/-- The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
|
||||
summing over components of altLeftHandedWeyl and leftHandedWeyl in the
|
||||
standard basis (i.e. the dot product).
|
||||
Physically, the contraction of a alt-left-handed Weyl fermion with a left-handed Weyl fermion.
|
||||
In index notation this is φ^a ψ_a. -/
|
||||
def altLeftContraction : altLeftHanded ⊗ leftHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift altLeftBi
|
||||
comm M := TensorProduct.ext' fun φ ψ => by
|
||||
change (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) ⬝ᵥ (M.1 *ᵥ ψ.toFin2ℂ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
|
||||
rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
|
||||
simp
|
||||
|
||||
lemma altLeftContraction_hom_tmul (φ : altLeftHanded) (ψ : leftHanded) :
|
||||
altLeftContraction.hom (φ ⊗ₜ ψ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ := by
|
||||
rw [altLeftContraction]
|
||||
erw [TensorProduct.lift.tmul]
|
||||
rfl
|
||||
|
||||
/--
|
||||
The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
|
||||
summing over components of rightHandedWeyl and altRightHandedWeyl in the
|
||||
standard basis (i.e. the dot product).
|
||||
The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
|
||||
In index notation this is ψ_{dot a} φ^{dot a}.
|
||||
-/
|
||||
def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift rightAltBi
|
||||
comm M := TensorProduct.ext' fun ψ φ => by
|
||||
change (M.1.map star *ᵥ ψ.toFin2ℂ) ⬝ᵥ (M.1⁻¹.conjTranspose *ᵥ φ.toFin2ℂ) =
|
||||
ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
|
||||
have h1 : (M.1)⁻¹ᴴ = ((M.1)⁻¹.map star)ᵀ := by rfl
|
||||
rw [dotProduct_mulVec, h1, vecMul_transpose, mulVec_mulVec]
|
||||
have h2 : ((M.1)⁻¹.map star * (M.1).map star) = 1 := by
|
||||
refine transpose_inj.mp ?_
|
||||
rw [transpose_mul]
|
||||
change M.1.conjTranspose * (M.1)⁻¹.conjTranspose = 1ᵀ
|
||||
rw [← @conjTranspose_mul]
|
||||
simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
|
||||
not_false_eq_true, nonsing_inv_mul, conjTranspose_one, transpose_one]
|
||||
rw [h2]
|
||||
simp only [one_mulVec, vec2_dotProduct, Fin.isValue, RightHandedModule.toFin2ℂEquiv_apply,
|
||||
AltRightHandedModule.toFin2ℂEquiv_apply]
|
||||
|
||||
/--
|
||||
The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
|
||||
summing over components of altRightHandedWeyl and rightHandedWeyl in the
|
||||
standard basis (i.e. the dot product).
|
||||
The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
|
||||
In index notation this is φ^{dot a} ψ_{dot a}.
|
||||
-/
|
||||
def altRightContraction : altRightHanded ⊗ rightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
|
||||
hom := TensorProduct.lift altRightBi
|
||||
comm M := TensorProduct.ext' fun φ ψ => by
|
||||
change (M.1⁻¹.conjTranspose *ᵥ φ.toFin2ℂ) ⬝ᵥ (M.1.map star *ᵥ ψ.toFin2ℂ) =
|
||||
φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
|
||||
have h1 : (M.1)⁻¹ᴴ = ((M.1)⁻¹.map star)ᵀ := by rfl
|
||||
rw [dotProduct_mulVec, h1, mulVec_transpose, vecMul_vecMul]
|
||||
have h2 : ((M.1)⁻¹.map star * (M.1).map star) = 1 := by
|
||||
refine transpose_inj.mp ?_
|
||||
rw [transpose_mul]
|
||||
change M.1.conjTranspose * (M.1)⁻¹.conjTranspose = 1ᵀ
|
||||
rw [← @conjTranspose_mul]
|
||||
simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
|
||||
not_false_eq_true, nonsing_inv_mul, conjTranspose_one, transpose_one]
|
||||
rw [h2]
|
||||
simp only [vecMul_one, vec2_dotProduct, Fin.isValue, AltRightHandedModule.toFin2ℂEquiv_apply,
|
||||
RightHandedModule.toFin2ℂEquiv_apply]
|
||||
|
||||
lemma leftAltContraction_apply_symm (ψ : leftHanded) (φ : altLeftHanded) :
|
||||
leftAltContraction.hom (ψ ⊗ₜ φ) = altLeftContraction.hom (φ ⊗ₜ ψ) := by
|
||||
rw [altLeftContraction_hom_tmul, leftAltContraction_hom_tmul]
|
||||
exact dotProduct_comm ψ.toFin2ℂ φ.toFin2ℂ
|
||||
|
||||
/-- A manifestation of the statement that `ψ ψ' = - ψ' ψ` where `ψ` and `ψ'`
|
||||
are `leftHandedWeyl`. -/
|
||||
lemma leftAltContraction_apply_leftHandedAltEquiv (ψ ψ' : leftHanded) :
|
||||
leftAltContraction.hom (ψ ⊗ₜ leftHandedAltEquiv.hom.hom ψ') =
|
||||
- leftAltContraction.hom (ψ' ⊗ₜ leftHandedAltEquiv.hom.hom ψ) := by
|
||||
rw [leftAltContraction_hom_tmul, leftAltContraction_hom_tmul,
|
||||
leftHandedAltEquiv_hom_hom_apply, leftHandedAltEquiv_hom_hom_apply]
|
||||
simp only [CategoryTheory.Monoidal.transportStruct_tensorUnit,
|
||||
CategoryTheory.Equivalence.symm_functor, Action.functorCategoryEquivalence_inverse,
|
||||
Action.FunctorCategoryEquivalence.inverse_obj_V, CategoryTheory.Monoidal.tensorUnit_obj,
|
||||
cons_mulVec, cons_dotProduct, zero_mul, one_mul, dotProduct_empty, add_zero, zero_add, neg_mul,
|
||||
empty_mulVec, LinearEquiv.apply_symm_apply, dotProduct_cons, mul_neg, neg_add_rev, neg_neg]
|
||||
ring
|
||||
|
||||
/-- A manifestation of the statement that `φ φ' = - φ' φ` where `φ` and `φ'` are
|
||||
`altLeftHandedWeyl`. -/
|
||||
lemma leftAltContraction_apply_leftHandedAltEquiv_inv (φ φ' : altLeftHanded) :
|
||||
leftAltContraction.hom (leftHandedAltEquiv.inv.hom φ ⊗ₜ φ') =
|
||||
- leftAltContraction.hom (leftHandedAltEquiv.inv.hom φ' ⊗ₜ φ) := by
|
||||
rw [leftAltContraction_hom_tmul, leftAltContraction_hom_tmul,
|
||||
leftHandedAltEquiv_inv_hom_apply, leftHandedAltEquiv_inv_hom_apply]
|
||||
simp only [CategoryTheory.Monoidal.transportStruct_tensorUnit,
|
||||
CategoryTheory.Equivalence.symm_functor, Action.functorCategoryEquivalence_inverse,
|
||||
Action.FunctorCategoryEquivalence.inverse_obj_V, CategoryTheory.Monoidal.tensorUnit_obj,
|
||||
cons_mulVec, cons_dotProduct, zero_mul, neg_mul, one_mul, dotProduct_empty, add_zero, zero_add,
|
||||
empty_mulVec, LinearEquiv.apply_symm_apply, neg_add_rev, neg_neg]
|
||||
ring
|
||||
|
||||
informal_lemma leftAltWeylContraction_symm_altLeftWeylContraction where
|
||||
math :≈ "The linear map altLeftWeylContraction is leftAltWeylContraction composed
|
||||
with the braiding of the tensor product."
|
||||
deps :≈ [``leftAltContraction, ``altLeftContraction]
|
||||
|
||||
informal_lemma altLeftWeylContraction_invariant where
|
||||
math :≈ "The contraction altLeftWeylContraction is invariant with respect to
|
||||
the action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl."
|
||||
deps :≈ [``altLeftContraction]
|
||||
|
||||
informal_lemma rightAltWeylContraction_invariant where
|
||||
math :≈ "The contraction rightAltWeylContraction is invariant with respect to
|
||||
the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
|
||||
deps :≈ [``rightAltContraction]
|
||||
|
||||
informal_lemma rightAltWeylContraction_symm_altRightWeylContraction where
|
||||
math :≈ "The linear map altRightWeylContraction is rightAltWeylContraction composed
|
||||
with the braiding of the tensor product."
|
||||
deps :≈ [``rightAltContraction, ``altRightContraction]
|
||||
|
||||
informal_lemma altRightWeylContraction_invariant where
|
||||
math :≈ "The contraction altRightWeylContraction is invariant with respect to
|
||||
the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl."
|
||||
deps :≈ [``altRightContraction]
|
||||
|
||||
end
|
||||
end Fermion
|
||||
221
HepLean/SpaceTime/WeylFermion/Metric.lean
Normal file
221
HepLean/SpaceTime/WeylFermion/Metric.lean
Normal file
|
|
@ -0,0 +1,221 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.SpaceTime.WeylFermion.Basic
|
||||
import HepLean.SpaceTime.WeylFermion.Contraction
|
||||
import Mathlib.LinearAlgebra.TensorProduct.Matrix
|
||||
import HepLean.SpaceTime.WeylFermion.Two
|
||||
/-!
|
||||
|
||||
# Metrics of Weyl fermions
|
||||
|
||||
We define the metrics for Weyl fermions, often denoted `ε` in the literature.
|
||||
These allow us to go from left-handed to alt-left-handed Weyl fermions and back,
|
||||
and from right-handed to alt-right-handed Weyl fermions and back.
|
||||
|
||||
-/
|
||||
|
||||
namespace Fermion
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open CategoryTheory.MonoidalCategory
|
||||
|
||||
/-- The raw `2x2` matrix corresponding to the metric for fermions. -/
|
||||
def metricRaw : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; -1, 0]
|
||||
|
||||
lemma comm_metricRaw (M : SL(2,ℂ)) : M.1 * metricRaw = metricRaw * (M.1⁻¹)ᵀ := by
|
||||
rw [metricRaw]
|
||||
rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
|
||||
rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
|
||||
Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
|
||||
simp only [Fin.isValue, mul_zero, mul_neg, mul_one, zero_add, add_zero, transpose_apply, of_apply,
|
||||
cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_fin_const, head_cons,
|
||||
cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, zero_smul, tail_cons, one_smul,
|
||||
empty_vecMul, neg_smul, neg_cons, neg_neg, neg_empty, empty_mul, Equiv.symm_apply_apply]
|
||||
|
||||
lemma metricRaw_comm (M : SL(2,ℂ)) : metricRaw * M.1 = (M.1⁻¹)ᵀ * metricRaw := by
|
||||
rw [metricRaw]
|
||||
rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
|
||||
rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
|
||||
Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
|
||||
simp only [Fin.isValue, zero_mul, one_mul, zero_add, neg_mul, add_zero, transpose_apply, of_apply,
|
||||
cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, head_fin_const, head_cons,
|
||||
cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, smul_cons, smul_eq_mul, mul_zero,
|
||||
mul_one, smul_empty, tail_cons, neg_smul, mul_neg, neg_cons, neg_neg, neg_zero, neg_empty,
|
||||
empty_vecMul, add_cons, empty_add_empty, empty_mul, Equiv.symm_apply_apply]
|
||||
|
||||
lemma star_comm_metricRaw (M : SL(2,ℂ)) : M.1.map star * metricRaw = metricRaw * ((M.1)⁻¹)ᴴ := by
|
||||
rw [metricRaw]
|
||||
rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
|
||||
rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
|
||||
eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᴴ]
|
||||
rw [eta_fin_two (!![M.1 0 0, M.1 0 1; M.1 1 0, M.1 1 1].map star)]
|
||||
simp
|
||||
|
||||
lemma metricRaw_comm_star (M : SL(2,ℂ)) : metricRaw * M.1.map star = ((M.1)⁻¹)ᴴ * metricRaw := by
|
||||
rw [metricRaw]
|
||||
rw [SpaceTime.SL2C.inverse_coe, eta_fin_two M.1]
|
||||
rw [SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
|
||||
eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᴴ]
|
||||
rw [eta_fin_two (!![M.1 0 0, M.1 0 1; M.1 1 0, M.1 1 1].map star)]
|
||||
simp
|
||||
|
||||
/-- The metric `εₐₐ` as an element of `(leftHanded ⊗ leftHanded).V`. -/
|
||||
def leftMetricVal : (leftHanded ⊗ leftHanded).V :=
|
||||
leftLeftToMatrix.symm (- metricRaw)
|
||||
|
||||
/-- The metric `εₐₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded`,
|
||||
making manifest its invariance under the action of `SL(2,ℂ)`. -/
|
||||
def leftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • leftMetricVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • leftMetricVal =
|
||||
(TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)) (x' • leftMetricVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, leftMetricVal, map_neg, neg_inj]
|
||||
erw [leftLeftToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
rw [comm_metricRaw, mul_assoc, ← @transpose_mul]
|
||||
simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
|
||||
not_false_eq_true, mul_nonsing_inv, transpose_one, mul_one]
|
||||
|
||||
/-- The metric `εᵃᵃ` as an element of `(altLeftHanded ⊗ altLeftHanded).V`. -/
|
||||
def altLeftMetricVal : (altLeftHanded ⊗ altLeftHanded).V :=
|
||||
altLeftaltLeftToMatrix.symm metricRaw
|
||||
|
||||
/-- The metric `εᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded`,
|
||||
making manifest its invariance under the action of `SL(2,ℂ)`. -/
|
||||
def altLeftMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ altLeftHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • altLeftMetricVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • altLeftMetricVal =
|
||||
(TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)) (x' • altLeftMetricVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, altLeftMetricVal]
|
||||
erw [altLeftaltLeftToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
rw [← metricRaw_comm, mul_assoc]
|
||||
simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
|
||||
not_false_eq_true, mul_nonsing_inv, mul_one]
|
||||
|
||||
/-- The metric `ε_{dot a}_{dot a}` as an element of `(rightHanded ⊗ rightHanded).V`. -/
|
||||
def rightMetricVal : (rightHanded ⊗ rightHanded).V :=
|
||||
rightRightToMatrix.symm (- metricRaw)
|
||||
|
||||
/-- The metric `ε_{dot a}_{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded`,
|
||||
making manifest its invariance under the action of `SL(2,ℂ)`. -/
|
||||
def rightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • rightMetricVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • rightMetricVal =
|
||||
(TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M)) (x' • rightMetricVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, rightMetricVal, map_neg, neg_inj]
|
||||
trans rightRightToMatrix.symm ((M.1).map star * metricRaw * ((M.1).map star)ᵀ)
|
||||
· apply congrArg
|
||||
rw [star_comm_metricRaw, mul_assoc]
|
||||
have h1 : ((M.1)⁻¹ᴴ * ((M.1).map star)ᵀ) = 1 := by
|
||||
trans (M.1)⁻¹ᴴ * ((M.1))ᴴ
|
||||
· rfl
|
||||
rw [← @conjTranspose_mul]
|
||||
simp only [SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq, one_ne_zero,
|
||||
not_false_eq_true, mul_nonsing_inv, conjTranspose_one]
|
||||
rw [h1]
|
||||
simp
|
||||
· rw [← rightRightToMatrix_ρ_symm metricRaw M]
|
||||
rfl
|
||||
|
||||
/-- The metric `ε^{dot a}^{dot a}` as an element of `(altRightHanded ⊗ altRightHanded).V`. -/
|
||||
def altRightMetricVal : (altRightHanded ⊗ altRightHanded).V :=
|
||||
altRightAltRightToMatrix.symm (metricRaw)
|
||||
|
||||
/-- The metric `ε^{dot a}^{dot a}` as a morphism
|
||||
`𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHanded`,
|
||||
making manifest its invariance under the action of `SL(2,ℂ)`. -/
|
||||
def altRightMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ altRightHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • altRightMetricVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • altRightMetricVal =
|
||||
(TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M)) (x' • altRightMetricVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V]
|
||||
trans altRightAltRightToMatrix.symm
|
||||
(((M.1)⁻¹).conjTranspose * metricRaw * (((M.1)⁻¹).conjTranspose)ᵀ)
|
||||
· rw [altRightMetricVal]
|
||||
apply congrArg
|
||||
rw [← metricRaw_comm_star, mul_assoc]
|
||||
have h1 : ((M.1).map star * (M.1)⁻¹ᴴᵀ) = 1 := by
|
||||
refine transpose_eq_one.mp ?_
|
||||
rw [@transpose_mul]
|
||||
simp only [transpose_transpose, RCLike.star_def]
|
||||
change (M.1)⁻¹ᴴ * (M.1)ᴴ = 1
|
||||
rw [← @conjTranspose_mul]
|
||||
simp
|
||||
rw [h1, mul_one]
|
||||
· rw [← altRightAltRightToMatrix_ρ_symm metricRaw M]
|
||||
rfl
|
||||
|
||||
end
|
||||
end Fermion
|
||||
487
HepLean/SpaceTime/WeylFermion/Two.lean
Normal file
487
HepLean/SpaceTime/WeylFermion/Two.lean
Normal file
|
|
@ -0,0 +1,487 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.SpaceTime.WeylFermion.Basic
|
||||
import HepLean.SpaceTime.WeylFermion.Contraction
|
||||
import Mathlib.LinearAlgebra.TensorProduct.Matrix
|
||||
/-!
|
||||
|
||||
# Tensor product of two Weyl fermion
|
||||
|
||||
-/
|
||||
|
||||
namespace Fermion
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open CategoryTheory.MonoidalCategory
|
||||
|
||||
/-!
|
||||
|
||||
## Equivalences to matrices.
|
||||
|
||||
-/
|
||||
|
||||
/-- Equivalence of `leftHanded ⊗ leftHanded` to `2 x 2` complex matrices. -/
|
||||
def leftLeftToMatrix : (leftHanded ⊗ leftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct leftBasis leftBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-- Equivalence of `altLeftHanded ⊗ altLeftHanded` to `2 x 2` complex matrices. -/
|
||||
def altLeftaltLeftToMatrix : (altLeftHanded ⊗ altLeftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct altLeftBasis altLeftBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-- Equivalence of `leftHanded ⊗ altLeftHanded` to `2 x 2` complex matrices. -/
|
||||
def leftAltLeftToMatrix : (leftHanded ⊗ altLeftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct leftBasis altLeftBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-- Equivalence of `altLeftHanded ⊗ leftHanded` to `2 x 2` complex matrices. -/
|
||||
def altLeftLeftToMatrix : (altLeftHanded ⊗ leftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct altLeftBasis leftBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-- Equivalence of `rightHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
|
||||
def rightRightToMatrix : (rightHanded ⊗ rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct rightBasis rightBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-- Equivalence of `altRightHanded ⊗ altRightHanded` to `2 x 2` complex matrices. -/
|
||||
def altRightAltRightToMatrix : (altRightHanded ⊗ altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct altRightBasis altRightBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-- Equivalence of `rightHanded ⊗ altRightHanded` to `2 x 2` complex matrices. -/
|
||||
def rightAltRightToMatrix : (rightHanded ⊗ altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct rightBasis altRightBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-- Equivalence of `altRightHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
|
||||
def altRightRightToMatrix : (altRightHanded ⊗ rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
|
||||
(Basis.tensorProduct altRightBasis rightBasis).repr ≪≫ₗ
|
||||
Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
|
||||
LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
|
||||
|
||||
/-!
|
||||
|
||||
## Group actions
|
||||
|
||||
-/
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `leftHanded ⊗ leftHanded` is equivalent to
|
||||
`M.1 * leftLeftToMatrix v * (M.1)ᵀ`. -/
|
||||
lemma leftLeftToMatrix_ρ (v : (leftHanded ⊗ leftHanded).V) (M : SL(2,ℂ)) :
|
||||
leftLeftToMatrix (TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M) v) =
|
||||
M.1 * leftLeftToMatrix v * (M.1)ᵀ := by
|
||||
nth_rewrite 1 [leftLeftToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(leftBasis.tensorProduct leftBasis) (leftBasis.tensorProduct leftBasis)
|
||||
(TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((leftBasis.tensorProduct leftBasis).repr (v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (leftBasis.tensorProduct leftBasis)
|
||||
(leftBasis.tensorProduct leftBasis) (TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
|
||||
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M)) (i, j) k)
|
||||
* leftLeftToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ j : Fin 2, M.1 i j * leftLeftToMatrix v j x) * M.1 j x
|
||||
= ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftLeftToMatrix v x1 x) * M.1 j x := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [leftBasis_ρ_apply, Finsupp.linearEquivFunOnFinite_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
rw [mul_assoc]
|
||||
nth_rewrite 2 [mul_comm]
|
||||
rw [← mul_assoc]
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `altLeftHanded ⊗ altLeftHanded` is equivalent to
|
||||
`(M.1⁻¹)ᵀ * leftLeftToMatrix v * (M.1⁻¹)`. -/
|
||||
lemma altLeftaltLeftToMatrix_ρ (v : (altLeftHanded ⊗ altLeftHanded).V) (M : SL(2,ℂ)) :
|
||||
altLeftaltLeftToMatrix (TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M) v) =
|
||||
(M.1⁻¹)ᵀ * altLeftaltLeftToMatrix v * (M.1⁻¹) := by
|
||||
nth_rewrite 1 [altLeftaltLeftToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(altLeftBasis.tensorProduct altLeftBasis) (altLeftBasis.tensorProduct altLeftBasis)
|
||||
(TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((altLeftBasis.tensorProduct altLeftBasis).repr v)))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (altLeftBasis.tensorProduct altLeftBasis)
|
||||
(altLeftBasis.tensorProduct altLeftBasis)
|
||||
(TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
|
||||
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M)) (i, j) k)
|
||||
* altLeftaltLeftToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftaltLeftToMatrix v x1 x) * (M.1)⁻¹ x j
|
||||
= ∑ x : Fin 2, ∑ x1 : Fin 2, ((M.1)⁻¹ x1 i * altLeftaltLeftToMatrix v x1 x) * (M.1)⁻¹ x j := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [altLeftBasis_ρ_apply, transpose_apply, Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `leftHanded ⊗ altLeftHanded` is equivalent to
|
||||
`M.1 * leftAltLeftToMatrix v * (M.1⁻¹)`. -/
|
||||
lemma leftAltLeftToMatrix_ρ (v : (leftHanded ⊗ altLeftHanded).V) (M : SL(2,ℂ)) :
|
||||
leftAltLeftToMatrix (TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M) v) =
|
||||
M.1 * leftAltLeftToMatrix v * (M.1⁻¹) := by
|
||||
nth_rewrite 1 [leftAltLeftToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(leftBasis.tensorProduct altLeftBasis) (leftBasis.tensorProduct altLeftBasis)
|
||||
(TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((leftBasis.tensorProduct altLeftBasis).repr (v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (leftBasis.tensorProduct altLeftBasis)
|
||||
(leftBasis.tensorProduct altLeftBasis)
|
||||
(TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M))
|
||||
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M)) (i, j) k)
|
||||
* leftAltLeftToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, M.1 i x1 * leftAltLeftToMatrix v x1 x) * (M.1⁻¹) x j
|
||||
= ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftAltLeftToMatrix v x1 x) * (M.1⁻¹) x j := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [leftBasis_ρ_apply, altLeftBasis_ρ_apply, transpose_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `altLeftHanded ⊗ leftHanded` is equivalent to
|
||||
`(M.1⁻¹)ᵀ * leftAltLeftToMatrix v * (M.1)ᵀ`. -/
|
||||
lemma altLeftLeftToMatrix_ρ (v : (altLeftHanded ⊗ leftHanded).V) (M : SL(2,ℂ)) :
|
||||
altLeftLeftToMatrix (TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M) v) =
|
||||
(M.1⁻¹)ᵀ * altLeftLeftToMatrix v * (M.1)ᵀ := by
|
||||
nth_rewrite 1 [altLeftLeftToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(altLeftBasis.tensorProduct leftBasis) (altLeftBasis.tensorProduct leftBasis)
|
||||
(TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((altLeftBasis.tensorProduct leftBasis).repr (v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (altLeftBasis.tensorProduct leftBasis)
|
||||
(altLeftBasis.tensorProduct leftBasis)
|
||||
(TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix altLeftBasis altLeftBasis) (altLeftHanded.ρ M))
|
||||
((LinearMap.toMatrix leftBasis leftBasis) (leftHanded.ρ M)) (i, j) k)
|
||||
* altLeftLeftToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1)⁻¹ x1 i * altLeftLeftToMatrix v x1 x) * M.1 j x
|
||||
= ∑ x : Fin 2, ∑ x1 : Fin 2, ((M.1)⁻¹ x1 i * altLeftLeftToMatrix v x1 x) * M.1 j x:= by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [altLeftBasis_ρ_apply, leftBasis_ρ_apply, transpose_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `rightHanded ⊗ rightHanded` is equivalent to
|
||||
`(M.1.map star) * rightRightToMatrix v * ((M.1.map star))ᵀ`. -/
|
||||
lemma rightRightToMatrix_ρ (v : (rightHanded ⊗ rightHanded).V) (M : SL(2,ℂ)) :
|
||||
rightRightToMatrix (TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M) v) =
|
||||
(M.1.map star) * rightRightToMatrix v * ((M.1.map star))ᵀ := by
|
||||
nth_rewrite 1 [rightRightToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(rightBasis.tensorProduct rightBasis) (rightBasis.tensorProduct rightBasis)
|
||||
(TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((rightBasis.tensorProduct rightBasis).repr (v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (rightBasis.tensorProduct rightBasis)
|
||||
(rightBasis.tensorProduct rightBasis)
|
||||
(TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M))
|
||||
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
|
||||
* rightRightToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1.map star) i x1 * rightRightToMatrix v x1 x) *
|
||||
(M.1.map star) j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
|
||||
((M.1.map star) i x1 * rightRightToMatrix v x1 x) * (M.1.map star) j x:= by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [rightBasis_ρ_apply, Finsupp.linearEquivFunOnFinite_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `altRightHanded ⊗ altRightHanded` is equivalent to
|
||||
`((M.1⁻¹).conjTranspose * rightRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ`. -/
|
||||
lemma altRightAltRightToMatrix_ρ (v : (altRightHanded ⊗ altRightHanded).V) (M : SL(2,ℂ)) :
|
||||
altRightAltRightToMatrix (TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M) v) =
|
||||
((M.1⁻¹).conjTranspose) * altRightAltRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ) := by
|
||||
nth_rewrite 1 [altRightAltRightToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(altRightBasis.tensorProduct altRightBasis) (altRightBasis.tensorProduct altRightBasis)
|
||||
(TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((altRightBasis.tensorProduct altRightBasis).repr (v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (altRightBasis.tensorProduct altRightBasis)
|
||||
(altRightBasis.tensorProduct altRightBasis)
|
||||
(TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M))
|
||||
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
|
||||
* altRightAltRightToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (↑M)⁻¹ᴴ i x1 * altRightAltRightToMatrix v x1 x) *
|
||||
(↑M)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
|
||||
((↑M)⁻¹ᴴ i x1 * altRightAltRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [altRightBasis_ρ_apply, transpose_apply, Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `rightHanded ⊗ altRightHanded` is equivalent to
|
||||
`(M.1.map star) * rightAltRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ`. -/
|
||||
lemma rightAltRightToMatrix_ρ (v : (rightHanded ⊗ altRightHanded).V) (M : SL(2,ℂ)) :
|
||||
rightAltRightToMatrix (TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M) v) =
|
||||
(M.1.map star) * rightAltRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ) := by
|
||||
nth_rewrite 1 [rightAltRightToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(rightBasis.tensorProduct altRightBasis) (rightBasis.tensorProduct altRightBasis)
|
||||
(TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((rightBasis.tensorProduct altRightBasis).repr (v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (rightBasis.tensorProduct altRightBasis)
|
||||
(rightBasis.tensorProduct altRightBasis)
|
||||
(TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M))
|
||||
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M)) (i, j) k)
|
||||
* rightAltRightToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, (M.1.map star) i x1 * rightAltRightToMatrix v x1 x)
|
||||
* (↑M)⁻¹ᴴ j x = ∑ x : Fin 2, ∑ x1 : Fin 2,
|
||||
((M.1.map star) i x1 * rightAltRightToMatrix v x1 x) * (↑M)⁻¹ᴴ j x := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [rightBasis_ρ_apply, altRightBasis_ρ_apply, transpose_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-- The group action of `SL(2,ℂ)` on `altRightHanded ⊗ rightHanded` is equivalent to
|
||||
`((M.1⁻¹).conjTranspose * rightAltRightToMatrix v * ((M.1.map star)).ᵀ`. -/
|
||||
lemma altRightRightToMatrix_ρ (v : (altRightHanded ⊗ rightHanded).V) (M : SL(2,ℂ)) :
|
||||
altRightRightToMatrix (TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M) v) =
|
||||
((M.1⁻¹).conjTranspose) * altRightRightToMatrix v * (M.1.map star)ᵀ := by
|
||||
nth_rewrite 1 [altRightRightToMatrix]
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.trans_apply]
|
||||
trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
|
||||
(altRightBasis.tensorProduct rightBasis) (altRightBasis.tensorProduct rightBasis)
|
||||
(TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)))
|
||||
*ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
|
||||
((altRightBasis.tensorProduct rightBasis).repr (v))))
|
||||
· apply congrArg
|
||||
have h1 := (LinearMap.toMatrix_mulVec_repr (altRightBasis.tensorProduct rightBasis)
|
||||
(altRightBasis.tensorProduct rightBasis)
|
||||
(TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) v)
|
||||
erw [h1]
|
||||
rfl
|
||||
rw [TensorProduct.toMatrix_map]
|
||||
funext i j
|
||||
change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
|
||||
((LinearMap.toMatrix altRightBasis altRightBasis) (altRightHanded.ρ M))
|
||||
((LinearMap.toMatrix rightBasis rightBasis) (rightHanded.ρ M)) (i, j) k)
|
||||
* altRightRightToMatrix v k.1 k.2) = _
|
||||
erw [Finset.sum_product]
|
||||
simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
|
||||
have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2,
|
||||
(↑M)⁻¹ᴴ i x1 * altRightRightToMatrix v x1 x) * (M.1.map star) j x
|
||||
= ∑ x : Fin 2, ∑ x1 : Fin 2, ((↑M)⁻¹ᴴ i x1 * altRightRightToMatrix v x1 x) *
|
||||
(M.1.map star) j x := by
|
||||
congr
|
||||
funext x
|
||||
rw [Finset.sum_mul]
|
||||
erw [h1]
|
||||
rw [Finset.sum_comm]
|
||||
congr
|
||||
funext x
|
||||
congr
|
||||
funext x1
|
||||
simp only [altRightBasis_ρ_apply, rightBasis_ρ_apply, transpose_apply,
|
||||
Action.instMonoidalCategory_tensorObj_V]
|
||||
ring
|
||||
|
||||
/-!
|
||||
|
||||
## The symm version of the group actions.
|
||||
|
||||
-/
|
||||
|
||||
lemma leftLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M) (leftLeftToMatrix.symm v) =
|
||||
leftLeftToMatrix.symm (M.1 * v * (M.1)ᵀ) := by
|
||||
have h1 := leftLeftToMatrix_ρ (leftLeftToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma altLeftaltLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M) (altLeftaltLeftToMatrix.symm v) =
|
||||
altLeftaltLeftToMatrix.symm ((M.1⁻¹)ᵀ * v * (M.1⁻¹)) := by
|
||||
have h1 := altLeftaltLeftToMatrix_ρ (altLeftaltLeftToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma leftAltLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M) (leftAltLeftToMatrix.symm v) =
|
||||
leftAltLeftToMatrix.symm (M.1 * v * (M.1⁻¹)) := by
|
||||
have h1 := leftAltLeftToMatrix_ρ (leftAltLeftToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma altLeftLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M) (altLeftLeftToMatrix.symm v) =
|
||||
altLeftLeftToMatrix.symm ((M.1⁻¹)ᵀ * v * (M.1)ᵀ) := by
|
||||
have h1 := altLeftLeftToMatrix_ρ (altLeftLeftToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma rightRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (rightHanded.ρ M) (rightHanded.ρ M) (rightRightToMatrix.symm v) =
|
||||
rightRightToMatrix.symm ((M.1.map star) * v * ((M.1.map star))ᵀ) := by
|
||||
have h1 := rightRightToMatrix_ρ (rightRightToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma altRightAltRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (altRightHanded.ρ M) (altRightHanded.ρ M) (altRightAltRightToMatrix.symm v) =
|
||||
altRightAltRightToMatrix.symm (((M.1⁻¹).conjTranspose) * v * ((M.1⁻¹).conjTranspose)ᵀ) := by
|
||||
have h1 := altRightAltRightToMatrix_ρ (altRightAltRightToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma rightAltRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M) (rightAltRightToMatrix.symm v) =
|
||||
rightAltRightToMatrix.symm ((M.1.map star) * v * (((M.1⁻¹).conjTranspose)ᵀ)) := by
|
||||
have h1 := rightAltRightToMatrix_ρ (rightAltRightToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
lemma altRightRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
|
||||
TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M) (altRightRightToMatrix.symm v) =
|
||||
altRightRightToMatrix.symm (((M.1⁻¹).conjTranspose) * v * (M.1.map star)ᵀ) := by
|
||||
have h1 := altRightRightToMatrix_ρ (altRightRightToMatrix.symm v) M
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, LinearEquiv.apply_symm_apply] at h1
|
||||
rw [← h1]
|
||||
simp
|
||||
|
||||
end
|
||||
end Fermion
|
||||
167
HepLean/SpaceTime/WeylFermion/Unit.lean
Normal file
167
HepLean/SpaceTime/WeylFermion/Unit.lean
Normal file
|
|
@ -0,0 +1,167 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.SpaceTime.WeylFermion.Basic
|
||||
import HepLean.SpaceTime.WeylFermion.Contraction
|
||||
import Mathlib.LinearAlgebra.TensorProduct.Matrix
|
||||
import HepLean.SpaceTime.WeylFermion.Two
|
||||
/-!
|
||||
|
||||
# Units of Weyl fermions
|
||||
|
||||
We define the units for Weyl fermions, often denoted `δ` in the literature.
|
||||
|
||||
-/
|
||||
|
||||
namespace Fermion
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open CategoryTheory.MonoidalCategory
|
||||
|
||||
/-- The left-alt-left unit `δₐᵃ` as an element of `(leftHanded ⊗ altLeftHanded).V`. -/
|
||||
def leftAltLeftUnitVal : (leftHanded ⊗ altLeftHanded).V :=
|
||||
leftAltLeftToMatrix.symm 1
|
||||
|
||||
/-- The left-alt-left unit `δₐᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded `,
|
||||
manifesting the invariance under the `SL(2,ℂ)` action. -/
|
||||
def leftAltLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ altLeftHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • leftAltLeftUnitVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • leftAltLeftUnitVal =
|
||||
(TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M)) (x' • leftAltLeftUnitVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, leftAltLeftUnitVal]
|
||||
erw [leftAltLeftToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
simp
|
||||
|
||||
/-- The alt-left-left unit `δᵃₐ` as an element of `(altLeftHanded ⊗ leftHanded).V`. -/
|
||||
def altLeftLeftUnitVal : (altLeftHanded ⊗ leftHanded).V :=
|
||||
altLeftLeftToMatrix.symm 1
|
||||
|
||||
/-- The alt-left-left unit `δᵃₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded `,
|
||||
manifesting the invariance under the `SL(2,ℂ)` action. -/
|
||||
def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • altLeftLeftUnitVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • altLeftLeftUnitVal =
|
||||
(TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)) (x' • altLeftLeftUnitVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, altLeftLeftUnitVal]
|
||||
erw [altLeftLeftToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
simp only [mul_one, ← transpose_mul, SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq,
|
||||
one_ne_zero, not_false_eq_true, mul_nonsing_inv, transpose_one]
|
||||
|
||||
/-- The right-alt-right unit `δ_{dot a}^{dot a}` as an element of
|
||||
`(rightHanded ⊗ altRightHanded).V`. -/
|
||||
def rightAltRightUnitVal : (rightHanded ⊗ altRightHanded).V :=
|
||||
rightAltRightToMatrix.symm 1
|
||||
|
||||
/-- The right-alt-right unit `δ_{dot a}^{dot a}` as a morphism
|
||||
`𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHanded`, manifesting
|
||||
the invariance under the `SL(2,ℂ)` action. -/
|
||||
def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • rightAltRightUnitVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • rightAltRightUnitVal =
|
||||
(TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M)) (x' • rightAltRightUnitVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, rightAltRightUnitVal]
|
||||
erw [rightAltRightToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
simp only [RCLike.star_def, mul_one]
|
||||
symm
|
||||
refine transpose_eq_one.mp ?h.h.h.a
|
||||
simp only [transpose_mul, transpose_transpose]
|
||||
change (M.1)⁻¹ᴴ * (M.1)ᴴ = 1
|
||||
rw [@conjTranspose_nonsing_inv]
|
||||
simp
|
||||
|
||||
/-- The alt-right-right unit `δ^{dot a}_{dot a}` as an element of
|
||||
`(rightHanded ⊗ altRightHanded).V`. -/
|
||||
def altRightRightUnitVal : (altRightHanded ⊗ rightHanded).V :=
|
||||
altRightRightToMatrix.symm 1
|
||||
|
||||
/-- The alt-right-right unit `δ^{dot a}_{dot a}` as a morphism
|
||||
`𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHanded`, manifesting
|
||||
the invariance under the `SL(2,ℂ)` action. -/
|
||||
def altRightRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altRightHanded ⊗ rightHanded where
|
||||
hom := {
|
||||
toFun := fun a =>
|
||||
let a' : ℂ := a
|
||||
a' • altRightRightUnitVal,
|
||||
map_add' := fun x y => by
|
||||
simp only [add_smul]
|
||||
map_smul' := fun m x => by
|
||||
simp only [smul_smul]
|
||||
rfl}
|
||||
comm M := by
|
||||
ext x : 2
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.tensorUnit_ρ', CategoryTheory.Category.id_comp, Action.tensor_ρ', ModuleCat.coe_comp,
|
||||
Function.comp_apply]
|
||||
let x' : ℂ := x
|
||||
change x' • altRightRightUnitVal =
|
||||
(TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (x' • altRightRightUnitVal)
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, _root_.map_smul]
|
||||
apply congrArg
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, altRightRightUnitVal]
|
||||
erw [altRightRightToMatrix_ρ_symm]
|
||||
apply congrArg
|
||||
simp only [mul_one, RCLike.star_def]
|
||||
symm
|
||||
change (M.1)⁻¹ᴴ * (M.1)ᴴ = 1
|
||||
rw [@conjTranspose_nonsing_inv]
|
||||
simp
|
||||
|
||||
end
|
||||
end Fermion
|
||||
|
|
@ -46,14 +46,14 @@ def discreteFunctorMapIso {c1 c2 : Discrete C} (h : c1 ⟶ c2) :
|
|||
|
||||
lemma discreteFun_hom_trans {c1 c2 c3 : Discrete C} (h1 : c1 = c2) (h2 : c2 = c3)
|
||||
(v : F.obj c1) : (F.map (eqToHom h2)).hom ((F.map (eqToHom h1)).hom v)
|
||||
= (F.map (eqToHom ( h1.trans h2))).hom v := by
|
||||
= (F.map (eqToHom (h1.trans h2))).hom v := by
|
||||
subst h2 h1
|
||||
simp_all only [eqToHom_refl, Discrete.functor_map_id, Action.id_hom, ModuleCat.id_apply]
|
||||
|
||||
/-- The linear equivalence between `(F.obj c1).V ≃ₗ[k] (F.obj c2).V` induced by an equality of
|
||||
`c1` and `c2`. -/
|
||||
def discreteFunctorMapEqIso {c1 c2 : Discrete C} (h : c1.as = c2.as) :
|
||||
(F.obj c1).V ≃ₗ[k] (F.obj c2).V := LinearEquiv.ofLinear
|
||||
(F.obj c1).V ≃ₗ[k] (F.obj c2).V := LinearEquiv.ofLinear
|
||||
(F.mapIso (Discrete.eqToIso h)).hom.hom (F.mapIso (Discrete.eqToIso h)).inv.hom
|
||||
(by
|
||||
ext x : 2
|
||||
|
|
@ -63,7 +63,7 @@ def discreteFunctorMapEqIso {c1 c2 : Discrete C} (h : c1.as = c2.as) :
|
|||
rw [ModuleCat.ext_iff] at h1
|
||||
have h1x := h1 x
|
||||
simp only [CategoryStruct.comp] at h1x
|
||||
simpa using h1x )
|
||||
simpa using h1x)
|
||||
(by
|
||||
ext x : 2
|
||||
simp only [Functor.mapIso_inv, eqToIso.inv, Functor.mapIso_hom, eqToIso.hom, LinearMap.coe_comp,
|
||||
|
|
@ -122,7 +122,6 @@ lemma objObj'_ρ_empty (g : G) : (objObj' F (𝟙_ (OverColor C))).ρ g = Linear
|
|||
funext i
|
||||
exact Empty.elim i
|
||||
|
||||
|
||||
open TensorProduct in
|
||||
@[simp]
|
||||
lemma objObj'_V_carrier (f : OverColor C) :
|
||||
|
|
@ -149,7 +148,6 @@ lemma mapToLinearEquiv'_tprod {f g : OverColor C} (m : f ⟶ g)
|
|||
rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]
|
||||
rfl
|
||||
|
||||
|
||||
/-- Given a morphism in `OverColor C` the corresopnding map of representations induced by
|
||||
reindexing. -/
|
||||
def objMap' {f g : OverColor C} (m : f ⟶ g) : objObj' F f ⟶ objObj' F g where
|
||||
|
|
@ -231,7 +229,6 @@ lemma μModEquiv_tmul_tprod {X Y : OverColor C}
|
|||
rw [PiTensorProduct.congr_tprod]
|
||||
rfl
|
||||
|
||||
|
||||
/-- The natural isomorphism corresponding to the tensorate. -/
|
||||
def μ (X Y : OverColor C) : objObj' F X ⊗ objObj' F Y ≅ objObj' F (X ⊗ Y) :=
|
||||
Action.mkIso (μModEquiv F X Y).toModuleIso
|
||||
|
|
@ -263,7 +260,6 @@ lemma μ_tmul_tprod {X Y : OverColor C} (p : (i : X.left) → F.obj (Discrete.mk
|
|||
discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by
|
||||
exact μModEquiv_tmul_tprod F p q
|
||||
|
||||
|
||||
lemma μ_natural_left {X Y : OverColor C} (f : X ⟶ Y) (Z : OverColor C) :
|
||||
MonoidalCategory.whiskerRight (objMap' F f) (objObj' F Z) ≫ (μ F Y Z).hom =
|
||||
(μ F X Z).hom ≫ objMap' F (MonoidalCategory.whiskerRight f Z) := by
|
||||
|
|
@ -301,7 +297,6 @@ lemma μ_natural_left {X Y : OverColor C} (f : X ⟶ Y) (Z : OverColor C) :
|
|||
Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv]
|
||||
rfl
|
||||
|
||||
|
||||
lemma μ_natural_right {X Y : OverColor C} (X' : OverColor C) (f : X ⟶ Y) :
|
||||
MonoidalCategory.whiskerLeft (objObj' F X') (objMap' F f) ≫ (μ F X' Y).hom =
|
||||
(μ F X' X).hom ≫ objMap' F (MonoidalCategory.whiskerLeft X' f) := by
|
||||
|
|
@ -337,7 +332,6 @@ lemma μ_natural_right {X Y : OverColor C} (X' : OverColor C) (f : X ⟶ Y) :
|
|||
rfl
|
||||
| Sum.inr i => rfl
|
||||
|
||||
|
||||
lemma associativity (X Y Z : OverColor C) :
|
||||
whiskerRight (μ F X Y).hom (objObj' F Z) ≫
|
||||
(μ F (X ⊗ Y) Z).hom ≫ objMap' F (associator X Y Z).hom =
|
||||
|
|
@ -533,7 +527,7 @@ def mapApp' (X : OverColor C) : (obj' F).obj X ⟶ (obj' F').obj X where
|
|||
funext i
|
||||
simpa using LinearMap.congr_fun ((η.app (Discrete.mk (X.hom i))).comm M) (x i)
|
||||
|
||||
lemma mapApp'_tprod (X : OverColor C) (p : (i : X.left) → F.obj (Discrete.mk (X.hom i))) :
|
||||
lemma mapApp'_tprod (X : OverColor C) (p : (i : X.left) → F.obj (Discrete.mk (X.hom i))) :
|
||||
(mapApp' η X).hom (PiTensorProduct.tprod k p) =
|
||||
PiTensorProduct.tprod k fun i => (η.app (Discrete.mk (X.hom i))).hom (p i) := by
|
||||
change (mapApp' η X).hom (PiTensorProduct.tprod k p) = _
|
||||
|
|
@ -618,7 +612,7 @@ end lift
|
|||
noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ MonoidalFunctor (OverColor C) (Rep k G) where
|
||||
obj F := lift.obj' F
|
||||
map η := lift.map' η
|
||||
map_id F := by
|
||||
map_id F := by
|
||||
simp only [lift.map']
|
||||
refine MonoidalNatTrans.ext' (fun X => ?_)
|
||||
ext x : 2
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue