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

feat: Unit and metric for Weyl

Browse source
This commit is contained in:
jstoobysmith 2024-10-15 11:23:08 +00:00
parent 98e2f1865d
commit 1ceffaa329
6 changed files with 928 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

50
HepLean/SpaceTime/WeylFermion/Basic.lean
View file

@ -9,6 +9,7 @@ import Mathlib.RepresentationTheory.Rep
import HepLean.Tensors.Basic
import HepLean.SpaceTime.WeylFermion.Modules
import Mathlib.Logic.Equiv.TransferInstance
import LLMlean
/-!
# Weyl fermions
@ -47,6 +48,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 [leftBasis]
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 +83,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 +115,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 +151,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.

45
HepLean/SpaceTime/WeylFermion/Contraction.lean
View file

@ -4,10 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.WeylFermion.Basic
import LLMlean
/-!
# Contraction of Weyl fermions
We define the contraction of Weyl fermions.
-/
namespace Fermion
@ -128,9 +131,7 @@ def altRightBi : altRightHanded →ₗ[ℂ] rightHanded →ₗ[ℂ] ℂ where
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 ψ φ
comm M := TensorProduct.ext' fun ψ φ => by
change (M.1 *ᵥ ψ.toFin2ℂ) ⬝ᵥ (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) = ψ.toFin2ℂ ⬝ᵥ φ.toFin2ℂ
rw [dotProduct_mulVec, vecMul_transpose, mulVec_mulVec]
simp
@ -148,9 +149,7 @@ lemma leftAltContraction_hom_tmul (ψ : leftHanded) (φ : altLeftHanded) :
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 φ ψ
comm M := TensorProduct.ext' fun φ ψ => by
change (M.1⁻¹ᵀ *ᵥ φ.toFin2ℂ) ⬝ᵥ (M.1 *ᵥ ψ.toFin2ℂ) = φ.toFin2ℂ ⬝ᵥ ψ.toFin2ℂ
rw [dotProduct_mulVec, mulVec_transpose, vecMul_vecMul]
simp
@ -170,13 +169,9 @@ The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
-/
def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where
hom := TensorProduct.lift rightAltBi
comm M := by
apply TensorProduct.ext'
intro ψ φ
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
rw [conjTranspose]
exact rfl
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 ?_
@ -189,23 +184,18 @@ def rightAltContraction : rightHanded ⊗ altRightHanded ⟶ 𝟙_ (Rep ℂ SL(2
simp only [one_mulVec, vec2_dotProduct, Fin.isValue, RightHandedModule.toFin2ℂEquiv_apply,
AltRightHandedModule.toFin2ℂEquiv_apply]
informal_definition altRightWeylContraction where
math :≈ "The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
/--
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]
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 := by
apply TensorProduct.ext'
intro φ ψ
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
rw [conjTranspose]
exact rfl
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 ?_
@ -270,13 +260,12 @@ informal_lemma rightAltWeylContraction_invariant where
informal_lemma rightAltWeylContraction_symm_altRightWeylContraction where
math :≈ "The linear map altRightWeylContraction is rightAltWeylContraction composed
with the braiding of the tensor product."
deps :≈ [``rightAltContraction, ``altRightWeylContraction]
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 :≈ [``altRightWeylContraction]
deps :≈ [``altRightContraction]
end
end Fermion

213
HepLean/SpaceTime/WeylFermion/Metric.lean Normal file
View file

@ -0,0 +1,213 @@
/-
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
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
let x' : ℂ := x
change x' • leftMetricVal =
(TensorProduct.map (leftHanded.ρ M) (leftHanded.ρ M)) (x' • leftMetricVal)
simp
apply congrArg
simp [leftMetricVal]
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
let x' : ℂ := x
change x' • altLeftMetricVal =
(TensorProduct.map (altLeftHanded.ρ M) (altLeftHanded.ρ M)) (x' • altLeftMetricVal)
simp
apply congrArg
simp [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
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
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
change (M.1)⁻¹ᴴ * (M.1)ᴴ = 1
rw [← @conjTranspose_mul]
simp
rw [h1, mul_one]
· rw [← altRightAltRightToMatrix_ρ_symm metricRaw M]
rfl
end
end Fermion

484
HepLean/SpaceTime/WeylFermion/Two.lean Normal file
View file

@ -0,0 +1,484 @@
/-
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

159
HepLean/SpaceTime/WeylFermion/Unit.lean Normal file
View file

@ -0,0 +1,159 @@
/-
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
let x' : ℂ := x
change x' • leftAltLeftUnitVal =
(TensorProduct.map (leftHanded.ρ M) (altLeftHanded.ρ M)) (x' • leftAltLeftUnitVal)
simp
apply congrArg
simp [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
let x' : ℂ := x
change x' • altLeftLeftUnitVal =
(TensorProduct.map (altLeftHanded.ρ M) (leftHanded.ρ M)) (x' • altLeftLeftUnitVal)
simp
apply congrArg
simp [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
let x' : ℂ := x
change x' • rightAltRightUnitVal =
(TensorProduct.map (rightHanded.ρ M) (altRightHanded.ρ M)) (x' • rightAltRightUnitVal)
simp
apply congrArg
simp [rightAltRightUnitVal]
erw [rightAltRightToMatrix_ρ_symm]
apply congrArg
simp
symm
refine transpose_eq_one.mp ?h.h.h.a
simp
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
let x' : ℂ := x
change x' • altRightRightUnitVal =
(TensorProduct.map (altRightHanded.ρ M) (rightHanded.ρ M)) (x' • altRightRightUnitVal)
simp
apply congrArg
simp [altRightRightUnitVal]
erw [altRightRightToMatrix_ρ_symm]
apply congrArg
simp
symm
change (M.1)⁻¹ᴴ * (M.1)ᴴ = 1
rw [@conjTranspose_nonsing_inv]
simp
end
end Fermion

5
HepLean/Tensors/OverColor/Iso.lean
View file

@ -52,6 +52,11 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by
fin_cases x
rfl
def finSwapTwo {n : ℕ} (i : Fin n) : Fin (2 + n) ≃ Fin n.succ.succ := by
let e1 := Equiv.swap (Fin.castAdd n (0 : Fin 2)) (Fin.natAdd 2 i)
let e2 := Equiv.swap (Fin.castAdd n (1 : Fin 2)) (Fin.natAdd 2 i)
/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
`i`th component. -/
def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=