Imports
Metrics as complex Lorentz tensors
@[ expose ] public section
Definitions.
The metric ηᵢᵢ as a complex Lorentz tensor.
The metric ηⁱⁱ as a complex Lorentz tensor.
The metric εᵃᵃ as a complex Lorentz tensor.
The metric ε^{dot a}^{dot a} as a complex Lorentz tensor.
The metric εₐₐ as a complex Lorentz tensor.
The metric ε_{dot a}_{dot a} as a complex Lorentz tensor.
Notation
The metric ηᵢᵢ as a complex Lorentz tensors.
scoped [ complexLorentzTensor ] notation "η'" => coMetric
The metric ηⁱⁱ as a complex Lorentz tensors.
scoped [ complexLorentzTensor ] notation "η" => contrMetric
The metric εᵃᵃ as a complex Lorentz tensors.
scoped [ complexLorentzTensor ] notation "εL" => leftMetric
The metric ε^{dot a}^{dot a} as a complex Lorentz tensors.
scoped [ complexLorentzTensor ] notation "εR" => rightMetric
The metric εₐₐ as a complex Lorentz tensors.
The metric ε_{dot a}_{dot a} as a complex Lorentz tensors.
fromConstPair
lemma coMetric_eq_fromConstPair : η' = fromConstPair ( S := complexLorentzTensor )
( c1 := .down ) ( c2 := .down ) Lorentz.coMetric := by ⊢ η' = fromConstPair Lorentz.coMetric
rw [ Lorentz.coMetric ⊢ η' =
fromConstPair
{
toFun := fun a =>
have a' := a ;
a' • Lorentz.coMetricVal ,
map_add' := ⋯ , map_smul' := ⋯ , isIntertwining' := ⋯ } ⊢ η' =
fromConstPair
{
toFun := fun a =>
have a' := a ;
a' • Lorentz.coMetricVal ,
map_add' := ⋯ , map_smul' := ⋯ , isIntertwining' := ⋯ } ] ⊢ η' =
fromConstPair
{
toFun := fun a =>
have a' := a ;
a' • Lorentz.coMetricVal ,
map_add' := ⋯ , map_smul' := ⋯ , isIntertwining' := ⋯ }
rfl All goals completed! 🐙
lemma contrMetric_eq_fromConstPair : η = fromConstPair ( S := complexLorentzTensor )
( c1 := .up ) ( c2 := .up ) Lorentz.contrMetric := by ⊢ η = fromConstPair Lorentz.contrMetric
rw [ Lorentz.contrMetric ⊢ η =
fromConstPair
{
toFun := fun a =>
have a' := a ;
a' • Lorentz.contrMetricVal ,
map_add' := ⋯ , map_smul' := ⋯ , isIntertwining' := ⋯ } ⊢ η =
fromConstPair
{
toFun := fun a =>
have a' := a ;
a' • Lorentz.contrMetricVal ,
map_add' := ⋯ , map_smul' := ⋯ , isIntertwining' := ⋯ } ] ⊢ η =
fromConstPair
{
toFun := fun a =>
have a' := a ;
a' • Lorentz.contrMetricVal ,
map_add' := ⋯ , map_smul' := ⋯ , isIntertwining' := ⋯ }
rfl All goals completed! 🐙 lemma leftMetric_eq_fromConstPair : εL = fromConstPair Fermion.leftMetric := rfl lemma rightMetric_eq_fromConstPair : εR = fromConstPair Fermion.rightMetric := rfl lemma dualLeftMetric_eq_fromConstPair : εL' = fromConstPair Fermion.dualLeftMetric := rfl lemma dualRightMetric_eq_fromConstPair : εR' = fromConstPair Fermion.dualRightMetric := rfl
fromPairT
complexCoBasis etc.
basis
ofRat
lemma coMetric_eq_ofRat : η' = ofRat fun f =>
if f 0 = Fin.cast ( by f : ComponentIdx ![ Color.down , Color.down ] ⊢ 4 = repDim ( ![ Color.down , Color.down ] 0 ) rfl All goals completed! 🐙 ) ( 0 : Fin 4 ) ∧ f 1 = Fin.cast ( by f : ComponentIdx ![ Color.down , Color.down ] ⊢ 4 = repDim ( ![ Color.down , Color.down ] 1 ) rfl All goals completed! 🐙 ) ( 0 : Fin 4 ) then 1 else
if f 0 = f 1 then - 1 else 0 := by ⊢ η' = ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
rw [ coMetric_eq_basis ⊢ ( ( ( ( ( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 0
| 1 => 0 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 1
| 1 => 1 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 2
| 1 => 2 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ( ( ( ( ( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 0
| 1 => 0 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 1
| 1 => 1 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 2
| 1 => 2 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ] ⊢ ( ( ( ( ( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 0
| 1 => 0 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 1
| 1 => 1 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 2
| 1 => 2 ) -
( Tensor.basis ![ Color.down , Color.down ] ) fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
conv_lhs =>
rw [ basis_eq_ofRat , basis_eq_ofRat , basis_eq_ofRat , basis_eq_ofRat ] | ( ( ( ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 }
rw [ ← map_sub , ⊢ ( ( ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ← map_sub , ⊢ ( ofRat
( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ← map_sub ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ] ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
congr e_6 ⊢ ( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
with_unfolding_all decide All goals completed! 🐙
lemma contrMetric_eq_ofRat : η = ofRat fun f =>
if f 0 = Fin.cast ( by f : ComponentIdx ![ Color.up , Color.up ] ⊢ 4 = repDim ( ![ Color.up , Color.up ] 0 ) rfl All goals completed! 🐙 ) ( 0 : Fin 4 ) ∧ f 1 = Fin.cast ( by f : ComponentIdx ![ Color.up , Color.up ] ⊢ 4 = repDim ( ![ Color.up , Color.up ] 1 ) rfl All goals completed! 🐙 ) ( 0 : Fin 4 ) then 1 else
if f 0 = f 1 then - 1 else 0 := by ⊢ η = ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
rw [ contrMetric_eq_basis ⊢ ( ( ( ( ( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 0
| 1 => 0 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 1
| 1 => 1 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 2
| 1 => 2 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ( ( ( ( ( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 0
| 1 => 0 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 1
| 1 => 1 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 2
| 1 => 2 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ] ⊢ ( ( ( ( ( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 0
| 1 => 0 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 1
| 1 => 1 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 2
| 1 => 2 ) -
( Tensor.basis ![ Color.up , Color.up ] ) fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
conv_lhs =>
rw [ basis_eq_ofRat , basis_eq_ofRat , basis_eq_ofRat , basis_eq_ofRat ] | ( ( ( ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 }
rw [ ← map_sub , ⊢ ( ( ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ← map_sub , ⊢ ( ofRat
( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ← map_sub ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0 ] ⊢ ofRat
( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
congr e_6 ⊢ ( ( ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 2
| 1 => 2 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 3
| 1 => 3 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
fun f => if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 0 then 1 else if f 0 = f 1 then - 1 else 0
with_unfolding_all decide All goals completed! 🐙
lemma leftMetric_eq_ofRat : εL = ofRat fun f =>
if f 0 = Fin.cast ( by f : ComponentIdx ![ Color.upL , Color.upL ] ⊢ 2 = repDim ( ![ Color.upL , Color.upL ] 0 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 1 = Fin.cast ( by f : ComponentIdx ![ Color.upL , Color.upL ] ⊢ 2 = repDim ( ![ Color.upL , Color.upL ] 1 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then - 1 else
if f 1 = Fin.cast ( by f : ComponentIdx ![ Color.upL , Color.upL ] ⊢ 2 = repDim ( ![ Color.upL , Color.upL ] 1 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 0 = Fin.cast ( by f : ComponentIdx ![ Color.upL , Color.upL ] ⊢ 2 = repDim ( ![ Color.upL , Color.upL ] 0 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then
1 else 0 := by ⊢ εL =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
rw [ leftMetric_eq_basis ⊢ ( ( - ( Tensor.basis ![ Color.upL , Color.upL ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) +
( Tensor.basis ![ Color.upL , Color.upL ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ⊢ ( ( - ( Tensor.basis ![ Color.upL , Color.upL ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) +
( Tensor.basis ![ Color.upL , Color.upL ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ] ⊢ ( ( - ( Tensor.basis ![ Color.upL , Color.upL ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) +
( Tensor.basis ![ Color.upL , Color.upL ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
conv_lhs =>
rw [ basis_eq_ofRat , basis_eq_ofRat ] | ( - ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 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 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 }
rw [ ← map_neg , ⊢ ( ofRat
( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 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 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ← map_add ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ] ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
congr e_6 ⊢ ( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
with_unfolding_all decide All goals completed! 🐙
lemma dualLeftMetric_eq_ofRat : εL' = ofRat fun f =>
if f 0 = Fin.cast ( by f : ComponentIdx ![ Color.downL , Color.downL ] ⊢ 2 = repDim ( ![ Color.downL , Color.downL ] 0 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 1 = Fin.cast ( by f : ComponentIdx ![ Color.downL , Color.downL ] ⊢ 2 = repDim ( ![ Color.downL , Color.downL ] 1 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then 1 else
if f 1 = Fin.cast ( by f : ComponentIdx ![ Color.downL , Color.downL ] ⊢ 2 = repDim ( ![ Color.downL , Color.downL ] 1 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 0 = Fin.cast ( by f : ComponentIdx ![ Color.downL , Color.downL ] ⊢ 2 = repDim ( ![ Color.downL , Color.downL ] 0 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then
- 1 else 0 := by ⊢ εL' =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
rw [ dualLeftMetric_eq_basis ⊢ ( ( ( Tensor.basis ![ Color.downL , Color.downL ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) -
( Tensor.basis ![ Color.downL , Color.downL ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ⊢ ( ( ( Tensor.basis ![ Color.downL , Color.downL ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) -
( Tensor.basis ![ Color.downL , Color.downL ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ] ⊢ ( ( ( Tensor.basis ![ Color.downL , Color.downL ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) -
( Tensor.basis ![ Color.downL , Color.downL ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
conv_lhs =>
rw [ basis_eq_ofRat , basis_eq_ofRat ] | ( ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 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 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 }
rw [ ← map_sub ⊢ ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ⊢ ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ] ⊢ ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
congr e_6 ⊢ ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
with_unfolding_all decide All goals completed! 🐙
lemma rightMetric_eq_ofRat : εR = ofRat fun f =>
if f 0 = Fin.cast ( by f : ComponentIdx ![ Color.upR , Color.upR ] ⊢ 2 = repDim ( ![ Color.upR , Color.upR ] 0 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 1 = Fin.cast ( by f : ComponentIdx ![ Color.upR , Color.upR ] ⊢ 2 = repDim ( ![ Color.upR , Color.upR ] 1 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then - 1 else
if f 1 = Fin.cast ( by f : ComponentIdx ![ Color.upR , Color.upR ] ⊢ 2 = repDim ( ![ Color.upR , Color.upR ] 1 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 0 = Fin.cast ( by f : ComponentIdx ![ Color.upR , Color.upR ] ⊢ 2 = repDim ( ![ Color.upR , Color.upR ] 0 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then 1 else 0 := by ⊢ εR =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
rw [ rightMetric_eq_basis ⊢ ( ( - ( Tensor.basis ![ Color.upR , Color.upR ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) +
( Tensor.basis ![ Color.upR , Color.upR ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ⊢ ( ( - ( Tensor.basis ![ Color.upR , Color.upR ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) +
( Tensor.basis ![ Color.upR , Color.upR ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ] ⊢ ( ( - ( Tensor.basis ![ Color.upR , Color.upR ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) +
( Tensor.basis ![ Color.upR , Color.upR ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
conv_lhs =>
rw [ basis_eq_ofRat , basis_eq_ofRat ] | ( - ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 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 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 }
rw [ ← map_neg , ⊢ ( ofRat
( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 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 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ← map_add ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0 ] ⊢ ofRat
( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
congr e_6 ⊢ ( ( - fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) +
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then - 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then 1 else 0
with_unfolding_all decide All goals completed! 🐙
lemma dualRightMetric_eq_ofRat : εR' = ofRat fun f =>
if f 0 = Fin.cast ( by f : ComponentIdx ![ Color.downR , Color.downR ] ⊢ 2 = repDim ( ![ Color.downR , Color.downR ] 0 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 1 = Fin.cast ( by f : ComponentIdx ![ Color.downR , Color.downR ] ⊢ 2 = repDim ( ![ Color.downR , Color.downR ] 1 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then 1 else
if f 1 = Fin.cast ( by f : ComponentIdx ![ Color.downR , Color.downR ] ⊢ 2 = repDim ( ![ Color.downR , Color.downR ] 1 ) rfl All goals completed! 🐙 ) ( 0 : Fin 2 ) ∧ f 0 = Fin.cast ( by f : ComponentIdx ![ Color.downR , Color.downR ] ⊢ 2 = repDim ( ![ Color.downR , Color.downR ] 0 ) rfl All goals completed! 🐙 ) ( 1 : Fin 2 ) then
- 1 else 0 := by ⊢ εR' =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
rw [ dualRightMetric_eq_basis ⊢ ( ( ( Tensor.basis ![ Color.downR , Color.downR ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) -
( Tensor.basis ![ Color.downR , Color.downR ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ⊢ ( ( ( Tensor.basis ![ Color.downR , Color.downR ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) -
( Tensor.basis ![ Color.downR , Color.downR ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ] ⊢ ( ( ( Tensor.basis ![ Color.downR , Color.downR ] ) fun x =>
match x with
| 0 => 0
| 1 => 1 ) -
( Tensor.basis ![ Color.downR , Color.downR ] ) fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
conv_lhs =>
rw [ basis_eq_ofRat , basis_eq_ofRat ] | ( ofRat fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 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 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 }
rw [ ← map_sub ⊢ ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ⊢ ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0 ] ⊢ ofRat
( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
ofRat fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
congr e_6 ⊢ ( (fun b' =>
if
(fun x =>
match x with
| 0 => 0
| 1 => 1 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) -
fun b' =>
if
(fun x =>
match x with
| 0 => 1
| 1 => 0 ) =
b' then
{ fst := 1 , snd := 0 }
else { fst := 0 , snd := 0 } ) =
fun f =>
if f 0 = Fin.cast ⋯ 0 ∧ f 1 = Fin.cast ⋯ 1 then 1 else if f 1 = Fin.cast ⋯ 0 ∧ f 0 = Fin.cast ⋯ 1 then - 1 else 0
with_unfolding_all decide All goals completed! 🐙
Group actions
The tensor coMetric is invariant under the action of SL(2,ℂ).
The tensor contrMetric is invariant under the action of SL(2,ℂ).
The tensor leftMetric is invariant under the action of SL(2,ℂ).
The tensor rightMetric is invariant under the action of SL(2,ℂ).
The tensor dualLeftMetric is invariant under the action of SL(2,ℂ).
The tensor dualRightMetric is invariant under the action of SL(2,ℂ).