Joseph Tooby-Smith
GitHub
commit
4cd823837a
1 changed files with 55 additions and 72 deletions
|
|
@ -1,11 +1,10 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import Mathlib.Logic.Function.CompTypeclasses
|
||||
import Mathlib.Data.Real.Basic
|
||||
import Mathlib.CategoryTheory.FintypeCat
|
||||
import Mathlib.Analysis.Normed.Field.Basic
|
||||
import Mathlib.LinearAlgebra.Matrix.Trace
|
||||
/-!
|
||||
|
|
@ -22,7 +21,6 @@ This will relation should be made explicit in the future.
|
|||
-- For modular operads see: [Raynor][raynor2021graphical]
|
||||
|
||||
-/
|
||||
/-! TODO: Replace `FintypeCat` throughout with `Type` and `Fintype`. -/
|
||||
/-! TODO: Do complex tensors, with Van der Waerden notation for fermions. -/
|
||||
/-! TODO: Generalize to maps into Lorentz tensors. -/
|
||||
/-!
|
||||
|
|
@ -37,7 +35,7 @@ inductive RealLorentzTensor.Colors where
|
|||
| up : RealLorentzTensor.Colors
|
||||
| down : RealLorentzTensor.Colors
|
||||
|
||||
/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`.-/
|
||||
/-- The association of colors with indices. For up and down this is `Fin 1 ⊕ Fin d`. -/
|
||||
def RealLorentzTensor.ColorsIndex (d : ℕ) (μ : RealLorentzTensor.Colors) : Type :=
|
||||
match μ with
|
||||
| RealLorentzTensor.Colors.up => Fin 1 ⊕ Fin d
|
||||
|
|
@ -51,42 +49,33 @@ instance (d : ℕ) (μ : RealLorentzTensor.Colors) : Fintype (RealLorentzTensor.
|
|||
/-- An `IndexValue` is a set of actual values an index can take. e.g. for a
|
||||
3-tensor (0, 1, 2). -/
|
||||
@[simp]
|
||||
def RealLorentzTensor.IndexValue {X : FintypeCat} (d : ℕ ) (c : X → RealLorentzTensor.Colors) :
|
||||
def RealLorentzTensor.IndexValue {X : Type} (d : ℕ) (c : X → RealLorentzTensor.Colors) :
|
||||
Type 0 := (x : X) → RealLorentzTensor.ColorsIndex d (c x)
|
||||
|
||||
/-- A Lorentz Tensor defined by its coordinate map. -/
|
||||
structure RealLorentzTensor (d : ℕ) (X : FintypeCat) where
|
||||
structure RealLorentzTensor (d : ℕ) (X : Type) where
|
||||
/-- The color associated to each index of the tensor. -/
|
||||
color : X → RealLorentzTensor.Colors
|
||||
/-- The coordinate map for the tensor. -/
|
||||
coord : RealLorentzTensor.IndexValue d color → ℝ
|
||||
|
||||
namespace RealLorentzTensor
|
||||
open CategoryTheory
|
||||
open Matrix
|
||||
universe u1
|
||||
variable {d : ℕ} {X Y Z : FintypeCat.{0}}
|
||||
variable {d : ℕ} {X Y Z : Type}
|
||||
|
||||
/-!
|
||||
|
||||
## Some equivalences in FintypeCat
|
||||
## Some equivalences of types
|
||||
|
||||
These come in use casting Lorentz tensors.
|
||||
There is likely a better way to deal with these castings.
|
||||
|
||||
-/
|
||||
|
||||
/-- An equivalence between an `X` which is empty and `FintypeCat.of Empty`. -/
|
||||
def equivToEmpty (X : FintypeCat) [IsEmpty X] : X ≃ FintypeCat.of Empty :=
|
||||
Equiv.equivEmpty _
|
||||
|
||||
/-- An equivalence between an `X ⊕ Empty` and `X`. -/
|
||||
def equivToSumEmpty (X : FintypeCat) : FintypeCat.of (X ⊕ Empty) ≃ X :=
|
||||
Equiv.sumEmpty (↑X) Empty
|
||||
|
||||
/-- An equivalence from `Empty ⊕ PUnit.{1}` to `Empty ⊕ Σ _ : Fin 1, PUnit`. -/
|
||||
def equivPUnitToSigma :
|
||||
FintypeCat.of (Empty ⊕ PUnit.{1}) ≃ FintypeCat.of (Empty ⊕ Σ _ : Fin 1, PUnit) where
|
||||
(Empty ⊕ PUnit.{1}) ≃ (Empty ⊕ Σ _ : Fin 1, PUnit) where
|
||||
toFun x := match x with
|
||||
| Sum.inr x => Sum.inr ⟨0, x⟩
|
||||
invFun x := match x with
|
||||
|
|
@ -114,7 +103,7 @@ lemma τ_involutive : Function.Involutive τ := by
|
|||
cases x <;> rfl
|
||||
|
||||
/-- The color associated with an element of `x ∈ X` for a tensor `T`. -/
|
||||
def ch {X : FintypeCat} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
|
||||
def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
|
||||
|
||||
/-- An equivalence of `ColorsIndex` between that of a color and that of its dual. -/
|
||||
def dualColorsIndex {d : ℕ} {μ : RealLorentzTensor.Colors}:
|
||||
|
|
@ -157,7 +146,7 @@ lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
|
|||
-/
|
||||
|
||||
/-- An equivalence of Index values from an equality of color maps. -/
|
||||
def castIndexValue {X : FintypeCat} {T S : X → Colors} (h : T = S) :
|
||||
def castIndexValue {X : Type} {T S : X → Colors} (h : T = S) :
|
||||
IndexValue d T ≃ IndexValue d S where
|
||||
toFun i := (fun μ => castColorsIndex (congrFun h μ) (i μ))
|
||||
invFun i := (fun μ => (castColorsIndex (congrFun h μ)).symm (i μ))
|
||||
|
|
@ -221,8 +210,8 @@ def congrSetMap (f : X ≃ Y) (T : RealLorentzTensor d X) : RealLorentzTensor d
|
|||
lemma congrSetMap_trans (f : X ≃ Y) (g : Y ≃ Z) (T : RealLorentzTensor d X) :
|
||||
congrSetMap g (congrSetMap f T) = congrSetMap (f.trans g) T := by
|
||||
apply ext (by rfl)
|
||||
have h1 : (congrSetIndexValue d (f.trans g) T.color) = (congrSetIndexValue d f T.color).trans
|
||||
(congrSetIndexValue d g ((Equiv.piCongrLeft' (fun _ => Colors) f) T.color)) := by
|
||||
have h1 : congrSetIndexValue d (f.trans g) T.color = (congrSetIndexValue d f T.color).trans
|
||||
(congrSetIndexValue d g $ Equiv.piCongrLeft' (fun _ => Colors) f T.color) := by
|
||||
exact Equiv.coe_inj.mp rfl
|
||||
simp only [congrSetMap, Equiv.piCongrLeft'_apply, IndexValue, Equiv.symm_trans_apply, h1,
|
||||
Equiv.cast_refl, Equiv.coe_refl, CompTriple.comp_eq]
|
||||
|
|
@ -246,8 +235,7 @@ lemma congrSet_trans (f : X ≃ Y) (g : Y ≃ Z) :
|
|||
funext T
|
||||
exact congrSetMap_trans f g T
|
||||
|
||||
lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := by
|
||||
rfl
|
||||
lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := rfl
|
||||
|
||||
/-!
|
||||
|
||||
|
|
@ -255,13 +243,9 @@ lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := by
|
|||
|
||||
-/
|
||||
|
||||
/-- An equivalence through commuting sums between types casted from `FintypeCat.of`.-/
|
||||
def sumCommFintypeCat (X Y : FintypeCat) : FintypeCat.of (X ⊕ Y) ≃ FintypeCat.of (Y ⊕ X) :=
|
||||
Equiv.sumComm X Y
|
||||
|
||||
/-- The sum of two color maps. -/
|
||||
def sumElimIndexColor (Tc : X → Colors) (Sc : Y → Colors) :
|
||||
FintypeCat.of (X ⊕ Y) → Colors :=
|
||||
(X ⊕ Y) → Colors :=
|
||||
Sum.elim Tc Sc
|
||||
|
||||
/-- The symmetry property on `sumElimIndexColor`. -/
|
||||
|
|
@ -273,7 +257,7 @@ lemma sumElimIndexColor_symm (Tc : X → Colors) (Sc : Y → Colors) : sumElimIn
|
|||
|
||||
/-- The sum of two index values for different color maps. -/
|
||||
@[simp]
|
||||
def sumElimIndexValue {X Y : FintypeCat} {TX : X → Colors} {TY : Y → Colors}
|
||||
def sumElimIndexValue {X Y : Type} {TX : X → Colors} {TY : Y → Colors}
|
||||
(i : IndexValue d TX) (j : IndexValue d TY) :
|
||||
IndexValue d (sumElimIndexColor TX TY) :=
|
||||
fun c => match c with
|
||||
|
|
@ -289,24 +273,23 @@ def inrIndexValue {Tc : X → Colors} {Sc : Y → Colors}
|
|||
(i : IndexValue d (sumElimIndexColor Tc Sc)) :
|
||||
IndexValue d Sc := fun y => i (Sum.inr y)
|
||||
|
||||
/-- An equivalence between index values formed by commuting sums.-/
|
||||
def sumCommIndexValue {X Y : FintypeCat} (Tc : X → Colors) (Sc : Y → Colors) :
|
||||
/-- An equivalence between index values formed by commuting sums. -/
|
||||
def sumCommIndexValue {X Y : Type} (Tc : X → Colors) (Sc : Y → Colors) :
|
||||
IndexValue d (sumElimIndexColor Tc Sc) ≃ IndexValue d (sumElimIndexColor Sc Tc) :=
|
||||
(congrSetIndexValue d (sumCommFintypeCat X Y) (sumElimIndexColor Tc Sc)).trans
|
||||
(castIndexValue ((sumElimIndexColor_symm Sc Tc).symm))
|
||||
(congrSetIndexValue d (Equiv.sumComm X Y) (sumElimIndexColor Tc Sc)).trans
|
||||
(castIndexValue (sumElimIndexColor_symm Sc Tc).symm)
|
||||
|
||||
lemma sumCommIndexValue_inlIndexValue {X Y : FintypeCat} {Tc : X → Colors} {Sc : Y → Colors}
|
||||
(i : IndexValue d (sumElimIndexColor Tc Sc)) :
|
||||
lemma sumCommIndexValue_inlIndexValue {X Y : Type} {Tc : X → Colors} {Sc : Y → Colors}
|
||||
(i : IndexValue d <| sumElimIndexColor Tc Sc) :
|
||||
inlIndexValue (sumCommIndexValue Tc Sc i) = inrIndexValue i := rfl
|
||||
|
||||
lemma sumCommIndexValue_inrIndexValue {X Y : FintypeCat} {Tc : X → Colors} {Sc : Y → Colors}
|
||||
(i : IndexValue d (sumElimIndexColor Tc Sc)) :
|
||||
lemma sumCommIndexValue_inrIndexValue {X Y : Type} {Tc : X → Colors} {Sc : Y → Colors}
|
||||
(i : IndexValue d <| sumElimIndexColor Tc Sc) :
|
||||
inrIndexValue (sumCommIndexValue Tc Sc i) = inlIndexValue i := rfl
|
||||
|
||||
/-- Equivalence between sets of `RealLorentzTensor` formed by commuting sums. -/
|
||||
@[simps!]
|
||||
def sumComm :
|
||||
RealLorentzTensor d (FintypeCat.of (X ⊕ Y)) ≃ RealLorentzTensor d (FintypeCat.of (Y ⊕ X)) :=
|
||||
def sumComm : RealLorentzTensor d (X ⊕ Y) ≃ RealLorentzTensor d (Y ⊕ X) :=
|
||||
congrSet (Equiv.sumComm X Y)
|
||||
|
||||
/-!
|
||||
|
|
@ -318,15 +301,15 @@ To define contraction and multiplication of Lorentz tensors we need to mark indi
|
|||
-/
|
||||
|
||||
/-- A `RealLorentzTensor` with `n` marked indices. -/
|
||||
def Marked (d : ℕ) (X : FintypeCat) (n : ℕ) : Type :=
|
||||
RealLorentzTensor d (FintypeCat.of (X ⊕ Σ _ : Fin n, PUnit))
|
||||
def Marked (d : ℕ) (X : Type) (n : ℕ) : Type :=
|
||||
RealLorentzTensor d (X ⊕ Σ _ : Fin n, PUnit)
|
||||
|
||||
namespace Marked
|
||||
|
||||
variable {n m : ℕ}
|
||||
|
||||
/-- The marked point. -/
|
||||
def markedPoint (X : FintypeCat) (i : Fin n) : FintypeCat.of (X ⊕ Σ _ : Fin n, PUnit) :=
|
||||
def markedPoint (X : Type) (i : Fin n) : (X ⊕ Σ _ : Fin n, PUnit) :=
|
||||
Sum.inr ⟨i, PUnit.unit⟩
|
||||
|
||||
/-- The colors of unmarked indices. -/
|
||||
|
|
@ -334,7 +317,7 @@ def unmarkedColor (T : Marked d X n) : X → Colors :=
|
|||
T.color ∘ Sum.inl
|
||||
|
||||
/-- The colors of marked indices. -/
|
||||
def markedColor (T : Marked d X n) : FintypeCat.of (Σ _ : Fin n, PUnit) → Colors :=
|
||||
def markedColor (T : Marked d X n) : (Σ _ : Fin n, PUnit) → Colors :=
|
||||
T.color ∘ Sum.inr
|
||||
|
||||
/-- The index values restricted to unmarked indices. -/
|
||||
|
|
@ -357,15 +340,15 @@ def oneMarkedIndexValue (T : Marked d X 1) (x : ColorsIndex d (T.color (markedPo
|
|||
|
||||
/-- Contruction of marked index values for the case of 2 marked index. -/
|
||||
def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPoint X 0)))
|
||||
(y : ColorsIndex d (T.color (markedPoint X 1))) :
|
||||
(y : ColorsIndex d <| T.color <| markedPoint X 1) :
|
||||
T.MarkedIndexValue := fun i =>
|
||||
match i with
|
||||
| ⟨0, PUnit.unit⟩ => x
|
||||
| ⟨1, PUnit.unit⟩ => y
|
||||
|
||||
/-- An equivalence of types used to turn the first marked index into an unmarked index. -/
|
||||
def unmarkFirstSet (X : FintypeCat) (n : ℕ) : FintypeCat.of (X ⊕ Σ _ : Fin n.succ, PUnit) ≃
|
||||
FintypeCat.of ((X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit) where
|
||||
def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Σ _ : Fin n.succ, PUnit) ≃
|
||||
((X ⊕ PUnit) ⊕ Σ _ : Fin n, PUnit) where
|
||||
toFun x := match x with
|
||||
| Sum.inl x => Sum.inl (Sum.inl x)
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => Sum.inl (Sum.inr PUnit.unit)
|
||||
|
|
@ -384,7 +367,7 @@ def unmarkFirstSet (X : FintypeCat) (n : ℕ) : FintypeCat.of (X ⊕ Σ _ : Fin
|
|||
| Sum.inr ⟨⟨i, h⟩, PUnit.unit⟩ => rfl
|
||||
|
||||
/-- Unmark the first marked index of a marked thensor. -/
|
||||
def unmarkFirst {X : FintypeCat} : Marked d X n.succ ≃ Marked d (FintypeCat.of (X ⊕ PUnit)) n :=
|
||||
def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ PUnit) n :=
|
||||
congrSet (unmarkFirstSet X n)
|
||||
|
||||
end Marked
|
||||
|
|
@ -400,23 +383,23 @@ open Marked
|
|||
is dual to the others. The contraction is done via
|
||||
`φ^μ ψ_μ = φ^0 ψ_0 + φ^1 ψ_1 + ...`. -/
|
||||
@[simps!]
|
||||
def mul {X Y : FintypeCat} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor ⟨0, PUnit.unit⟩ = τ (S.markedColor ⟨0, PUnit.unit⟩)) :
|
||||
RealLorentzTensor d (FintypeCat.of (X ⊕ Y)) where
|
||||
RealLorentzTensor d (X ⊕ Y) where
|
||||
color := sumElimIndexColor T.unmarkedColor S.unmarkedColor
|
||||
coord := fun i => ∑ x,
|
||||
T.coord (castIndexValue T.sumElimIndexColor_of_marked
|
||||
(sumElimIndexValue (inlIndexValue i) (T.oneMarkedIndexValue x))) *
|
||||
T.coord (castIndexValue T.sumElimIndexColor_of_marked $
|
||||
sumElimIndexValue (inlIndexValue i) (T.oneMarkedIndexValue x)) *
|
||||
S.coord (castIndexValue S.sumElimIndexColor_of_marked $
|
||||
sumElimIndexValue (inrIndexValue i) (S.oneMarkedIndexValue $ congrColorsDual h x))
|
||||
|
||||
/-- Multiplication is well behaved with regard to swapping tensors. -/
|
||||
lemma sumComm_mul {X Y : FintypeCat} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
lemma sumComm_mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
||||
(h : T.markedColor ⟨0, PUnit.unit⟩ = τ (S.markedColor ⟨0, PUnit.unit⟩)) :
|
||||
sumComm (mul T S h) = mul S T (color_eq_dual_symm h) := by
|
||||
refine ext' (sumElimIndexColor_symm S.unmarkedColor T.unmarkedColor).symm ?_
|
||||
change (mul T S h).coord ∘
|
||||
(congrSetIndexValue d (sumCommFintypeCat X Y) (mul T S h).color).symm = _
|
||||
(congrSetIndexValue d (Equiv.sumComm X Y) (mul T S h).color).symm = _
|
||||
rw [Equiv.comp_symm_eq]
|
||||
funext i
|
||||
simp only [mul_coord, IndexValue, mul_color, Function.comp_apply, sumComm_apply_color]
|
||||
|
|
@ -426,7 +409,7 @@ lemma sumComm_mul {X Y : FintypeCat} (T : Marked d X 1) (S : Marked d Y 1)
|
|||
rw [mul_comm]
|
||||
repeat apply congrArg
|
||||
rw [← congrColorsDual_symm h]
|
||||
exact (Equiv.apply_eq_iff_eq_symm_apply (congrColorsDual h)).mp rfl
|
||||
exact (Equiv.apply_eq_iff_eq_symm_apply <| congrColorsDual h).mp rfl
|
||||
|
||||
/-! TODO: Following the ethos of modular operads, prove properties of multiplication. -/
|
||||
|
||||
|
|
@ -438,7 +421,7 @@ lemma sumComm_mul {X Y : FintypeCat} (T : Marked d X 1) (S : Marked d Y 1)
|
|||
-/
|
||||
|
||||
/-- The contraction of the marked indices in a tensor with two marked indices. -/
|
||||
def contr {X : FintypeCat} (T : Marked d X 2)
|
||||
def contr {X : Type} (T : Marked d X 2)
|
||||
(h : T.markedColor ⟨0, PUnit.unit⟩ = τ (T.markedColor ⟨1, PUnit.unit⟩)) :
|
||||
RealLorentzTensor d X where
|
||||
color := T.unmarkedColor
|
||||
|
|
@ -460,7 +443,7 @@ action of the Lorentz group. They are provided for constructive purposes.
|
|||
-/
|
||||
|
||||
/-- A 0-tensor from a real number. -/
|
||||
def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d (FintypeCat.of Empty) where
|
||||
def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun _ => r
|
||||
|
||||
|
|
@ -468,23 +451,23 @@ def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d (FintypeCat.of Empty) where
|
|||
|
||||
Note: This is not the same as rising indices on `ofVecDown`. -/
|
||||
def ofVecUp {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Marked d (FintypeCat.of Empty) 1 where
|
||||
Marked d Empty 1 where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun i => v (i (Sum.inr ⟨0, PUnit.unit⟩))
|
||||
coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
|
||||
|
||||
/-- A marked 1-tensor with a single down index constructed from a vector.
|
||||
|
||||
Note: This is not the same as lowering indices on `ofVecUp`. -/
|
||||
def ofVecDown {d : ℕ} (v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
Marked d (FintypeCat.of Empty) 1 where
|
||||
Marked d Empty 1 where
|
||||
color := fun _ => Colors.down
|
||||
coord := fun i => v (i (Sum.inr ⟨0, PUnit.unit⟩))
|
||||
coord := fun i => v <| i <| Sum.inr <| ⟨0, PUnit.unit⟩
|
||||
|
||||
/-- A tensor with two up indices constructed from a matrix.
|
||||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d (FintypeCat.of Empty) 2 where
|
||||
Marked d Empty 2 where
|
||||
color := fun _ => Colors.up
|
||||
coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
|
||||
|
|
@ -492,7 +475,7 @@ def ofMatUpUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
|||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d (FintypeCat.of Empty) 2 where
|
||||
Marked d Empty 2 where
|
||||
color := fun _ => Colors.down
|
||||
coord := fun i => m (i (Sum.inr ⟨0, PUnit.unit⟩)) (i (Sum.inr ⟨1, PUnit.unit⟩))
|
||||
|
||||
|
|
@ -501,7 +484,7 @@ def ofMatDownDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
|||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
@[simps!]
|
||||
def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d (FintypeCat.of Empty) 2 where
|
||||
Marked d Empty 2 where
|
||||
color := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => Colors.up
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => Colors.down
|
||||
|
|
@ -511,7 +494,7 @@ def ofMatUpDown {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
|||
|
||||
Note: This is not the same as rising or lowering indices on other `ofMat...`. -/
|
||||
def ofMatDownUp {d : ℕ} (m : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
|
||||
Marked d (FintypeCat.of Empty) 2 where
|
||||
Marked d Empty 2 where
|
||||
color := fun i => match i with
|
||||
| Sum.inr ⟨0, PUnit.unit⟩ => Colors.down
|
||||
| Sum.inr ⟨1, PUnit.unit⟩ => Colors.up
|
||||
|
|
@ -542,7 +525,7 @@ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
|
|||
/-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
|
||||
@[simp]
|
||||
lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet (@equivToEmpty (FintypeCat.of (Empty ⊕ Empty)) instIsEmptySum)
|
||||
congrSet (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
|
||||
(mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
|
|
@ -553,8 +536,8 @@ lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d
|
|||
/-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
|
||||
@[simp]
|
||||
lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet (@equivToEmpty (FintypeCat.of (Empty ⊕ Empty)) instIsEmptySum)
|
||||
(mul (ofVecDown v₁) (ofVecUp v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
|
||||
congrSet (Equiv.equivEmpty (Empty ⊕ Empty))
|
||||
(mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
exact Empty.elim i
|
||||
|
|
@ -563,8 +546,8 @@ lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d
|
|||
|
||||
lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
(v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet ((equivToSumEmpty (FintypeCat.of (Empty ⊕ PUnit.{1}))).trans equivPUnitToSigma)
|
||||
(mul (unmarkFirst (ofMatUpDown M)) (ofVecUp v) (by rfl)) = ofVecUp (M *ᵥ v) := by
|
||||
congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
|
||||
(mul (unmarkFirst $ ofMatUpDown M) (ofVecUp v) rfl) = ofVecUp (M *ᵥ v) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
|
||||
|
|
@ -575,8 +558,8 @@ lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d)
|
|||
|
||||
lemma mul_ofMatDownUp_ofVecDown_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
|
||||
(v : Fin 1 ⊕ Fin d → ℝ) :
|
||||
congrSet ((equivToSumEmpty (FintypeCat.of (Empty ⊕ PUnit.{1}))).trans equivPUnitToSigma)
|
||||
(mul (unmarkFirst (ofMatDownUp M)) (ofVecDown v) (by rfl)) = ofVecDown (M *ᵥ v) := by
|
||||
congrSet ((Equiv.sumEmpty (Empty ⊕ PUnit.{1}) Empty).trans equivPUnitToSigma)
|
||||
(mul (unmarkFirst $ ofMatDownUp M) (ofVecDown v) rfl) = ofVecDown (M *ᵥ v) := by
|
||||
refine ext' ?_ ?_
|
||||
· funext i
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, congrSet_apply_color, mul_color, Equiv.symm_symm]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue