From 98e2f1865dcaaecd11704c68887db60a903dae13 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 15 Oct 2024 06:08:56 +0000 Subject: [PATCH 1/4] feat: Update Contraction --- HepLean/SpaceTime/WeylFermion/Basic.lean | 168 ----------- .../SpaceTime/WeylFermion/Contraction.lean | 282 ++++++++++++++++++ HepLean/Tensors/OverColor/Discrete.lean | 59 ++++ HepLean/Tensors/OverColor/Iso.lean | 16 + HepLean/Tensors/OverColor/Lift.lean | 30 ++ HepLean/Tensors/Tree/Basic.lean | 197 +++++++++++- 6 files changed, 572 insertions(+), 180 deletions(-) create mode 100644 HepLean/SpaceTime/WeylFermion/Contraction.lean create mode 100644 HepLean/Tensors/OverColor/Discrete.lean diff --git a/HepLean/SpaceTime/WeylFermion/Basic.lean b/HepLean/SpaceTime/WeylFermion/Basic.lean index 5165b03b..8cfeea95 100644 --- a/HepLean/SpaceTime/WeylFermion/Basic.lean +++ b/HepLean/SpaceTime/WeylFermion/Basic.lean @@ -224,174 +224,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 diff --git a/HepLean/SpaceTime/WeylFermion/Contraction.lean b/HepLean/SpaceTime/WeylFermion/Contraction.lean new file mode 100644 index 00000000..7902b898 --- /dev/null +++ b/HepLean/SpaceTime/WeylFermion/Contraction.lean @@ -0,0 +1,282 @@ +/- +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 + +-/ + +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 := 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 + +/-- +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 := by + apply TensorProduct.ext' + intro ψ φ + 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 + 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] + +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] + +def altRightContraction : altRightHanded ⊗ rightHanded ⟶ 𝟙_ (Rep ℂ SL(2,ℂ)) where + hom := TensorProduct.lift altRightBi + comm M := by + apply TensorProduct.ext' + intro φ ψ + 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 + 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, ``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 diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean new file mode 100644 index 00000000..048b4ba6 --- /dev/null +++ b/HepLean/Tensors/OverColor/Discrete.lean @@ -0,0 +1,59 @@ +/- +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.Tensors.OverColor.Basic +import HepLean.Tensors.OverColor.Lift +import HepLean.Mathematics.PiTensorProduct +import HepLean.Tensors.OverColor.Iso +/-! + +# Discrete color category + +-/ + +namespace IndexNotation +namespace OverColor +namespace Discrete + +open CategoryTheory +open MonoidalCategory +open TensorProduct +variable {C k : Type} [CommRing k] {G : Type} [Group G] + +variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F') +noncomputable section + +def pair : Discrete C ⥤ Rep k G := F ⊗ F + +def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ + (lift.obj F).obj (OverColor.mk ![c,c]) := by + symm + apply ((lift.obj F).mapIso fin2Iso).trans + apply ((lift.obj F).μIso _ _).symm.trans + apply tensorIso ?_ ?_ + · symm + apply (forgetLiftApp F c).symm.trans + refine (lift.obj F).mapIso (mkIso ?_) + funext x + fin_cases x + rfl + · symm + apply (forgetLiftApp F c).symm.trans + refine (lift.obj F).mapIso (mkIso ?_) + funext x + fin_cases x + rfl + + +def pairτ (τ : C → C) : Discrete C ⥤ Rep k G := + F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) + +def τPair (τ : C → C) : Discrete C ⥤ Rep k G := + ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) ⊗ F + +end +end Discrete +end OverColor +end IndexNotation diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean index 93113e3a..f9c163ca 100644 --- a/HepLean/Tensors/OverColor/Iso.lean +++ b/HepLean/Tensors/OverColor/Iso.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Tensors.OverColor.Functors +import HepLean.Tensors.OverColor.Lift /-! ## Isomorphisms in the OverColor category @@ -39,6 +40,18 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 := subst h rfl)) +def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by + let e1 : Fin 2 ≃ Fin 1 ⊕ Fin 1 := (finSumFinEquiv (n := 1)).symm + apply (equivToIso e1).trans + apply (mkSum _).trans + refine tensorIso (mkIso ?_) (mkIso ?_) + · funext x + fin_cases x + rfl + · funext x + fin_cases x + rfl + /-- 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 := @@ -158,6 +171,9 @@ def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C) rw [h] rfl)) +variable {k : Type} [CommRing k] {G : Type} [Group G] + + /-- The Isomorphism between a `Fin n.succ.succ → C` and the product containing an object in the image of `contrPair` based on the given values. -/ def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ) diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 74b6e083..a1d485cc 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -23,6 +23,7 @@ interfact more generally with tensors. namespace IndexNotation namespace OverColor + open CategoryTheory open MonoidalCategory open TensorProduct @@ -661,10 +662,39 @@ def forget : MonoidalFunctor (OverColor C) (Rep k G) ⥤ (Discrete C ⥤ Rep k G obj F := Discrete.functor fun c => F.obj (incl.obj (Discrete.mk c)) map η := Discrete.natTrans fun c => η.app (incl.obj c) +variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F') + +noncomputable section + +def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))).V ≃ₗ[k] + (F.obj (Discrete.mk c)).V := + (PiTensorProduct.subsingletonEquiv 0 : + (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c) ) + +def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1 ) => c)) + ≅ F.obj (Discrete.mk c) := + Action.mkIso (forgetLiftAppV F c).toModuleIso + (fun g => by + refine LinearMap.ext (fun x => ?_) + simp only [forgetLiftAppV, Fin.isValue, LinearEquiv.toModuleIso_hom] + refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by + simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp, + Function.comp_apply, hy] + simp only [CategoryStruct.comp, Fin.isValue, Functor.id_obj, + PiTensorProduct.tprodCoeff_eq_smul_tprod, map_smul, LinearMap.coe_comp, LinearEquiv.coe_coe, + Function.comp_apply] + apply congrArg + erw [PiTensorProduct.subsingletonEquiv_apply_tprod] + simp only [lift, lift.obj', lift.objObj'_V_carrier, Fin.isValue] + erw [lift.objObj'_ρ_tprod] + erw [PiTensorProduct.subsingletonEquiv_apply_tprod] + rfl) + informal_definition forgetLift where math :≈ "The natural isomorphism between `lift (C := C) ⋙ forget` and `Functor.id (Discrete C ⥤ Rep k G)`." deps :≈ [``forget, ``lift] +end end OverColor end IndexNotation diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean index d8832454..cc98dadc 100644 --- a/HepLean/Tensors/Tree/Basic.lean +++ b/HepLean/Tensors/Tree/Basic.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Tensors.OverColor.Iso +import HepLean.Tensors.OverColor.Discrete +import HepLean.Tensors.OverColor.Lift import Mathlib.CategoryTheory.Monoidal.NaturalTransformation /-! @@ -31,16 +33,22 @@ structure TensorStruct where k_commRing : CommRing k /-- A `MonoidalFunctor` from `OverColor C` giving the rep corresponding to a map of colors `X → C`. -/ - F : MonoidalFunctor (OverColor C) (Rep k G) + FDiscrete : Discrete C ⥤ Rep k G /-- A map from `C` to `C`. An involution. -/ τ : C → C - /- - μContr : OverColor.contrPair C τ ⊗⋙ F ⟶ OverColor.const C ⊗⋙ F - dual : (OverColor.map τ ⊗⋙ F) ≅ F-/ + τ_involution : Function.Involutive τ + /-- The natural transformation describing contraction. -/ + contr : OverColor.Discrete.pairτ F τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G) + /-- The natural transformation describing the metric. -/ + metricNat : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FDiscrete + /-- The natural transformation describing the unit. -/ + unit : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.τPair FDiscrete τ /-- A specification of the dimension of each color in C. This will be used for explicit evaluation of tensors. -/ evalNo : C → ℕ +noncomputable section + namespace TensorStruct variable (S : TensorStruct) @@ -49,6 +57,113 @@ instance : CommRing S.k := S.k_commRing instance : Group S.G := S.G_group +/-- The lift of the functor `S.F` to a monoidal functor. -/ +def F : MonoidalFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete + +def metric (c : S.C) : S.F.obj (OverColor.mk ![c, c]) := + (OverColor.Discrete.pairIso S.FDiscrete c).hom.hom <| + (S.metricNat.app (Discrete.mk c)).hom (1 : S.k) + +def contrNLE {n : ℕ} {i j : Fin n} (h : i ≠ j) : 2 ≤ n := by + omega + +def contrNPred {n : ℕ} {i j : Fin n} (h : i ≠ j) : n.pred.pred.succ.succ = n := by + simp_all only [ne_eq, Nat.pred_eq_sub_one, Nat.succ_eq_add_one] + have hi : i < n := i.isLt + have hj : j < n := j.isLt + by_contra hn + have hn : n = 0 ∨ n =1 := by omega + cases hn + · omega + · omega + +def contrFstSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) : + Fin n.pred.pred.succ.succ := Fin.castOrderIso (contrNPred hineqj).symm i + +def contrSndSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) : + Fin n.pred.pred.succ := (Fin.predAbove 0 (contrFstSucc hineqj)).predAbove + (Fin.castOrderIso (contrNPred hineqj).symm j) + +@[simp] +lemma contrSndSucc_succAbove {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) : + (contrFstSucc hineqj).succAbove (contrSndSucc hineqj) = + Fin.castOrderIso (contrNPred hineqj).symm j := by + simp [contrFstSucc, contrSndSucc, Fin.succAbove, + Fin.predAbove] + split_ifs + · rename_i h1 h2 + rw [Fin.lt_def] at h1 h2 + simp_all [Fin.lt_def, Fin.ext_iff] + intro h + omega + · rename_i h1 h2 + rw [Fin.lt_def] at h1 h2 + simp_all [Fin.ext_iff] + rw [Fin.lt_def] + simp only [Fin.coe_cast, Fin.val_fin_lt] + rw [Fin.lt_def] + omega + · rename_i h1 h2 + rw [Fin.lt_def] at h1 h2 + simp_all [Fin.ext_iff] + rw [Fin.lt_def] + simp only [Fin.coe_cast, Fin.val_fin_lt] + omega + · rename_i h1 h2 + rw [Fin.lt_def] at h1 h2 + simp_all [Fin.ext_iff] + rw [Fin.lt_def] + simp only [Fin.coe_cast, Fin.val_fin_lt] + omega + + +def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C) + (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : + S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj (Discrete.mk (c i))) ⊗ + (OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) := + (S.F.mapIso (OverColor.equivToIso (OverColor.finExtractTwo i j))).trans <| + (S.F.mapIso (OverColor.mkSum (c ∘ (OverColor.finExtractTwo i j).symm))).trans <| + (S.F.μIso _ _).symm.trans <| by + refine tensorIso ?_ (S.F.mapIso (OverColor.mkIso (by ext x; simp))) + apply (S.F.mapIso (OverColor.mkSum (((c ∘ ⇑(OverColor.finExtractTwo i j).symm) ∘ Sum.inl)))).trans + apply (S.F.μIso _ _).symm.trans + apply tensorIso ?_ ?_ + · symm + apply (OverColor.forgetLiftApp S.FDiscrete (c i)).symm.trans + apply S.F.mapIso + apply OverColor.mkIso + funext x + fin_cases x + rfl + · symm + apply (OverColor.forgetLiftApp S.FDiscrete (S.τ (c i))).symm.trans + apply S.F.mapIso + apply OverColor.mkIso + funext x + fin_cases x + simp [h] + +def contrMap' {n : ℕ} (c : Fin n.succ.succ → S.C) + (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : + S.F.obj (OverColor.mk c) ⟶ + (OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) := + (S.contrIso c i j h).hom ≫ + (tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫ + (MonoidalCategory.leftUnitor _).hom + +def contrMap {n : ℕ} (c : Fin n → S.C) + (i j : Fin n) (hij : i ≠ j) (h : c j = S.τ (c i)) : + S.F.obj (OverColor.mk c) ⟶ + (OverColor.lift.obj S.FDiscrete).obj + (OverColor.mk ((c ∘ Fin.cast (contrNPred hij)) ∘ Fin.succAbove (contrFstSucc hij) ∘ + Fin.succAbove (contrSndSucc hij))) := by + refine (S.F.mapIso (OverColor.equivToIso (Fin.castOrderIso (contrNPred hij)).toEquiv.symm)).hom ≫ + S.contrMap' (c ∘ Fin.cast (contrNPred hij)) (contrFstSucc hij) (contrSndSucc hij) ?_ + simp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, contrSndSucc_succAbove, + Fin.castOrderIso_apply, Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self] + simpa [contrFstSucc] using h + + end TensorStruct /-- A syntax tree for tensor expressions. -/ @@ -60,12 +175,11 @@ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Typ | prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : TensorTree S c) (t1 : TensorTree S c1) : TensorTree S (Sum.elim c c1 ∘ finSumFinEquiv.symm) | smul {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c - | mult {n m : ℕ} {c : Fin n.succ → S.C} {c1 : Fin m.succ → S.C} : - (i : Fin n.succ) → (j : Fin m.succ) → TensorTree S c → TensorTree S c1 → - TensorTree S (Sum.elim (c ∘ Fin.succAbove i) (c1 ∘ Fin.succAbove j) ∘ finSumFinEquiv.symm) - | contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) → - (j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c → - TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j) + | contr {n : ℕ} {c : Fin n → S.C} : (i j : Fin n) → + (hij : i ≠ j) → (h : c j = S.τ (c i)) → TensorTree S c → + TensorTree S ((c ∘ Fin.cast (TensorStruct.contrNPred hij)) ∘ + Fin.succAbove (TensorStruct.contrFstSucc hij) ∘ + Fin.succAbove (TensorStruct.contrSndSucc hij)) | jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c → TensorTree S (Function.update c i (S.τ (c i))) | eval {n : ℕ} {c : Fin n.succ → S.C} : @@ -76,6 +190,7 @@ namespace TensorTree variable {S : TensorStruct} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c) +def metric : TensorTree S ![] open MonoidalCategory open TensorProduct @@ -86,8 +201,7 @@ def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun | perm _ t => t.size + 1 | smul _ t => t.size + 1 | prod t1 t2 => t1.size + t2.size + 1 - | mult _ _ t1 t2 => t1.size + t2.size + 1 - | contr _ _ _ t => t.size + 1 + | contr _ _ _ _ t => t.size + 1 | jiggle _ t => t.size + 1 | eval _ _ t => t.size + 1 @@ -102,6 +216,63 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over | smul a t => a • t.tensor | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) + | contr i j hij h t => (S.contrMap _ i j hij h).hom t.tensor + | jiggle i t => by + rename_i n c' + let T := (tensorNode (S.metric (S.τ (c' i)))) + let T2 := (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom + ((S.F.μ _ _).hom (T.tensor ⊗ₜ t.tensor)) + let e1 : Fin (2 + n) ≃ Fin (2 + n) := + (Equiv.swap (Fin.castAdd n (0 : Fin 2)) (Fin.natAdd 2 i)) + let T3 := (S.F.map ((OverColor.equivToIso e1).hom)).hom T2 + let T4 := (S.contrMap _ (Fin.castAdd n (0 : Fin 2)) (Fin.castAdd n (1 : Fin 2)) + (by + simp only [Fin.isValue, ne_eq, + Fin.ext_iff, Fin.coe_castAdd, Fin.val_zero, Fin.coe_natAdd] + omega) + (by + simp [e1] + rw [Equiv.swap_apply_of_ne_of_ne] + · simp [Fin.ext_iff] + rfl + · simp [Fin.ext_iff] + · simp [Fin.ext_iff] + omega)).hom T3 + refine (S.F.map ?_).hom T4 + refine (OverColor.equivToIso (Fin.castOrderIso (by simp : (2 + n).pred.pred = n)).toEquiv).hom ≫ ?_ + refine (OverColor.mkIso ?_).hom + funext x + simp + trans Sum.elim ![S.τ (c' i), S.τ (c' i)] c' (finSumFinEquiv.symm + (e1.symm (Fin.natAdd 2 x))) + congr + simp [Fin.ext_iff] + simp [Fin.succAbove] + split_ifs + · rename_i h1 h2 + rw [Fin.lt_def] at h1 h2 + simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc] + · rename_i h1 h2 + rw [Fin.lt_def] at h1 h2 + simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc] + simp [Fin.predAbove, Fin.lt_def] at h1 + · rename_i h1 h2 + rw [Fin.lt_def] at h1 h2 + simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc] + · simp + omega + simp [e1] + by_cases hi: x= i + · subst hi + simp + · rw [Equiv.swap_apply_of_ne_of_ne] + · simp + rw [Function.update] + simp [hi] + · simp [Fin.ext_iff] + · simp [Fin.ext_iff] + omega + | _ => 0 lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : @@ -110,3 +281,5 @@ lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : end end TensorTree + +end From 1ceffaa329850b7c275a940edd4a02cb4ab059b2 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 15 Oct 2024 11:23:08 +0000 Subject: [PATCH 2/4] feat: Unit and metric for Weyl --- HepLean/SpaceTime/WeylFermion/Basic.lean | 50 ++ .../SpaceTime/WeylFermion/Contraction.lean | 45 +- HepLean/SpaceTime/WeylFermion/Metric.lean | 213 ++++++++ HepLean/SpaceTime/WeylFermion/Two.lean | 484 ++++++++++++++++++ HepLean/SpaceTime/WeylFermion/Unit.lean | 159 ++++++ HepLean/Tensors/OverColor/Iso.lean | 5 + 6 files changed, 928 insertions(+), 28 deletions(-) create mode 100644 HepLean/SpaceTime/WeylFermion/Metric.lean create mode 100644 HepLean/SpaceTime/WeylFermion/Two.lean create mode 100644 HepLean/SpaceTime/WeylFermion/Unit.lean diff --git a/HepLean/SpaceTime/WeylFermion/Basic.lean b/HepLean/SpaceTime/WeylFermion/Basic.lean index 8cfeea95..df26bedb 100644 --- a/HepLean/SpaceTime/WeylFermion/Basic.lean +++ b/HepLean/SpaceTime/WeylFermion/Basic.lean @@ -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. diff --git a/HepLean/SpaceTime/WeylFermion/Contraction.lean b/HepLean/SpaceTime/WeylFermion/Contraction.lean index 7902b898..623a32f1 100644 --- a/HepLean/SpaceTime/WeylFermion/Contraction.lean +++ b/HepLean/SpaceTime/WeylFermion/Contraction.lean @@ -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 diff --git a/HepLean/SpaceTime/WeylFermion/Metric.lean b/HepLean/SpaceTime/WeylFermion/Metric.lean new file mode 100644 index 00000000..67e6f12d --- /dev/null +++ b/HepLean/SpaceTime/WeylFermion/Metric.lean @@ -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 diff --git a/HepLean/SpaceTime/WeylFermion/Two.lean b/HepLean/SpaceTime/WeylFermion/Two.lean new file mode 100644 index 00000000..087cc2b9 --- /dev/null +++ b/HepLean/SpaceTime/WeylFermion/Two.lean @@ -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 diff --git a/HepLean/SpaceTime/WeylFermion/Unit.lean b/HepLean/SpaceTime/WeylFermion/Unit.lean new file mode 100644 index 00000000..0066baec --- /dev/null +++ b/HepLean/SpaceTime/WeylFermion/Unit.lean @@ -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 diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean index f9c163ca..c2348c6c 100644 --- a/HepLean/Tensors/OverColor/Iso.lean +++ b/HepLean/Tensors/OverColor/Iso.lean @@ -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 := From ec69deaff22c1f92f5fbf8d1c5d9172c1a84e825 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 16 Oct 2024 16:38:36 +0000 Subject: [PATCH 3/4] refactor: Index notation --- HepLean.lean | 4 +- HepLean/Tensors/ComplexLorentz/Basic.lean | 99 +++- HepLean/Tensors/ComplexLorentz/ColorFun.lean | 497 ------------------ .../ComplexLorentz/ContrNatTransform.lean | 107 ---- HepLean/Tensors/ComplexLorentz/Examples.lean | 41 +- .../Tensors/ComplexLorentz/TensorStruct.lean | 36 -- HepLean/Tensors/OverColor/Discrete.lean | 9 +- HepLean/Tensors/OverColor/Iso.lean | 33 +- HepLean/Tensors/OverColor/Lift.lean | 8 + HepLean/Tensors/Tree/Basic.lean | 207 +++----- HepLean/Tensors/Tree/Dot.lean | 24 +- HepLean/Tensors/Tree/Elab.lean | 97 +++- 12 files changed, 298 insertions(+), 864 deletions(-) delete mode 100644 HepLean/Tensors/ComplexLorentz/ColorFun.lean delete mode 100644 HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean delete mode 100644 HepLean/Tensors/ComplexLorentz/TensorStruct.lean diff --git a/HepLean.lean b/HepLean.lean index 5a5b5442..59f67440 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -111,10 +111,7 @@ import HepLean.StandardModel.HiggsBoson.Potential import HepLean.StandardModel.Representations import HepLean.Tensors.Basic import HepLean.Tensors.ComplexLorentz.Basic -import HepLean.Tensors.ComplexLorentz.ColorFun -import HepLean.Tensors.ComplexLorentz.ContrNatTransform import HepLean.Tensors.ComplexLorentz.Examples -import HepLean.Tensors.ComplexLorentz.TensorStruct import HepLean.Tensors.Contraction import HepLean.Tensors.EinsteinNotation.Basic import HepLean.Tensors.EinsteinNotation.IndexNotation @@ -138,6 +135,7 @@ import HepLean.Tensors.IndexNotation.IndexString import HepLean.Tensors.IndexNotation.TensorIndex import HepLean.Tensors.MulActionTensor import HepLean.Tensors.OverColor.Basic +import HepLean.Tensors.OverColor.Discrete import HepLean.Tensors.OverColor.Functors import HepLean.Tensors.OverColor.Iso import HepLean.Tensors.OverColor.Lift diff --git a/HepLean/Tensors/ComplexLorentz/Basic.lean b/HepLean/Tensors/ComplexLorentz/Basic.lean index 6098084b..dc557437 100644 --- a/HepLean/Tensors/ComplexLorentz/Basic.lean +++ b/HepLean/Tensors/ComplexLorentz/Basic.lean @@ -4,7 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Tensors.OverColor.Basic +import HepLean.Tensors.Tree.Dot +import HepLean.SpaceTime.WeylFermion.Contraction +import HepLean.SpaceTime.WeylFermion.Metric +import HepLean.SpaceTime.WeylFermion.Unit +import HepLean.SpaceTime.LorentzVector.Complex.Contraction +import HepLean.SpaceTime.LorentzVector.Complex.Metric +import HepLean.SpaceTime.LorentzVector.Complex.Unit import HepLean.Mathematics.PiTensorProduct +import HepLean.SpaceTime.PauliMatrices.AsTensor /-! ## Complex Lorentz tensors @@ -30,34 +38,71 @@ inductive Color | up : Color | down : Color -/-- The involution taking a colour to its dual. -/ -def τ : Color → Color - | Color.upL => Color.downL - | Color.downL => Color.upL - | Color.upR => Color.downR - | Color.downR => Color.upR - | Color.up => Color.down - | Color.down => Color.up - -/-- The function taking a color to the dimension of the basis of vectors. -/ -def evalNo : Color → ℕ - | Color.upL => 2 - | Color.downL => 2 - | Color.upR => 2 - | Color.downR => 2 - | Color.up => 4 - | Color.down => 4 - noncomputable section -/-- The corresponding representations associated with a color. -/ -def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) := - match c with - | Color.upL => Fermion.altLeftHanded - | Color.downL => Fermion.leftHanded - | Color.upR => Fermion.altRightHanded - | Color.downR => Fermion.rightHanded - | Color.up => Lorentz.complexContr - | Color.down => Lorentz.complexCo + +/-- The tensor structure for complex Lorentz tensors. -/ +def complexLorentzTensor : TensorStruct where + C := Fermion.Color + G := SL(2, ℂ) + G_group := inferInstance + k := ℂ + k_commRing := inferInstance + FDiscrete := Discrete.functor fun c => + match c with + | Color.upL => Fermion.leftHanded + | Color.downL => Fermion.altLeftHanded + | Color.upR => Fermion.rightHanded + | Color.downR => Fermion.altRightHanded + | Color.up => Lorentz.complexContr + | Color.down => Lorentz.complexCo + τ := fun c => + match c with + | Color.upL => Color.downL + | Color.downL => Color.upL + | Color.upR => Color.downR + | Color.downR => Color.upR + | Color.up => Color.down + | Color.down => Color.up + τ_involution c := by + match c with + | Color.upL => rfl + | Color.downL => rfl + | Color.upR => rfl + | Color.downR => rfl + | Color.up => rfl + | Color.down => rfl + contr := Discrete.natTrans fun c => + match c with + | Discrete.mk Color.upL => Fermion.leftAltContraction + | Discrete.mk Color.downL => Fermion.altLeftContraction + | Discrete.mk Color.upR => Fermion.rightAltContraction + | Discrete.mk Color.downR => Fermion.altRightContraction + | Discrete.mk Color.up => Lorentz.contrCoContraction + | Discrete.mk Color.down => Lorentz.coContrContraction + metric := Discrete.natTrans fun c => + match c with + | Discrete.mk Color.upL => Fermion.leftMetric + | Discrete.mk Color.downL => Fermion.altLeftMetric + | Discrete.mk Color.upR => Fermion.rightMetric + | Discrete.mk Color.downR => Fermion.altRightMetric + | Discrete.mk Color.up => Lorentz.contrMetric + | Discrete.mk Color.down => Lorentz.coMetric + unit := Discrete.natTrans fun c => + match c with + | Discrete.mk Color.upL => Fermion.altLeftLeftUnit + | Discrete.mk Color.downL => Fermion.leftAltLeftUnit + | Discrete.mk Color.upR => Fermion.altRightRightUnit + | Discrete.mk Color.downR => Fermion.rightAltRightUnit + | Discrete.mk Color.up => Lorentz.coContrUnit + | Discrete.mk Color.down => Lorentz.contrCoUnit + evalNo := fun c => + match c with + | Color.upL => 2 + | Color.downL => 2 + | Color.upR => 2 + | Color.downR => 2 + | Color.up => 4 + | Color.down => 4 end end Fermion diff --git a/HepLean/Tensors/ComplexLorentz/ColorFun.lean b/HepLean/Tensors/ComplexLorentz/ColorFun.lean deleted file mode 100644 index 66c72874..00000000 --- a/HepLean/Tensors/ComplexLorentz/ColorFun.lean +++ /dev/null @@ -1,497 +0,0 @@ -/- -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.Tensors.ComplexLorentz.Basic -import HepLean.Tensors.OverColor.Basic -import HepLean.Mathematics.PiTensorProduct -/-! - -## Monodial functor from color cat. - --/ -namespace Fermion - -noncomputable section - -open Matrix -open MatrixGroups -open Complex -open TensorProduct -open IndexNotation -open CategoryTheory - -/-- The linear equivalence between `colorToRep c1` and `colorToRep c2` when `c1 = c2`. -/ -def colorToRepCongr {c1 c2 : Color} (h : c1 = c2) : colorToRep c1 ≃ₗ[ℂ] colorToRep c2 where - toFun := Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h) - invFun := (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)).symm - map_add' x y := by - subst h - rfl - map_smul' x y := by - subst h - rfl - left_inv x := Equiv.symm_apply_apply (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)) x - right_inv x := Equiv.apply_symm_apply (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)) x - -lemma colorToRepCongr_comm_ρ {c1 c2 : Color} (h : c1 = c2) (M : SL(2, ℂ)) (x : (colorToRep c1)) : - (colorToRepCongr h) ((colorToRep c1).ρ M x) = (colorToRep c2).ρ M ((colorToRepCongr h) x) := by - subst h - rfl - -namespace colorFun - -/-- Given a object in `OverColor Color` the correpsonding tensor product of representations. -/ -def obj' (f : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of { - toFun := fun M => PiTensorProduct.map (fun x => (colorToRep (f.hom x)).ρ M), - map_one' := by - simp - map_mul' := fun M N => by - simp only [CategoryTheory.Functor.id_obj, _root_.map_mul] - ext x : 2 - simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]} - -lemma obj'_ρ (f : OverColor Color) (M : SL(2, ℂ)) : (obj' f).ρ M = - PiTensorProduct.map (fun x => (colorToRep (f.hom x)).ρ M) := rfl - -lemma obj'_ρ_tprod (f : OverColor Color) (M : SL(2, ℂ)) - (x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) : - (obj' f).ρ M ((PiTensorProduct.tprod ℂ) x) = - PiTensorProduct.tprod ℂ (fun i => (colorToRep (f.hom i)).ρ M (x i)) := by - rw [obj'_ρ] - change (PiTensorProduct.map fun x => (colorToRep (f.hom x)).ρ M) ((PiTensorProduct.tprod ℂ) x) = - (PiTensorProduct.tprod ℂ) fun i => ((colorToRep (f.hom i)).ρ M) (x i) - rw [PiTensorProduct.map_tprod] - -/-- Given a morphism in `OverColor Color` the corresopnding linear equivalence between `obj' _` - induced by reindexing. -/ -def mapToLinearEquiv' {f g : OverColor Color} (m : f ⟶ g) : (obj' f).V ≃ₗ[ℂ] (obj' g).V := - (PiTensorProduct.reindex ℂ (fun x => colorToRep (f.hom x)) (OverColor.Hom.toEquiv m)).trans - (PiTensorProduct.congr (fun i => colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))) - -lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g) - (x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) : - mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) = - PiTensorProduct.tprod ℂ (fun i => (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i)) - (x ((OverColor.Hom.toEquiv m).symm i))) := by - rw [mapToLinearEquiv'] - simp only [CategoryTheory.Functor.id_obj, LinearEquiv.trans_apply] - change (PiTensorProduct.congr fun i => colorToRepCongr _) - ((PiTensorProduct.reindex ℂ (fun x => CoeSort.coe (colorToRep (f.hom x))) - (OverColor.Hom.toEquiv m)) ((PiTensorProduct.tprod ℂ) x)) = _ - rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod] - rfl - -/-- Given a morphism in `OverColor Color` the corresopnding map of representations induced by - reindexing. -/ -def map' {f g : OverColor Color} (m : f ⟶ g) : obj' f ⟶ obj' g where - hom := (mapToLinearEquiv' m).toLinearMap - comm M := by - ext x : 2 - refine PiTensorProduct.induction_on' x ?_ (by - intro x y hx hy - simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp, - Function.comp_apply, hy]) - intro r x - simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, - _root_.map_smul, ModuleCat.coe_comp, Function.comp_apply] - apply congrArg - change (mapToLinearEquiv' m) (((obj' f).ρ M) ((PiTensorProduct.tprod ℂ) x)) = - ((obj' g).ρ M) ((mapToLinearEquiv' m) ((PiTensorProduct.tprod ℂ) x)) - rw [mapToLinearEquiv'_tprod, obj'_ρ_tprod] - erw [mapToLinearEquiv'_tprod, obj'_ρ_tprod] - apply congrArg - funext i - rw [colorToRepCongr_comm_ρ] - -end colorFun - -/-- The functor between `OverColor Color` and `Rep ℂ SL(2, ℂ)` taking a map of colors - to the corresponding tensor product representation. -/ -@[simps! obj_V_carrier] -def colorFun : OverColor Color ⥤ Rep ℂ SL(2, ℂ) where - obj := colorFun.obj' - map := colorFun.map' - map_id f := by - ext x - refine PiTensorProduct.induction_on' x (fun r x => ?_) (fun x y hx hy => by - simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp, - Function.comp_apply, hy]) - simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, - _root_.map_smul, Action.id_hom, ModuleCat.id_apply] - apply congrArg - erw [colorFun.mapToLinearEquiv'_tprod] - exact congrArg _ (funext (fun i => rfl)) - map_comp {X Y Z} f g := by - ext x - refine PiTensorProduct.induction_on' x (fun r x => ?_) (fun x y hx hy => by - simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp, - Function.comp_apply, hy]) - simp only [Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, _root_.map_smul, - Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply] - apply congrArg - rw [colorFun.map', colorFun.map', colorFun.map'] - change (colorFun.mapToLinearEquiv' (CategoryTheory.CategoryStruct.comp f g)) - ((PiTensorProduct.tprod ℂ) x) = - (colorFun.mapToLinearEquiv' g) ((colorFun.mapToLinearEquiv' f) ((PiTensorProduct.tprod ℂ) x)) - rw [colorFun.mapToLinearEquiv'_tprod, colorFun.mapToLinearEquiv'_tprod] - erw [colorFun.mapToLinearEquiv'_tprod] - refine congrArg _ (funext (fun i => ?_)) - simp only [colorToRepCongr, Function.comp_apply, Equiv.cast_symm, LinearEquiv.coe_mk, - Equiv.cast_apply, cast_cast, cast_inj] - rfl - -namespace colorFun - -open CategoryTheory -open MonoidalCategory - -lemma map_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom i))) - (f : X ⟶ Y) : (colorFun.map f).hom (PiTensorProduct.tprod ℂ p) = - PiTensorProduct.tprod ℂ fun (i : Y.left) => colorToRepCongr - (OverColor.Hom.toEquiv_comp_inv_apply f i) (p ((OverColor.Hom.toEquiv f).symm i)) := by - change (colorFun.map' f).hom ((PiTensorProduct.tprod ℂ) p) = _ - simp only [map', mapToLinearEquiv', Functor.id_obj] - erw [LinearEquiv.trans_apply] - change (PiTensorProduct.congr fun i => colorToRepCongr _) - ((PiTensorProduct.reindex ℂ (fun x => _) (OverColor.Hom.toEquiv f)) - ((PiTensorProduct.tprod ℂ) p)) = _ - rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod] - -lemma obj_ρ_tprod (f : OverColor Color) (M : SL(2, ℂ)) - (x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) : - (colorFun.obj f).ρ M ((PiTensorProduct.tprod ℂ) x) = - PiTensorProduct.tprod ℂ (fun i => (colorToRep (f.hom i)).ρ M (x i)) := by - exact obj'_ρ_tprod _ _ _ - -@[simp] -lemma obj_ρ_empty (g : SL(2, ℂ)) : (colorFun.obj (𝟙_ (OverColor Color))).ρ g = LinearMap.id := by - erw [colorFun.obj'_ρ] - ext x - refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by - simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp, - Function.comp_apply, hy] - erw [hx, hy] - rfl - simp only [OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj, - OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.tprodCoeff_eq_smul_tprod, - _root_.map_smul, PiTensorProduct.map_tprod, LinearMap.id_coe, id_eq] - apply congrArg - apply congrArg - funext i - exact Empty.elim i - -/-- The unit natural isomorphism. -/ -def ε : 𝟙_ (Rep ℂ SL(2, ℂ)) ≅ colorFun.obj (𝟙_ (OverColor Color)) where - hom := { - hom := (PiTensorProduct.isEmptyEquiv Empty).symm.toLinearMap - comm := fun M => by - refine LinearMap.ext (fun x => ?_) - simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorUnit_left, - OverColor.instMonoidalCategoryStruct_tensorUnit_hom, - Action.instMonoidalCategory_tensorUnit_V, Action.tensorUnit_ρ', Functor.id_obj, - Category.id_comp, LinearEquiv.coe_coe] - erw [obj_ρ_empty M] - rfl} - inv := { - hom := (PiTensorProduct.isEmptyEquiv Empty).toLinearMap - comm := fun M => by - refine LinearMap.ext (fun x => ?_) - simp only [Action.instMonoidalCategory_tensorUnit_V, colorFun_obj_V_carrier, - OverColor.instMonoidalCategoryStruct_tensorUnit_left, - OverColor.instMonoidalCategoryStruct_tensorUnit_hom, Functor.id_obj, Action.tensorUnit_ρ'] - erw [obj_ρ_empty M] - rfl} - hom_inv_id := by - ext1 - simp only [Action.instMonoidalCategory_tensorUnit_V, CategoryStruct.comp, - OverColor.instMonoidalCategoryStruct_tensorUnit_hom, - OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj, Action.Hom.comp_hom, - colorFun_obj_V_carrier, LinearEquiv.comp_coe, LinearEquiv.symm_trans_self, - LinearEquiv.refl_toLinearMap, Action.id_hom] - rfl - inv_hom_id := by - ext1 - simp only [CategoryStruct.comp, OverColor.instMonoidalCategoryStruct_tensorUnit_hom, - OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj, Action.Hom.comp_hom, - colorFun_obj_V_carrier, Action.instMonoidalCategory_tensorUnit_V, LinearEquiv.comp_coe, - LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, Action.id_hom] - rfl - -/-- An auxillary equivalence, and trivial, of modules needed to define `μModEquiv`. -/ -def colorToRepSumEquiv {X Y : OverColor Color} (i : X.left ⊕ Y.left) : - Sum.elim (fun i => colorToRep (X.hom i)) (fun i => colorToRep (Y.hom i)) i ≃ₗ[ℂ] - colorToRep (Sum.elim X.hom Y.hom i) := - match i with - | Sum.inl _ => LinearEquiv.refl _ _ - | Sum.inr _ => LinearEquiv.refl _ _ - -/-- The equivalence of modules corresonding to the tensorate. -/ -def μModEquiv (X Y : OverColor Color) : - (colorFun.obj X ⊗ colorFun.obj Y).V ≃ₗ[ℂ] colorFun.obj (X ⊗ Y) := - HepLean.PiTensorProduct.tmulEquiv ≪≫ₗ PiTensorProduct.congr colorToRepSumEquiv - -lemma μModEquiv_tmul_tprod {X Y : OverColor Color}(p : (i : X.left) → (colorToRep (X.hom i))) - (q : (i : Y.left) → (colorToRep (Y.hom i))) : - (μModEquiv X Y) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) = - (PiTensorProduct.tprod ℂ) fun i => - (colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor p q i) := by - rw [μModEquiv] - simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V, - Functor.id_obj, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj] - rw [LinearEquiv.trans_apply] - erw [HepLean.PiTensorProduct.tmulEquiv_tmul_tprod] - change (PiTensorProduct.congr colorToRepSumEquiv) ((PiTensorProduct.tprod ℂ) - (HepLean.PiTensorProduct.elimPureTensor p q)) = _ - rw [PiTensorProduct.congr_tprod] - rfl - -/-- The natural isomorphism corresponding to the tensorate. -/ -def μ (X Y : OverColor Color) : colorFun.obj X ⊗ colorFun.obj Y ≅ colorFun.obj (X ⊗ Y) where - hom := { - hom := (μModEquiv X Y).toLinearMap - comm := fun M => by - refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_) - simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp, - Action.instMonoidalCategory_tensorObj_V, Action.tensor_ρ', LinearMap.coe_comp, - Function.comp_apply] - change (μModEquiv X Y) (((((colorFun.obj X).ρ M) (PiTensorProduct.tprod ℂ p)) ⊗ₜ[ℂ] - (((colorFun.obj Y).ρ M) (PiTensorProduct.tprod ℂ q)))) = ((colorFun.obj (X ⊗ Y)).ρ M) - ((μModEquiv X Y) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)) - rw [μModEquiv_tmul_tprod] - erw [obj'_ρ_tprod, obj'_ρ_tprod, obj'_ρ_tprod] - rw [μModEquiv_tmul_tprod] - apply congrArg - funext i - match i with - | Sum.inl i => - rfl - | Sum.inr i => - rfl - } - inv := { - hom := (μModEquiv X Y).symm.toLinearMap - comm := fun M => by - simp only [Action.instMonoidalCategory_tensorObj_V, CategoryStruct.comp, - colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.tensor_ρ'] - erw [LinearEquiv.eq_comp_toLinearMap_symm,LinearMap.comp_assoc, - LinearEquiv.toLinearMap_symm_comp_eq] - refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_) - simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp, - Action.instMonoidalCategory_tensorObj_V, Action.tensor_ρ', LinearMap.coe_comp, - Function.comp_apply] - symm - change (μModEquiv X Y) (((((colorFun.obj X).ρ M) (PiTensorProduct.tprod ℂ p)) ⊗ₜ[ℂ] - (((colorFun.obj Y).ρ M) (PiTensorProduct.tprod ℂ q)))) = ((colorFun.obj (X ⊗ Y)).ρ M) - ((μModEquiv X Y) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)) - rw [μModEquiv_tmul_tprod] - erw [obj'_ρ_tprod, obj'_ρ_tprod, obj'_ρ_tprod] - rw [μModEquiv_tmul_tprod] - apply congrArg - funext i - match i with - | Sum.inl i => - rfl - | Sum.inr i => - rfl} - hom_inv_id := by - ext1 - simp only [Action.instMonoidalCategory_tensorObj_V, CategoryStruct.comp, Action.Hom.comp_hom, - colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.comp_coe, - LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, Action.id_hom] - rfl - inv_hom_id := by - ext1 - simp only [CategoryStruct.comp, Action.instMonoidalCategory_tensorObj_V, Action.Hom.comp_hom, - colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.comp_coe, - LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, Action.id_hom] - rfl - -lemma μ_tmul_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom i))) - (q : (i : Y.left) → (colorToRep (Y.hom i))) : - (μ X Y).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) = - (PiTensorProduct.tprod ℂ) fun i => - (colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor p q i) := by - exact μModEquiv_tmul_tprod p q - -lemma μ_natural_left {X Y : OverColor Color} (f : X ⟶ Y) (Z : OverColor Color) : - MonoidalCategory.whiskerRight (colorFun.map f) (colorFun.obj Z) ≫ (μ Y Z).hom = - (μ X Z).hom ≫ colorFun.map (MonoidalCategory.whiskerRight f Z) := by - ext1 - refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_) - simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp, - Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V, - Action.instMonoidalCategory_whiskerRight_hom, LinearMap.coe_comp, Function.comp_apply] - change _ = (colorFun.map (MonoidalCategory.whiskerRight f Z)).hom - ((μ X Z).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)) - rw [μ_tmul_tprod] - change _ = (colorFun.map (f ▷ Z)).hom - ((PiTensorProduct.tprod ℂ) fun i => (colorToRepSumEquiv i) - (HepLean.PiTensorProduct.elimPureTensor p q i)) - rw [colorFun.map_tprod] - have h1 : (((colorFun.map f).hom ▷ (colorFun.obj Z).V) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] - (PiTensorProduct.tprod ℂ) q)) = ((colorFun.map f).hom - ((PiTensorProduct.tprod ℂ) p) ⊗ₜ[ℂ] ((PiTensorProduct.tprod ℂ) q)) := by rfl - erw [h1] - rw [colorFun.map_tprod] - change (μ Y Z).hom.hom (((PiTensorProduct.tprod ℂ) fun i => (colorToRepCongr _) - (p ((OverColor.Hom.toEquiv f).symm i))) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) = _ - rw [μ_tmul_tprod] - apply congrArg - funext i - match i with - | Sum.inl i => rfl - | Sum.inr i => rfl - -lemma μ_natural_right {X Y : OverColor Color} (X' : OverColor Color) (f : X ⟶ Y) : - MonoidalCategory.whiskerLeft (colorFun.obj X') (colorFun.map f) ≫ (μ X' Y).hom = - (μ X' X).hom ≫ colorFun.map (MonoidalCategory.whiskerLeft X' f) := by - ext1 - refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_) - simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp, - Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V, - Action.instMonoidalCategory_whiskerLeft_hom, LinearMap.coe_comp, Function.comp_apply] - change _ = (colorFun.map (X' ◁ f)).hom ((μ X' X).hom.hom - ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)) - rw [μ_tmul_tprod] - change _ = (colorFun.map (X' ◁ f)).hom ((PiTensorProduct.tprod ℂ) fun i => - (colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor p q i)) - rw [map_tprod] - have h1 : (((colorFun.obj X').V ◁ (colorFun.map f).hom) - ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)) - = ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (colorFun.map f).hom ((PiTensorProduct.tprod ℂ) q)) := by - rfl - erw [h1] - rw [map_tprod] - change (μ X' Y).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) fun i => - (colorToRepCongr _) (q ((OverColor.Hom.toEquiv f).symm i))) = _ - rw [μ_tmul_tprod] - apply congrArg - funext i - match i with - | Sum.inl i => rfl - | Sum.inr i => rfl - -lemma associativity (X Y Z : OverColor Color) : - whiskerRight (μ X Y).hom (colorFun.obj Z) ≫ - (μ (X ⊗ Y) Z).hom ≫ colorFun.map (associator X Y Z).hom = - (associator (colorFun.obj X) (colorFun.obj Y) (colorFun.obj Z)).hom ≫ - whiskerLeft (colorFun.obj X) (μ Y Z).hom ≫ (μ X (Y ⊗ Z)).hom := by - ext1 - refine HepLean.PiTensorProduct.induction_assoc' (fun p q m => ?_) - simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp, - Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V, - Action.instMonoidalCategory_whiskerRight_hom, LinearMap.coe_comp, Function.comp_apply, - Action.instMonoidalCategory_whiskerLeft_hom, Action.instMonoidalCategory_associator_hom_hom] - change (colorFun.map (α_ X Y Z).hom).hom ((μ (X ⊗ Y) Z).hom.hom - ((((μ X Y).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] - (PiTensorProduct.tprod ℂ) q)) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) m))) = - (μ X (Y ⊗ Z)).hom.hom ((((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] ((μ Y Z).hom.hom - ((PiTensorProduct.tprod ℂ) q ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) m))))) - rw [μ_tmul_tprod, μ_tmul_tprod] - change (colorFun.map (α_ X Y Z).hom).hom ((μ (X ⊗ Y) Z).hom.hom - (((PiTensorProduct.tprod ℂ) fun i => (colorToRepSumEquiv i) - (HepLean.PiTensorProduct.elimPureTensor p q i)) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) m)) = - (μ X (Y ⊗ Z)).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) fun i => - (colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor q m i)) - rw [μ_tmul_tprod, μ_tmul_tprod] - erw [map_tprod] - apply congrArg - funext i - match i with - | Sum.inl i => rfl - | Sum.inr (Sum.inl i) => rfl - | Sum.inr (Sum.inr i) => rfl - -lemma left_unitality (X : OverColor Color) : (leftUnitor (colorFun.obj X)).hom = - whiskerRight colorFun.ε.hom (colorFun.obj X) ≫ - (μ (𝟙_ (OverColor Color)) X).hom ≫ colorFun.map (leftUnitor X).hom := by - ext1 - apply HepLean.PiTensorProduct.induction_mod_tmul (fun x q => ?_) - simp only [colorFun_obj_V_carrier, Equivalence.symm_inverse, - Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, - Action.instMonoidalCategory_tensorUnit_V, Functor.id_obj, - Action.instMonoidalCategory_leftUnitor_hom_hom, CategoryStruct.comp, Action.Hom.comp_hom, - Action.instMonoidalCategory_tensorObj_V, OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorUnit_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, - Action.instMonoidalCategory_whiskerRight_hom, LinearMap.coe_comp, Function.comp_apply] - change TensorProduct.lid ℂ (colorFun.obj X) (x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) = - (colorFun.map (λ_ X).hom).hom ((μ (𝟙_ (OverColor Color)) X).hom.hom - ((((PiTensorProduct.isEmptyEquiv Empty).symm x) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q))) - simp only [Functor.id_obj, lid_tmul, colorFun_obj_V_carrier, - OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorUnit_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V, - Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, - OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.isEmptyEquiv, - LinearEquiv.coe_symm_mk] - rw [TensorProduct.smul_tmul, TensorProduct.tmul_smul] - erw [LinearMap.map_smul, LinearMap.map_smul] - apply congrArg - change _ = (colorFun.map (λ_ X).hom).hom ((μ (𝟙_ (OverColor Color)) X).hom.hom - ((PiTensorProduct.tprod ℂ) _ ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)) - rw [μ_tmul_tprod] - erw [map_tprod] - rfl - -lemma right_unitality (X : OverColor Color) : (MonoidalCategory.rightUnitor (colorFun.obj X)).hom = - whiskerLeft (colorFun.obj X) ε.hom ≫ - (μ X (𝟙_ (OverColor Color))).hom ≫ colorFun.map (MonoidalCategory.rightUnitor X).hom := by - ext1 - apply HepLean.PiTensorProduct.induction_tmul_mod (fun p x => ?_) - simp only [colorFun_obj_V_carrier, Functor.id_obj, Equivalence.symm_inverse, - Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, - Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_rightUnitor_hom_hom, - CategoryStruct.comp, Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V, - OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorUnit_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_whiskerLeft_hom, - LinearMap.coe_comp, Function.comp_apply] - change TensorProduct.rid ℂ (colorFun.obj X) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] x) = - (colorFun.map (ρ_ X).hom).hom ((μ X (𝟙_ (OverColor Color))).hom.hom - ((((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] ((PiTensorProduct.isEmptyEquiv Empty).symm x))))) - simp only [Functor.id_obj, rid_tmul, colorFun_obj_V_carrier, - OverColor.instMonoidalCategoryStruct_tensorObj_left, - OverColor.instMonoidalCategoryStruct_tensorUnit_left, - OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V, - Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, - OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.isEmptyEquiv, - LinearEquiv.coe_symm_mk, tmul_smul] - erw [LinearMap.map_smul, LinearMap.map_smul] - apply congrArg - change _ = (colorFun.map (ρ_ X).hom).hom ((μ X (𝟙_ (OverColor Color))).hom.hom - ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) _)) - rw [μ_tmul_tprod] - erw [map_tprod] - rfl - -end colorFun - -/-- The monoidal functor between `OverColor Color` and `Rep ℂ SL(2, ℂ)` taking a map of colors - to the corresponding tensor product representation. -/ -def colorFunMon : MonoidalFunctor (OverColor Color) (Rep ℂ SL(2, ℂ)) where - toFunctor := colorFun - ε := colorFun.ε.hom - μ X Y := (colorFun.μ X Y).hom - μ_natural_left := colorFun.μ_natural_left - μ_natural_right := colorFun.μ_natural_right - associativity := colorFun.associativity - left_unitality := colorFun.left_unitality - right_unitality := colorFun.right_unitality - -end -end Fermion diff --git a/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean b/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean deleted file mode 100644 index 6ea9e115..00000000 --- a/HepLean/Tensors/ComplexLorentz/ContrNatTransform.lean +++ /dev/null @@ -1,107 +0,0 @@ -/- -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.Tensors.OverColor.Basic -import HepLean.Tensors.ComplexLorentz.ColorFun -import HepLean.Mathematics.PiTensorProduct -/-! - -## The contraction monoidal natural transformation - --/ - -namespace Fermion - -noncomputable section - -open Matrix -open MatrixGroups -open Complex -open TensorProduct -open IndexNotation -open CategoryTheory -open MonoidalCategory - -namespace pairwiseRepFun - -/-- Given an object `c : OverColor Color` the representation defined by - `⨂[R] x, colorToRep (c.hom x) ⊗[R] colorToRep (τ (c.hom x))`. -/ -def obj' (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of { - toFun := fun M => PiTensorProduct.map (fun x => - TensorProduct.map ((colorToRep (c.hom x)).ρ M) ((colorToRep (τ (c.hom x))).ρ M)), - map_one' := by - simp - map_mul' := fun x y => by - simp only [Functor.id_obj, _root_.map_mul] - ext x' : 2 - simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply] - apply congrArg - funext i - change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _) (x' i) - rw [← TensorProduct.map_comp] - rfl} - -/-- Given a morphism in `OverColor Color` the corresopnding linear equivalence between `obj' _` - induced by reindexing. -/ -def mapToLinearEquiv' {f g : OverColor Color} (m : f ⟶ g) : (obj' f).V ≃ₗ[ℂ] (obj' g).V := - (PiTensorProduct.reindex ℂ (fun x => (colorToRep (f.hom x)).V ⊗[ℂ] (colorToRep (τ (f.hom x))).V) - (OverColor.Hom.toEquiv m)).trans - (PiTensorProduct.congr (fun i => - TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i)) - ((colorToRepCongr (congrArg τ (OverColor.Hom.toEquiv_symm_apply m i)))))) - -lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g) - (x : (i : f.left) → (colorToRep (f.hom i)).V ⊗[ℂ] (colorToRep (τ (f.hom i))).V) : - mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) = - PiTensorProduct.tprod ℂ fun i => - (TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i)) - (colorToRepCongr (mapToLinearEquiv'.proof_4 m i))) (x ((OverColor.Hom.toEquiv m).symm i)) := by - simp only [mapToLinearEquiv', Functor.id_obj, LinearEquiv.trans_apply] - change (PiTensorProduct.congr fun i => TensorProduct.congr (colorToRepCongr _) - (colorToRepCongr _)) ((PiTensorProduct.reindex ℂ - (fun x => ↑(colorToRep (f.hom x)).V ⊗[ℂ] ↑(colorToRep (τ (f.hom x))).V) - (OverColor.Hom.toEquiv m)) ((PiTensorProduct.tprod ℂ) x)) = _ - rw [PiTensorProduct.reindex_tprod] - erw [PiTensorProduct.congr_tprod] - rfl - -end pairwiseRepFun - -/- - -def contrPairPairwiseRep (c : OverColor Color) : - (colorFunMon.obj c) ⊗ colorFunMon.obj ((OverColor.map τ).obj c) ⟶ - pairwiseRep c where - hom := TensorProduct.lift (PiTensorProduct.map₂ (fun x => - TensorProduct.mk ℂ (colorToRep (c.hom x)).V (colorToRep (τ (c.hom x))).V)) - comm M := by - refine HepLean.PiTensorProduct.induction_tmul (fun x y => ?_) - simp only [Functor.id_obj, CategoryStruct.comp, Action.instMonoidalCategory_tensorObj_V, - Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, - Action.FunctorCategoryEquivalence.functor_obj_obj, Action.tensor_ρ', LinearMap.coe_comp, - Function.comp_apply] - change (TensorProduct.lift - (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V - ↑(colorToRep (τ (c.hom x))).V)) - ((TensorProduct.map _ _) - ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y)) = _ - rw [TensorProduct.map_tmul] - erw [colorFun.obj_ρ_tprod, colorFun.obj_ρ_tprod] - simp only [Functor.id_obj, lift.tmul] - erw [PiTensorProduct.map₂_tprod_tprod] - change _ = ((pairwiseRep c).ρ M) - ((TensorProduct.lift - (PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V - ↑(colorToRep (τ (c.hom x))).V)) - ((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y)) - simp only [mk_apply, Functor.id_obj, lift.tmul] - rw [PiTensorProduct.map₂_tprod_tprod] - simp only [pairwiseRep, Functor.id_obj, Rep.coe_of, Rep.of_ρ, MonoidHom.coe_mk, OneHom.coe_mk, - mk_apply] - erw [PiTensorProduct.map_tprod] - rfl --/ -end -end Fermion diff --git a/HepLean/Tensors/ComplexLorentz/Examples.lean b/HepLean/Tensors/ComplexLorentz/Examples.lean index d5894607..4dd9c4a0 100644 --- a/HepLean/Tensors/ComplexLorentz/Examples.lean +++ b/HepLean/Tensors/ComplexLorentz/Examples.lean @@ -3,8 +3,8 @@ 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.Tensors.Tree.Basic -import HepLean.Tensors.ComplexLorentz.TensorStruct +import HepLean.Tensors.Tree.Elab +import HepLean.Tensors.ComplexLorentz.Basic /-! ## The tensor structure for complex Lorentz tensors @@ -22,21 +22,36 @@ open CategoryTheory noncomputable section -namespace complexLorentzTensor +namespace Fermion -/-- The color map for a 2d tensor with the first index up and the second index down. -/ -def upDown : Fin 2 → complexLorentzTensor.C - | 0 => Fermion.Color.up - | 1 => Fermion.Color.down +/-! -variable (T S : complexLorentzTensor.F.obj (OverColor.mk upDown)) +## Example tensor trees -/- -import HepLean.Tensors.Tree.Elab +-/ +open MatrixGroups +open Matrix +example (v : Fermion.leftHanded) : TensorTree complexLorentzTensor ![Color.upL] := + {v | i}ᵀ + +example (v : Fermion.leftHanded ⊗ Lorentz.complexContr) : + TensorTree complexLorentzTensor ![Color.upL, Color.up] := + {v | i j}ᵀ -#check {T | i m ⊗ S | m l}ᵀ.dot -#check {T | i m ⊗ S | l τ(m)}ᵀ.dot +example : + TensorTree complexLorentzTensor ![Color.downR, Color.downR] := + {Fermion.altRightMetric | μ j}ᵀ + +lemma fin_three_expand {R : Type} (f : Fin 3 → R) : f = ![f 0, f 1, f 2]:= by + funext x + fin_cases x <;> rfl +/- +example : True := + let f := + {Lorentz.coMetric | + μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ + sorry -/ -end complexLorentzTensor +end Fermion end diff --git a/HepLean/Tensors/ComplexLorentz/TensorStruct.lean b/HepLean/Tensors/ComplexLorentz/TensorStruct.lean deleted file mode 100644 index d08dda5c..00000000 --- a/HepLean/Tensors/ComplexLorentz/TensorStruct.lean +++ /dev/null @@ -1,36 +0,0 @@ -/- -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.Tensors.Tree.Basic -import HepLean.Tensors.ComplexLorentz.ColorFun -/-! - -## The tensor structure for complex Lorentz tensors - --/ -open IndexNotation -open CategoryTheory -open MonoidalCategory -open Matrix -open MatrixGroups -open Complex -open TensorProduct -open IndexNotation -open CategoryTheory - -noncomputable section - -/-- The tensor structure for complex Lorentz tensors. -/ -def complexLorentzTensor : TensorStruct where - C := Fermion.Color - G := SL(2, ℂ) - G_group := inferInstance - k := ℂ - k_commRing := inferInstance - F := Fermion.colorFunMon - τ := Fermion.τ - evalNo := Fermion.evalNo - -end diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean index 048b4ba6..40dc3eaa 100644 --- a/HepLean/Tensors/OverColor/Discrete.lean +++ b/HepLean/Tensors/OverColor/Discrete.lean @@ -25,10 +25,12 @@ variable {C k : Type} [CommRing k] {G : Type} [Group G] variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F') noncomputable section +/-- The functor taking `c` to `F c ⊗ F c`. -/ def pair : Discrete C ⥤ Rep k G := F ⊗ F -def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ - (lift.obj F).obj (OverColor.mk ![c,c]) := by +/-- The isomorphism between the image of `(pair F).obj` and + `(lift.obj F).obj (OverColor.mk ![c,c])`. -/ +def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverColor.mk ![c,c]) := by symm apply ((lift.obj F).mapIso fin2Iso).trans apply ((lift.obj F).μIso _ _).symm.trans @@ -46,10 +48,11 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ fin_cases x rfl - +/-- The functor taking `c` to `F c ⊗ F (τ c)`. -/ def pairτ (τ : C → C) : Discrete C ⥤ Rep k G := F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) +/-- The functor taking `c` to `F (τ c) ⊗ F c`. -/ def τPair (τ : C → C) : Discrete C ⥤ Rep k G := ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) ⊗ F diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean index c2348c6c..d8d133ea 100644 --- a/HepLean/Tensors/OverColor/Iso.lean +++ b/HepLean/Tensors/OverColor/Iso.lean @@ -40,6 +40,8 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 := subst h rfl)) +/-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of + the `Fin 1 → C` maps defined by `c 0` and `c 1`. -/ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by let e1 : Fin 2 ≃ Fin 1 ⊕ Fin 1 := (finSumFinEquiv (n := 1)).symm apply (equivToIso e1).trans @@ -52,11 +54,6 @@ 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 := @@ -191,5 +188,31 @@ def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin (contrPairFin1Fin1 τ ((c ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) (by simpa using h)) <| mkIso (by ext x; simp) + +/-- Given a function `c` from `Fin 1` to `C`, this function returns a morphism + from `mk c` to `mk ![c 0]`. --/ +def permFinOne (c : Fin 1 → C) : mk c ⟶ mk ![c 0] := + (mkIso (by + funext x + fin_cases x + rfl)).hom + +/-- This a function that takes a function `c` from `Fin 2` to `C` and +returns a morphism from `mk c` to `mk ![c 0, c 1]`. --/ +def permFinTwo (c : Fin 2 → C) : mk c ⟶ mk ![c 0, c 1] := + (mkIso (by + funext x + fin_cases x <;> + rfl)).hom + +/-- This is a function that takes a function `c` from `Fin 3` to `C` and returns a morphism + from `mk c` to `mk ![c 0, c 1, c 2]`. --/ +def permFinThree (c : Fin 3 → C) : mk c ⟶ mk ![c 0, c 1, c 2] := + (mkIso (by + funext x + fin_cases x <;> + rfl)).hom + + end OverColor end IndexNotation diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 412e54dc..5df84622 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -660,11 +660,19 @@ variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F') noncomputable section +/-- +The `forgetLiftAppV` function takes an object `c` of type `C` and returns a linear equivalence +between the vector space obtained by applying the lift of `F` and that obtained by applying +`F`. +--/ def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))).V ≃ₗ[k] (F.obj (Discrete.mk c)).V := (PiTensorProduct.subsingletonEquiv 0 : (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c) ) +/-- The `forgetLiftAppV` function takes an object `c` of type `C` and returns a isomorphism +between the objects obtained by applying the lift of `F` and that obtained by applying +`F`. -/ def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1 ) => c)) ≅ F.obj (Discrete.mk c) := Action.mkIso (forgetLiftAppV F c).toModuleIso diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean index cc98dadc..03c93e99 100644 --- a/HepLean/Tensors/Tree/Basic.lean +++ b/HepLean/Tensors/Tree/Basic.lean @@ -38,9 +38,9 @@ structure TensorStruct where τ : C → C τ_involution : Function.Involutive τ /-- The natural transformation describing contraction. -/ - contr : OverColor.Discrete.pairτ F τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G) + contr : OverColor.Discrete.pairτ FDiscrete τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G) /-- The natural transformation describing the metric. -/ - metricNat : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FDiscrete + metric : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FDiscrete /-- The natural transformation describing the unit. -/ unit : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.τPair FDiscrete τ /-- A specification of the dimension of each color in C. This will be used for explicit @@ -60,66 +60,18 @@ instance : Group S.G := S.G_group /-- The lift of the functor `S.F` to a monoidal functor. -/ def F : MonoidalFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete +/- def metric (c : S.C) : S.F.obj (OverColor.mk ![c, c]) := (OverColor.Discrete.pairIso S.FDiscrete c).hom.hom <| (S.metricNat.app (Discrete.mk c)).hom (1 : S.k) +-/ -def contrNLE {n : ℕ} {i j : Fin n} (h : i ≠ j) : 2 ≤ n := by - omega - -def contrNPred {n : ℕ} {i j : Fin n} (h : i ≠ j) : n.pred.pred.succ.succ = n := by - simp_all only [ne_eq, Nat.pred_eq_sub_one, Nat.succ_eq_add_one] - have hi : i < n := i.isLt - have hj : j < n := j.isLt - by_contra hn - have hn : n = 0 ∨ n =1 := by omega - cases hn - · omega - · omega - -def contrFstSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) : - Fin n.pred.pred.succ.succ := Fin.castOrderIso (contrNPred hineqj).symm i - -def contrSndSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) : - Fin n.pred.pred.succ := (Fin.predAbove 0 (contrFstSucc hineqj)).predAbove - (Fin.castOrderIso (contrNPred hineqj).symm j) - -@[simp] -lemma contrSndSucc_succAbove {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) : - (contrFstSucc hineqj).succAbove (contrSndSucc hineqj) = - Fin.castOrderIso (contrNPred hineqj).symm j := by - simp [contrFstSucc, contrSndSucc, Fin.succAbove, - Fin.predAbove] - split_ifs - · rename_i h1 h2 - rw [Fin.lt_def] at h1 h2 - simp_all [Fin.lt_def, Fin.ext_iff] - intro h - omega - · rename_i h1 h2 - rw [Fin.lt_def] at h1 h2 - simp_all [Fin.ext_iff] - rw [Fin.lt_def] - simp only [Fin.coe_cast, Fin.val_fin_lt] - rw [Fin.lt_def] - omega - · rename_i h1 h2 - rw [Fin.lt_def] at h1 h2 - simp_all [Fin.ext_iff] - rw [Fin.lt_def] - simp only [Fin.coe_cast, Fin.val_fin_lt] - omega - · rename_i h1 h2 - rw [Fin.lt_def] at h1 h2 - simp_all [Fin.ext_iff] - rw [Fin.lt_def] - simp only [Fin.coe_cast, Fin.val_fin_lt] - omega - - +/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and + a `j` in `Fin n.succ` allowing us to undertake contraction. -/ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : - S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj (Discrete.mk (c i))) ⊗ + S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj + (Discrete.mk (c i))) ⊗ (OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) := (S.F.mapIso (OverColor.equivToIso (OverColor.finExtractTwo i j))).trans <| (S.F.mapIso (OverColor.mkSum (c ∘ (OverColor.finExtractTwo i j).symm))).trans <| @@ -143,7 +95,13 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C) fin_cases x simp [h] -def contrMap' {n : ℕ} (c : Fin n.succ.succ → S.C) +/-- +`contrMap` is a function that takes a natural number `n`, a function `c` from +`Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type +`Fin n.succ`, and a proof `h` that `c (i.succAbove j) = S.τ (c i)`. It returns a morphism +corresponding to the contraction of the `i`th index with the `i.succAbove j` index. +--/ +def contrMap {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : S.F.obj (OverColor.mk c) ⟶ (OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) := @@ -151,37 +109,47 @@ def contrMap' {n : ℕ} (c : Fin n.succ.succ → S.C) (tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫ (MonoidalCategory.leftUnitor _).hom -def contrMap {n : ℕ} (c : Fin n → S.C) - (i j : Fin n) (hij : i ≠ j) (h : c j = S.τ (c i)) : - S.F.obj (OverColor.mk c) ⟶ - (OverColor.lift.obj S.FDiscrete).obj - (OverColor.mk ((c ∘ Fin.cast (contrNPred hij)) ∘ Fin.succAbove (contrFstSucc hij) ∘ - Fin.succAbove (contrSndSucc hij))) := by - refine (S.F.mapIso (OverColor.equivToIso (Fin.castOrderIso (contrNPred hij)).toEquiv.symm)).hom ≫ - S.contrMap' (c ∘ Fin.cast (contrNPred hij)) (contrFstSucc hij) (contrSndSucc hij) ?_ - simp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, contrSndSucc_succAbove, - Fin.castOrderIso_apply, Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self] - simpa [contrFstSucc] using h - - end TensorStruct /-- A syntax tree for tensor expressions. -/ inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Type where + /-- A general tensor node. -/ | tensorNode {n : ℕ} {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : TensorTree S c + /-- A node consisting of a single vector. -/ + | vecNode {c : S.C} (v : S.FDiscrete.obj (Discrete.mk c)) : TensorTree S ![c] + /-- A node consisting of a two tensor. -/ + | twoNode {c1 c2 : S.C} + (v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) : + TensorTree S ![c1, c2] + /-- A node consisting of a three tensor. -/ + | threeNode {c1 c2 c3 : S.C} + (v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗ + S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] + /-- A general constant node. -/ + | constNode {n : ℕ} {c : Fin n → S.C} (T : 𝟙_ (Rep S.k S.G) ⟶ S.F.obj (OverColor.mk c)) : + TensorTree S c + /-- A constant vector. -/ + | constVecNode {c : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c)) : + TensorTree S ![c] + /-- A constant two tensor (e.g. metric and unit). -/ + | constTwoNode {c1 c2 : S.C} + (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) : + TensorTree S ![c1, c2] + /-- A constant three tensor (e.g. Pauli-matrices). -/ + | constThreeNode {c1 c2 c3 : S.C} + (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗ + S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] + /-- A node corresponding to the addition of two tensors. -/ | add {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c → TensorTree S c + /-- A node corresponding to the permutation of indices of a tensor. -/ | perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) : TensorTree S c1 | prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (t : TensorTree S c) (t1 : TensorTree S c1) : TensorTree S (Sum.elim c c1 ∘ finSumFinEquiv.symm) | smul {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c - | contr {n : ℕ} {c : Fin n → S.C} : (i j : Fin n) → - (hij : i ≠ j) → (h : c j = S.τ (c i)) → TensorTree S c → - TensorTree S ((c ∘ Fin.cast (TensorStruct.contrNPred hij)) ∘ - Fin.succAbove (TensorStruct.contrFstSucc hij) ∘ - Fin.succAbove (TensorStruct.contrSndSucc hij)) - | jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c → - TensorTree S (Function.update c i (S.τ (c i))) + | contr {n : ℕ} {c : Fin n.succ.succ → S.C} : (i : Fin n.succ.succ) → + (j : Fin n.succ) → (h : c (i.succAbove j) = S.τ (c i)) → TensorTree S c → + TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j) | eval {n : ℕ} {c : Fin n.succ → S.C} : (i : Fin n.succ) → (x : Fin (S.evalNo (c i))) → TensorTree S c → TensorTree S (c ∘ Fin.succAbove i) @@ -190,19 +158,40 @@ namespace TensorTree variable {S : TensorStruct} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c) -def metric : TensorTree S ![] open MonoidalCategory open TensorProduct +/-- The node `twoNode` of a tensor tree, with all arguments explicit. -/ +abbrev twoNodeE (S : TensorStruct) (c1 c2 : S.C) + (v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) : + TensorTree S ![c1, c2] := twoNode v + +/-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/ +abbrev constTwoNodeE (S : TensorStruct) (c1 c2 : S.C) + (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) : + TensorTree S ![c1, c2] := constTwoNode v + +/-- The node `constThreeNodeE` of a tensor tree, with all arguments explicit. -/ +abbrev constThreeNodeE (S : TensorStruct) (c1 c2 c3 : S.C) + (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗ + S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] := + constThreeNode v + /-- The number of nodes in a tensor tree. -/ def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun | tensorNode _ => 1 + | vecNode _ => 1 + | twoNode _ => 1 + | threeNode _ => 1 + | constNode _ => 1 + | constVecNode _ => 1 + | constTwoNode _ => 1 + | constThreeNode _ => 1 | add t1 t2 => t1.size + t2.size + 1 | perm _ t => t.size + 1 | smul _ t => t.size + 1 | prod t1 t2 => t1.size + t2.size + 1 - | contr _ _ _ _ t => t.size + 1 - | jiggle _ t => t.size + 1 + | contr _ _ _ t => t.size + 1 | eval _ _ t => t.size + 1 noncomputable section @@ -216,63 +205,7 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over | smul a t => a • t.tensor | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) - | contr i j hij h t => (S.contrMap _ i j hij h).hom t.tensor - | jiggle i t => by - rename_i n c' - let T := (tensorNode (S.metric (S.τ (c' i)))) - let T2 := (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom - ((S.F.μ _ _).hom (T.tensor ⊗ₜ t.tensor)) - let e1 : Fin (2 + n) ≃ Fin (2 + n) := - (Equiv.swap (Fin.castAdd n (0 : Fin 2)) (Fin.natAdd 2 i)) - let T3 := (S.F.map ((OverColor.equivToIso e1).hom)).hom T2 - let T4 := (S.contrMap _ (Fin.castAdd n (0 : Fin 2)) (Fin.castAdd n (1 : Fin 2)) - (by - simp only [Fin.isValue, ne_eq, - Fin.ext_iff, Fin.coe_castAdd, Fin.val_zero, Fin.coe_natAdd] - omega) - (by - simp [e1] - rw [Equiv.swap_apply_of_ne_of_ne] - · simp [Fin.ext_iff] - rfl - · simp [Fin.ext_iff] - · simp [Fin.ext_iff] - omega)).hom T3 - refine (S.F.map ?_).hom T4 - refine (OverColor.equivToIso (Fin.castOrderIso (by simp : (2 + n).pred.pred = n)).toEquiv).hom ≫ ?_ - refine (OverColor.mkIso ?_).hom - funext x - simp - trans Sum.elim ![S.τ (c' i), S.τ (c' i)] c' (finSumFinEquiv.symm - (e1.symm (Fin.natAdd 2 x))) - congr - simp [Fin.ext_iff] - simp [Fin.succAbove] - split_ifs - · rename_i h1 h2 - rw [Fin.lt_def] at h1 h2 - simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc] - · rename_i h1 h2 - rw [Fin.lt_def] at h1 h2 - simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc] - simp [Fin.predAbove, Fin.lt_def] at h1 - · rename_i h1 h2 - rw [Fin.lt_def] at h1 h2 - simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc] - · simp - omega - simp [e1] - by_cases hi: x= i - · subst hi - simp - · rw [Equiv.swap_apply_of_ne_of_ne] - · simp - rw [Function.update] - simp [hi] - · simp [Fin.ext_iff] - · simp [Fin.ext_iff] - omega - + | contr i j h t => (S.contrMap _ i j h).hom t.tensor | _ => 0 lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : diff --git a/HepLean/Tensors/Tree/Dot.lean b/HepLean/Tensors/Tree/Dot.lean index 58125227..fa9a6bd1 100644 --- a/HepLean/Tensors/Tree/Dot.lean +++ b/HepLean/Tensors/Tree/Dot.lean @@ -20,6 +20,20 @@ namespace TensorTree def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → String := fun | tensorNode _ => " node" ++ toString m ++ " [label=\"T" ++ toString nt ++ "\"];\n" + | vecNode T => + " node" ++ toString m ++ " [label=\"vec " ++ toString nt ++ "\"];\n" + | twoNode T => + " node" ++ toString m ++ " [label=\"vec2\", shape=box];\n" + | threeNode T => + " node" ++ toString m ++ " [label=\"vec3\", shape=box];\n" + | constNode T => + " node" ++ toString m ++ " [label=\"const " ++ toString nt ++ "\"];\n" + | constVecNode T => + " node" ++ toString m ++ " [label=\"constVec " ++ toString nt ++ "\"];\n" + | constTwoNode T => + " node" ++ toString m ++ " [label=\"constVec2\", shape=box];\n" + | constThreeNode T => + " node" ++ toString m ++ " [label=\"constVec3\", shape=box];\n" | add t1 t2 => let addNode := " node" ++ toString m ++ " [label=\"+\", shape=box];\n" let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n" @@ -39,20 +53,10 @@ def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTr let smulNode := " node" ++ toString m ++ " [label=\"smul\", shape=box];\n" let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n" smulNode ++ dotString (m + 1) nt t ++ edge1 - | mult _ _ t1 t2 => - let multNode := " node" ++ toString m ++ " [label=\"mult\", shape=box];\n" - let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n" - let edge2 := " node" ++ toString m ++ " -> node" ++ toString (t1.size + m + 2) ++ ";\n" - multNode ++ dotString (m + 1) nt t1 ++ dotString (2 * t1.size + m + 2) (nt + 1) t2 - ++ edge1 ++ edge2 | eval _ _ t1 => let evalNode := " node" ++ toString m ++ " [label=\"eval\", shape=box];\n" let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n" evalNode ++ dotString (m + 1) nt t1 ++ edge1 - | jiggle i t1 => - let jiggleNode := " node" ++ toString m ++ " [label=\"τ\", shape=box];\n" - let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n" - jiggleNode ++ dotString (m + 1) nt t1 ++ edge1 | contr i j _ t1 => let contrNode := " node" ++ toString m ++ " [label=\"contr " ++ toString i ++ " " ++ toString j ++ "\", shape=box];\n" diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean index 69c193a9..c82069d7 100644 --- a/HepLean/Tensors/Tree/Elab.lean +++ b/HepLean/Tensors/Tree/Elab.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith import HepLean.Tensors.Tree.Basic import Lean.Elab.Term import HepLean.Tensors.Tree.Dot +import HepLean.Tensors.ComplexLorentz.Basic /-! ## Elaboration of tensor trees @@ -82,6 +83,7 @@ def indexToDual (stx : Syntax) : Bool := match stx with | `(indexExpr| τ($_)) => true | _ => false + /-! ## Tensor expressions @@ -136,15 +138,72 @@ partial def getIndices (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := def getNoIndicesExact (stx : Syntax) : TermElabM ℕ := do let expr ← elabTerm stx none let type ← inferType expr - match type with - | Expr.app _ (Expr.app _ (Expr.app _ c)) => - let typeC ← inferType c - match typeC with - | Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n))) _)) _ _ => - return n - | _ => throwError "Could not extract number of indices from tensor (getNoIndicesExact). " - | _ => - throwError "Could not extract number of indices from tensor (getNoIndicesExact)." + let strType := toString type + let n := (String.splitOn strType "CategoryTheory.MonoidalCategoryStruct.tensorObj").length + match n with + | 1 => + match type with + | Expr.app _ (Expr.app _ (Expr.app _ c)) => + let typeC ← inferType c + match typeC with + | Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n))) _)) _ _ => + return n + | _ => throwError "Could not extract number of indices from tensor (getNoIndicesExact). " + | _ => return 1 + | k => return k + +/-- The construction of an expression corresponding to the type of a given string once parsed. -/ +def stringToType (str : String) : TermElabM Expr := do + let env ← getEnv + let stx := Parser.runParserCategory env `term str + match stx with + | Except.error _ => throwError "Could not create type from string (stringToType). " + | Except.ok stx => elabTerm stx none + +/-- The syntax associated with a terminal node of a tensor tree. -/ +def termNodeSyntax (T : Term) : TermElabM Term := do + let expr ← elabTerm T none + let type ← inferType expr + let strType := toString type + let n := (String.splitOn strType "CategoryTheory.MonoidalCategoryStruct.tensorObj").length + let const := (String.splitOn strType "Quiver.Hom").length + match n, const with + | 1, 1 => + match type with + | Expr.app _ (Expr.app _ (Expr.app _ c)) => + let typeC ← inferType c + match typeC with + | Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal _))) _)) _ _ => + return Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T] + | _ => throwError "Could not create terminal node syntax (termNodeSyntax). " + | _ => return Syntax.mkApp (mkIdent ``TensorTree.vecNode) #[T] + | 2, 1 => + match ← isDefEq type (← stringToType "CoeSort.coe leftHanded ⊗ CoeSort.coe Lorentz.complexContr") with + | true => return Syntax.mkApp (mkIdent ``TensorTree.twoNodeE) + #[mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.up, T] + | _ => return Syntax.mkApp (mkIdent ``TensorTree.twoNode) #[T] + | 3, 1 => return Syntax.mkApp (mkIdent ``TensorTree.threeNode) #[T] + | 1, 2 => return Syntax.mkApp (mkIdent ``TensorTree.constVecNode) #[T] + | 2, 2 => + match ← isDefEq type (← stringToType + "𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexCo ⊗ Lorentz.complexCo") with + | true => + println! "here" + return Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[ + mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.down, + mkIdent ``Fermion.Color.down, T] + | _ => return Syntax.mkApp (mkIdent ``TensorTree.constTwoNode) #[T] + | 3, 2 => + /- Specific types. -/ + match ← isDefEq type (← stringToType + "𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexContr ⊗ Fermion.leftHanded ⊗ Fermion.rightHanded") with + | true => + return Syntax.mkApp (mkIdent ``TensorTree.constThreeNodeE) #[ + mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.up, + mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.upR, T] + | _ => + return Syntax.mkApp (mkIdent ``TensorTree.constThreeNode) #[T] + | _, _ => throwError "Could not create terminal node syntax (termNodeSyntax). " /-- The positions in getIndicesNode which get evaluated, and the value they take. -/ partial def getEvalPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do @@ -159,19 +218,6 @@ def evalSyntax (l : List (ℕ × ℕ)) (T : Term) : Term := l.foldl (fun T' (x1, x2) => Syntax.mkApp (mkIdent ``TensorTree.eval) #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x2), T']) T -/-- The positions in getIndicesNode which get dualized. -/ -partial def getDualPos (stx : Syntax) : TermElabM (List ℕ) := do - let ind ← getIndices stx - let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x) - let indEnum := indFilt.enum - let duals := indEnum.filter (fun x => indexToDual x.2) - return duals.map (fun x => x.1) - -/-- For each element of `l : List ℕ` applies `TensorTree.jiggle` to the given term. -/ -def dualSyntax (l : List ℕ) (T : Term) : Term := - l.foldl (fun T' x => Syntax.mkApp (mkIdent ``TensorTree.jiggle) - #[Syntax.mkNumLit (toString x), T']) T - /-- The pairs of positions in getIndicesNode which get contracted. -/ partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do let ind ← getIndices stx @@ -192,7 +238,7 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do /-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/ def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term := l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr) - #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T + #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent `sorry, mkIdent ``rfl, T']) T /-- Creates the syntax associated with a tensor node. -/ def syntaxFull (stx : Syntax) : TermElabM Term := do @@ -202,10 +248,9 @@ def syntaxFull (stx : Syntax) : TermElabM Term := do let rawIndex ← getNoIndicesExact T if indices.length ≠ rawIndex then throwError "The number of indices does not match the tensor {T}." - let tensorNodeSyntax := Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T] + let tensorNodeSyntax ← termNodeSyntax T let evalSyntax := evalSyntax (← getEvalPos stx) tensorNodeSyntax - let dualSyntax := dualSyntax (← getDualPos stx) evalSyntax - let contrSyntax := contrSyntax (← getContrPos stx) dualSyntax + let contrSyntax := contrSyntax (← getContrPos stx) evalSyntax return contrSyntax | _ => throwError "Unsupported tensor expression syntax in elaborateTensorNode: {stx}" From c73ae1aae693a22ad65c82b609d1bdb28ad00cbd Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 16 Oct 2024 16:42:20 +0000 Subject: [PATCH 4/4] refactor: Lint --- HepLean/Tensors/OverColor/Discrete.lean | 6 +++--- HepLean/Tensors/OverColor/Iso.lean | 7 ++----- HepLean/Tensors/OverColor/Lift.lean | 8 ++++---- HepLean/Tensors/Tree/Basic.lean | 10 +++++----- HepLean/Tensors/Tree/Elab.lean | 11 +++++++---- 5 files changed, 21 insertions(+), 21 deletions(-) diff --git a/HepLean/Tensors/OverColor/Discrete.lean b/HepLean/Tensors/OverColor/Discrete.lean index 40dc3eaa..a8c27f48 100644 --- a/HepLean/Tensors/OverColor/Discrete.lean +++ b/HepLean/Tensors/OverColor/Discrete.lean @@ -29,7 +29,7 @@ noncomputable section def pair : Discrete C ⥤ Rep k G := F ⊗ F /-- The isomorphism between the image of `(pair F).obj` and - `(lift.obj F).obj (OverColor.mk ![c,c])`. -/ + `(lift.obj F).obj (OverColor.mk ![c,c])`. -/ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverColor.mk ![c,c]) := by symm apply ((lift.obj F).mapIso fin2Iso).trans @@ -50,11 +50,11 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol /-- The functor taking `c` to `F c ⊗ F (τ c)`. -/ def pairτ (τ : C → C) : Discrete C ⥤ Rep k G := - F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) + F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) /-- The functor taking `c` to `F (τ c) ⊗ F c`. -/ def τPair (τ : C → C) : Discrete C ⥤ Rep k G := - ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) ⊗ F + ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) ⊗ F end end Discrete diff --git a/HepLean/Tensors/OverColor/Iso.lean b/HepLean/Tensors/OverColor/Iso.lean index d8d133ea..5400aff9 100644 --- a/HepLean/Tensors/OverColor/Iso.lean +++ b/HepLean/Tensors/OverColor/Iso.lean @@ -42,7 +42,7 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 := /-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of the `Fin 1 → C` maps defined by `c 0` and `c 1`. -/ -def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by +def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by let e1 : Fin 2 ≃ Fin 1 ⊕ Fin 1 := (finSumFinEquiv (n := 1)).symm apply (equivToIso e1).trans apply (mkSum _).trans @@ -175,7 +175,6 @@ def contrPairFin1Fin1 (τ : C → C) (c : Fin 1 ⊕ Fin 1 → C) variable {k : Type} [CommRing k] {G : Type} [Group G] - /-- The Isomorphism between a `Fin n.succ.succ → C` and the product containing an object in the image of `contrPair` based on the given values. -/ def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin n.succ.succ) @@ -188,7 +187,6 @@ def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin (contrPairFin1Fin1 τ ((c ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) (by simpa using h)) <| mkIso (by ext x; simp) - /-- Given a function `c` from `Fin 1` to `C`, this function returns a morphism from `mk c` to `mk ![c 0]`. --/ def permFinOne (c : Fin 1 → C) : mk c ⟶ mk ![c 0] := @@ -197,7 +195,7 @@ def permFinOne (c : Fin 1 → C) : mk c ⟶ mk ![c 0] := fin_cases x rfl)).hom -/-- This a function that takes a function `c` from `Fin 2` to `C` and +/-- This a function that takes a function `c` from `Fin 2` to `C` and returns a morphism from `mk c` to `mk ![c 0, c 1]`. --/ def permFinTwo (c : Fin 2 → C) : mk c ⟶ mk ![c 0, c 1] := (mkIso (by @@ -213,6 +211,5 @@ def permFinThree (c : Fin 3 → C) : mk c ⟶ mk ![c 0, c 1, c 2] := fin_cases x <;> rfl)).hom - end OverColor end IndexNotation diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 5df84622..b6f29efd 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -666,14 +666,14 @@ between the vector space obtained by applying the lift of `F` and that obtained `F`. --/ def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))).V ≃ₗ[k] - (F.obj (Discrete.mk c)).V := + (F.obj (Discrete.mk c)).V := (PiTensorProduct.subsingletonEquiv 0 : - (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c) ) + (⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c)) /-- The `forgetLiftAppV` function takes an object `c` of type `C` and returns a isomorphism between the objects obtained by applying the lift of `F` and that obtained by applying -`F`. -/ -def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1 ) => c)) +`F`. -/ +def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c)) ≅ F.obj (Discrete.mk c) := Action.mkIso (forgetLiftAppV F c).toModuleIso (fun g => by diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean index 03c93e99..afafd41b 100644 --- a/HepLean/Tensors/Tree/Basic.lean +++ b/HepLean/Tensors/Tree/Basic.lean @@ -67,7 +67,7 @@ def metric (c : S.C) : S.F.obj (OverColor.mk ![c, c]) := -/ /-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and - a `j` in `Fin n.succ` allowing us to undertake contraction. -/ + a `j` in `Fin n.succ` allowing us to undertake contraction. -/ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C) (i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) : S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj @@ -168,12 +168,12 @@ abbrev twoNodeE (S : TensorStruct) (c1 c2 : S.C) /-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/ abbrev constTwoNodeE (S : TensorStruct) (c1 c2 : S.C) - (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) : + (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) : TensorTree S ![c1, c2] := constTwoNode v /-- The node `constThreeNodeE` of a tensor tree, with all arguments explicit. -/ -abbrev constThreeNodeE (S : TensorStruct) (c1 c2 c3 : S.C) - (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗ +abbrev constThreeNodeE (S : TensorStruct) (c1 c2 c3 : S.C) + (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗ S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] := constThreeNode v @@ -205,7 +205,7 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over | smul a t => a • t.tensor | prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom ((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) - | contr i j h t => (S.contrMap _ i j h).hom t.tensor + | contr i j h t => (S.contrMap _ i j h).hom t.tensor | _ => 0 lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean index c82069d7..388872dc 100644 --- a/HepLean/Tensors/Tree/Elab.lean +++ b/HepLean/Tensors/Tree/Elab.lean @@ -178,9 +178,11 @@ def termNodeSyntax (T : Term) : TermElabM Term := do | _ => throwError "Could not create terminal node syntax (termNodeSyntax). " | _ => return Syntax.mkApp (mkIdent ``TensorTree.vecNode) #[T] | 2, 1 => - match ← isDefEq type (← stringToType "CoeSort.coe leftHanded ⊗ CoeSort.coe Lorentz.complexContr") with + match ← isDefEq type (← stringToType + "CoeSort.coe leftHanded ⊗ CoeSort.coe Lorentz.complexContr") with | true => return Syntax.mkApp (mkIdent ``TensorTree.twoNodeE) - #[mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.up, T] + #[mkIdent ``Fermion.complexLorentzTensor, + mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.up, T] | _ => return Syntax.mkApp (mkIdent ``TensorTree.twoNode) #[T] | 3, 1 => return Syntax.mkApp (mkIdent ``TensorTree.threeNode) #[T] | 1, 2 => return Syntax.mkApp (mkIdent ``TensorTree.constVecNode) #[T] @@ -191,7 +193,7 @@ def termNodeSyntax (T : Term) : TermElabM Term := do println! "here" return Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[ mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.down, - mkIdent ``Fermion.Color.down, T] + mkIdent ``Fermion.Color.down, T] | _ => return Syntax.mkApp (mkIdent ``TensorTree.constTwoNode) #[T] | 3, 2 => /- Specific types. -/ @@ -238,7 +240,8 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do /-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/ def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term := l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr) - #[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent `sorry, mkIdent ``rfl, T']) T + #[Syntax.mkNumLit (toString x1), + Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T /-- Creates the syntax associated with a tensor node. -/ def syntaxFull (stx : Syntax) : TermElabM Term := do