Imports
/- 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 -/ module public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Basic public import Physlib.Relativity.PauliMatrices.AsTensor public import Physlib.Relativity.Tensors.ComplexTensor.Metrics.Basic

Pauli matrices as a tensor

@[expose] public section

Tensorial structure

The tensorial structure on the type Fin 1 ⊕ Fin 3 → Matrix (Fin 2) (Fin 2) ℂ and properties thereof.

The equivalence between the type of indices of a [.up, .upL, .upR] tensor and (Fin 1 ⊕ Fin 3) × Fin 2 × Fin 2.

def indexEquiv : ComponentIdx (S := complexLorentzTensor) ![.up, .upL, .upR] (Fin 1 Fin 3) × Fin 2 × Fin 2 where toFun v := (finSumFinEquiv.symm (v 0 : Fin 4), v 1, v 2) invFun v := fun | 0 => finSumFinEquiv v.1 | 1 => v.2.1 | 2 => v.2.2 left_inv v := v:ComponentIdx ![Color.up, Color.upL, Color.upR](fun v x => match x with | 0 => finSumFinEquiv v.1 | 1 => v.2.1 | 2 => v.2.2) ((fun v => (finSumFinEquiv.symm (v 0), v 1, v 2)) v) = v v:ComponentIdx ![Color.up, Color.upL, Color.upR]x:Fin (Nat.succ 0).succ.succ(fun v x => match x with | 0 => finSumFinEquiv v.1 | 1 => v.2.1 | 2 => v.2.2) ((fun v => (finSumFinEquiv.symm (v 0), v 1, v 2)) v) x = v x v:ComponentIdx ![Color.up, Color.upL, Color.upR]x:Fin (Nat.succ 0).succ.succ(match x with | 0 => v 0 | 1 => v 1 | 2 => v 2) = v x v:ComponentIdx ![Color.up, Color.upL, Color.upR](match (fun i => i) 0, with | 0 => v 0 | 1 => v 1 | 2 => v 2) = v ((fun i => i) 0, )v:ComponentIdx ![Color.up, Color.upL, Color.upR](match (fun i => i) 1, with | 0 => v 0 | 1 => v 1 | 2 => v 2) = v ((fun i => i) 1, )v:ComponentIdx ![Color.up, Color.upL, Color.upR](match (fun i => i) 2, with | 0 => v 0 | 1 => v 1 | 2 => v 2) = v ((fun i => i) 2, ) v:ComponentIdx ![Color.up, Color.upL, Color.upR](match (fun i => i) 0, with | 0 => v 0 | 1 => v 1 | 2 => v 2) = v ((fun i => i) 0, )v:ComponentIdx ![Color.up, Color.upL, Color.upR](match (fun i => i) 1, with | 0 => v 0 | 1 => v 1 | 2 => v 2) = v ((fun i => i) 1, )v:ComponentIdx ![Color.up, Color.upL, Color.upR](match (fun i => i) 2, with | 0 => v 0 | 1 => v 1 | 2 => v 2) = v ((fun i => i) 2, ) All goals completed! 🐙 right_inv v := v:(Fin 1 Fin 3) × Fin 2 × Fin 2(fun v => (finSumFinEquiv.symm (v 0), v 1, v 2)) ((fun v x => match x with | 0 => finSumFinEquiv v.1 | 1 => v.2.1 | 2 => v.2.2) v) = v All goals completed! 🐙
instance tensorial : TensorSpecies.Tensorial complexLorentzTensor ![.up, .upL, .upR] (Fin 1 Fin 3 Matrix (Fin 2) (Fin 2) ) where toTensor := LinearEquiv.symm <| Equiv.toLinearEquiv ((Tensor.basis (S := complexLorentzTensor) ![.up, .upL, .upR]).repr.toEquiv.trans <| Finsupp.equivFunOnFinite.trans <| (Equiv.piCongrLeft' _ indexEquiv).trans <| (Equiv.curry _ _ _).trans <| Equiv.piCongrRight fun _ => Equiv.curry _ _ _) { map_add := fun x y => x:complexLorentzTensor.Tensor ![Color.up, Color.upL, Color.upR]y:complexLorentzTensor.Tensor ![Color.up, Color.upL, Color.upR]((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr.toEquiv.trans (Finsupp.equivFunOnFinite.trans ((Equiv.piCongrLeft' (fun a => ) indexEquiv).trans ((Equiv.curry (Fin 1 Fin 3) (Fin 2 × Fin 2) ).trans (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ))))) (x + y) = ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr.toEquiv.trans (Finsupp.equivFunOnFinite.trans ((Equiv.piCongrLeft' (fun a => ) indexEquiv).trans ((Equiv.curry (Fin 1 Fin 3) (Fin 2 × Fin 2) ).trans (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ))))) x + ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr.toEquiv.trans (Finsupp.equivFunOnFinite.trans ((Equiv.piCongrLeft' (fun a => ) indexEquiv).trans ((Equiv.curry (Fin 1 Fin 3) (Fin 2 × Fin 2) ).trans (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ))))) y x:complexLorentzTensor.Tensor ![Color.up, Color.upL, Color.upR]y:complexLorentzTensor.Tensor ![Color.up, Color.upL, Color.upR](Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ) (Function.curry ((Equiv.piCongrLeft' (fun a => ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr x + (Tensor.basis ![Color.up, Color.upL, Color.upR]).repr y)))) = (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ) (Function.curry ((Equiv.piCongrLeft' (fun a => ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr x)))) + (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ) (Function.curry ((Equiv.piCongrLeft' (fun a => ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr y)))) All goals completed! 🐙 map_smul := fun c x => c:x:complexLorentzTensor.Tensor ![Color.up, Color.upL, Color.upR]((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr.toEquiv.trans (Finsupp.equivFunOnFinite.trans ((Equiv.piCongrLeft' (fun a => ) indexEquiv).trans ((Equiv.curry (Fin 1 Fin 3) (Fin 2 × Fin 2) ).trans (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ))))) (c x) = c ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr.toEquiv.trans (Finsupp.equivFunOnFinite.trans ((Equiv.piCongrLeft' (fun a => ) indexEquiv).trans ((Equiv.curry (Fin 1 Fin 3) (Fin 2 × Fin 2) ).trans (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ))))) x c:x:complexLorentzTensor.Tensor ![Color.up, Color.upL, Color.upR](Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ) (Function.curry ((Equiv.piCongrLeft' (fun a => ) indexEquiv) (Finsupp.equivFunOnFinite (c (Tensor.basis ![Color.up, Color.upL, Color.upR]).repr x)))) = c (Equiv.piCongrRight fun x => Equiv.curry (Fin 2) (Fin 2) ) (Function.curry ((Equiv.piCongrLeft' (fun a => ) indexEquiv) (Finsupp.equivFunOnFinite ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr x)))) All goals completed! 🐙}lemma toTensor_symm_apply (p : ℂT[.up, .upL, .upR]) : (toTensor (self := tensorial)).symm p = ((Equiv.piCongrRight fun _ => Equiv.curry _ _ _) <| (Equiv.curry _ _ _) <| Equiv.piCongrLeft' _ indexEquiv <| Finsupp.equivFunOnFinite <| (Tensor.basis (S := complexLorentzTensor) _).repr p) := rflb:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2(if indexEquiv.symm (μ, α, β) = b then 1 else 0) = if b 0 = finSumFinEquiv μ b 1 = α b 2 = β then 1 else 0 b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2(indexEquiv.symm (μ, α, β) = b) = (b 0 = finSumFinEquiv μ b 1 = α b 2 = β) b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2(fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b b 0 = finSumFinEquiv μ b 1 = α b 2 = β b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2(fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b b 0 = finSumFinEquiv μ b 1 = α b 2 = βb:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2b 0 = finSumFinEquiv μ b 1 = α b 2 = β (fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2(fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b b 0 = finSumFinEquiv μ b 1 = α b 2 = β b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:(fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = bb 0 = finSumFinEquiv μ b 1 = α b 2 = β μ:Fin 1 Fin 3α:Fin 2β:Fin 2(fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) 0 = finSumFinEquiv μ (fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) 1 = α (fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) 2 = β All goals completed! 🐙 b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2b 0 = finSumFinEquiv μ b 1 = α b 2 = β (fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = β(fun x => match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = βx:Fin 3(match x with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b x b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = β(match (fun i => i) 0, with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b ((fun i => i) 0, )b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = β(match (fun i => i) 1, with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b ((fun i => i) 1, )b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = β(match (fun i => i) 2, with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b ((fun i => i) 2, ) b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = β(match (fun i => i) 0, with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b ((fun i => i) 0, ) All goals completed! 🐙 b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = β(match (fun i => i) 1, with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b ((fun i => i) 1, ) All goals completed! 🐙 b:(x : Fin (Nat.succ 0).succ.succ) Fin (repDim (![Color.up, Color.upL, Color.upR] x))μ:Fin 1 Fin 3α:Fin 2β:Fin 2h:b 0 = finSumFinEquiv μ b 1 = α b 2 = β(match (fun i => i) 2, with | 0 => finSumFinEquiv μ | 1 => α | 2 => β) = b ((fun i => i) 2, ) All goals completed! 🐙

Pauli matrices as a tensor

The Pauli matrices as a tensor toTensor pauliMatrix in ℂT[.up, .upL, .upR].

scoped[PauliMatrix] notation "σ^^^" => toTensor pauliMatrix
σ (Sum.inr 2) 1 1 = 0 - 1 All goals completed! 🐙b:ComponentIdx ![Color.up, Color.upL, Color.upR]((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr ((((((((ofRat fun b' => if (fun x => match x with | 0 => 0 | 1 => 0 | 2 => 0) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + ofRat fun b' => if (fun x => match x with | 0 => 0 | 1 => 1 | 2 => 1) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + ofRat fun b' => if (fun x => match x with | 0 => 1 | 1 => 0 | 2 => 1) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + ofRat fun b' => if (fun x => match x with | 0 => 1 | 1 => 1 | 2 => 0) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - I ofRat fun b' => if (fun x => match x with | 0 => 2 | 1 => 0 | 2 => 1) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + I ofRat fun b' => if (fun x => match x with | 0 => 2 | 1 => 1 | 2 => 0) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + ofRat fun b' => if (fun x => match x with | 0 => 3 | 1 => 0 | 2 => 0) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - ofRat fun b' => if (fun x => match x with | 0 => 3 | 1 => 1 | 2 => 1) = b' then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })) b = ((Tensor.basis ![Color.up, Color.upL, Color.upR]).repr (ofRat fun b => if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0)) b b:ComponentIdx ![Color.up, Color.upL, Color.upR]Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 0 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 0 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 1 | 1 => 0 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 1 | 1 => 1 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 2 | 1 => 0 | 2 => 1) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 2 | 1 => 1 | 2 => 0) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 3 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - Physlib.RatComplexNum.toComplexNum (if (fun x => match x with | 0 => 3 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 ¬b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) b:ComponentIdx ![Color.up, Color.upL, Color.upR]Physlib.RatComplexNum.toComplexNum ((((((((if (fun x => match x with | 0 => 0 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 0 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 1 | 1 => 0 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 1 | 1 => 1 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - if (fun x => match x with | 0 => 2 | 1 => 0 | 2 => 1) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 2 | 1 => 1 | 2 => 0) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 3 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - if (fun x => match x with | 0 => 3 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 ¬b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) b:ComponentIdx ![Color.up, Color.upL, Color.upR]((((((((if (fun x => match x with | 0 => 0 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 0 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 1 | 1 => 0 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 1 | 1 => 1 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - if (fun x => match x with | 0 => 2 | 1 => 0 | 2 => 1) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 2 | 1 => 1 | 2 => 0) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 3 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - if (fun x => match x with | 0 => 3 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 ¬b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0 (b : ComponentIdx ![Color.up, Color.upL, Color.upR]), ((((((((if (fun x => match x with | 0 => 0 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 0 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 1 | 1 => 0 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 1 | 1 => 1 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - if (fun x => match x with | 0 => 2 | 1 => 0 | 2 => 1) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 2 | 1 => 1 | 2 => 0) = b then { fst := 0, snd := 1 } * { fst := 1, snd := 0 } else { fst := 0, snd := 1 } * { fst := 0, snd := 0 }) + if (fun x => match x with | 0 => 3 | 1 => 0 | 2 => 0) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) - if (fun x => match x with | 0 => 3 | 1 => 1 | 2 => 1) = b then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 ¬b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0 All goals completed! 🐙Λ:SL(2, )toTensor.symm (toTensor σ) = σ All goals completed! 🐙Λ:SL(2, )Λ fromConstTriple asConsTensor = fromConstTriple asConsTensor All goals completed! 🐙

Variations of the pauli tensor

The Pauli matrices as the complex Lorentz tensor σ_μ^α^{dot β}.

abbrev pauliCo : ℂT[.down, .upL, .upR] := permT id (IsReindexing.auto) {η' | μ ν σ^^^ | ν α β}ᵀ
@[inherit_doc pauliCo] scoped[PauliMatrix] notation "σ_^^" => PauliMatrix.pauliCo

The Pauli matrices as the complex Lorentz tensor σ_μ_{dot β}_α.

abbrev pauliCoDown : ℂT[.down, .downR, .downL] := permT id (IsReindexing.auto) {σ_^^ | μ α β εR' | β β' εL' | α α' }ᵀ
@[inherit_doc pauliCoDown] scoped[PauliMatrix] notation "σ___" => PauliMatrix.pauliCoDown

The Pauli matrices as the complex Lorentz tensor σ^μ_{dot β}_α.

abbrev pauliContrDown : ℂT[.up, .downR, .downL] := permT id (IsReindexing.auto) {σ^^^ | μ α β εR' | β β' εL' | α α'}ᵀ
@[inherit_doc pauliContrDown] scoped[PauliMatrix] notation "σ^__" => PauliMatrix.pauliContrDown

Different forms

b:ComponentIdx ![Color.down, Color.upL, Color.upR]Physlib.RatComplexNum.toComplexNum (∑ x, ((if (ComponentIdx.prod x).1 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).1 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod x).1 0 = (ComponentIdx.prod x).1 1 then -1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast 0 (ComponentIdx.prod x).2 1 = (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 1 (ComponentIdx.prod x).2 1 (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 2 (ComponentIdx.prod x).2 1 = Fin.cast 0 (ComponentIdx.prod x).2 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).2 0 = Fin.cast 2 (ComponentIdx.prod x).2 1 = Fin.cast 1 (ComponentIdx.prod x).2 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).2 0 = Fin.cast 3 (ComponentIdx.prod x).2 1 = Fin.cast 0 (ComponentIdx.prod x).2 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 3 (ComponentIdx.prod x).2 1 = Fin.cast 1 (ComponentIdx.prod x).2 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) * if (x 1) = ((basisIdxCongr ) (x 2)) then 1 else 0) = Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) b:ComponentIdx ![Color.down, Color.upL, Color.upR](∑ x, ((if (ComponentIdx.prod x).1 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).1 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod x).1 0 = (ComponentIdx.prod x).1 1 then -1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast 0 (ComponentIdx.prod x).2 1 = (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 1 (ComponentIdx.prod x).2 1 (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 2 (ComponentIdx.prod x).2 1 = Fin.cast 0 (ComponentIdx.prod x).2 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).2 0 = Fin.cast 2 (ComponentIdx.prod x).2 1 = Fin.cast 1 (ComponentIdx.prod x).2 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).2 0 = Fin.cast 3 (ComponentIdx.prod x).2 1 = Fin.cast 0 (ComponentIdx.prod x).2 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 3 (ComponentIdx.prod x).2 1 = Fin.cast 1 (ComponentIdx.prod x).2 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) * if (x 1) = ((basisIdxCongr ) (x 2)) then 1 else 0) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 } (b : ComponentIdx ![Color.down, Color.upL, Color.upR]), (∑ x, ((if (ComponentIdx.prod x).1 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).1 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod x).1 0 = (ComponentIdx.prod x).1 1 then -1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast 0 (ComponentIdx.prod x).2 1 = (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 1 (ComponentIdx.prod x).2 1 (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 2 (ComponentIdx.prod x).2 1 = Fin.cast 0 (ComponentIdx.prod x).2 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).2 0 = Fin.cast 2 (ComponentIdx.prod x).2 1 = Fin.cast 1 (ComponentIdx.prod x).2 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).2 0 = Fin.cast 3 (ComponentIdx.prod x).2 1 = Fin.cast 0 (ComponentIdx.prod x).2 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast 3 (ComponentIdx.prod x).2 1 = Fin.cast 1 (ComponentIdx.prod x).2 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) * if (x 1) = ((basisIdxCongr ) (x 2)) then 1 else 0) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 } All goals completed! 🐙b:ComponentIdx ![Color.down, Color.downR, Color.downL]Physlib.RatComplexNum.toComplexNum (∑ x, ((∑ x_1, ((if (ComponentIdx.prod x_1).1 0 = Fin.cast 0 (ComponentIdx.prod x_1).1 1 = (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 1 (ComponentIdx.prod x_1).1 1 (ComponentIdx.prod x_1).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x_1 2) = ((basisIdxCongr ) (x_1 3)) then 1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x 1) = ((basisIdxCongr ) (x 3)) then 1 else 0) = Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) b:ComponentIdx ![Color.down, Color.downR, Color.downL](∑ x, ((∑ x_1, ((if (ComponentIdx.prod x_1).1 0 = Fin.cast 0 (ComponentIdx.prod x_1).1 1 = (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 1 (ComponentIdx.prod x_1).1 1 (ComponentIdx.prod x_1).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x_1 2) = ((basisIdxCongr ) (x_1 3)) then 1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x 1) = ((basisIdxCongr ) (x 3)) then 1 else 0) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 } (b : ComponentIdx ![Color.down, Color.downR, Color.downL]), (∑ x, ((∑ x_1, ((if (ComponentIdx.prod x_1).1 0 = Fin.cast 0 (ComponentIdx.prod x_1).1 1 = (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 1 (ComponentIdx.prod x_1).1 1 (ComponentIdx.prod x_1).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x_1 2) = ((basisIdxCongr ) (x_1 3)) then 1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x 1) = ((basisIdxCongr ) (x 3)) then 1 else 0) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 } All goals completed! 🐙b:ComponentIdx ![Color.up, Color.downR, Color.downL]Physlib.RatComplexNum.toComplexNum (∑ x, ((∑ x_1, ((if (ComponentIdx.prod x_1).1 0 = Fin.cast 0 (ComponentIdx.prod x_1).1 1 = (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 1 (ComponentIdx.prod x_1).1 1 (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x_1 2) = ((basisIdxCongr ) (x_1 3)) then 1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x 1) = ((basisIdxCongr ) (x 3)) then 1 else 0) = Physlib.RatComplexNum.toComplexNum (if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := -1, snd := 0 } else 0) b:ComponentIdx ![Color.up, Color.downR, Color.downL](∑ x, ((∑ x_1, ((if (ComponentIdx.prod x_1).1 0 = Fin.cast 0 (ComponentIdx.prod x_1).1 1 = (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 1 (ComponentIdx.prod x_1).1 1 (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x_1 2) = ((basisIdxCongr ) (x_1 3)) then 1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x 1) = ((basisIdxCongr ) (x 3)) then 1 else 0) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := -1, snd := 0 } else 0 (b : ComponentIdx ![Color.up, Color.downR, Color.downL]), (∑ x, ((∑ x_1, ((if (ComponentIdx.prod x_1).1 0 = Fin.cast 0 (ComponentIdx.prod x_1).1 1 = (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 1 (ComponentIdx.prod x_1).1 1 (ComponentIdx.prod x_1).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 2 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 0 (ComponentIdx.prod x_1).1 2 = Fin.cast 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x_1).1 0 = Fin.cast 3 (ComponentIdx.prod x_1).1 1 = Fin.cast 1 (ComponentIdx.prod x_1).1 2 = Fin.cast 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x_1).2 1 = Fin.cast dualRightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x_1).2 0 = Fin.cast dualRightMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x_1 2) = ((basisIdxCongr ) (x_1 3)) then 1 else 0) * if (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 1 then 1 else if (ComponentIdx.prod x).2 1 = Fin.cast dualLeftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 0 = Fin.cast dualLeftMetric_eq_ofRat._proof_1 1 then -1 else 0) * if (x 1) = ((basisIdxCongr ) (x 3)) then 1 else 0) = if b 0 = Fin.cast 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 1 b 1 b 2 then { fst := -1, snd := 0 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 0 b 2 = Fin.cast 1 then { fst := 0, snd := 1 } else if b 0 = Fin.cast 2 b 1 = Fin.cast 1 b 2 = Fin.cast 0 then { fst := 0, snd := -1 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 1 b 2 = Fin.cast 1 then { fst := 1, snd := 0 } else if b 0 = Fin.cast 3 b 1 = Fin.cast 0 b 2 = Fin.cast 0 then { fst := -1, snd := 0 } else 0 All goals completed! 🐙

Group actions

The tensor pauliCo is invariant under the action of SL(2,ℂ).

set_option backward.isDefEq.respectTransparency false inAll goals completed! 🐙

The tensor pauliCoDown is invariant under the action of SL(2,ℂ).

set_option backward.isDefEq.respectTransparency false in set_option maxRecDepth 2000 inAll goals completed! 🐙

The tensor pauliContrDown is invariant under the action of SL(2,ℂ).

set_option backward.isDefEq.respectTransparency false inAll goals completed! 🐙