diff --git a/PhysLean.lean b/PhysLean.lean index 488846ea..0ae64611 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -67,9 +67,10 @@ import PhysLean.Lorentz.ComplexTensor.Lemmas import PhysLean.Lorentz.ComplexTensor.Metrics.Basic import PhysLean.Lorentz.ComplexTensor.Metrics.Basis import PhysLean.Lorentz.ComplexTensor.Metrics.Lemmas +import PhysLean.Lorentz.ComplexTensor.OfRat import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basic import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basis -import PhysLean.Lorentz.ComplexTensor.PauliMatrices.CoContractContr +import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Relations import PhysLean.Lorentz.ComplexTensor.Units.Basic import PhysLean.Lorentz.ComplexTensor.Units.Symm import PhysLean.Lorentz.ComplexVector.Basic @@ -107,6 +108,7 @@ import PhysLean.Mathematics.List import PhysLean.Mathematics.List.InsertIdx import PhysLean.Mathematics.List.InsertionSort import PhysLean.Mathematics.PiTensorProduct +import PhysLean.Mathematics.RatComplexNum import PhysLean.Mathematics.SO3.Basic import PhysLean.Mathematics.SchurTriangulation import PhysLean.Meta.AllFilePaths @@ -197,6 +199,7 @@ import PhysLean.Tensors.TensorSpecies.Contractions.Categorical import PhysLean.Tensors.TensorSpecies.Contractions.ContrMap import PhysLean.Tensors.TensorSpecies.DualRepIso import PhysLean.Tensors.TensorSpecies.MetricTensor +import PhysLean.Tensors.TensorSpecies.OfInt import PhysLean.Tensors.TensorSpecies.Pure import PhysLean.Tensors.TensorSpecies.UnitTensor import PhysLean.Tensors.Tree.Basic diff --git a/PhysLean/FlavorPhysics/CKMMatrix/Basic.lean b/PhysLean/FlavorPhysics/CKMMatrix/Basic.lean index f720bb2e..9db6ff20 100644 --- a/PhysLean/FlavorPhysics/CKMMatrix/Basic.lean +++ b/PhysLean/FlavorPhysics/CKMMatrix/Basic.lean @@ -323,7 +323,7 @@ lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) : fin_cases i <;> fin_cases j <;> simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, zero_mul, add_zero, mul_zero, _root_.map_mul, mul_re, I_re, ofReal_re, I_im, ofReal_im, sub_self, Real.exp_zero, - one_mul, mul_one, Complex.abs_exp, Fin.mk_one, cons_val_one, head_cons, zero_add, + one_mul, mul_one, Complex.abs_exp, Fin.mk_one, cons_val_one, head_cons, zero_add, head_fin_const, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, tail_val', head_val'] all_goals change Complex.abs (0 * _ + _) = _ diff --git a/PhysLean/Lorentz/ComplexTensor/Basic.lean b/PhysLean/Lorentz/ComplexTensor/Basic.lean index 8657c5c7..708eec47 100644 --- a/PhysLean/Lorentz/ComplexTensor/Basic.lean +++ b/PhysLean/Lorentz/ComplexTensor/Basic.lean @@ -277,11 +277,24 @@ instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} : instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} : Fintype (OverColor.mk c).left := Fin.fintype n +instance : CharZero complexLorentzTensor.k := instCharZero + /-- The equality of two maps in `OverColor C` from objects based on `Fin _` is decidable. -/ instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (σ σ' : OverColor.mk c ⟶ OverColor.mk c1) : Decidable (σ = σ') := decidable_of_iff _ (OverColor.Hom.ext_iff σ σ') +@[simp] +lemma k_instSub : @HSub.hSub complexLorentzTensor.k complexLorentzTensor.k complexLorentzTensor.k + instHSub = @HSub.hSub ℂ ℂ ℂ instHSub := by rfl + +@[simp] +lemma k_instAdd : @HAdd.hAdd complexLorentzTensor.k + complexLorentzTensor.k complexLorentzTensor.k instHAdd = @HAdd.hAdd ℂ ℂ ℂ instHAdd := by rfl + +@[simp] +lemma k_neg : @Neg.neg complexLorentzTensor.k = @Neg.neg ℂ := by rfl + end complexLorentzTensor end diff --git a/PhysLean/Lorentz/ComplexTensor/Basis.lean b/PhysLean/Lorentz/ComplexTensor/Basis.lean index 5dee6b2e..ac432263 100644 --- a/PhysLean/Lorentz/ComplexTensor/Basis.lean +++ b/PhysLean/Lorentz/ComplexTensor/Basis.lean @@ -42,6 +42,13 @@ def basisVector {n : ℕ} (c : Fin n → complexLorentzTensor.C) complexLorentzTensor.F.obj (OverColor.mk c) := PiTensorProduct.tprod ℂ (fun i => complexLorentzTensor.basis (c i) (b i)) +lemma basisVector_eq_tensorBasis {n : ℕ} (c : Fin n → complexLorentzTensor.C) + (b : Π j, Fin (complexLorentzTensor.repDim (c j))) : + basisVector c b = complexLorentzTensor.tensorBasis c b := by + rw [basisVector, TensorSpecies.tensorBasis_eq_basisVector] + simp only [OverColor.mk_left, Functor.id_obj, OverColor.mk_hom, TensorSpecies.basisVector] + rfl + lemma perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C} {c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1) (i : Fin m) : diff --git a/PhysLean/Lorentz/ComplexTensor/Metrics/Basis.lean b/PhysLean/Lorentz/ComplexTensor/Metrics/Basis.lean index c1e2163d..c170158b 100644 --- a/PhysLean/Lorentz/ComplexTensor/Metrics/Basis.lean +++ b/PhysLean/Lorentz/ComplexTensor/Metrics/Basis.lean @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import PhysLean.Lorentz.ComplexTensor.Metrics.Basic +import PhysLean.Lorentz.ComplexTensor.OfRat import PhysLean.Lorentz.ComplexTensor.Basis +import PhysLean.Tensors.TensorSpecies.OfInt /-! ## Metrics and basis expansions @@ -52,6 +54,30 @@ lemma coMetric_basis_expand : {η' | μ ν}ᵀ.tensor = simp only [Fin.isValue, Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply] rfl +lemma coMetric_tensorBasis : η' = + complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 0) + - complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 1) + - complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 2) + - complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 3) := by + trans {η' | μ ν}ᵀ.tensor + · simp + · rw [coMetric_basis_expand] + simp [basisVector_eq_tensorBasis] + +lemma coMetric_eq_ofRat : η' = ofRat fun f => + if f 0 = 0 ∧ f 1 = 0 then 1 else + if f 0 = f 1 then - 1 else 0 := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [coMetric_tensorBasis] + repeat rw [tensorBasis_eq_ofRat] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply, + ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons] + simp only [← map_sub, Fin.isValue] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + /-- Provides the explicit expansion of the co-metric tensor in terms of the basis elements, as a tensor tree. -/ lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor = @@ -61,8 +87,13 @@ lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor = (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 3))))).tensor := coMetric_basis_expand +/-! + +## contrMetric + +-/ /-- The expansion of the Lorentz contravariant metric in terms of basis vectors. -/ -lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor = +lemma contrMetric_basis_expand : {η | μ ν}ᵀ.tensor = basisVector ![Color.up, Color.up] (fun _ => 0) - basisVector ![Color.up, Color.up] (fun _ => 1) - basisVector ![Color.up, Color.up] (fun _ => 2) @@ -87,14 +118,38 @@ lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor = simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply] rfl +lemma contrMetric_tensorBasis : η = + complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 0) + - complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 1) + - complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 2) + - complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 3) := by + trans {η | μ ν}ᵀ.tensor + · simp + · rw [contrMetric_basis_expand] + simp [basisVector_eq_tensorBasis] + +lemma contrMetric_eq_ofRat : η = ofRat fun f => + if f 0 = 0 ∧ f 1 = 0 then 1 else + if f 0 = f 1 then - 1 else 0 := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [contrMetric_tensorBasis] + repeat rw [tensorBasis_eq_ofRat] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply, + ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons] + simp only [← map_sub, Fin.isValue] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + /-- The expansion of the Lorentz contravariant metric in terms of basis vectors as a structured tensor tree. -/ -lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor = +lemma contrMetric_basis_expand_tree : {η | μ ν}ᵀ.tensor = (TensorTree.add (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 0))) <| TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 1)))) <| TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 2)))) <| (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 3))))).tensor := - contrMatrix_basis_expand + contrMetric_basis_expand /-- The expansion of the Fermionic left metric in terms of basis vectors. -/ lemma leftMetric_expand : {εL | α β}ᵀ.tensor = @@ -115,6 +170,31 @@ lemma leftMetric_expand : {εL | α β}ᵀ.tensor = · rfl · rfl +lemma leftMetric_tensorBasis : εL = + - complexLorentzTensor.tensorBasis ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1) + + complexLorentzTensor.tensorBasis ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by + trans {εL | μ ν}ᵀ.tensor + · simp + · rw [leftMetric_expand] + simp [basisVector_eq_tensorBasis] + +lemma leftMetric_eq_ofRat : εL = ofRat fun f => + if f 0 = 0 ∧ f 1 = 1 then - 1 else + if f 1 = 0 ∧ f 0 = 1 then 1 else 0 := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [leftMetric_tensorBasis] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg, + Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one, + head_cons] + repeat rw [tensorBasis_eq_ofRat] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply, + ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons] + simp only [Fin.isValue, k_neg, ← map_neg, k_instAdd, ← map_add] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + /-- The expansion of the Fermionic left metric in terms of basis vectors as a structured tensor tree. -/ lemma leftMetric_expand_tree : {εL | α β}ᵀ.tensor = @@ -141,6 +221,31 @@ lemma altLeftMetric_expand : {εL' | α β}ᵀ.tensor = · rfl · rfl +lemma altLeftMetric_tensorBasis : εL' = + complexLorentzTensor.tensorBasis ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1) + - complexLorentzTensor.tensorBasis ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0) := by + trans {εL' | μ ν}ᵀ.tensor + · simp + · rw [altLeftMetric_expand] + simp [basisVector_eq_tensorBasis] + +lemma altLeftMetric_eq_ofRat : εL' = ofRat fun f => + if f 0 = 0 ∧ f 1 = 1 then 1 else + if f 1 = 0 ∧ f 0 = 1 then - 1 else 0 := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [altLeftMetric_tensorBasis] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg, + Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one, + head_cons] + repeat rw [tensorBasis_eq_ofRat] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply, + ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons] + simp only [Fin.isValue, ← map_sub] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + /-- The expansion of the Fermionic alt-left metric in terms of basis vectors as a structured tensor tree. -/ lemma altLeftMetric_expand_tree : {εL' | α β}ᵀ.tensor = @@ -169,6 +274,31 @@ lemma rightMetric_expand : {εR | α β}ᵀ.tensor = · rfl · rfl +lemma rightMetric_tensorBasis : εR = + - complexLorentzTensor.tensorBasis ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1) + + complexLorentzTensor.tensorBasis ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0) := by + trans {εR | μ ν}ᵀ.tensor + · simp + · rw [rightMetric_expand] + simp [basisVector_eq_tensorBasis] + +lemma rightMetric_eq_ofRat : εR = ofRat fun f => + if f 0 = 0 ∧ f 1 = 1 then - 1 else + if f 1 = 0 ∧ f 0 = 1 then 1 else 0 := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [rightMetric_tensorBasis] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg, + Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one, + head_cons] + repeat rw [tensorBasis_eq_ofRat] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply, + ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons] + simp only [Fin.isValue, k_neg, ← map_neg, k_instAdd, ← map_add] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + /-- The expansion of the Fermionic right metric in terms of basis vectors as a structured tensor tree. -/ lemma rightMetric_expand_tree : {εR | α β}ᵀ.tensor = @@ -195,6 +325,31 @@ lemma altRightMetric_expand : {εR' | α β}ᵀ.tensor = · rfl · rfl +lemma altRightMetric_tensorBasis : εR' = + complexLorentzTensor.tensorBasis ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1) + - complexLorentzTensor.tensorBasis ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0) := by + trans {εR' | μ ν}ᵀ.tensor + · simp + · rw [altRightMetric_expand] + simp [basisVector_eq_tensorBasis] + +lemma altRightMetric_eq_ofRat : εR' = ofRat fun f => + if f 0 = 0 ∧ f 1 = 1 then 1 else + if f 1 = 0 ∧ f 0 = 1 then - 1 else 0 := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [altRightMetric_tensorBasis] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg, + Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one, + head_cons] + repeat rw [tensorBasis_eq_ofRat] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply, + ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons] + simp only [Fin.isValue, ← map_sub] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + /-- The expansion of the Fermionic alt-right metric in terms of basis vectors as a structured tensor tree. -/ lemma altRightMetric_expand_tree : {εR' | α β}ᵀ.tensor = diff --git a/PhysLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean b/PhysLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean index d2f9b2da..95759339 100644 --- a/PhysLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean +++ b/PhysLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean @@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith -/ import PhysLean.Lorentz.ComplexTensor.Metrics.Basis import PhysLean.Lorentz.ComplexTensor.Units.Basic +import PhysLean.Tensors.TensorSpecies.OfInt /-! ## Basic lemmas regarding metrics @@ -32,28 +33,78 @@ namespace complexLorentzTensor -/ /-- The covariant metric is symmetric `{η' | μ ν = η' | ν μ}ᵀ`. -/ -informal_lemma coMetric_symm where - deps := [``coMetric] +lemma coMetric_symm : {η' | μ ν = η' | ν μ}ᵀ := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, coMetric_eq_ofRat, Fin.isValue, cons_val_zero, + cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply, + perm_tensorBasis_repr_apply, OverColor.mk_hom, OverColor.equivToHomEq_toEquiv] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + decide /-- The contravariant metric is symmetric `{η | μ ν = η | ν μ}ᵀ`. -/ -informal_lemma contrMetric_symm where - deps := [``contrMetric] +lemma contrMetric_symm : {η | μ ν = η | ν μ}ᵀ := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, contrMetric_eq_ofRat, Fin.isValue, cons_val_zero, + cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply, + perm_tensorBasis_repr_apply, OverColor.mk_hom, OverColor.equivToHomEq_toEquiv] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + decide /-- The left metric is antisymmetric `{εL | α α' = - εL | α' α}ᵀ`. -/ -informal_lemma leftMetric_antisymm where - deps := [``leftMetric] +lemma leftMetric_antisymm : {εL | α α' = - (εL| α' α)}ᵀ := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, leftMetric_eq_ofRat, Fin.isValue, cons_val_zero, + cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply, + perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom, + OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg] + simp only [Fin.isValue, ← map_neg] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + decide /-- The right metric is antisymmetric `{εR | β β' = - εR | β' β}ᵀ`. -/ -informal_lemma rightMetric_antisymm where - deps := [``rightMetric] +lemma rightMetric_antisymm : {εR | β β' = - (εR| β' β)}ᵀ := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, rightMetric_eq_ofRat, Fin.isValue, cons_val_zero, + cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply, + perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom, + OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg] + simp only [Fin.isValue, ← map_neg] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + decide /-- The alt-left metric is antisymmetric `{εL' | α α' = - εL' | α' α}ᵀ`. -/ -informal_lemma altLeftMetric_antisymm where - deps := [``altLeftMetric] +lemma altLeftMetric_antisymm : {εL' | α α' = - (εL' | α' α)}ᵀ := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, altLeftMetric_eq_ofRat, Fin.isValue, cons_val_zero, + cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply, + perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom, + OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg] + simp only [Fin.isValue, ← map_neg] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + decide /-- The alt-right metric is antisymmetric `{εR' | β β' = - εR' | β' β}ᵀ`. -/ -informal_lemma altRightMetric_antisymm where - deps := [``altRightMetric] +lemma altRightMetric_antisymm : {εR' | α α' = - (εR' | α' α)}ᵀ := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, altRightMetric_eq_ofRat, Fin.isValue, + cons_val_zero, cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply, + perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom, + OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg] + simp only [Fin.isValue, ← map_neg] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + decide /-! diff --git a/PhysLean/Lorentz/ComplexTensor/OfRat.lean b/PhysLean/Lorentz/ComplexTensor/OfRat.lean new file mode 100644 index 00000000..cb9a8573 --- /dev/null +++ b/PhysLean/Lorentz/ComplexTensor/OfRat.lean @@ -0,0 +1,95 @@ +/- +Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +import PhysLean.Lorentz.ComplexTensor.Basic +import PhysLean.Mathematics.RatComplexNum +/-! + +# Basis for tensors in a tensor species + +-/ + +open IndexNotation +open CategoryTheory +open MonoidalCategory + +namespace complexLorentzTensor +open OverColor +open PhysLean.RatComplexNum +open PhysLean + +variable (S : TensorSpecies) + +/--A complex Lorentz tensor from a map + `(Π j, Fin (complexLorentzTensor.repDim (c j))) → RatComplexNum`. All + complex Lorentz tensors with rational coefficents with respect to the basis are of this + form. -/ +noncomputable def ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (f : (Π j, Fin (complexLorentzTensor.repDim (c j))) → RatComplexNum) : + complexLorentzTensor.F.obj (OverColor.mk c) := + (complexLorentzTensor.tensorBasis c).repr.symm <| + (Finsupp.linearEquivFunOnFinite complexLorentzTensor.k complexLorentzTensor.k + ((j : Fin n) → Fin (complexLorentzTensor.repDim (c j)))).symm <| + (fun j => toComplexNum (f j)) + +@[simp] +lemma ofRat_tensorBasis_repr_apply {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (f : (Π j, Fin (complexLorentzTensor.repDim (c j))) → RatComplexNum) + (b : Π j, Fin (complexLorentzTensor.repDim (c j))) : + (complexLorentzTensor.tensorBasis c).repr (ofRat f) b = toComplexNum (f b) := by + simp [ofRat] + rfl + +lemma tensorBasis_eq_ofRat {n : ℕ} {c : Fin n → complexLorentzTensor.C} + (b : Π j, Fin (complexLorentzTensor.repDim (c j))) : + complexLorentzTensor.tensorBasis c b + = ofRat (fun b' => if b = b' then ⟨1, 0⟩ else ⟨0, 0⟩) := by + apply (complexLorentzTensor.tensorBasis c).repr.injective + simp only [Basis.repr_self] + ext b' + simp only [ofRat_tensorBasis_repr_apply] + rw [Finsupp.single_apply, toComplexNum] + simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] + split + simp only [Rat.cast_one, Rat.cast_zero, zero_mul, add_zero] + simp + +lemma contr_basis_ratComplexNum {c : complexLorentzTensor.C} + (i : Fin (complexLorentzTensor.repDim c)) + (j : Fin (complexLorentzTensor.repDim (complexLorentzTensor.τ c))) : + complexLorentzTensor.castToField + ((complexLorentzTensor.contr.app (Discrete.mk c)).hom + (complexLorentzTensor.basis c i ⊗ₜ + complexLorentzTensor.basis (complexLorentzTensor.τ c) j)) + = toComplexNum (if i.val = j.val then 1 else 0) := by + match c with + | Color.upL => + change Fermion.leftAltContraction.hom (Fermion.leftBasis i ⊗ₜ Fermion.altLeftBasis j) = _ + rw [Fermion.leftAltContraction_basis] + simp + | Color.downL => + change Fermion.altLeftContraction.hom (Fermion.altLeftBasis i ⊗ₜ Fermion.leftBasis j) = _ + rw [Fermion.altLeftContraction_basis] + simp + | Color.upR => + change Fermion.rightAltContraction.hom (Fermion.rightBasis i ⊗ₜ Fermion.altRightBasis j) = _ + rw [Fermion.rightAltContraction_basis] + simp + | Color.downR => + change Fermion.rightAltContraction.hom (Fermion.rightBasis i ⊗ₜ Fermion.altRightBasis j) = _ + rw [Fermion.rightAltContraction_basis] + simp + | Color.up => + change Lorentz.contrCoContraction.hom + (Lorentz.complexContrBasisFin4 i ⊗ₜ Lorentz.complexCoBasisFin4 j) = _ + rw [Lorentz.contrCoContraction_basis] + simp + | Color.down => + change Lorentz.contrCoContraction.hom + (Lorentz.complexContrBasisFin4 i ⊗ₜ Lorentz.complexCoBasisFin4 j) = _ + rw [Lorentz.contrCoContraction_basis] + simp + +end complexLorentzTensor diff --git a/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean b/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean index 793c3ca2..46dca95e 100644 --- a/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean +++ b/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basic.lean @@ -25,7 +25,7 @@ noncomputable section namespace complexLorentzTensor open Fermion -TODO "Move this file from Lorentz.ComplexTensors to Lorentz.PauliMatrices - +TODO "Move this file from Lorentz.ComplexTensors to Lorentz.PauliMatrices - there is no point having two folders for Pauli matrices." /-! diff --git a/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean b/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean index c880c5a3..3210e757 100644 --- a/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean +++ b/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean @@ -65,6 +65,51 @@ lemma pauliContr_in_basis : {pauliContr | μ α β}ᵀ.tensor = | (1 : Fin 3) => rfl | (2 : Fin 3) => rfl +lemma pauliContr_tensorBasis : pauliContr = + complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 0 | 1 => 0 | 2 => 0) + + complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 0 | 1 => 1 | 2 => 1) + + complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 1 | 1 => 0 | 2 => 1) + + complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 1 | 1 => 1 | 2 => 0) + - I • complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 2 | 1 => 0 | 2 => 1) + + I • complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 2 | 1 => 1 | 2 => 0) + + complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 3 | 1 => 0 | 2 => 0) + - complexLorentzTensor.tensorBasis ![Color.up, Color.upL, Color.upR] + (fun | 0 => 3 | 1 => 1 | 2 => 1) := by + trans {pauliContr | μ α β}ᵀ.tensor + · simp + rw [pauliContr_in_basis] + simp [basisVector_eq_tensorBasis] + +lemma pauliContr_ofRat : pauliContr = ofRat (fun b => + if b = (fun | (0 : Fin 3) => 0 | 1 => 0 | 2 => 0) then ⟨1, 0⟩ else + if b = (fun | 0 => 0 | 1 => 1 | 2 => 1) then ⟨1, 0⟩ else + if b = (fun | 0 => 1 | 1 => 0 | 2 => 1) then ⟨1, 0⟩ else + if b = (fun | 0 => 1 | 1 => 1 | 2 => 0) then ⟨1, 0⟩ else + if b = (fun | 0 => 2 | 1 => 0 | 2 => 1) then ⟨0, -1⟩ else + if b = (fun | 0 => 2 | 1 => 1 | 2 => 0) then ⟨0, 1⟩ else + if b = (fun | 0 => 3 | 1 => 0 | 2 => 0) then ⟨1, 0⟩ else + if b = (fun | 0 => 3 | 1 => 1 | 2 => 1) then ⟨-1, 0⟩ else 0) := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [pauliContr_tensorBasis] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg, + Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one, + head_cons] + repeat rw [tensorBasis_eq_ofRat] + simp [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply, + ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons] + simp only [Fin.isValue, ← map_add, ← map_sub] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + lemma pauliContr_basis_expand_tree : {pauliContr | μ α β}ᵀ.tensor = (TensorTree.add (tensorNode (basisVector ![Color.up, Color.upL, Color.upR] (fun | 0 => 0 | 1 => 0 | 2 => 0))) <| @@ -543,6 +588,45 @@ lemma pauliCo_basis_expand : pauliCo simp only [neg_smul, one_smul] abel +lemma pauliCo_tensorBasis : pauliCo = + complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0) + + complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 0 | 1 => 1 | 2 => 1) + - complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1) + - complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0) + + I • complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1) + - I • complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0) + - complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0) + + complexLorentzTensor.tensorBasis pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1) := by + rw [pauliCo_basis_expand] + simp [basisVector_eq_tensorBasis] + +set_option maxRecDepth 1000 +lemma pauliCo_ofRat : pauliCo = ofRat (fun b => + if b = (fun | (0 : Fin 3) => 0 | 1 => 0 | 2 => 0) then ⟨1, 0⟩ else + if b = (fun | 0 => 0 | 1 => 1 | 2 => 1) then ⟨1, 0⟩ else + if b = (fun | 0 => 1 | 1 => 0 | 2 => 1) then ⟨-1, 0⟩ else + if b = (fun | 0 => 1 | 1 => 1 | 2 => 0) then ⟨-1, 0⟩ else + if b = (fun | 0 => 2 | 1 => 0 | 2 => 1) then ⟨0, 1⟩ else + if b = (fun | 0 => 2 | 1 => 1 | 2 => 0) then ⟨0, -1⟩ else + if b = (fun | 0 => 3 | 1 => 0 | 2 => 0) then ⟨-1, 0⟩ else + if b = (fun | 0 => 3 | 1 => 1 | 2 => 1) then ⟨1, 0⟩ else ⟨0, 0⟩) := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + rw [pauliCo] + rw [TensorTree.contr_tensorBasis_repr_apply] + conv_lhs => + enter [2, x] + rw [TensorTree.prod_tensorBasis_repr_apply] + simp [coMetric_eq_ofRat, pauliContr_ofRat] + erw [← _root_.map_mul] + erw [contr_basis_ratComplexNum] + erw [← _root_.map_mul] + rw [← map_sum] + rw [ofRat_tensorBasis_repr_apply] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + with_unfolding_all decide + lemma pauliCo_basis_expand_tree : {pauliCo | μ α β}ᵀ.tensor = (TensorTree.add (tensorNode (basisVector pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0))) <| diff --git a/PhysLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean b/PhysLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean deleted file mode 100644 index fbb7314a..00000000 --- a/PhysLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean +++ /dev/null @@ -1,546 +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 PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basis -/-! - -## Contractiong of indices of Pauli matrix. - -The main result of this file is `pauliMatrix_contract_pauliMatrix` which states that -`η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`. - -The current way this result is proved is by using tensor tree manipulations. -There is likely a more direct path to this result. - --/ -open IndexNotation -open CategoryTheory -open MonoidalCategory -open Matrix -open MatrixGroups -open Complex -open TensorProduct -open IndexNotation -open CategoryTheory -open TensorTree -open OverColor.Discrete -noncomputable section - -namespace complexLorentzTensor -open Fermion - -/-- The map to colors one gets when contracting the 4-vector indices pauli matrices. -/ -def pauliMatrixContrPauliMatrixMap := ((Sum.elim - ((Sum.elim ![Color.down, Color.down] ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ - Fin.succAbove 1 ∘ Fin.succAbove 1) ![Color.up, Color.upL, Color.upR] ∘ ⇑finSumFinEquiv.symm) ∘ - Fin.succAbove 0 ∘ Fin.succAbove 2) - -lemma pauliMatrix_contr_lower_0_0_0 : - {(basisVector pauliCoMap (fun | 0 => 0 | 1 => 0 | 2 => 0)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; rhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 1 - funext k - fin_cases k <;> rfl - · congr 1 - funext k - fin_cases k <;> rfl - -lemma pauliMatrix_contr_lower_0_1_1 : - {(basisVector pauliCoMap (fun | 0 => 0 | 1 => 1 | 2 => 1)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - enter [1, 1, 1, 1, 1, 1, 1, 1] - rw [contrBasisVectorMul_pos (by decide)] - conv => - enter [1, 1, 1, 1, 1, 1, 1, 2, 1] - rw [contrBasisVectorMul_pos (by decide)] - conv => - enter [1, 1, 1, 1, 1, 1, 2, 1] - rw [contrBasisVectorMul_neg (by decide)] - conv => - enter [1, 1, 1, 1, 1, 2, 1] - rw [contrBasisVectorMul_neg (by decide)] - conv => - enter [1, 1, 1, 1, 2, 2, 1] - rw [contrBasisVectorMul_neg (by decide)] - conv => - enter [1, 1, 1, 2, 2, 1] - rw [contrBasisVectorMul_neg (by decide)] - conv => - enter [1, 1, 2, 1] - rw [contrBasisVectorMul_neg (by decide)] - conv => - enter [1, 2, 2, 1] - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 1 - decide - · congr 1 - decide - -lemma pauliMatrix_contr_lower_1_0_1 : - {(basisVector pauliCoMap (fun | 0 => 1 | 1 => 0 | 2 => 1)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; rhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 1 - decide - · congr 1 - decide - -lemma pauliMatrix_contr_lower_1_1_0 : - {(basisVector pauliCoMap (fun | 0 => 1 | 1 => 1 | 2 => 0)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) - + basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; rhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 1 - decide - · congr 1 - decide - -lemma pauliMatrix_contr_lower_2_0_1 : - {(basisVector pauliCoMap (fun | 0 => 2 | 1 => 0 | 2 => 1)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) - + (I) • - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; rhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 2 - decide - · congr 2 - decide - -lemma pauliMatrix_contr_lower_2_1_0 : - {(basisVector pauliCoMap (fun | 0 => 2 | 1 => 1 | 2 => 0)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - (-I) • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) - + (I) • - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; lhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; rhs; rhs; lhs; - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 2 - decide - · congr 2 - decide - -lemma pauliMatrix_contr_lower_3_0_0 : - {(basisVector pauliCoMap (fun | 0 => 3 | 1 => 0 | 2 => 0)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) - + (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap - (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; rhs; lhs; - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; rhs; rhs; lhs; - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 2 - decide - · congr 2 - decide - -lemma pauliMatrix_contr_lower_3_1_1 : - {(basisVector pauliCoMap (fun | 0 => 3 | 1 => 1 | 2 => 1)) | μ α β ⊗ - pauliContr | μ α' β'}ᵀ.tensor = - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) - + (-1 : ℂ) • - basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1) := by - conv => - lhs - rw [basis_contr_pauliMatrix_basis_tree_expand_tensor] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; lhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; lhs; rhs; rhs; lhs - rw [contrBasisVectorMul_neg (by decide)] - conv => - lhs; lhs; rhs; lhs; - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs; rhs; rhs; lhs; - rw [contrBasisVectorMul_pos (by decide)] - conv => - lhs - simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add] - rw [basisVectorContrPauli, basisVectorContrPauli] - /- Simplifying. -/ - congr 1 - · congr 2 - decide - · congr 2 - decide - -TODO "Work out why `pauliCo_prod_basis_expand'` is needed, since it is exactly the same - as `pauliCo_prod_basis_expand` which is defined in another file. One will see that - replacing instances of `pauliCo_prod_basis_expand'` with `pauliCo_prod_basis_expand` - does not work." - -/-- This lemma is exactly the same as `pauliCo_prod_basis_expand`. - It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why - `pauliMatrix_lower_basis_expand_prod` does not work. -/ -private lemma pauliCo_prod_basis_expand' {n : ℕ} {c : Fin n → complexLorentzTensor.C} - (t : TensorTree complexLorentzTensor c) : - (TensorTree.prod (tensorNode pauliCo) t).tensor = - ((((tensorNode - (basisVector pauliCoMap fun | 0 => 0 | 1 => 0 | 2 => 0)).prod t).add - (((tensorNode - (basisVector pauliCoMap fun | 0 => 0 | 1 => 1 | 2 => 1)).prod t).add - ((TensorTree.smul (-1) ((tensorNode - (basisVector pauliCoMap fun | 0 => 1 | 1 => 0 | 2 => 1)).prod t)).add - ((TensorTree.smul (-1) ((tensorNode - (basisVector pauliCoMap fun | 0 => 1 | 1 => 1 | 2 => 0)).prod t)).add - ((TensorTree.smul I ((tensorNode - (basisVector pauliCoMap fun | 0 => 2 | 1 => 0 | 2 => 1)).prod t)).add - ((TensorTree.smul (-I) ((tensorNode - (basisVector pauliCoMap fun | 0 => 2 | 1 => 1 | 2 => 0)).prod t)).add - ((TensorTree.smul (-1) ((tensorNode - (basisVector pauliCoMap fun | 0 => 3 | 1 => 0 | 2 => 0)).prod t)).add - ((tensorNode - (basisVector pauliCoMap fun | 0 => 3 | 1 => 1 | 2 => 1)).prod - t))))))))).tensor := by - exact pauliCo_prod_basis_expand _ - -lemma pauliCo_contr_pauliContr_expand_aux : - {pauliCo | μ α β ⊗ pauliContr | μ α' β'}ᵀ.tensor - = ((tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1)).add - ((tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1)).add - ((TensorTree.smul (-1) (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul (-1) (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul I (tensorNode - ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) + - I • - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul (-I) (tensorNode - ((-I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) + - I • basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 0 | 2 => 1 | 3 => 0))).add - ((TensorTree.smul (-1) (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 0 | 3 => 0) + - (-1 : ℂ) • - basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1))).add - (tensorNode - ((basisVector pauliMatrixContrPauliMatrixMap fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) + - (-1 : ℂ) • basisVector pauliMatrixContrPauliMatrixMap - fun | 0 => 1 | 1 => 1 | 2 => 1 | 3 => 1))))))))).tensor := by - rw [contr_tensor_eq <| pauliCo_prod_basis_expand' _] - /- Moving contraction through addition. -/ - rw [contr_add] - rw [add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| contr_add _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| contr_add _ _] - /- Moving contraction through smul. -/ - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| - contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| contr_smul _ _] - /- Replacing the contractions. -/ - rw [add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_0_0_0] - rw [add_tensor_eq_snd <| add_tensor_eq_fst <| eq_tensorNode_of_eq_tensor <| - pauliMatrix_contr_lower_0_1_1] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| - eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_0_1] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| - smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_1_1_0] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor <| - pauliMatrix_contr_lower_2_0_1] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| eq_tensorNode_of_eq_tensor - <| pauliMatrix_contr_lower_2_1_0] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| - eq_tensorNode_of_eq_tensor <| pauliMatrix_contr_lower_3_0_0] - rw [add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| eq_tensorNode_of_eq_tensor <| - pauliMatrix_contr_lower_3_1_1] - -lemma pauliCo_contr_pauliContr_expand : - {pauliCo | ν α β ⊗ pauliContr | ν α' β'}ᵀ.tensor = - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 0 | 2 => 1 | 3 => 1) - + 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 1 | 2 => 0 | 3 => 0) - - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) - - 2 • basisVector pauliMatrixContrPauliMatrixMap (fun | 0 => 1 | 1 => 0 | 2 => 0 | 3 => 1) := by - rw [pauliCo_contr_pauliContr_expand_aux] - simp only [Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, neg_smul, - one_smul, add_tensor, tensorNode_tensor, smul_tensor, smul_add, smul_neg, _root_.smul_smul, - neg_mul, _root_.neg_neg] - ring_nf - rw [Complex.I_sq] - simp only [neg_smul, one_smul, _root_.neg_neg] - abel - -/-- The statement that `η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`. -/ -theorem pauliCo_contr_pauliContr : - {pauliCo | ν α β ⊗ pauliContr | ν α' β' = 2 •ₜ εL | α α' ⊗ εR | β β'}ᵀ := by - rw [pauliCo_contr_pauliContr_expand] - rw [perm_tensor_eq <| smul_tensor_eq <| leftMetric_prod_rightMetric_tree] - rw [perm_smul] - /- Moving perm through adds. -/ - rw [smul_tensor_eq <| perm_add _ _ _] - rw [smul_tensor_eq <| add_tensor_eq_snd <| perm_add _ _ _] - rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| perm_add _ _ _] - /- Moving perm through smul. -/ - rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| perm_smul _ _ _] - rw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd - <| add_tensor_eq_fst <| perm_smul _ _ _] - /- Perm acting on basis. -/ - erw [smul_tensor_eq <| add_tensor_eq_fst <| perm_basisVector_tree _ _] - erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_fst <| smul_tensor_eq <| - perm_basisVector_tree _ _] - erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_fst <| - smul_tensor_eq <| perm_basisVector_tree _ _] - erw [smul_tensor_eq <| add_tensor_eq_snd <| add_tensor_eq_snd <| add_tensor_eq_snd <| - perm_basisVector_tree _ _] - /- Simplifying. -/ - simp only [smul_tensor, add_tensor, tensorNode_tensor] - have h1 (b0011 b1100 b0110 b1001 : CoeSort.coe (complexLorentzTensor.F.obj - (OverColor.mk pauliMatrixContrPauliMatrixMap))) : - ((2 • b0011 + 2 • b1100) - 2 • b0110 - 2 • b1001) = (2 : ℂ) • ((b0011) + - (((-1 : ℂ)• b0110) + (((-1 : ℂ) •b1001) + b1100))) := by - trans (2 : ℂ) • b0011 + (2 : ℂ) • b1100 - ((2 : ℂ) • b0110) - ((2 : ℂ) • b1001) - · repeat rw [two_smul] - · simp only [neg_smul, one_smul, smul_add, smul_neg] - abel - rw [h1] - congr - · decide - · decide - · decide - · decide - -end complexLorentzTensor diff --git a/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Relations.lean b/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Relations.lean new file mode 100644 index 00000000..d6884ef5 --- /dev/null +++ b/PhysLean/Lorentz/ComplexTensor/PauliMatrices/Relations.lean @@ -0,0 +1,79 @@ +/- +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 PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basis +/-! + +## Contractiong of indices of Pauli matrix. + +The main result of this file is `pauliMatrix_contract_pauliMatrix` which states that +`η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}`. + +The current way this result is proved is by using tensor tree manipulations. +There is likely a more direct path to this result. + +-/ +open IndexNotation +open CategoryTheory +open MonoidalCategory +open Matrix +open MatrixGroups +open Complex +open TensorProduct +open IndexNotation +open CategoryTheory +open TensorTree +open OverColor.Discrete +noncomputable section + +namespace complexLorentzTensor +open Fermion + +/-- The statement that `ηᵤᵥ σᵘᵃᵇ σᵛᵃ'ᵇ' = 2 εᵃᵃ' εᵇᵇ'`. -/ +theorem pauliCo_contr_pauliContr : + {pauliCo | ν α β ⊗ pauliContr | ν α' β' = 2 •ₜ εL | α α' ⊗ εR | β β'}ᵀ := by + apply (complexLorentzTensor.tensorBasis _).repr.injective + ext b + conv_rhs => + rw [TensorTree.perm_tensorBasis_repr_apply] + rw [TensorTree.smul_tensorBasis_repr] + simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero, + Function.comp_apply, OverColor.mk_hom, OverColor.equivToHomEq_toEquiv, Finsupp.coe_smul, + Pi.smul_apply, smul_eq_mul] + rw (transparency := .instances) [TensorTree.prod_tensorBasis_repr_apply] + simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero, + Function.comp_apply, tensorNode_tensor] + rw [leftMetric_eq_ofRat, rightMetric_eq_ofRat] + simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero, + Function.comp_apply, cons_val_zero, cons_val_one, head_cons, ofRat_tensorBasis_repr_apply] + rw [← PhysLean.RatComplexNum.toComplexNum.map_mul] + erw [PhysLean.RatComplexNum.ofNat_mul_toComplexNum 2] + rw [TensorTree.contr_tensorBasis_repr_apply] + conv_lhs => + enter [2, x] + rw [TensorTree.prod_tensorBasis_repr_apply] + simp only [pauliCo_ofRat, pauliContr_ofRat] + simp only [Fin.isValue, Function.comp_apply, + tensorNode_tensor, ofRat_tensorBasis_repr_apply, Monoidal.tensorUnit_obj, + Action.instMonoidalCategory_tensorUnit_V, Equivalence.symm_inverse, + Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj, + Functor.comp_obj, Discrete.functor_obj_eq_as, Fin.zero_succAbove, Fin.reduceSucc, + Fin.cast_eq_self, Nat.cast_ofNat, mul_ite, mul_neg, mul_one, mul_zero] + left + rw (transparency := .instances) [ofRat_tensorBasis_repr_apply] + rw [← PhysLean.RatComplexNum.toComplexNum.map_mul] + conv_lhs => + enter [2, x] + right + rw (transparency := .instances) [contr_basis_ratComplexNum] + conv_lhs => + enter [2, x] + rw [← PhysLean.RatComplexNum.toComplexNum.map_mul] + rw [← map_sum PhysLean.RatComplexNum.toComplexNum] + apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr + revert b + decide +kernel + +end complexLorentzTensor diff --git a/PhysLean/Lorentz/PauliMatrices/AsTensor.lean b/PhysLean/Lorentz/PauliMatrices/AsTensor.lean index df3c3a2e..a32b1971 100644 --- a/PhysLean/Lorentz/PauliMatrices/AsTensor.lean +++ b/PhysLean/Lorentz/PauliMatrices/AsTensor.lean @@ -189,7 +189,7 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ /-- The map `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ rightHanded` corresponding to Pauli matrices, when evaluated on `1` corresponds to the tensor `PauliMatrix.asTensor`. -/ lemma asConsTensor_apply_one : asConsTensor.hom (1 : ℂ) = asTensor := by - change (1 : ℂ) • asTensor = asTensor + change (1 : ℂ) • asTensor = asTensor simp only [asConsTensor, one_smul] end diff --git a/PhysLean/Lorentz/Weyl/Unit.lean b/PhysLean/Lorentz/Weyl/Unit.lean index 81abb993..699d7256 100644 --- a/PhysLean/Lorentz/Weyl/Unit.lean +++ b/PhysLean/Lorentz/Weyl/Unit.lean @@ -157,7 +157,7 @@ def rightAltRightUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ altRightHa simp lemma rightAltRightUnit_apply_one : rightAltRightUnit.hom (1 : ℂ) = rightAltRightUnitVal := by - change (1 : ℂ) • rightAltRightUnitVal = rightAltRightUnitVal + change (1 : ℂ) • rightAltRightUnitVal = rightAltRightUnitVal simp only [rightAltRightUnit, one_smul] /-- The alt-right-right unit `δ_{dot a}^{dot a}` as an element of diff --git a/PhysLean/Mathematics/RatComplexNum.lean b/PhysLean/Mathematics/RatComplexNum.lean new file mode 100644 index 00000000..3435c2f8 --- /dev/null +++ b/PhysLean/Mathematics/RatComplexNum.lean @@ -0,0 +1,245 @@ +/- +Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +import Mathlib.Analysis.Complex.Basic +/-! +# Rational complex numbers + +-/ + +namespace PhysLean + +/-- Rational complex numbers. This type is mainly used when decidability is needed. -/ +structure RatComplexNum where + /-- The real part of a `RatComplexNum`. -/ + fst : ℚ + /-- The imaginary part of a `RatComplexNum`. -/ + snd : ℚ + +namespace RatComplexNum + +@[ext] +lemma ext {x y : RatComplexNum} (h1 : x.1 = y.1) (h2 : x.2 = y.2) : x = y := by + cases x + cases y + simp at h1 h2 + subst h1 h2 + rfl + +/-- The equivalence as a type of `RatComplexNum` with `ℚ × ℚ`. -/ +def equivToProd : RatComplexNum ≃ ℚ × ℚ where + toFun := fun x => (x.1, x.2) + invFun := fun x => ⟨x.1, x.2⟩ + left_inv := by + intro x + cases x + rfl + right_inv := by + intro x + cases x + rfl + +instance : DecidableEq RatComplexNum := Equiv.decidableEq equivToProd + +instance : AddCommGroup RatComplexNum where + add := fun x y => ⟨x.fst + y.fst, x.snd + y.snd⟩ + add_assoc := by + intro a b c + match a, b, c with + | ⟨a1, a2⟩, ⟨b1, b2⟩, ⟨c1, c2⟩ => + ext + · change a1 + b1 + c1 = a1 + (b1 + c1) + ring + · change a2 + b2 + c2 = a2 + (b2 + c2) + ring + zero := ⟨0, 0⟩ + zero_add := by + intro a + match a with + | ⟨a1, a2⟩ => + ext + · change 0 + a1 = a1 + simp + · change 0 + a2 = a2 + simp + add_zero := by + intro a + match a with + | ⟨a1, a2⟩ => + ext + · change a1 + 0 = a1 + simp + · change a2 + 0 = a2 + simp + nsmul := fun n x => ⟨n • x.fst, n • x.snd⟩ + neg := fun x => ⟨-x.fst, -x.snd⟩ + zsmul := fun n x => ⟨n • x.1, n • x.2⟩ + neg_add_cancel := by + intro a + match a with + | ⟨a1, a2⟩ => + ext + · change -a1 + a1 = 0 + simp + · change -a2 + a2 = 0 + simp + add_comm := by + intro x y + match x, y with + | ⟨x1, x2⟩, ⟨y1, y2⟩ => + ext + · change x1 + y1 = y1 + x1 + simp [add_comm] + · change x2 + y2 = y2 + x2 + simp [add_comm] + +instance : Ring RatComplexNum where + mul := fun x y => ⟨x.fst * y.fst - x.snd * y.snd, x.fst * y.snd + x.snd * y.fst⟩ + one := ⟨1, 0⟩ + mul_assoc := by + intro x y z + match x, y, z with + | ⟨x1, x2⟩, ⟨y1, y2⟩, ⟨z1, z2⟩ => + ext + · change (x1 * y1 - x2 * y2) * z1 - (x1 * y2 + x2 * y1) * z2 = + x1 * (y1 * z1 - y2 * z2) - x2 * (y1 * z2 + y2 * z1) + ring + · change (x1 * y1 - x2 * y2) * z2 + (x1 * y2 + x2 * y1) * z1 = + x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 - y2 * z2) + ring + one_mul := by + intro x + match x with + | ⟨x1, x2⟩ => + ext + · change 1 * x1 - 0 * x2 = x1 + simp + · change 1 * x2 + 0 * x1 = x2 + simp + mul_one := by + intro x + match x with + | ⟨x1, x2⟩ => + ext + · change x1 * 1 - x2 * 0 = x1 + simp + · change x1 * 0 + x2 * 1 = x2 + simp + + left_distrib := by + intro a b c + match a, b, c with + | ⟨a1, a2⟩, ⟨b1, b2⟩, ⟨c1, c2⟩ => + ext + · change a1 * (b1 + c1) - a2 * (b2 + c2) = + (a1 * b1 - a2 * b2) + (a1 * c1 - a2 * c2) + ring + · change a1 * (b2 + c2) + a2 * (b1 + c1) = + (a1 * b2 + a2 * b1) + (a1 * c2 + a2 * c1) + ring + right_distrib := by + intro a b c + match a, b, c with + | ⟨b1, b2⟩, ⟨c1, c2⟩, ⟨a1, a2⟩ => + ext + · change (b1 + c1) * a1 - (b2 + c2) * a2 = + (b1 * a1 - b2 * a2) + (c1 * a1 - c2 * a2) + ring + · change (b1 + c1) * a2 + (b2 + c2) * a1 = + (b1 * a2 + b2 * a1) + (c1 * a2 + c2 * a1) + ring + zero_mul := by + intro a + match a with + | ⟨a1, a2⟩ => + ext + · change 0 * a1 - 0 * a2 = 0 + simp + · change 0 * a2 + 0 * a1 = 0 + simp + mul_zero := by + intro a + match a with + | ⟨a1, a2⟩ => + ext + · change a1 * 0 - a2 * 0 = 0 + simp + · change a1 * 0 + a2 * 0 = 0 + simp + zsmul := fun n x => ⟨n • x.1, n • x.2⟩ + neg_add_cancel := by + intro a + match a with + | ⟨a1, a2⟩ => + ext + · change -a1 + a1 = 0 + simp + · change -a2 + a2 = 0 + simp + +@[simp] +lemma one_fst : (1 : RatComplexNum).fst = 1 := rfl + +@[simp] +lemma one_snd : (1 : RatComplexNum).snd = 0 := rfl + +@[simp] +lemma add_fst (x y : RatComplexNum) : (x + y).fst = x.fst + y.fst := rfl + +@[simp] +lemma add_snd (x y : RatComplexNum) : (x + y).snd = x.snd + y.snd := rfl + +@[simp] +lemma mul_fst (x y : RatComplexNum) : (x * y).fst = x.fst * y.fst - x.snd * y.snd := rfl + +@[simp] +lemma mul_snd (x y : RatComplexNum) : (x * y).snd = x.fst * y.snd + x.snd * y.fst := rfl + +@[simp] +lemma zero_fst : (0 : RatComplexNum).fst = 0 := rfl + +@[simp] +lemma zero_snd : (0 : RatComplexNum).snd = 0 := rfl + +open Complex + +/-- The inclusion of `RatComplexNum` into the complex numbers. -/ +noncomputable def toComplexNum : RatComplexNum →+* ℂ where + toFun := fun x => x.fst + x.snd * I + map_one' := by + simp + map_add' a b := by + simp only [add_fst, Rat.cast_add, add_snd] + ring + map_mul' a b := by + simp only [mul_fst, Rat.cast_sub, Rat.cast_mul, mul_snd, Rat.cast_add] + ring_nf + simp only [I_sq, mul_neg, mul_one] + ring + map_zero' := by + simp + +@[simp] +lemma I_mul_toComplexNum (a : RatComplexNum) : I * toComplexNum a = toComplexNum (⟨0, 1⟩ * a) := by + simp [toComplexNum] + ring_nf + simp only [I_sq, neg_mul, one_mul] + ring + +lemma ofNat_mul_toComplexNum (n : ℕ) (a : RatComplexNum) : + n * toComplexNum a = toComplexNum (n * a) := by + simp only [map_mul, map_natCast] + +lemma toComplexNum_injective : Function.Injective toComplexNum := by + intro a b ha + simp [toComplexNum] at ha + rw [@Complex.ext_iff] at ha + simp at ha + ext + · exact ha.1 + · exact ha.2 + +end RatComplexNum +end PhysLean diff --git a/PhysLean/Meta/Basic.lean b/PhysLean/Meta/Basic.lean index 81fec45b..8e4108a5 100644 --- a/PhysLean/Meta/Basic.lean +++ b/PhysLean/Meta/Basic.lean @@ -142,7 +142,7 @@ def getDeclString (name : Name) : CoreM String := do | none => return "" /-- Given a name, returns the source code defining that name, - starting with the def ... or lemma... etc. -/ + starting with the def ... or lemma... etc. -/ def getDeclStringNoDoc (name : Name) : CoreM String := do let declerationString ← getDeclString name let headerLine (line : String) : Bool := diff --git a/PhysLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/PhysLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean index 24260be6..7bd8dcd7 100644 --- a/PhysLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean +++ b/PhysLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean @@ -230,7 +230,7 @@ The proof of this result ultimately goes as follows - `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ` (considered as a list with one element) with `ofCrAnList φsn` as a sum of super commutators, one for each element of `φsn`. -- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to rearrange +- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to rearrange terms. - Properties of ordered lists, and `normalOrderSign_eraseIdx` are then used to complete the proof. -/ @@ -356,7 +356,7 @@ The proof ultimately goes as follows: `crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)`. -- It used that `anPart φ * 𝓝(φ₀φ₁…φₙ)` is equal to +- It used that `anPart φ * 𝓝(φ₀φ₁…φₙ)` is equal to `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]` diff --git a/PhysLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean b/PhysLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean index 6d6522c2..c1d9957e 100644 --- a/PhysLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean +++ b/PhysLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean @@ -41,7 +41,7 @@ lemma staticWickTerm_empty_nil : /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, and an element `φ` of - `𝓕.FieldOp`, then `(φsΛ ↩Λ φ 0 none).staticWickTerm` is equal to + `𝓕.FieldOp`, then `(φsΛ ↩Λ φ 0 none).staticWickTerm` is equal to `φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)` @@ -118,7 +118,7 @@ holds `φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ 0 k).staticWickTerm` -where the sum is over all `k` in `Option φsΛ.uncontracted`, so `k` is either `none` or `some k`. +where the sum is over all `k` in `Option φsΛ.uncontracted`, so `k` is either `none` or `some k`. The proof proceeds as follows: - `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as diff --git a/PhysLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean b/PhysLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean index e75e3c31..3980070b 100644 --- a/PhysLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean +++ b/PhysLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean @@ -112,7 +112,7 @@ For a list `φs` of `𝓕.FieldOp`, then `𝓣(φs)` is equal to the sum of - `∑ φsΛ, φsΛ.wickTerm` where the sum is over all Wick contraction `φsΛ` which have no contractions of equal time. -- `∑ φsΛ, φsΛ.sign • φsΛ.timeContract * (∑ φssucΛ, φssucΛ.wickTerm)`, where +- `∑ φsΛ, φsΛ.sign • φsΛ.timeContract * (∑ φssucΛ, φssucΛ.wickTerm)`, where the first sum is over all Wick contraction `φsΛ` which only have equal time contractions and the second sum is over all Wick contraction `φssucΛ` of the uncontracted elements of `φsΛ` which do not have any equal time contractions. diff --git a/PhysLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/PhysLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean index ff815d07..75ec7e37 100644 --- a/PhysLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean +++ b/PhysLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean @@ -72,7 +72,7 @@ lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp simpa using congrFun hg x /-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`, - `ofCrAnListF φs` is defined as the element of `𝓕.FieldOpFreeAlgebra` + `ofCrAnListF φs` is defined as the element of `𝓕.FieldOpFreeAlgebra` obtained by the product of `ofCrAnListF φ` for each `φ` in `φs`. For example `ofCrAnListF [φ₁, φ₂, φ₃] = ofCrAnOpF φ₁ * ofCrAnOpF φ₂ * ofCrAnOpF φ₃`. The set of all `ofCrAnListF φs` forms a basis of `FieldOpFreeAlgebra 𝓕`. -/ @@ -91,8 +91,8 @@ lemma ofCrAnListF_append (φs φs' : List 𝓕.CrAnFieldOp) : lemma ofCrAnListF_singleton (φ : 𝓕.CrAnFieldOp) : ofCrAnListF [φ] = ofCrAnOpF φ := by simp [ofCrAnListF] -/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`, - `ofFieldOpF φ` is the element of `𝓕.FieldOpFreeAlgebra` formed by summing over +/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`, + `ofFieldOpF φ` is the element of `𝓕.FieldOpFreeAlgebra` formed by summing over `ofCrAnOpF` of the creation and annihilation parts of `φ`. diff --git a/PhysLean/PerturbationTheory/FieldSpecification/Basic.lean b/PhysLean/PerturbationTheory/FieldSpecification/Basic.lean index 508f47c5..2d461640 100644 --- a/PhysLean/PerturbationTheory/FieldSpecification/Basic.lean +++ b/PhysLean/PerturbationTheory/FieldSpecification/Basic.lean @@ -88,7 +88,7 @@ As an example, if `f` corresponds to a Weyl-fermion field, then - `position f e x`, `e` would correspond to a Lorentz index `a`, and `position f e x` would, once represented in the operator algebra, be proportional to the operator - `∑ s, ∫ d³p/(…) (xₐ(p,s) a(p, s) e ^ (-i p x) + yₐ(p,s) a†(p, s) e ^ (-i p x))`. + `∑ s, ∫ d³p/(…) (xₐ(p,s) a(p, s) e ^ (-i p x) + yₐ(p,s) a†(p, s) e ^ (-i p x))`. - `outAsymp f e p`, `e` would correspond to a spin `s`, and `outAsymp f e p` would, once represented in the operator algebra, be proportional to the diff --git a/PhysLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean b/PhysLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean index 91151894..11eba04a 100644 --- a/PhysLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean +++ b/PhysLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean @@ -83,7 +83,7 @@ As an example, if `f` corresponds to a Weyl-fermion field, it would contribute - For each each Lorentz index `a`, an element corresponding to the creation part of a position operator: - `∑ s, ∫ d³p/(…) (xₐ (p,s) a(p, s) e ^ (-i p x))`. + `∑ s, ∫ d³p/(…) (xₐ (p,s) a(p, s) e ^ (-i p x))`. - For each each Lorentz index `a`,an element corresponding to annihilation part of a position operator: @@ -106,7 +106,7 @@ lemma crAnFieldOpToFieldOp_prod (s : 𝓕.FieldOp) (t : 𝓕.fieldOpToCrAnType s field operator. otherwise it takes `φ` to `annihilate`. - -/ +-/ def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate | ⟨FieldOp.inAsymp _, _⟩ => CreateAnnihilate.create | ⟨FieldOp.position _, CreateAnnihilate.create⟩ => CreateAnnihilate.create diff --git a/PhysLean/Tensors/OverColor/Lift.lean b/PhysLean/Tensors/OverColor/Lift.lean index 66b70983..9a0fa529 100644 --- a/PhysLean/Tensors/OverColor/Lift.lean +++ b/PhysLean/Tensors/OverColor/Lift.lean @@ -174,8 +174,7 @@ def ε : 𝟙_ (Rep k G) ≅ objObj' F (𝟙_ (OverColor C)) := simp only [objObj'_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, - ModuleCat.comp_apply] + Category.id_comp, LinearEquiv.coe_coe, ModuleCat.comp_apply] rw [ModuleCat.hom_comp, ModuleCat.hom_comp] simp only [objObj'_V_carrier, instMonoidalCategoryStruct_tensorUnit_left, instMonoidalCategoryStruct_tensorUnit_hom, LinearEquiv.toModuleIso_hom, ModuleCat.hom_ofHom, @@ -338,7 +337,7 @@ lemma μ_natural_right {X Y : OverColor C} (X' : OverColor C) (f : X ⟶ Y) : rw [objMap'_tprod] rw [ModuleCat.Hom.hom, ConcreteCategory.hom] simp only [ModuleCat.instConcreteCategoryLinearMapIdCarrier, LinearMap.coe_comp, - Function.comp_apply] + Function.comp_apply] conv_lhs => right change (PiTensorProduct.tprod k) p ⊗ₜ[k] (objMap' F f).hom ((PiTensorProduct.tprod k) q) @@ -843,7 +842,7 @@ def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c refine LinearMap.ext (fun x => ?_) rw [ModuleCat.Hom.hom, ConcreteCategory.hom, ModuleCat.Hom.hom, ConcreteCategory.hom] simp only [ModuleCat.instConcreteCategoryLinearMapIdCarrier, LinearMap.coe_comp, - Function.comp_apply] + Function.comp_apply] simp only [forgetLiftAppV, Fin.isValue] refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by simp_rw [map_add, hx, hy] diff --git a/PhysLean/Tensors/TensorSpecies/Basic.lean b/PhysLean/Tensors/TensorSpecies/Basic.lean index b441b7cd..7bb7868e 100644 --- a/PhysLean/Tensors/TensorSpecies/Basic.lean +++ b/PhysLean/Tensors/TensorSpecies/Basic.lean @@ -221,7 +221,7 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) rw [TensorProduct.map_tmul] conv_lhs => erw [lift.map_tprod] - simp only [ CategoryStruct.comp, Functor.id_obj, + simp only [CategoryStruct.comp, Functor.id_obj, instMonoidalCategoryStruct_tensorObj_hom, mk_hom, Sum.elim_inl, Function.comp_apply, instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv, Equiv.refl_symm] congr 1 @@ -332,7 +332,7 @@ lemma tensorToVec_naturality_eqToHom_apply (c c1 : S.C) (h : c = c1) -/ /-- The lift of a linear map `(S.F.obj (OverColor.mk c) →ₗ[S.k] E)` to a - multi-linear map from `fun i => S.FD.obj (Discrete.mk (c i))` (i.e. pure tensors) to `E`. -/ + multi-linear map from `fun i => S.FD.obj (Discrete.mk (c i))` (i.e. pure tensors) to `E`. -/ def liftTensor {n : ℕ} {c : Fin n → S.C} {E : Type} [AddCommMonoid E] [Module S.k E]: MultilinearMap S.k (fun i => S.FD.obj (Discrete.mk (c i))) E ≃ₗ[S.k] (S.F.obj (OverColor.mk c) →ₗ[S.k] E) := diff --git a/PhysLean/Tensors/TensorSpecies/Basis.lean b/PhysLean/Tensors/TensorSpecies/Basis.lean index 29a7afdc..5084d234 100644 --- a/PhysLean/Tensors/TensorSpecies/Basis.lean +++ b/PhysLean/Tensors/TensorSpecies/Basis.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import PhysLean.Tensors.TensorSpecies.Basic +import PhysLean.Tensors.TensorSpecies.Contractions.ContrMap /-! # Basis for tensors in a tensor species @@ -14,7 +15,6 @@ open IndexNotation open CategoryTheory open MonoidalCategory - namespace TensorSpecies open OverColor @@ -22,8 +22,8 @@ variable (S : TensorSpecies) noncomputable section /-- - The multi-linear map from `(fun i => S.FD.obj (Discrete.mk (c i)))` to `S.k` giving - the coordinate with respect to the basis described by `b`. + The multi-linear map from `(fun i => S.FD.obj (Discrete.mk (c i)))` to `S.k` giving + the coordinate with respect to the basis described by `b`. -/ def coordinateMultiLinearSingle {n : ℕ} (c : Fin n → S.C) (b : Π j, Fin (S.repDim (c j))) : MultilinearMap S.k (fun i => S.FD.obj (Discrete.mk (c i))) S.k where @@ -61,9 +61,9 @@ def coordinateMultiLinearSingle {n : ℕ} (c : Fin n → S.C) (b : Π j, Fin (S. simp only [mul_assoc, hjx] /-- - The multi-linear map from `(fun i => S.FD.obj (Discrete.mk (c i)))` to - `((Π j, Fin (S.repDim (c j))) → S.k)` giving - the coordinates with respect to the basis defined in `S`. + The multi-linear map from `(fun i => S.FD.obj (Discrete.mk (c i)))` to + `((Π j, Fin (S.repDim (c j))) → S.k)` giving + the coordinates with respect to the basis defined in `S`. -/ def coordinateMultiLinear {n : ℕ} (c : Fin n → S.C) : MultilinearMap S.k (fun i => S.FD.obj (Discrete.mk (c i))) @@ -80,7 +80,7 @@ def coordinateMultiLinear {n : ℕ} (c : Fin n → S.C) : /-- The linear map from tensors to coordinates. -/ def coordinate {n : ℕ} (c : Fin n → S.C) : - S.F.obj (OverColor.mk c) →ₗ[S.k] ((Π j, Fin (S.repDim (c j))) → S.k) := + S.F.obj (OverColor.mk c) →ₗ[S.k] ((Π j, Fin (S.repDim (c j))) → S.k) := (S.liftTensor (c := c)).toFun (S.coordinateMultiLinear c) lemma coordinate_tprod {n : ℕ} (c : Fin n → S.C) (x : (i : Fin n) → S.FD.obj (Discrete.mk (c i))) : @@ -120,7 +120,7 @@ def fromCoordinates {n : ℕ} (c : Fin n → S.C) : map_smul' fb r := by simp [smul_smul, Finset.smul_sum] -lemma coordinate_fromCoordinate_left_inv {n : ℕ} (c : Fin n → S.C) : +lemma coordinate_fromCoordinate_left_inv {n : ℕ} (c : Fin n → S.C) : Function.LeftInverse (S.fromCoordinates c) (S.coordinate c) := by intro x refine PiTensorProduct.induction_on' x (fun r b => ?_) <| fun x y hx hy => by @@ -133,7 +133,7 @@ lemma coordinate_fromCoordinate_left_inv {n : ℕ} (c : Fin n → S.C) : coordinateMultiLinearSingle, MultilinearMap.coe_mk, LinearMap.coe_mk, AddHom.coe_mk] have h1 (x : (j : Fin n) → Fin (S.repDim (c j))) : (∏ i : Fin n, ((S.basis (c i)).repr (b i)) (x i)) • - ((PiTensorProduct.tprod S.k) fun i => (S.basis (c i) (x i)) ) + ((PiTensorProduct.tprod S.k) fun i => (S.basis (c i) (x i))) = (PiTensorProduct.tprod S.k) fun i => (((S.basis (c i)).repr (b i)) (x i)) • (S.basis (c i) (x i)) := Eq.symm @@ -151,20 +151,19 @@ lemma coordinate_fromCoordinate_left_inv {n : ℕ} (c : Fin n → S.C) : simp only [mk_hom] exact Basis.sum_equivFun (S.basis (c i)) (b i) -lemma coordinate_fromCoordinate_right_inv {n : ℕ} (c : Fin n → S.C) : +lemma coordinate_fromCoordinate_right_inv {n : ℕ} (c : Fin n → S.C) : Function.RightInverse (S.fromCoordinates c) (S.coordinate c) := by intro x simp only [fromCoordinates, LinearMap.coe_mk, AddHom.coe_mk, map_sum, map_smul] funext fb simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] - change ∑ gb : (j : Fin n) → Fin (S.repDim (c j)), x gb * - ((S.coordinate c) (S.basisVector c gb) fb) = _ + change ∑ gb : (j : Fin n) → Fin (S.repDim (c j)), x gb * + ((S.coordinate c) (S.basisVector c gb) fb) = _ conv_lhs => enter [2, x] rw [coordinate_basisVector] simp - /-- The basis of tensors. -/ def tensorBasis {n : ℕ} (c : Fin n → S.C) : Basis (Π j, Fin (S.repDim (c j))) S.k (S.F.obj (OverColor.mk c)) where @@ -186,16 +185,23 @@ lemma tensorBasis_eq_basisVector {n : ℕ} (c : Fin n → S.C) (b : Π j, Fin (S end - namespace TensorBasis variable {S : TensorSpecies} +lemma tensorBasis_repr_tprod {n : ℕ} {c : Fin n → S.C} + (x : (i : Fin n) → S.FD.obj (Discrete.mk (c i))) + (b : Π j, Fin (S.repDim (c j))) : + (S.tensorBasis c).repr (PiTensorProduct.tprod S.k x) b = + ∏ i, (S.basis (c i)).repr (x i) (b i) := by + change S.coordinate c (PiTensorProduct.tprod S.k x) b = _ + rw [coordinate_tprod] + rfl + /-- The equivalence between the indexing set of basis of Lorentz tensors induced by an equivalence on indices. -/ def congr {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} - (σ : Fin n ≃ Fin m) - (h : ∀ i, c i = c1 (σ i)) : + (σ : Fin n ≃ Fin m) (h : ∀ i, c i = c1 (σ i)) : (Π j, Fin (S.repDim (c1 j))) ≃ Π j, Fin (S.repDim (c j)) where toFun b := fun i => Fin.cast (congrArg S.repDim (h i).symm) (b (σ i)) invFun b := fun i => Fin.cast (congrArg S.repDim (by simp [h])) (b (σ.symm i)) @@ -214,9 +220,104 @@ def congr {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} · exact Equiv.symm_apply_apply σ i · exact Equiv.symm_apply_apply σ i +/-- The equivalence between the coordinate parameters + `(Π j, Fin (S.repDim (Sum.elim c c1 j)))` and + `(Π j, Fin (S.repDim (c j))) × (Π j, Fin (S.repDim (c1 j)))` formed by + splitting up based on `j`. -/ +def elimEquiv {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} : + (Π j, Fin (S.repDim (Sum.elim c c1 j))) ≃ + (Π j, Fin (S.repDim (c j))) × (Π j, Fin (S.repDim (c1 j))) where + toFun b := (fun i => b (Sum.inl i), fun i => b (Sum.inr i)) + invFun b := fun i => Sum.elim (fun i => b.1 i) (fun j => b.2 j) i + left_inv b := by + funext i + cases i + · simp + · simp + right_inv b := by + simp + +/-- The equivalence between the coordinate parameters + `(Π j, Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j))))` and + `(Π j, Fin (S.repDim (c j))) × (Π j, Fin (S.repDim (c1 j)))` formed by + splitting up based on `j`. -/ +def prodEquiv {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} : + (Π j, Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) ≃ + (Π j, Fin (S.repDim (c j))) × (Π j, Fin (S.repDim (c1 j))) := + (Equiv.piCongrLeft _ finSumFinEquiv.symm).trans elimEquiv + +@[simp] +lemma prodEquiv_apply_fst {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} + (b : Π j, Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) + (j : Fin n) : + (prodEquiv b).1 j = (Fin.cast (by simp) (b (Fin.castAdd m j))) := by + simp [prodEquiv, elimEquiv, Fin.cast_eq_cast] + exact eqRec_eq_cast _ (Equiv.apply_symm_apply finSumFinEquiv.symm (Sum.inl j)) + +@[simp] +lemma prodEquiv_apply_snd {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} + (b : Π j, Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) + (j : Fin m) : + (prodEquiv b).2 j = (Fin.cast (by simp) (b (Fin.natAdd n j))) := by + simp [prodEquiv, elimEquiv, Fin.cast_eq_cast] + exact eqRec_eq_cast _ (Equiv.apply_symm_apply finSumFinEquiv.symm (Sum.inr j)) + +lemma tensorBasis_prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} + (b : Π j, Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) : + S.tensorBasis (Sum.elim c c1 ∘ finSumFinEquiv.symm) b = + (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom + ((Functor.LaxMonoidal.μ S.F _ _).hom + (S.tensorBasis c (prodEquiv b).1 ⊗ₜ[S.k] S.tensorBasis c1 (prodEquiv b).2)) := by + rw [tensorBasis_eq_basisVector, basisVector] + rw [tensorBasis_eq_basisVector, basisVector] + rw [tensorBasis_eq_basisVector, basisVector] + simp only [F_def] + conv_rhs => + right + erw [lift.μ_tmul_tprod] + erw [lift.objMap'_tprod] + congr + funext i + simp [lift.discreteFunctorMapEqIso] + have hj (j : Fin n ⊕ Fin m) (hj : finSumFinEquiv.symm i = j) : (S.basis (Sum.elim c c1 j)) (b i) = + (lift.discreteSumEquiv' S.FD j) + (PhysLean.PiTensorProduct.elimPureTensor (fun i => (S.basis (c i)) ((prodEquiv b).1 i)) + (fun i => (S.basis (c1 i)) ((prodEquiv b).2 i)) j) := by + match j with + | Sum.inl j => + simp [PhysLean.PiTensorProduct.elimPureTensor, lift.discreteSumEquiv'] + have hi : i = finSumFinEquiv (Sum.inl j) := + (Equiv.symm_apply_eq finSumFinEquiv).mp hj + subst hi + congr + simp only [finSumFinEquiv_apply_left] + ext + simp only [Fin.val_natCast, Fin.coe_cast] + refine Nat.mod_eq_of_lt ?_ + simpa using (b (Fin.castAdd m j)).2 + | Sum.inr j => + simp [PhysLean.PiTensorProduct.elimPureTensor, lift.discreteSumEquiv'] + have hi : i = finSumFinEquiv (Sum.inr j) := + (Equiv.symm_apply_eq finSumFinEquiv).mp hj + subst hi + congr + simp only [finSumFinEquiv_apply_right] + ext + simp only [Fin.val_natCast, Fin.coe_cast] + refine Nat.mod_eq_of_lt ?_ + simpa using (b (Fin.natAdd n j)).2 + have hj := hj (finSumFinEquiv.symm i) rfl + refine Eq.trans (Eq.trans ?_ hj) ?_ + congr + exact Eq.symm (Fin.cast_val_eq_self (b i)) + congr + funext i + simp only [prodEquiv_apply_fst] + funext i + simp + lemma map_tensorBasis {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} - {σ : (OverColor.mk c) ⟶ (OverColor.mk c1)} - (b : Π j, Fin (S.repDim (c j))) : + {σ : (OverColor.mk c) ⟶ (OverColor.mk c1)} (b : Π j, Fin (S.repDim (c j))) : (S.F.map σ).hom.hom (S.tensorBasis c b) = S.tensorBasis c1 ((congr (OverColor.Hom.toEquiv σ) (OverColor.Hom.toEquiv_comp_apply σ)).symm b) := by @@ -232,6 +333,62 @@ lemma map_tensorBasis {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} rw [FD_map_basis] exact OverColor.Hom.toEquiv_symm_apply σ i +lemma contrMap_tensorBasis {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)} + (b : Π j, Fin (S.repDim (c j))) : + (S.contrMap c i j h).hom (S.tensorBasis c b) = + (S.contr.app (Discrete.mk (c i))).hom + (S.basis (c i) (b i) ⊗ₜ[S.k] S.basis (S.τ (c i)) (Fin.cast (by rw [h]) (b (i.succAbove j)))) • + (S.tensorBasis (c ∘ i.succAbove ∘ j.succAbove) + (fun k => b ((i.succAbove ∘ j.succAbove) k))) := by + rw [tensorBasis_eq_basisVector, basisVector, tensorBasis_eq_basisVector, basisVector] + rw [contrMap_tprod] + congr 1 + /- The coefficent. -/ + · simp only [castToField, Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as, + Function.comp_apply] + congr 2 + exact FD_map_basis S h (b (i.succAbove j)) + +/-- Given a coordinate parameter + `b : Π k, Fin (S.repDim ((c ∘ i.succAbove ∘ j.succAbove) k)))`, the + coordinate parameter `Π k, Fin (S.repDim (c k))` which map down to `b`. -/ +def ContrSection {n : ℕ} {c : Fin n.succ.succ → S.C} + {i : Fin n.succ.succ} {j : Fin n.succ} + (b : Π k, Fin (S.repDim ((c ∘ i.succAbove ∘ j.succAbove) k))) : + Finset (Π k, Fin (S.repDim (c k))) := + {b' : Π k, Fin (S.repDim (c k)) | ∀ k, b' ((i.succAbove ∘ j.succAbove) k) = b k} + end TensorBasis +open TensorBasis + +lemma pairIsoSep_tensorBasis_repr {c c1 : S.C} + (t : (S.FD.obj { as := c } ⊗ S.FD.obj { as := c1 }).V) + (b : ((j : Fin (Nat.succ 0).succ) → Fin (S.repDim (![c, c1] j)))) : + (S.tensorBasis ![c, c1]).repr + ((OverColor.Discrete.pairIsoSep S.FD).hom.hom t) b = + (Basis.tensorProduct (S.basis c) (S.basis c1)).repr t (b 0, b 1) := by + let P (t : ((S.FD.obj { as := c } ⊗ S.FD.obj { as := c1 }).V)) := + (S.tensorBasis ![c, c1]).repr + ((OverColor.Discrete.pairIsoSep S.FD).hom.hom t) b = + (Basis.tensorProduct (S.basis c) (S.basis c1)).repr t (b 0, b 1) + change P t + apply TensorProduct.induction_on + · simp [P] + · intro x y + simp [P] + conv_lhs => + left + right + erw [Discrete.pairIsoSep_tmul] + erw [tensorBasis_repr_tprod] + simp only [Nat.reduceAdd, Nat.succ_eq_add_one, mk_hom, Fin.prod_univ_two, Fin.isValue, + Matrix.cons_val_zero, Fin.cases_zero, Matrix.cons_val_one, Matrix.head_cons, P] + rw [mul_comm] + rfl + · intro x y hx hy + simp_all [P] end TensorSpecies diff --git a/PhysLean/Tensors/TensorSpecies/Contractions/ContrMap.lean b/PhysLean/Tensors/TensorSpecies/Contractions/ContrMap.lean index 53c6102e..ea588d1a 100644 --- a/PhysLean/Tensors/TensorSpecies/Contractions/ContrMap.lean +++ b/PhysLean/Tensors/TensorSpecies/Contractions/ContrMap.lean @@ -203,7 +203,7 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C) rw [lift.map_tprod] conv_lhs => enter [2, 2, 2, 2] - rw (transparency := .instances) [lift.map_tprod] + rw (transparency := .instances) [lift.map_tprod] conv_lhs => enter [2, 2, 2] rw (transparency := .instances) [lift.μIso_inv_tprod] @@ -257,7 +257,7 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C) funext d simp only [mk_hom, Function.comp_apply, lift.discreteFunctorMapEqIso, Functor.mapIso_hom, eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, - Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply, ] + Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply] change (S.FD.map (eqToHom _)).hom ((x ((PhysLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) = _ simp only [Nat.succ_eq_add_one] diff --git a/PhysLean/Tensors/TensorSpecies/OfInt.lean b/PhysLean/Tensors/TensorSpecies/OfInt.lean new file mode 100644 index 00000000..e576d2b0 --- /dev/null +++ b/PhysLean/Tensors/TensorSpecies/OfInt.lean @@ -0,0 +1,48 @@ +/- +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 PhysLean.Tensors.TensorSpecies.Basis +/-! + +# Basis for tensors in a tensor species + +-/ + +open IndexNotation +open CategoryTheory +open MonoidalCategory + +namespace TensorSpecies +open OverColor + +variable (S : TensorSpecies) + +/-- A tensor from a `(Π j, Fin (S.repDim (c j))) → ℤ`. All tensors + which have integer coefficents with respect to `tensorBasis` are of this form. -/ +noncomputable def tensorOfInt {n : ℕ} {c : Fin n → S.C} + (f : (Π j, Fin (S.repDim (c j))) → ℤ) : + S.F.obj (OverColor.mk c) := + (S.tensorBasis c).repr.symm <| + (Finsupp.linearEquivFunOnFinite S.k S.k ((j : Fin n) → Fin (S.repDim (c j)))).symm <| + (fun j => Int.cast (f j)) + +@[simp] +lemma tensorOfInt_tensorBasis_repr_apply {n : ℕ} {c : Fin n → S.C} + (f : (Π j, Fin (S.repDim (c j))) → ℤ) (b : Π j, Fin (S.repDim (c j))) : + (S.tensorBasis c).repr (S.tensorOfInt f) b = Int.cast (f b) := by + simp [tensorOfInt] + rfl + +lemma tensorBasis_eq_ofInt {n : ℕ} {c : Fin n → S.C} + (b : Π j, Fin (S.repDim (c j))) : + S.tensorBasis c b + = S.tensorOfInt (fun b' => if b = b' then 1 else 0) := by + apply (S.tensorBasis c).repr.injective + simp only [Basis.repr_self] + ext b' + simp only [tensorOfInt_tensorBasis_repr_apply, Int.cast_ite, Int.cast_one, Int.cast_zero] + rw [Finsupp.single_apply] + +end TensorSpecies diff --git a/PhysLean/Tensors/Tree/Basic.lean b/PhysLean/Tensors/Tree/Basic.lean index 83e77d13..a0244e44 100644 --- a/PhysLean/Tensors/Tree/Basic.lean +++ b/PhysLean/Tensors/Tree/Basic.lean @@ -308,8 +308,158 @@ lemma add_tensorBasis_repr (t1 t2 : TensorTree S c) : rw [add_tensor] simp +lemma prod_tensorBasis_repr_apply {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} + (t : TensorTree S c) (t1 : TensorTree S c1) + (b : Π j, Fin (S.repDim ((Sum.elim c c1 ∘ finSumFinEquiv.symm) j))) : + (S.tensorBasis (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)).repr (prod t t1).tensor b = + (S.tensorBasis c).repr t.tensor (TensorBasis.prodEquiv b).1 * + (S.tensorBasis c1).repr t1.tensor (TensorBasis.prodEquiv b).2 := by + simp only [prod_tensor] + let P (t : S.F.obj (OverColor.mk c)) + (ht : t ∈ Submodule.span S.k (Set.range (S.tensorBasis c))) (t1 : S.F.obj (OverColor.mk c1)) + (ht1 : t1 ∈ Submodule.span S.k (Set.range (S.tensorBasis c1))) : + Prop := ((S.tensorBasis (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)).repr + ((ConcreteCategory.hom (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom) + ((ConcreteCategory.hom (Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom) + (t ⊗ₜ[S.k] t1)))) b = + ((S.tensorBasis c).repr t) (TensorBasis.prodEquiv b).1 * + ((S.tensorBasis c1).repr t1) (TensorBasis.prodEquiv b).2 + change P t.tensor (Basis.mem_span _ t.tensor) t1.tensor (Basis.mem_span _ t1.tensor) + apply Submodule.span_induction + · intro t1 ht1 + let Pt (t : S.F.obj (OverColor.mk c)) + (ht : t ∈ Submodule.span S.k (Set.range (S.tensorBasis c))) := P t ht t1 (Basis.mem_span _ t1) + change Pt t.tensor (Basis.mem_span _ t.tensor) + apply Submodule.span_induction + · intro t ht + simp at ht ht1 + obtain ⟨b1, rfl⟩ := ht + obtain ⟨b2, rfl⟩ := ht1 + simp only [Function.comp_apply, Action.instMonoidalCategory_tensorObj_V, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, Basis.repr_self, Pt, P] + trans (S.tensorBasis (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)).repr + (S.tensorBasis (Sum.elim c c1 ∘ finSumFinEquiv.symm) + (TensorBasis.prodEquiv.symm (b1, b2))) b + · congr 2 + rw [TensorBasis.tensorBasis_prod] + simp + simp only [Function.comp_apply, Basis.repr_self, Pt, P] + rw [MonoidAlgebra.single_apply, MonoidAlgebra.single_apply, MonoidAlgebra.single_apply] + obtain ⟨b, rfl⟩ := TensorBasis.prodEquiv.symm.surjective b + simp only [EmbeddingLike.apply_eq_iff_eq, Equiv.apply_symm_apply, mul_ite, mul_one, mul_zero] + match b with + | (b1', b2') => + simp only [Prod.mk.injEq] + simp_all only [Set.mem_range, exists_apply_eq_apply] + obtain ⟨fst, snd⟩ := b + split + next h => simp_all only [↓reduceIte] + next h => + simp_all only [not_and] + split + next h_1 => + subst h_1 + simp_all only [not_true_eq_false, imp_false, ↓reduceIte] + next h_1 => simp_all only [not_false_eq_true, implies_true] + · simp [Pt, P] + · intro x y hx hy hP1 hP2 + simp_all only [Set.mem_range, Function.comp_apply, Action.instMonoidalCategory_tensorObj_V, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, add_tmul, map_add, Finsupp.coe_add, + Pi.add_apply, add_mul, Pt, P] + · intro x hx a hP + simp_all only [Set.mem_range, Function.comp_apply, Action.instMonoidalCategory_tensorObj_V, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, smul_tmul, tmul_smul, map_smul, + Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, Pt, P] + ring + · simp [P] + · intro x y hx hy hP1 hP2 + simp_all only [Function.comp_apply, Action.instMonoidalCategory_tensorObj_V, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, tmul_add, map_add, Finsupp.coe_add, + Pi.add_apply, mul_add, P] + · intro x hx a hP + simp_all only [Function.comp_apply, Action.instMonoidalCategory_tensorObj_V, + Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, tmul_smul, map_smul, Finsupp.coe_smul, + Pi.smul_apply, smul_eq_mul, P] + ring + +lemma contr_tensorBasis_repr_apply {n : ℕ} {c : Fin (n + 1 + 1) → S.C} {i : Fin (n + 1 + 1)} + {j : Fin (n + 1)} {h : c (i.succAbove j) = S.τ (c i)} (t : TensorTree S c) + (b : Π k, Fin (S.repDim (c (i.succAbove (j.succAbove k))))) : + (S.tensorBasis (c ∘ i.succAbove ∘ j.succAbove)).repr (contr i j h t).tensor b = + ∑ (b' : TensorBasis.ContrSection b), + ((S.tensorBasis c).repr t.tensor b'.1) * + S.castToField ((S.contr.app (Discrete.mk (c i))).hom + (S.basis (c i) (b'.1 i) ⊗ₜ[S.k] S.basis (S.τ (c i)) (Fin.cast (by rw [h]) + (b'.1 (i.succAbove j))))) := by + simp only [contr_tensor] + let P (t : S.F.obj (OverColor.mk c)) + (ht : t ∈ Submodule.span S.k (Set.range (S.tensorBasis c))) : Prop := + ((S.tensorBasis (c ∘ i.succAbove ∘ j.succAbove)).repr + ((ConcreteCategory.hom (S.contrMap c i j h).hom) t)) b = + ∑ (b' : TensorBasis.ContrSection b), + ((S.tensorBasis c).repr t b'.1) * + S.castToField ((S.contr.app (Discrete.mk (c i))).hom + (S.basis (c i) (b'.1 i) ⊗ₜ[S.k] + S.basis (S.τ (c i)) (Fin.cast (by rw [h]) (b'.1 (i.succAbove j))))) + change P t.tensor (Basis.mem_span _ t.tensor) + apply Submodule.span_induction + · intro t ht + simp only [Set.mem_range] at ht + obtain ⟨b', rfl⟩ := ht + simp [P] + rw [TensorBasis.contrMap_tensorBasis] + simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, + Nat.succ_eq_add_one, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, + Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, + Discrete.functor_obj_eq_as, Function.comp_apply, map_smul, Basis.repr_self, + Finsupp.smul_single, smul_eq_mul, mul_one, P] + by_cases hb : b' ∈ TensorBasis.ContrSection b + · rw [Finsupp.single_apply] + rw [Finset.sum_eq_single ⟨b', hb⟩] + rw [TensorBasis.ContrSection] at hb + simp at hb + simp only [hb, ↓reduceIte, Finsupp.single_eq_same, one_mul, P] + rfl + intro b'' hb'' hbb'' + rw [Finsupp.single_apply] + have hx := Subtype.eq_iff.mpr.mt hbb'' + simp only [P] at hx + simp only [ite_mul, one_mul, zero_mul, ite_eq_right_iff, P] + exact fun a => False.elim (hx (id (Eq.symm a))) + simp + · rw [Finsupp.single_apply] + rw [if_neg] + rw [Finset.sum_eq_zero] + intro x hx + rw [Finsupp.single_apply] + rw [if_neg] + simp only [zero_mul, P] + by_contra hxb + subst hxb + simp_all only [Finset.mem_attach, Set.mem_range, exists_apply_eq_apply, Nat.succ_eq_add_one, + Finset.coe_mem, not_true_eq_false, P] + rw [funext_iff] + simp only [not_forall, P] + simpa [TensorBasis.ContrSection] using hb + · simp [P] + · intro x y hx hy hP1 hP2 + simp [P] at hP1 hP2 ⊢ + rw [hP1, hP2] + rw [← Finset.sum_add_distrib] + simp [add_mul] + · intro x hx a hP + simp [P] at hP ⊢ + rw [hP] + rw [Finset.mul_sum] + simp [mul_assoc] + @[simp] -lemma perm_tensorBasis_repr_apply {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} +lemma perm_tensorBasis_repr_apply {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} {σ : (OverColor.mk c) ⟶ (OverColor.mk c1)} (t : TensorTree S c) (b : Π j, Fin (S.repDim (c1 j))) : (S.tensorBasis c1).repr (perm σ t).tensor b =