Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Nikolai Kashcheev, Joseph Tooby-Smith
-/
module
public import Physlib.Relativity.Tensors.ComplexTensor.BasicComplex Lorentz tensors from real Lorentz tensors
i. Overview
In this module we describe how to pass from real Lorentz tensors to complex Lorentz tensors in a functorial way. Specifically, we construct a canonical equivariant semilinear map
toComplex : ℝT(3, c) →ₛₗ[Complex.ofRealHom] ℂT(colorToComplex ∘ c)
which is compatible with the natural operations on tensors (permutations of indices, tensor products, contractions and evaluations).
ii. Key results
The main definitions and statements are:
colorToComplex upgrades the colour of a real Lorentz tensor to the
corresponding complex Lorentz colour.
TensorSpecies.Tensor.ComponentIdx.complexify transports component indices
along colorToComplex.
toComplex is the basic semilinear map from real to complex Lorentz tensors.
toComplex_basis and toComplex_pure_basisVector show that toComplex
sends basis tensors to basis tensors.
toComplex_eq_zero_iff and toComplex_injective show that toComplex is
injective.
toComplex_equivariant states that toComplex is equivariant for the action
of the complexified Lorentz group.
permT_toComplex, prodT_toComplex, contrT_toComplex and evalT_toComplex
express that toComplex commutes with the basic tensor operations.
iii. Table of contents
A. Colours and component indices
B. The semilinear map toComplex
B.1. Expression in the tensor basis
B.2. Behaviour on basis vectors and injectivity
B.3. Equivariance under the Lorentz action
C. Compatibility with permutations: permT
D. Compatibility with tensor products: prodT
E. Compatibility with contraction: contrT
F. Compatibility with evaluation: evalT
iv. References
The general formalism of Lorentz tensors and their operations is developed in other parts of the library; here we only specialise to the passage from real to complex Lorentz tensors.
@[expose] public sectionA. Colours and component indices
We first explain how the Lorentz colour data and component indices for real tensors are transported to the complex setting.
The map from colors of real Lorentz tensors to complex Lorentz tensors.
def colorToComplex (c : realLorentzTensor.Color) : complexLorentzTensor.Color :=
match c with
| .up => .up
| .down => .downlemma repDim_colorToComplex {c : realLorentzTensor.Color} :
complexLorentzTensor.repDim (colorToComplex c) = 4 := c:Color⊢ repDim (colorToComplex c) = 4
⊢ repDim (colorToComplex Color.up) = 4⊢ repDim (colorToComplex Color.down) = 4 ⊢ repDim (colorToComplex Color.up) = 4⊢ repDim (colorToComplex Color.down) = 4 All goals completed! 🐙
simp helper: reduce match c j after a case split on c j
(avoids dependent rw / Pi.smul_apply).
All goals completed! 🐙All goals completed! 🐙lemma colorToComplex_comp_eq_match {n} (c : Fin n → realLorentzTensor.Color) (j : Fin n) :
(colorToComplex ∘ c) j =
(match c j with
| .up => complexLorentzTensor.Color.up
| .down => complexLorentzTensor.Color.down) := n:ℕc:Fin n → Colorj:Fin n⊢ (colorToComplex ∘ c) j =
match c j with
| Color.up => complexLorentzTensor.Color.up
| Color.down => complexLorentzTensor.Color.down
n:ℕc:Fin n → Colorj:Fin nhc:c j = Color.up⊢ (colorToComplex ∘ c) j =
match Color.up with
| Color.up => complexLorentzTensor.Color.up
| Color.down => complexLorentzTensor.Color.downn:ℕc:Fin n → Colorj:Fin nhc:c j = Color.down⊢ (colorToComplex ∘ c) j =
match Color.down with
| Color.up => complexLorentzTensor.Color.up
| Color.down => complexLorentzTensor.Color.down n:ℕc:Fin n → Colorj:Fin nhc:c j = Color.up⊢ (colorToComplex ∘ c) j =
match Color.up with
| Color.up => complexLorentzTensor.Color.up
| Color.down => complexLorentzTensor.Color.downn:ℕc:Fin n → Colorj:Fin nhc:c j = Color.down⊢ (colorToComplex ∘ c) j =
match Color.down with
| Color.up => complexLorentzTensor.Color.up
| Color.down => complexLorentzTensor.Color.down All goals completed! 🐙@[simp]
lemma ComponentIdx.complexify_apply {n} {c : Fin n → realLorentzTensor.Color}
(f : ComponentIdx (S := realLorentzTensor) c) (j : Fin n) :
(ComponentIdx.complexify f) j = Fin.cast repDim_colorToComplex.symm (finSumFinEquiv (f j)) :=
rfl@[simp]
lemma ComponentIdx.complexify_toFun_apply {n} {c : Fin n → realLorentzTensor.Color}
(f : ComponentIdx (S := realLorentzTensor) c) (j : Fin n) :
(ComponentIdx.complexify.toFun f) j = (ComponentIdx.complexify f) j :=
rfl
B. The semilinear map toComplex
We now define the basic semilinear map from real Lorentz tensors to complex Lorentz tensors. It is characterised by sending the standard tensor basis on the real side to the corresponding basis on the complex side, and is therefore determined by the behaviour on components.
n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor c⊢ toComplex v =
∑ i,
((Tensor.basis c).repr v) (ComponentIdx.complexify.symm (ComponentIdx.complexify i)) •
(Tensor.basis (colorToComplex ∘ c)) (ComponentIdx.complexify i)
exact Finset.sum_congr rfl fun i _ => n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor ci:ComponentIdx cx✝:i ∈ Finset.univ⊢ ((Tensor.basis c).repr v) i • (Tensor.basis (colorToComplex ∘ c)) (ComponentIdx.complexify i) =
((Tensor.basis c).repr v) (ComponentIdx.complexify.symm (ComponentIdx.complexify i)) •
(Tensor.basis (colorToComplex ∘ c)) (ComponentIdx.complexify i) All goals completed! 🐙
The representation of toComplex v in the complexified basis equals
the real representation coerced to complex.
n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor ci:ComponentIdx c⊢ (∑ x,
(Tensor.basis (colorToComplex ∘ c)).repr
(((Tensor.basis c).repr v) (ComponentIdx.complexify.symm x) • (Tensor.basis (colorToComplex ∘ c)) x))
(ComponentIdx.complexify i) =
↑(((Tensor.basis c).repr v) i)
All goals completed! 🐙
toComplex sends basis elements to basis elements.
@[simp]
lemma toComplex_basis {n} {c : Fin n → realLorentzTensor.Color}
(i : ComponentIdx (S := realLorentzTensor) c) :
toComplex (c := c) ((Tensor.basis (S := realLorentzTensor) c) i) =
(Tensor.basis (S := complexLorentzTensor) (colorToComplex ∘ c)) i.complexify := n:ℕc:Fin n → Colori:ComponentIdx c⊢ toComplex ((Tensor.basis c) i) = (Tensor.basis (colorToComplex ∘ c)) (ComponentIdx.complexify i)
n:ℕc:Fin n → Colori:ComponentIdx c⊢ ∑ i_1,
((Tensor.basis c).repr ((Tensor.basis c) i)) i_1 •
(Tensor.basis (colorToComplex ∘ c)) (ComponentIdx.complexify i_1) =
(Tensor.basis (colorToComplex ∘ c)) (ComponentIdx.complexify i)
All goals completed! 🐙
toComplex on a pure basis vector.
@[simp]
lemma toComplex_pure_basisVector {n} {c : Fin n → realLorentzTensor.Color}
(b : ComponentIdx (S := realLorentzTensor) c) :
toComplex (c := c) (Pure.basisVector c b |>.toTensor)
=
(Pure.basisVector (colorToComplex ∘ c) b.complexify).toTensor := n:ℕc:Fin n → Colorb:ComponentIdx c⊢ toComplex (Pure.basisVector c b).toTensor = (Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b)).toTensor
All goals completed! 🐙lemma toComplex_map_smul {n} (c : Fin n → realLorentzTensor.Color) (r : ℝ) (t : ℝT(3, c)) :
toComplex (c := c) (r • t) = (Complex.ofReal r) • toComplex (c := c) t :=
(toComplex (c := c)).map_smulₛₗ r t@[simp]
lemma toComplex_eq_zero_iff {n} (c : Fin n → realLorentzTensor.Color) (v : ℝT(3, c)) :
toComplex v = 0 ↔ v = 0 := n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor c⊢ toComplex v = 0 ↔ v = 0
n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor c⊢ toComplex v = 0 → v = 0n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor c⊢ v = 0 → toComplex v = 0
n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor c⊢ toComplex v = 0 → v = 0 n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor ch:toComplex v = 0⊢ v = 0
n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor ch:toComplex v = 0⊢ (Tensor.basis c).repr v = (Tensor.basis c).repr 0
n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor ch:toComplex v = 0i:ComponentIdx c⊢ ((Tensor.basis c).repr v) i = ((Tensor.basis c).repr 0) i
All goals completed! 🐙
n:ℕc:Fin n → Colorv:realLorentzTensor.Tensor c⊢ v = 0 → toComplex v = 0 n:ℕc:Fin n → Color⊢ toComplex 0 = 0
All goals completed! 🐙
The map toComplex is injective.
lemma toComplex_injective {n} (c : Fin n → realLorentzTensor.Color) :
Function.Injective (toComplex (c := c)) :=
(injective_iff_map_eq_zero' toComplex).mpr (toComplex_eq_zero_iff c)pure
lemma toComplexVector_up_eq_inclCongrRealLorentz (v : Lorentz.ContrMod 3) :
toComplexVector Color.up v = Lorentz.inclCongrRealLorentz v := v:Lorentz.ContrMod 3⊢ (toComplexVector Color.up) v = Lorentz.inclCongrRealLorentz v
v:Lorentz.ContrMod 3⊢ (toComplexVector Color.up) v = ∑ i, v.toFin1dℝ i • Lorentz.complexContrBasis iv:Lorentz.ContrMod 3⊢ ∑ i, v.toFin1dℝ i • Lorentz.complexContrBasis i = Lorentz.inclCongrRealLorentz v
v:Lorentz.ContrMod 3⊢ (toComplexVector Color.up) v = ∑ i, v.toFin1dℝ i • Lorentz.complexContrBasis i All goals completed! 🐙
v:Lorentz.ContrMod 3⊢ ∑ i, v.toFin1dℝ i • Lorentz.complexContrBasis i = Lorentz.inclCongrRealLorentz v conv_rhs => v:Lorentz.ContrMod 3| Lorentz.inclCongrRealLorentz (∑ i, v.toFin1dℝ i • Lorentz.ContrMod.stdBasis i)
v:Lorentz.ContrMod 3⊢ ∑ x, v.toFin1dℝ x • Lorentz.inclCongrRealLorentz (Lorentz.ContrMod.stdBasis x) =
∑ x, v.toFin1dℝ x • Lorentz.inclCongrRealLorentz (Lorentz.ContrMod.stdBasis x)
All goals completed! 🐙lemma toComplexVector_down_eq_inclCoRealLorentz (v : Lorentz.CoMod 3) :
toComplexVector Color.down v = Lorentz.inclCoRealLorentz v := v:Lorentz.CoMod 3⊢ (toComplexVector Color.down) v = Lorentz.inclCoRealLorentz v
v:Lorentz.CoMod 3⊢ (toComplexVector Color.down) v = ∑ i, v.toFin1dℝ i • Lorentz.complexCoBasis iv:Lorentz.CoMod 3⊢ ∑ i, v.toFin1dℝ i • Lorentz.complexCoBasis i = Lorentz.inclCoRealLorentz v
v:Lorentz.CoMod 3⊢ (toComplexVector Color.down) v = ∑ i, v.toFin1dℝ i • Lorentz.complexCoBasis i v:Lorentz.CoMod 3⊢ v.val (Sum.inl 0) • Lorentz.complexCoBasis (Sum.inl 0) +
∑ a₂, v.val (Sum.inr a₂) • Lorentz.complexCoBasis (Sum.inr a₂) =
v.toFin1dℝ (Sum.inl 0) • Lorentz.complexCoBasis (Sum.inl 0) +
∑ a₂, v.toFin1dℝ (Sum.inr a₂) • Lorentz.complexCoBasis (Sum.inr a₂)
All goals completed! 🐙
v:Lorentz.CoMod 3⊢ ∑ i, v.toFin1dℝ i • Lorentz.complexCoBasis i = Lorentz.inclCoRealLorentz v conv_rhs => v:Lorentz.CoMod 3| Lorentz.inclCoRealLorentz (∑ i, v.toFin1dℝ i • Lorentz.CoMod.stdBasis i)
v:Lorentz.CoMod 3⊢ ∑ x, v.toFin1dℝ x • Lorentz.inclCoRealLorentz (Lorentz.CoMod.stdBasis x) =
∑ x, v.toFin1dℝ x • Lorentz.inclCoRealLorentz (Lorentz.CoMod.stdBasis x)
All goals completed! 🐙n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3px:match c x with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h2:4 = repDim (colorToComplex (c x))h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)⊢ P (c x) px φx h2
n:ℕc✝:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)c:Colorpx:match c with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex c)⊢ P c px φx h2
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ P Color.up px φx h2n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ P Color.down px φx h2
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ P Color.up px φx h2 n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ (Lorentz.complexContrBasisFin4.repr
({ toFun := fun v => ∑ x, (Lorentz.contrBasis.repr v) x • Lorentz.complexContrBasisFin4 (finSumFinEquiv x),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
↑((Lorentz.contrBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ (Lorentz.complexContrBasisFin4.repr
({ toFun := fun v => ∑ x, (Lorentz.contrBasis.repr v) x • Lorentz.complexContrBasisFin4 (finSumFinEquiv x),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
(∑ x,
Lorentz.complexContrBasisFin4.repr
((Lorentz.contrBasis.repr px) x • Lorentz.complexContrBasisFin4 (finSumFinEquiv x)))
(finSumFinEquiv φx)n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ (∑ x,
Lorentz.complexContrBasisFin4.repr
((Lorentz.contrBasis.repr px) x • Lorentz.complexContrBasisFin4 (finSumFinEquiv x)))
(finSumFinEquiv φx) =
↑((Lorentz.contrBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ (Lorentz.complexContrBasisFin4.repr
({ toFun := fun v => ∑ x, (Lorentz.contrBasis.repr v) x • Lorentz.complexContrBasisFin4 (finSumFinEquiv x),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
(∑ x,
Lorentz.complexContrBasisFin4.repr
((Lorentz.contrBasis.repr px) x • Lorentz.complexContrBasisFin4 (finSumFinEquiv x)))
(finSumFinEquiv φx) n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ (Lorentz.complexContrBasisFin4.repr
({
toFun := fun v =>
(Lorentz.contrBasis.repr v) (Sum.inl 0) • Lorentz.complexContrBasisFin4 (finSumFinEquiv (Sum.inl 0)) +
∑ a₂,
(Lorentz.contrBasis.repr v) (Sum.inr a₂) • Lorentz.complexContrBasisFin4 (finSumFinEquiv (Sum.inr a₂)),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
(Lorentz.complexContrBasisFin4.repr
((Lorentz.contrBasis.repr px) (Sum.inl 0) • Lorentz.complexContrBasisFin4 (finSumFinEquiv (Sum.inl 0))))
(finSumFinEquiv φx) +
∑ c,
(Lorentz.complexContrBasisFin4.repr
((Lorentz.contrBasis.repr px) (Sum.inr c) • Lorentz.complexContrBasisFin4 (finSumFinEquiv (Sum.inr c))))
(finSumFinEquiv φx)
All goals completed! 🐙
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ ∑ x, (Lorentz.complexContrBasis.repr ((Lorentz.contrBasis.repr px) x • Lorentz.complexContrBasis x)) φx =
↑((Lorentz.contrBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ ∑ x, (Lorentz.complexContrBasis.repr ((Lorentz.contrBasis.repr px) x • Lorentz.complexContrBasis x)) φx =
∑ x, (Lorentz.contrBasis.repr px) x • (Lorentz.complexContrBasis.repr (Lorentz.complexContrBasis x)) φxn:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ ∑ x, (Lorentz.contrBasis.repr px) x • (Lorentz.complexContrBasis.repr (Lorentz.complexContrBasis x)) φx =
↑((Lorentz.contrBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ ∑ x, (Lorentz.complexContrBasis.repr ((Lorentz.contrBasis.repr px) x • Lorentz.complexContrBasis x)) φx =
∑ x, (Lorentz.contrBasis.repr px) x • (Lorentz.complexContrBasis.repr (Lorentz.complexContrBasis x)) φx n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.up)⊢ (Lorentz.complexContrBasis.repr ((Lorentz.contrBasis.repr px) (Sum.inl 0) • Lorentz.complexContrBasis (Sum.inl 0))) φx +
∑ a₂,
(Lorentz.complexContrBasis.repr
((Lorentz.contrBasis.repr px) (Sum.inr a₂) • Lorentz.complexContrBasis (Sum.inr a₂)))
φx =
↑((Lorentz.contrBasis.repr px) (Sum.inl 0)) * (Finsupp.single (Sum.inl 0) 1) φx +
∑ a₂, ↑((Lorentz.contrBasis.repr px) (Sum.inr a₂)) * (Finsupp.single (Sum.inr a₂) 1) φx
All goals completed! 🐙
All goals completed! 🐙
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ P Color.down px φx h2 n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ (Lorentz.complexCoBasisFin4.repr
({ toFun := fun v => ∑ x, (Lorentz.coBasis.repr v) x • Lorentz.complexCoBasisFin4 (finSumFinEquiv x),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
↑((Lorentz.coBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ (Lorentz.complexCoBasisFin4.repr
({ toFun := fun v => ∑ x, (Lorentz.coBasis.repr v) x • Lorentz.complexCoBasisFin4 (finSumFinEquiv x),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
(∑ x, Lorentz.complexCoBasisFin4.repr ((Lorentz.coBasis.repr px) x • Lorentz.complexCoBasisFin4 (finSumFinEquiv x)))
(finSumFinEquiv φx)n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ (∑ x, Lorentz.complexCoBasisFin4.repr ((Lorentz.coBasis.repr px) x • Lorentz.complexCoBasisFin4 (finSumFinEquiv x)))
(finSumFinEquiv φx) =
↑((Lorentz.coBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ (Lorentz.complexCoBasisFin4.repr
({ toFun := fun v => ∑ x, (Lorentz.coBasis.repr v) x • Lorentz.complexCoBasisFin4 (finSumFinEquiv x),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
(∑ x, Lorentz.complexCoBasisFin4.repr ((Lorentz.coBasis.repr px) x • Lorentz.complexCoBasisFin4 (finSumFinEquiv x)))
(finSumFinEquiv φx) n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ (Lorentz.complexCoBasisFin4.repr
({
toFun := fun v =>
(Lorentz.coBasis.repr v) (Sum.inl 0) • Lorentz.complexCoBasisFin4 (finSumFinEquiv (Sum.inl 0)) +
∑ a₂, (Lorentz.coBasis.repr v) (Sum.inr a₂) • Lorentz.complexCoBasisFin4 (finSumFinEquiv (Sum.inr a₂)),
map_add' := ⋯, map_smul' := ⋯ }
px))
(finSumFinEquiv φx) =
(Lorentz.complexCoBasisFin4.repr
((Lorentz.coBasis.repr px) (Sum.inl 0) • Lorentz.complexCoBasisFin4 (finSumFinEquiv (Sum.inl 0))))
(finSumFinEquiv φx) +
∑ c,
(Lorentz.complexCoBasisFin4.repr
((Lorentz.coBasis.repr px) (Sum.inr c) • Lorentz.complexCoBasisFin4 (finSumFinEquiv (Sum.inr c))))
(finSumFinEquiv φx)
All goals completed! 🐙
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ ∑ x, (Lorentz.complexCoBasis.repr ((Lorentz.coBasis.repr px) x • Lorentz.complexCoBasis x)) φx =
↑((Lorentz.coBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ ∑ x, (Lorentz.complexCoBasis.repr ((Lorentz.coBasis.repr px) x • Lorentz.complexCoBasis x)) φx =
∑ x, (Lorentz.coBasis.repr px) x • (Lorentz.complexCoBasis.repr (Lorentz.complexCoBasis x)) φxn:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ ∑ x, (Lorentz.coBasis.repr px) x • (Lorentz.complexCoBasis.repr (Lorentz.complexCoBasis x)) φx =
↑((Lorentz.coBasis.repr px) φx)
n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ ∑ x, (Lorentz.complexCoBasis.repr ((Lorentz.coBasis.repr px) x • Lorentz.complexCoBasis x)) φx =
∑ x, (Lorentz.coBasis.repr px) x • (Lorentz.complexCoBasis.repr (Lorentz.complexCoBasis x)) φx n:ℕc:Fin n → Colorx:Fin nφx:Fin 1 ⊕ Fin 3h1:RingHomInvPair (RingHom.id ℂ) (RingHom.id ℂ)h3:RingHomInvPair (RingHom.id ℝ) (RingHom.id ℝ)b:(c : Color) → Basis (Fin (repDim (colorToComplex c))) ℂ (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.basis
| Color.downL => Fermion.DualLeftHandedWeyl.basis
| Color.upR => Fermion.RightHandedWeyl.basis
| Color.downR => Fermion.DualRightHandedWeyl.basis
| complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
| complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4b':(c : Color) → Basis (Fin 1 ⊕ Fin 3) ℝ (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.contrBasis
| Color.down => Lorentz.coBasisP:(c : Color) → modules 3 c → Fin 1 ⊕ Fin 3 → 4 = repDim (colorToComplex c) → Prop := fun c px φx h2 => ((b c).repr ((toComplexVector c) px)) (Fin.cast h2 (finSumFinEquiv φx)) = ↑(((b' c).repr px) φx)px:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3h2:4 = repDim (colorToComplex Color.down)⊢ (Lorentz.complexCoBasis.repr ((Lorentz.coBasis.repr px) (Sum.inl 0) • Lorentz.complexCoBasis (Sum.inl 0))) φx +
∑ a₂,
(Lorentz.complexCoBasis.repr ((Lorentz.coBasis.repr px) (Sum.inr a₂) • Lorentz.complexCoBasis (Sum.inr a₂))) φx =
↑((Lorentz.coBasis.repr px) (Sum.inl 0)) * (Finsupp.single (Sum.inl 0) 1) φx +
∑ a₂, ↑((Lorentz.coBasis.repr px) (Sum.inr a₂)) * (Finsupp.single (Sum.inr a₂) 1) φx
All goals completed! 🐙
All goals completed! 🐙lemma actionP_toComplexPure {n : ℕ} (c : Fin n → Color) (p : Pure realLorentzTensor c)
(Λ : SL(2, ℂ)) :
Λ • toComplexPure p = toComplexPure (toLorentzGroup Λ • p) := n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)⊢ Λ • toComplexPure p = toComplexPure (toLorentzGroup Λ • p)
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin n⊢ (Λ • toComplexPure p) i = toComplexPure (toLorentzGroup Λ • p) i
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin n⊢ ((match colorToComplex (c i) with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRep)
Λ)
((toComplexVector (c i)) (p i)) =
(toComplexVector (c i))
(((match c i with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.rep)
(toLorentzGroup Λ))
(p i))
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRep⊢ ((match colorToComplex (c i) with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRep)
Λ)
((toComplexVector (c i)) (p i)) =
(toComplexVector (c i))
(((match c i with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.rep)
(toLorentzGroup Λ))
(p i))
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.rep⊢ ((match colorToComplex (c i) with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRep)
Λ)
((toComplexVector (c i)) (p i)) =
(toComplexVector (c i))
(((match c i with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.rep)
(toLorentzGroup Λ))
(p i))
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)⊢ ((match colorToComplex (c i) with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRep)
Λ)
((toComplexVector (c i)) (p i)) =
(toComplexVector (c i))
(((match c i with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.rep)
(toLorentzGroup Λ))
(p i))
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)⊢ P (c i) (p i)
n:ℕc:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)p:match c i with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ P (c i) p
n:ℕc✝:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)c:Colorp:match c with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ P c p
n:ℕc:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)p:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ P Color.up pn:ℕc:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)p:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ P Color.down p
n:ℕc:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)p:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ P Color.up p n:ℕc:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)p:match Color.up with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ (Lorentz.ContrℂModule.SL2CRep Λ) ((toComplexVector Color.up) p) =
(toComplexVector Color.up) ((Lorentz.ContrMod.rep (toLorentzGroup Λ)) p)
All goals completed! 🐙
n:ℕc:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)p:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ P Color.down p n:ℕc:Fin n → Colorp✝:Tensor.Pure realLorentzTensor cΛ:SL(2, ℂ)i:Fin nb:(c : Color) → Representation ℂ SL(2, ℂ) (complexLorentzTensor.modules (colorToComplex c)) :=
fun c =>
match colorToComplex c with
| Color.upL => Fermion.LeftHandedWeyl.rep
| Color.downL => Fermion.DualLeftHandedWeyl.rep
| Color.upR => Fermion.RightHandedWeyl.rep
| Color.downR => Fermion.DualRightHandedWeyl.rep
| complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
| complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRepb':(c : Color) → Representation ℝ (↑(LorentzGroup 3)) (modules 3 c) :=
fun c =>
match c with
| Color.up => Lorentz.ContrMod.rep
| Color.down => Lorentz.CoMod.repP:(c : Color) → modules 3 c → Prop := fun c px => ((b c) Λ) ((toComplexVector c) px) = (toComplexVector c) (((b' c) (toLorentzGroup Λ)) px)p:match Color.down with
| Color.up => Lorentz.ContrMod 3
| Color.down => Lorentz.CoMod 3⊢ (Lorentz.CoℂModule.SL2CRep Λ) ((toComplexVector Color.down) p) =
(toComplexVector Color.down) ((Lorentz.CoMod.rep (toLorentzGroup Λ)) p)
All goals completed! 🐙lemma toComplex_pure {n : ℕ} (c : Fin n → Color) (p : Pure realLorentzTensor c) :
toComplex p.toTensor = (toComplexPure p).toTensor := n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor c⊢ toComplex p.toTensor = (toComplexPure p).toTensor
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor c⊢ (Tensor.basis (colorToComplex ∘ c)).repr (toComplex p.toTensor) =
(Tensor.basis (colorToComplex ∘ c)).repr (toComplexPure p).toTensor
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cφ:ComponentIdx (colorToComplex ∘ c)⊢ ((Tensor.basis (colorToComplex ∘ c)).repr (toComplex p.toTensor)) φ =
((Tensor.basis (colorToComplex ∘ c)).repr (toComplexPure p).toTensor) φ
n:ℕc:Fin n → Colorp:Tensor.Pure realLorentzTensor cφ:ComponentIdx c⊢ ((Tensor.basis (colorToComplex ∘ c)).repr (toComplex p.toTensor)) (ComponentIdx.complexify φ) =
((Tensor.basis (colorToComplex ∘ c)).repr (toComplexPure p).toTensor) (ComponentIdx.complexify φ)
All goals completed! 🐙B.3. Equivariance under the Lorentz action
Finally we record that toComplex is equivariant for the natural action of
SL(2, ℂ) (and hence the induced Lorentz action) on tensors.
The map toComplex is equivariant.
set_option backward.isDefEq.respectTransparency false inAll goals completed! 🐙
n:ℕc:Fin n → ColorΛ:SL(2, ℂ)r:ℝt:realLorentzTensor.Tensor ch:Λ • toComplex t = toComplex (toLorentzGroup Λ • t)⊢ Λ • toComplex (r • t) = toComplex (toLorentzGroup Λ • r • t) All goals completed! 🐙
n:ℕc:Fin n → ColorΛ:SL(2, ℂ)t1:realLorentzTensor.Tensor ct2:realLorentzTensor.Tensor ca✝¹:Λ • toComplex t1 = toComplex (toLorentzGroup Λ • t1)a✝:Λ • toComplex t2 = toComplex (toLorentzGroup Λ • t2)⊢ Λ • toComplex (t1 + t2) = toComplex (toLorentzGroup Λ • (t1 + t2)) All goals completed! 🐙
C. Compatibility with permutations: permT
We first show that complexification is compatible with permutation of tensor
slots. On colours this is encoded in the IsReindexing predicate, and on tensors
by the operator permT.
The IsReindexing condition is preserved under colorToComplex.
@[simp] lemma isReindexing_colorToComplex {n m : ℕ}
{c : Fin n → realLorentzTensor.Color} {c1 : Fin m → realLorentzTensor.Color}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ) :
IsReindexing (colorToComplex ∘ c) (colorToComplex ∘ c1) σ :=
⟨h.1, fun i => congrArg colorToComplex (h.2 i)⟩
permT sends basis vectors to basis vectors.
@[simp] lemma permT_basis_real {n m : ℕ}
{c : Fin n → realLorentzTensor.Color} {c1 : Fin m → realLorentzTensor.Color}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ)
(b : ComponentIdx (S := realLorentzTensor) c) :
permT (S := realLorentzTensor) σ h ((Tensor.basis (S := realLorentzTensor) c) b)
= (Tensor.basis (S := realLorentzTensor) c1)
(fun j => b (σ j)) := n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σb:ComponentIdx c⊢ (permT σ h) ((Tensor.basis c) b) = (Tensor.basis c1) fun j => b (σ j)
All goals completed! 🐙@[simp] lemma permT_basis_complex {n m : ℕ}
{c : Fin n → complexLorentzTensor.Color} {c1 : Fin m → complexLorentzTensor.Color}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ)
(b : ComponentIdx (S := complexLorentzTensor) c) :
permT (S := complexLorentzTensor) σ h ((Tensor.basis (S := complexLorentzTensor) c) b)
=
(Tensor.basis (S := complexLorentzTensor) c1)
(fun j => Fin.cast
(n:ℕm:ℕc:Fin n → complexLorentzTensor.Colorc1:Fin m → complexLorentzTensor.Colorσ:Fin m → Fin nh:IsReindexing c c1 σb:ComponentIdx cj:Fin m⊢ repDim (c (σ j)) = repDim (c1 j)
-- from the color agreement we get the repDim agreement
-- if one has `h.2 j : c1 j = c (σ j)`, then replace it with `(h.2 j).symm`
All goals completed! 🐙)
(b (σ j))) := n:ℕm:ℕc:Fin n → complexLorentzTensor.Colorc1:Fin m → complexLorentzTensor.Colorσ:Fin m → Fin nh:IsReindexing c c1 σb:ComponentIdx c⊢ (permT σ h) ((Tensor.basis c) b) = (Tensor.basis c1) fun j => Fin.cast ⋯ (b (σ j))
All goals completed! 🐙
The map toComplex commutes with permT.
lemma permT_toComplex {n m : ℕ}
{c : Fin n → realLorentzTensor.Color}
{c1 : Fin m → realLorentzTensor.Color}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ) (t : ℝT(3, c)) :
toComplex (permT (S := realLorentzTensor) σ h t)
=
permT (S := complexLorentzTensor) σ (isReindexing_colorToComplex (c := c) (c1 := c1) h)
(toComplex (c := c) t) := n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σt:realLorentzTensor.Tensor c⊢ toComplex ((permT σ h) t) = (permT σ ⋯) (toComplex t)
induction t using induction_on_basis with
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σb:ComponentIdx c⊢ toComplex ((permT σ h) ((Tensor.basis c) b)) = (permT σ ⋯) (toComplex ((Tensor.basis c) b))
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σb:ComponentIdx c⊢ (Tensor.basis (colorToComplex ∘ c1)) (ComponentIdx.complexify fun j => b (σ j)) =
(Tensor.basis (colorToComplex ∘ c1)) fun j => Fin.cast ⋯ (ComponentIdx.complexify b (σ j))
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σb:ComponentIdx c⊢ (ComponentIdx.complexify fun j => b (σ j)) = fun j => Fin.cast ⋯ (ComponentIdx.complexify b (σ j))
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σb:ComponentIdx cj:Fin m⊢ ComponentIdx.complexify (fun j => b (σ j)) j = Fin.cast ⋯ (ComponentIdx.complexify b (σ j))
All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σ⊢ toComplex ((permT σ h) 0) = (permT σ ⋯) (toComplex 0) All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σr:ℝt:realLorentzTensor.Tensor cht:toComplex ((permT σ h) t) = (permT σ ⋯) (toComplex t)⊢ toComplex ((permT σ h) (r • t)) = (permT σ ⋯) (toComplex (r • t)) All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorσ:Fin m → Fin nh:IsReindexing c c1 σt1:realLorentzTensor.Tensor ct2:realLorentzTensor.Tensor ch1:toComplex ((permT σ h) t1) = (permT σ ⋯) (toComplex t1)h2:toComplex ((permT σ h) t2) = (permT σ ⋯) (toComplex t2)⊢ toComplex ((permT σ h) (t1 + t2)) = (permT σ ⋯) (toComplex (t1 + t2)) All goals completed! 🐙
D. Compatibility with tensor products: prodT
colorToComplex commutes with Fin.append (as functions).
@[simp]
lemma colorToComplex_append {n m : ℕ}
(c : Fin n → realLorentzTensor.Color) (c1 : Fin m → realLorentzTensor.Color) :
(colorToComplex ∘ Fin.append c c1) = Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1) := n:ℕm:ℕc:Fin n → Colorc1:Fin m → Color⊢ colorToComplex ∘ Fin.append c c1 = Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1)
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorx:Fin (n + m)⊢ (colorToComplex ∘ Fin.append c c1) x = Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1) x
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorx:Fin (n + m)i:Fin n⊢ (colorToComplex ∘ Fin.append c c1) (Fin.castAdd m i) =
Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1) (Fin.castAdd m i)n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorx:Fin (n + m)j:Fin m⊢ (colorToComplex ∘ Fin.append c c1) (Fin.natAdd n j) =
Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1) (Fin.natAdd n j) n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorx:Fin (n + m)i:Fin n⊢ (colorToComplex ∘ Fin.append c c1) (Fin.castAdd m i) =
Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1) (Fin.castAdd m i)n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorx:Fin (n + m)j:Fin m⊢ (colorToComplex ∘ Fin.append c c1) (Fin.natAdd n j) =
Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1) (Fin.natAdd n j) All goals completed! 🐙lemma isReindexing_prodTColorToComplex {n m : ℕ}
{c : Fin n → realLorentzTensor.Color} {c1 : Fin m → realLorentzTensor.Color} :
IsReindexing (Fin.append (colorToComplex ∘ c) (colorToComplex ∘ c1))
(colorToComplex ∘ Fin.append c c1)
(id : Fin (n + m) → Fin (n + m)) :=
⟨Function.bijective_id, fun i => (congrFun (colorToComplex_append c c1) i).symm⟩private lemma cast_componentIdx_apply {n : ℕ} {c c' : Fin n → complexLorentzTensor.Color}
(h : c' = c) (f : ComponentIdx (S := complexLorentzTensor) c') (x : Fin n) :
(cast (congr_arg ComponentIdx h) f) x =
Fin.cast (congr_arg (fun c => complexLorentzTensor.repDim (c x)) h) (f x) := n:ℕc:Fin n → complexLorentzTensor.Colorc':Fin n → complexLorentzTensor.Colorh:c' = cf:ComponentIdx c'x:Fin n⊢ cast ⋯ f x = Fin.cast ⋯ (f x)
n:ℕc':Fin n → complexLorentzTensor.Colorf:ComponentIdx c'x:Fin n⊢ cast ⋯ f x = Fin.cast ⋯ (f x)
All goals completed! 🐙@[simp]
private lemma cast_componentIdx_eq_fun {n : ℕ}
{c c' : Fin n → complexLorentzTensor.Color}
(h : c' = c) (f : ComponentIdx (S := complexLorentzTensor) c') :
cast (congr_arg ComponentIdx h) f =
(fun x =>
Fin.cast (congr_arg (fun col => complexLorentzTensor.repDim (col x)) h) (f x)) :=
funext fun x => cast_componentIdx_apply h f x
complexify commutes with prod of component indices.
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx cb1:ComponentIdx c1val✝:Fin m⊢ ↑(Fin.cast ⋯ (finSumFinEquiv (ComponentIdx.prod.symm (b, b1) (finSumFinEquiv (Sum.inr val✝))))) =
↑(cast ⋯ (ComponentIdx.prod.symm (ComponentIdx.complexify b, ComponentIdx.complexify b1))
(finSumFinEquiv (Sum.inr val✝)))
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx cb1:ComponentIdx c1val✝:Fin m⊢ ↑(finSumFinEquiv (b1 val✝)) = ↑((basisIdxCongr ⋯) (Fin.cast ⋯ (finSumFinEquiv (b1 val✝))))
erw [n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx cb1:ComponentIdx c1val✝:Fin n⊢ ↑(finSumFinEquiv (b val✝)) = ↑(Fin.cast ⋯ (Fin.cast ⋯ (finSumFinEquiv (b val✝))))n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx cb1:ComponentIdx c1val✝:Fin m⊢ ↑(finSumFinEquiv (b1 val✝)) = ↑(Fin.cast ⋯ (Fin.cast ⋯ (finSumFinEquiv (b1 val✝))))
All goals completed! 🐙
The map toComplex commutes with prodT.
set_option backward.isDefEq.respectTransparency false inlemma prodT_toComplex {n m : ℕ}
{c : Fin n → realLorentzTensor.Color}
{c1 : Fin m → realLorentzTensor.Color}
(t : ℝT(3, c)) (t1 : ℝT(3, c1)) :
toComplex (c := Fin.append c c1) (prodT (S := realLorentzTensor) t t1)
=
prodTColorToComplex (c := c) (c1 := c1)
(toComplex (c := c) t) (toComplex (c := c1) t1) := n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colort:realLorentzTensor.Tensor ct1:realLorentzTensor.Tensor c1⊢ toComplex ((prodT t) t1) = prodTColorToComplex (toComplex t) (toComplex t1)
-- Double induction on the tensor basis: first over `t`, then over `t1`. The zero, scalar and
-- additive cases follow from linearity of `prodT`, `toComplex` and `prodTColorToComplex`.
induction t using induction_on_basis with
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colort1:realLorentzTensor.Tensor c1b:ComponentIdx c⊢ toComplex ((prodT ((Tensor.basis c) b)) t1) = prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex t1)
induction t1 using induction_on_basis with
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx cb1:ComponentIdx c1⊢ toComplex ((prodT ((Tensor.basis c) b)) ((Tensor.basis c1) b1)) =
prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex ((Tensor.basis c1) b1))
All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx c⊢ toComplex ((prodT ((Tensor.basis c) b)) 0) = prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex 0) All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx cr:ℝta:realLorentzTensor.Tensor c1hta:toComplex ((prodT ((Tensor.basis c) b)) ta) = prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex ta)⊢ toComplex ((prodT ((Tensor.basis c) b)) (r • ta)) =
prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex (r • ta)) All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colorb:ComponentIdx cta:realLorentzTensor.Tensor c1tb:realLorentzTensor.Tensor c1hta:toComplex ((prodT ((Tensor.basis c) b)) ta) = prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex ta)htb:toComplex ((prodT ((Tensor.basis c) b)) tb) = prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex tb)⊢ toComplex ((prodT ((Tensor.basis c) b)) (ta + tb)) =
prodTColorToComplex (toComplex ((Tensor.basis c) b)) (toComplex (ta + tb)) All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colort1:realLorentzTensor.Tensor c1⊢ toComplex ((prodT 0) t1) = prodTColorToComplex (toComplex 0) (toComplex t1) All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colort1:realLorentzTensor.Tensor c1r:ℝta:realLorentzTensor.Tensor chta:toComplex ((prodT ta) t1) = prodTColorToComplex (toComplex ta) (toComplex t1)⊢ toComplex ((prodT (r • ta)) t1) = prodTColorToComplex (toComplex (r • ta)) (toComplex t1) All goals completed! 🐙
n:ℕm:ℕc:Fin n → Colorc1:Fin m → Colort1:realLorentzTensor.Tensor c1ta:realLorentzTensor.Tensor ctb:realLorentzTensor.Tensor chta:toComplex ((prodT ta) t1) = prodTColorToComplex (toComplex ta) (toComplex t1)htb:toComplex ((prodT tb) t1) = prodTColorToComplex (toComplex tb) (toComplex t1)⊢ toComplex ((prodT (ta + tb)) t1) = prodTColorToComplex (toComplex (ta + tb)) (toComplex t1) All goals completed! 🐙
E. Compatibility with contraction: contrT
τ commutes with colorToComplex on the Lorentz up/down colors.
@[simp]
lemma tau_colorToComplex (x : realLorentzTensor.Color) :
(complexLorentzTensor).τ (colorToComplex x) = colorToComplex ((realLorentzTensor).τ x) := x:Color⊢ complexLorentzTensor.τ (colorToComplex x) = colorToComplex (realLorentzTensor.τ x)
⊢ complexLorentzTensor.τ (colorToComplex Color.up) = colorToComplex (realLorentzTensor.τ Color.up)⊢ complexLorentzTensor.τ (colorToComplex Color.down) = colorToComplex (realLorentzTensor.τ Color.down) ⊢ complexLorentzTensor.τ (colorToComplex Color.up) = colorToComplex (realLorentzTensor.τ Color.up)⊢ complexLorentzTensor.τ (colorToComplex Color.down) = colorToComplex (realLorentzTensor.τ Color.down) All goals completed! 🐙
complexify commutes with precomposition by succSuccAbove.
We use fun k => b (Fin.succSuccAbove i j k) and direct application
(ComponentIdx.complexify b) (Fin.succSuccAbove i j m) rather than composition so that
dependent ComponentIdx types unify correctly (avoiding Function.comp type mismatch).
@[simp]
lemma ComponentIdx.complexify_comp_succSuccAbove
{n : ℕ} {c : Fin (n + 1 + 1) → realLorentzTensor.Color}
{i j : Fin (n + 1 + 1)} (b : ComponentIdx (S := realLorentzTensor) c) (m : Fin n) :
(ComponentIdx.complexify (c := c ∘ Fin.succSuccAbove i j)
(fun k => b (Fin.succSuccAbove i j k))) m =
(ComponentIdx.complexify (c := c) b) (Fin.succSuccAbove i j m) := n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:ComponentIdx cm:Fin n⊢ ComponentIdx.complexify (fun k => b (i.succSuccAbove j k)) m = ComponentIdx.complexify b (i.succSuccAbove j m)
All goals completed! 🐙
For a real basis vector, toComplex(contrP(basisVector c b)) equals
contrP(basisVector (colorToComplex ∘ c) (complexify b)) (complex species).
n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ realLorentzTensor.τ (c i) = c jb:ComponentIdx cc':Fin n → Color := c ∘ i.succSuccAbove j⊢ (Tensor.basis (colorToComplex ∘ c')) (ComponentIdx.complexify fun k => b (i.succSuccAbove j k)) =
(Tensor.basis ((colorToComplex ∘ c) ∘ i.succSuccAbove j)) fun m => ComponentIdx.complexify b (i.succSuccAbove j m)
All goals completed! 🐙
The map toComplex commutes with contrT.
set_option backward.isDefEq.respectTransparency false inn:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ realLorentzTensor.τ (c i) = c jb:ComponentIdx c⊢ toComplex (Pure.contrP i j h (Pure.basisVector c b)) =
Pure.contrP i j ⋯ (Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b))
All goals completed! 🐙
n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ realLorentzTensor.τ (c i) = c j⊢ toComplex ((contrT n i j h) 0) = (contrT n i j ⋯) (toComplex 0) All goals completed! 🐙
n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ realLorentzTensor.τ (c i) = c jr:ℝt:realLorentzTensor.Tensor cht:toComplex ((contrT n i j h) t) = (contrT n i j ⋯) (toComplex t)⊢ toComplex ((contrT n i j h) (r • t)) = (contrT n i j ⋯) (toComplex (r • t)) All goals completed! 🐙
n:ℕc:Fin (n + 1 + 1) → Colori:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ realLorentzTensor.τ (c i) = c jt1:realLorentzTensor.Tensor ct2:realLorentzTensor.Tensor ch1:toComplex ((contrT n i j h) t1) = (contrT n i j ⋯) (toComplex t1)h2:toComplex ((contrT n i j h) t2) = (contrT n i j ⋯) (toComplex t2)⊢ toComplex ((contrT n i j h) (t1 + t2)) = (contrT n i j ⋯) (toComplex (t1 + t2)) All goals completed! 🐙
F. Compatibility with evaluation: evalT
complexify commutes with precomposition by succAbove.
@[simp]
lemma ComponentIdx.complexify_comp_succAbove
{n : ℕ} {c : Fin (n + 1) → realLorentzTensor.Color} (i : Fin (n + 1))
(b : ComponentIdx (S := realLorentzTensor) c) (m : Fin n) :
(ComponentIdx.complexify (c := c ∘ i.succAbove) (fun k => b (i.succAbove k))) m =
(ComponentIdx.complexify (c := c) b) (i.succAbove m) := n:ℕc:Fin (n + 1) → Colori:Fin (n + 1)b:ComponentIdx cm:Fin n⊢ ComponentIdx.complexify (fun k => b (i.succAbove k)) m = ComponentIdx.complexify b (i.succAbove m)
All goals completed! 🐙
For a real basis vector, toComplex(evalP(basisVector c b)) equals
evalP(basisVector (colorToComplex ∘ c) (complexify b)) (complex species).
set_option backward.isDefEq.respectTransparency false inn:ℕc:Fin (n + 1) → Colori:Fin (n + 1)b:Fin 1 ⊕ Fin 3b':ComponentIdx chdrop:(Pure.basisVector c b').drop i = Pure.basisVector (c ∘ i.succAbove) fun k => b' (i.succAbove k)h:b' i = bhdrop':(Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b')).drop i =
Pure.basisVector (colorToComplex ∘ c ∘ i.succAbove) (ComponentIdx.complexify fun k => b' (i.succAbove k))⊢ (Pure.basisVector (colorToComplex ∘ c ∘ i.succAbove) (ComponentIdx.complexify fun k => b' (i.succAbove k))).toTensor =
(permT id ⋯)
(Pure.basisVector (colorToComplex ∘ c ∘ i.succAbove) (ComponentIdx.complexify fun k => b' (i.succAbove k))).toTensor
All goals completed! 🐙
n:ℕc:Fin (n + 1) → Colori:Fin (n + 1)b:Fin 1 ⊕ Fin 3b':ComponentIdx chdrop:(Pure.basisVector c b').drop i = Pure.basisVector (c ∘ i.succAbove) fun k => b' (i.succAbove k)h:¬b' i = b⊢ ↑(if b' i = b then 1 else 0) • toComplex (Pure.basisVector (c ∘ i.succAbove) fun k => b' (i.succAbove k)).toTensor =
(permT id ⋯)
((if Fin.cast ⋯ (finSumFinEquiv (b' i)) = Fin.cast ⋯ (finSumFinEquiv b) then 1 else 0) •
((Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b')).drop i).toTensor) All goals completed! 🐙
The map toComplex commutes with evalT.
n:ℕc:Fin (n + 1) → Colori:Fin (n + 1)b:Fin 1 ⊕ Fin 3b':ComponentIdx c⊢ toComplex (Pure.evalP i b (Pure.basisVector c b')) =
(permT id ⋯)
(Pure.evalP i (evalIdxToComplex i b) (Pure.basisVector (colorToComplex ∘ c) (ComponentIdx.complexify b')))
All goals completed! 🐙
n:ℕc:Fin (n + 1) → Colori:Fin (n + 1)b:Fin 1 ⊕ Fin 3⊢ toComplex ((evalT i b) 0) = evalTColorToComplex i b (toComplex 0) All goals completed! 🐙
n:ℕc:Fin (n + 1) → Colori:Fin (n + 1)b:Fin 1 ⊕ Fin 3r:ℝt':realLorentzTensor.Tensor cht':toComplex ((evalT i b) t') = evalTColorToComplex i b (toComplex t')⊢ toComplex ((evalT i b) (r • t')) = evalTColorToComplex i b (toComplex (r • t')) All goals completed! 🐙
n:ℕc:Fin (n + 1) → Colori:Fin (n + 1)b:Fin 1 ⊕ Fin 3t1:realLorentzTensor.Tensor ct2:realLorentzTensor.Tensor ch1:toComplex ((evalT i b) t1) = evalTColorToComplex i b (toComplex t1)h2:toComplex ((evalT i b) t2) = evalTColorToComplex i b (toComplex t2)⊢ toComplex ((evalT i b) (t1 + t2)) = evalTColorToComplex i b (toComplex (t1 + t2)) All goals completed! 🐙