DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #247 from HEPLean/Add_more_Docs

Browse source 
docs: Adding some documentation for lemmas
This commit is contained in:
Joseph Tooby-Smith 2024-11-28 06:29:24 +00:00 • committed by GitHub
commit 8fce521e3f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
24 changed files with 338 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

41
HepLean/AnomalyCancellation/PureU1/Basic.lean
View file

@ -70,15 +70,15 @@ def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := Tri
def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).Charges) :=
(accCubeTriLinSymm).toCubic
/-- The cubic ACC for the pure-`U(1)` anomaly equations is equal to the sum of the cubed
charges. -/
lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).Charges) :
accCube n S = ∑ i : Fin n, S i ^ 3:= by
rw [accCube, TriLinearSymm.toCubic]
change accCubeTriLinSymm S S S = _
rw [accCubeTriLinSymm]
simp only [PureU1Charges_numberCharges, TriLinearSymm.mk₃_toFun_apply_apply]
apply Finset.sum_congr
· rfl
· exact fun x _ => Eq.symm (pow_three' (S x))
exact Finset.sum_congr rfl fun x _ => Eq.symm (pow_three' (S x))
end PureU1
@ -105,18 +105,21 @@ def pureU1EqCharges {n m : ℕ} (h : n = m) :
open BigOperators
lemma pureU1_linear {n : ℕ} (S : (PureU1 n.succ).LinSols) :
/-- A solution to the pure U(1) accs satisfies the linear ACCs. -/
lemma pureU1_linear {n : ℕ} (S : (PureU1 n).LinSols) :
∑ i, S.val i = 0 := by
have hS := S.linearSol
simp only [succ_eq_add_one, PureU1_numberLinear, PureU1_linearACCs] at hS
exact hS 0
lemma pureU1_cube {n : ℕ} (S : (PureU1 n.succ).Sols) :
/-- A solution to the pure U(1) accs satisfies the cubic ACCs. -/
lemma pureU1_cube {n : ℕ} (S : (PureU1 n).Sols) :
∑ i, (S.val i) ^ 3 = 0 := by
have hS := S.cubicSol
erw [PureU1.accCube_explicit] at hS
exact hS
rw [← PureU1.accCube_explicit]
exact S.cubicSol
/-- The last charge of a solution to the linear ACCs is equal to the negation of the sum
of the other charges. -/
lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
S.val (Fin.last n) = - ∑ i : Fin n, S.val i.castSucc := by
have hS := pureU1_linear S
@ -124,25 +127,23 @@ lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
rw [Fin.sum_univ_castSucc] at hS
linear_combination hS
/-- Two solutions to the Linear ACCs for `n.succ` areq equal if their first `n` charges are
equal. -/
lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
(h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T := by
apply ACCSystemLinear.LinSols.ext
funext i
by_cases hi : i ≠ Fin.last n
· have hiCast : ∃ j : Fin n, j.castSucc = i := by
exact Fin.exists_castSucc_eq.mpr hi
obtain ⟨j, hj⟩ := hiCast
rw [← hj]
rcases Fin.eq_castSucc_or_eq_last i with hi | hi
· obtain ⟨j, hj⟩ := hi
subst hj
exact h j
· simp only [succ_eq_add_one, PureU1_numberCharges, ne_eq, Decidable.not_not] at hi
rw [hi, pureU1_last, pureU1_last]
simp only [neg_inj]
apply Finset.sum_congr
· rfl
· exact fun j _ => h j
· rw [hi, pureU1_last, pureU1_last]
exact neg_inj.mpr (Finset.sum_congr rfl fun j _ => h j)
namespace PureU1
/-- The `j`th charge of a sum of pure-`U(1)` charges is equal to the sum of
their `j`th charges. -/
lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
(∑ i : Fin k, (f i)) j = ∑ i : Fin k, (f i) j := by
induction k
@ -153,6 +154,8 @@ lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
erw [← hlt]
rfl
/-- The `j`th charge of a sum of solutions to the linear ACC is equal to the sum of
their `j`th charges. -/
lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
(∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by
induction k

1
HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
View file

@ -124,6 +124,7 @@ def asBasis : Basis (Fin n) ℚ ((PureU1 n.succ).LinSols) where
instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) :=
Module.Finite.of_basis asBasis
/-- The module of solutions to the linear pure-U(1) acc has rank equal to `n`. -/
lemma finrank_AnomalyFreeLinear :
Module.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by
have h := Module.mk_finrank_eq_card_basis (@asBasis n)

3
HepLean/AnomalyCancellation/SM/NoGrav/Basic.lean
View file

@ -36,16 +36,19 @@ namespace SMNoGrav
variable {n : ℕ}
/-- The charges in `(SMNoGrav n).LinSols` satisfy the `SU(2)` anomaly-equation. -/
lemma SU2Sol (S : (SMNoGrav n).LinSols) : accSU2 S.val = 0 := by
have hS := S.linearSol
simp only [SMNoGrav_numberLinear, SMNoGrav_linearACCs, Fin.isValue] at hS
exact hS 0
/-- The charges in `(SMNoGrav n).LinSols` satisfy the `SU(3)` anomaly-equation. -/
lemma SU3Sol (S : (SMNoGrav n).LinSols) : accSU3 S.val = 0 := by
have hS := S.linearSol
simp only [SMNoGrav_numberLinear, SMNoGrav_linearACCs, Fin.isValue] at hS
exact hS 1
/-- The charges in `(SMNoGrav n).Sols` satisfy the cubic anomaly-equation. -/
lemma cubeSol (S : (SMNoGrav n).Sols) : accCube S.val = 0 := by
exact S.cubicSol

8
HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
View file

@ -25,6 +25,8 @@ open SMCharges
open SMACCs
open BigOperators
/-- For a set of 1 family SM charges satisfying all ACCs except the gravitational,
the charge of `Q` is zero if and only if `E` is zero. -/
lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
E S.val (0 : Fin 1) = 0 := by
let S' := linearParameters.bijection.symm S.1.1
@ -34,6 +36,8 @@ lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
rw [← hS'] at hC
exact Iff.intro (fun hQ => S'.cubic_zero_Q'_zero hC hQ) (fun hE => S'.cubic_zero_E'_zero hC hE)
/-- For a set of 1-family SM charges satisfying all ACCs except the gravitational,
if the `Q` charge is zero then the charges satisfy the gravitional ACCs. -/
lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
accGrav S.val = 0 := by
rw [accGrav]
@ -48,6 +52,8 @@ lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
simp_all
linear_combination 3 * h2
/-- For a set of 1-family SM charges satisfying all ACCs except the gravitational,
if the `Q` charge is not zero then the charges satisfy the gravitional ACCs. -/
lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0) :
accGrav S.val = 0 := by
have hE := E_zero_iff_Q_zero.mpr.mt hQ
@ -59,7 +65,7 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0
rw [← hS'] at hC ⊢
exact S'.grav_of_cubic hC
/-- Any solution to the ACCs without gravity satisfies the gravitational ACC. -/
/-- Any solution to the 1-family ACCs without gravity satisfies the gravitational ACC. -/
theorem accGravSatisfied {S : (SMNoGrav 1).Sols} :
accGrav S.val = 0 := by
by_cases hQ : Q S.val (0 : Fin 1)= 0

21
HepLean/AnomalyCancellation/SM/Permutations.lean
View file

@ -7,6 +7,7 @@ import HepLean.AnomalyCancellation.SM.Basic
import Mathlib.Tactic.Polyrith
import Mathlib.RepresentationTheory.Basic
/-!
# Permutations of SM with no RHN.
We define the group of permutations for the SM charges with no RHN.
@ -63,10 +64,14 @@ def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMCharges n).Charge
erw [toSMSpecies_toSpecies_inv]
rfl
/-- The species chages of a set of charges acted on by a family permutation is the permutation
of those species charges with the corresponding part of the family permutation. -/
lemma repCharges_toSpecies (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
erw [toSMSpecies_toSpecies_inv]
/-- The sum over every charge in any species to some power `m` is invariant under the group
action. -/
lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
@ -74,31 +79,35 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Cha
exact Fintype.sum_equiv (f⁻¹ j) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) x)
(fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl)
/-- The gravitional anomaly equations is invariant under family permutations. -/
lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accGrav (repCharges f S) = accGrav S :=
accGrav_ext
(by simpa using toSpecies_sum_invariant 1 f S)
accGrav (repCharges f S) = accGrav S := accGrav_ext
(by simpa using toSpecies_sum_invariant 1 f S)
/-- The `SU(2)` anomaly equation is invariant under family permutations. -/
lemma accSU2_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accSU2 (repCharges f S) = accSU2 S :=
accSU2_ext
(by simpa using toSpecies_sum_invariant 1 f S)
accSU2 (repCharges f S) = accSU2 S := accSU2_ext
(by simpa using toSpecies_sum_invariant 1 f S)
/-- The `SU(3)` anomaly equation is invariant under family permutations. -/
lemma accSU3_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accSU3 (repCharges f S) = accSU3 S :=
accSU3_ext
(by simpa using toSpecies_sum_invariant 1 f S)
/-- The `Y²` anomaly equation is invariant under family permutations. -/
lemma accYY_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accYY (repCharges f S) = accYY S :=
accYY_ext
(by simpa using toSpecies_sum_invariant 1 f S)
/-- The quadratic anomaly equation is invariant under family permutations. -/
lemma accQuad_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accQuad (repCharges f S) = accQuad S :=
accQuad_ext
(toSpecies_sum_invariant 2 f S)
/-- The cubic anomaly equation is invariant under family permutations. -/
lemma accCube_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accCube (repCharges f S) = accCube S :=
accCube_ext (fun j => toSpecies_sum_invariant 3 f S j)

31
HepLean/FlavorPhysics/CKMMatrix/Basic.lean
View file

@ -29,6 +29,7 @@ leading diagonal. -/
def phaseShiftMatrix (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
![![cexp (I * a), 0, 0], ![0, cexp (I * b), 0], ![0, 0, cexp (I * c)]]
/-- The phase shift matrix for zero-phases is the identity. -/
lemma phaseShiftMatrix_one : phaseShiftMatrix 0 0 0 = 1 := by
ext i j
fin_cases i <;> fin_cases j
@ -41,6 +42,8 @@ lemma phaseShiftMatrix_one : phaseShiftMatrix 0 0 0 = 1 := by
Fin.isValue, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, head_cons, empty_val',
cons_val_fin_one, head_fin_const, one_apply_eq]
/-- The conjugate transpose of the phase shift matrix is the phase-shift matrix
with negated phases. -/
lemma phaseShiftMatrix_star (a b c : ℝ) :
(phaseShiftMatrix a b c)ᴴ = phaseShiftMatrix (- a) (- b) (- c) := by
funext i j
@ -53,6 +56,8 @@ lemma phaseShiftMatrix_star (a b c : ℝ) :
· rfl
· rfl
/-- The multiple of two phase shift matrices is equal to the phase shift matrix with
added phases. -/
lemma phaseShiftMatrix_mul (a b c d e f : ℝ) :
phaseShiftMatrix a b c * phaseShiftMatrix d e f = phaseShiftMatrix (a + d) (b + e) (c + f) := by
ext i j
@ -76,12 +81,17 @@ def phaseShift (a b c : ℝ) : unitaryGroup (Fin 3) ℂ :=
rw [phaseShiftMatrix_star, phaseShiftMatrix_mul, ← phaseShiftMatrix_one]
simp only [phaseShiftMatrix, add_neg_cancel, ofReal_zero, mul_zero, exp_zero]⟩
/-- The underlying matrix of the phase-shift element of the unitary group is the
phase-shift matrix. -/
lemma phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMatrix a b c := rfl
/-- The equivalence relation between CKM matrices. -/
/-- The relation on unitary matrices (CKM matrices) satisfied if two unitary matrices
are related by phase shifts of quarks. -/
def PhaseShiftRelation (U V : unitaryGroup (Fin 3) ℂ) : Prop :=
∃ a b c e f g, U = phaseShift a b c * V * phaseShift e f g
/-- The relation `PhaseShiftRelation` is reflective. -/
lemma phaseShiftRelation_refl (U : unitaryGroup (Fin 3) ℂ) : PhaseShiftRelation U U := by
use 0, 0, 0, 0, 0, 0
rw [Subtype.ext_iff_val]
@ -89,6 +99,7 @@ lemma phaseShiftRelation_refl (U : unitaryGroup (Fin 3) ℂ) : PhaseShiftRelatio
rw [phaseShiftMatrix_one]
simp only [one_mul, mul_one]
/-- The relation `PhaseShiftRelation` is symmetric. -/
lemma phaseShiftRelation_symm {U V : unitaryGroup (Fin 3) ℂ} :
PhaseShiftRelation U V → PhaseShiftRelation V U := by
intro h
@ -103,6 +114,7 @@ lemma phaseShiftRelation_symm {U V : unitaryGroup (Fin 3) ℂ} :
simp only [phaseShiftMatrix_mul, neg_add_cancel, phaseShiftMatrix_one, one_mul, add_neg_cancel,
mul_one]
/-- The relation `PhaseShiftRelation` is transitive. -/
lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
PhaseShiftRelation U V → PhaseShiftRelation V W → PhaseShiftRelation U W := by
intro hUV hVW
@ -114,6 +126,7 @@ lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
rw [mul_assoc, mul_assoc, phaseShiftMatrix_mul, ← mul_assoc, ← mul_assoc, phaseShiftMatrix_mul,
add_comm k e, add_comm l f, add_comm m g]
/-- The relation `PhaseShiftRelation` is an equivalence relation. -/
lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
refl := phaseShiftRelation_refl
symm := phaseShiftRelation_symm
@ -122,6 +135,7 @@ lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
/-- The type of CKM matrices. -/
def CKMMatrix : Type := unitaryGroup (Fin 3) ℂ
/-- Two CKM matrices are equal if their underlying unitary matrices are equal. -/
lemma CKMMatrix_ext {U V : CKMMatrix} (h : U.val = V.val) : U = V := by
cases U
cases V
@ -164,12 +178,15 @@ def phaseShiftApply (V : CKMMatrix) (a b c d e f : ℝ) : CKMMatrix :=
phaseShift a b c * ↑V * phaseShift d e f
namespace phaseShiftApply
/-- A CKM matrix is equivalent to a phase-shift of itself. -/
lemma equiv (V : CKMMatrix) (a b c d e f : ℝ) :
V ≈ phaseShiftApply V a b c d e f := by
symm
use a, b, c, d, e, f
rfl
/-- The `ud` component of the CKM matrix obtained after applying a phase shift. -/
lemma ud (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 0 0 = cexp (a * I + d * I) * V.1 0 0 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -182,6 +199,7 @@ lemma ud (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `us` component of the CKM matrix obtained after applying a phase shift. -/
lemma us (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 0 1 = cexp (a * I + e * I) * V.1 0 1 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -193,6 +211,7 @@ lemma us (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `ub` component of the CKM matrix obtained after applying a phase shift. -/
lemma ub (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 0 2 = cexp (a * I + f * I) * V.1 0 2 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -204,6 +223,7 @@ lemma ub (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `cd` component of the CKM matrix obtained after applying a phase shift. -/
lemma cd (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 1 0= cexp (b * I + d * I) * V.1 1 0 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -216,6 +236,7 @@ lemma cd (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `cs` component of the CKM matrix obtained after applying a phase shift. -/
lemma cs (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 1 1 = cexp (b * I + e * I) * V.1 1 1 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -227,6 +248,7 @@ lemma cs (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `cb` component of the CKM matrix obtained after applying a phase shift. -/
lemma cb (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 1 2 = cexp (b * I + f * I) * V.1 1 2 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -238,6 +260,7 @@ lemma cb (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `td` component of the CKM matrix obtained after applying a phase shift. -/
lemma td (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 2 0= cexp (c * I + d * I) * V.1 2 0 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -251,6 +274,7 @@ lemma td (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `ts` component of the CKM matrix obtained after applying a phase shift. -/
lemma ts (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 2 1 = cexp (c * I + e * I) * V.1 2 1 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -263,6 +287,7 @@ lemma ts (V : CKMMatrix) (a b c d e f : ℝ) :
rw [exp_add]
ring_nf
/-- The `tb` component of the CKM matrix obtained after applying a phase shift. -/
lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
(phaseShiftApply V a b c d e f).1 2 2 = cexp (c * I + f * I) * V.1 2 2 := by
simp only [Fin.isValue, phaseShiftApply_coe]
@ -281,6 +306,8 @@ end phaseShiftApply
@[simp]
def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := Complex.abs (V i j)
/-- If two CKM matrices are equivalent (under phase shifts), then their absolute values
are the same. -/
lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
VAbs' V i j = VAbs' U i j := by
simp only [VAbs']
@ -396,6 +423,8 @@ def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb
/-- The ratio of the `cs` and `cb` elements of a CKM matrix. -/
scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V
/-- Multiplicying the ratio of the `cs` by `cb` element of a CKM matriz by the `cb` element
returns the `cs` element, as long as the `cb` element is non-zero. -/
lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0) : [V]cs = Rcscb V * [V]cb := by
rw [Rcscb]
exact (div_mul_cancel₀ [V]cs h).symm

3
HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
View file

@ -28,6 +28,7 @@ namespace Invariant
def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
[V]us * [V]cb * conj [V]ub * conj [V]cs
/-- The complex jarlskog invariant is equal for equivalent CKM matrices. -/
lemma jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) :
jarlskogℂCKM V = jarlskogℂCKM U := by
obtain ⟨a, b, c, e, f, g, h⟩ := h
@ -50,7 +51,7 @@ def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ :=
Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv
/-- An invariant for CKM mtrices corresponding to the square of the absolute values
of the `us`, `ub` and `cb` elements multipled together divied by `(VudAbs V ^ 2 + VusAbs V ^2)` .
of the `us`, `ub` and `cb` elements multipled together divided by `(VudAbs V ^ 2 + VusAbs V ^2)`.
-/
def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ :=
VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2)

11
HepLean/FlavorPhysics/CKMMatrix/Relations.lean
View file

@ -23,6 +23,7 @@ open ComplexConjugate
section rows
/-- The absolute value squared of any rwo of a CKM matrix is `1`, in terms of `Vabs`. -/
lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
(VAbs i 0 V) ^ 2 + (VAbs i 1 V) ^ 2 + (VAbs i 2 V) ^ 2 = 1 := by
obtain ⟨V, hV⟩ := Quot.exists_rep V
@ -37,25 +38,31 @@ lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
rw [← ofReal_inj]
simpa using ht
/-- The absolute value squared of the first rwo of a CKM matrix is `1`, in terms of `abs`. -/
lemma fst_row_normalized_abs (V : CKMMatrix) : abs [V]ud ^ 2 + abs [V]us ^ 2 + abs [V]ub ^ 2 = 1 :=
VAbs_sum_sq_row_eq_one ⟦V⟧ 0
/-- The absolute value squared of the second rwo of a CKM matrix is `1`, in terms of `abs`. -/
lemma snd_row_normalized_abs (V : CKMMatrix) : abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 :=
VAbs_sum_sq_row_eq_one ⟦V⟧ 1
/-- The absolute value squared of the thid rwo of a CKM matrix is `1`, in terms of `abs`. -/
lemma thd_row_normalized_abs (V : CKMMatrix) : abs [V]td ^ 2 + abs [V]ts ^ 2 + abs [V]tb ^ 2 = 1 :=
VAbs_sum_sq_row_eq_one ⟦V⟧ 2
/-- The absolute value squared of the first rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
lemma fst_row_normalized_normSq (V : CKMMatrix) :
normSq [V]ud + normSq [V]us + normSq [V]ub = 1 := by
repeat rw [← Complex.sq_abs]
exact V.fst_row_normalized_abs
/-- The absolute value squared of the second rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
lemma snd_row_normalized_normSq (V : CKMMatrix) :
normSq [V]cd + normSq [V]cs + normSq [V]cb = 1 := by
repeat rw [← Complex.sq_abs]
exact V.snd_row_normalized_abs
/-- The absolute value squared of the third rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
lemma thd_row_normalized_normSq (V : CKMMatrix) :
normSq [V]td + normSq [V]ts + normSq [V]tb = 1 := by
repeat rw [← Complex.sq_abs]
@ -63,10 +70,10 @@ lemma thd_row_normalized_normSq (V : CKMMatrix) :
lemma normSq_Vud_plus_normSq_Vus (V : CKMMatrix) :
normSq [V]ud + normSq [V]us = 1 - normSq [V]ub := by
linear_combination (fst_row_normalized_normSq V)
linear_combination fst_row_normalized_normSq V
lemma VudAbs_sq_add_VusAbs_sq : VudAbs V ^ 2 + VusAbs V ^2 = 1 - VubAbs V ^2 := by
linear_combination (VAbs_sum_sq_row_eq_one V 0)
linear_combination VAbs_sum_sq_row_eq_one V 0
lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
[V]ud ≠ 0 ∨ [V]us ≠ 0 ↔ abs [V]ub ≠ 1 := by

96
HepLean/FlavorPhysics/CKMMatrix/Rows.lean
View file

@ -42,6 +42,7 @@ def tRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]td, [V]ts, [V]tb]
/-- The `t`th row of the CKM matrix. -/
scoped[CKMMatrix] notation (name := t_row) "[" V "]t" => tRow V
/-- The up-quark row of the CKM matrix is normalized to `1`. -/
lemma uRow_normalized (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]u = 1 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
@ -52,6 +53,7 @@ lemma uRow_normalized (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]u = 1 := by
rw [mul_comm (V.1 0 0) _, mul_comm (V.1 0 1) _, mul_comm (V.1 0 2) _] at ht
exact ht
/-- The charm-quark row of the CKM matrix is normalized to `1`. -/
lemma cRow_normalized (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]c = 1 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
@ -62,46 +64,7 @@ lemma cRow_normalized (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]c = 1 := by
rw [mul_comm (V.1 1 0) _, mul_comm (V.1 1 1) _, mul_comm (V.1 1 2) _] at ht
exact ht
lemma uRow_cRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]c = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 1) 0
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
one_ne_zero, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
lemma uRow_tRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]t = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 2) 0
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
lemma cRow_uRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]u = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 0) 1
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
zero_ne_one, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
lemma cRow_tRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]t = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 2) 1
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
/-- The top-quark row of the CKM matrix is normalized to `1`. -/
lemma tRow_normalized (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]t = 1 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
@ -112,6 +75,51 @@ lemma tRow_normalized (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]t = 1 := by
rw [mul_comm (V.1 2 0) _, mul_comm (V.1 2 1) _, mul_comm (V.1 2 2) _] at ht
exact ht
/-- The up-quark row of the CKM matrix is orthogonal to the charm-quark row. -/
lemma uRow_cRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]c = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 1) 0
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
one_ne_zero, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
/-- The up-quark row of the CKM matrix is orthogonal to the top-quark row. -/
lemma uRow_tRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]t = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 2) 0
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
/-- The charm-quark row of the CKM matrix is orthogonal to the up-quark row. -/
lemma cRow_uRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]u = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 0) 1
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
zero_ne_one, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
/-- The charm-quark row of the CKM matrix is orthogonal to the top-quark row. -/
lemma cRow_tRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]t = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
rw [mem_unitaryGroup_iff] at hV
have ht := congrFun (congrFun hV 2) 1
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
/-- The top-quark row of the CKM matrix is orthogonal to the up-quark row. -/
lemma tRow_uRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]u = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
@ -122,6 +130,7 @@ lemma tRow_uRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]u = 0 := by
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
exact ht
/-- The top-quark row of the CKM matrix is orthogonal to the charm-quark row. -/
lemma tRow_cRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]c = 0 := by
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
have hV := V.prop
@ -166,6 +175,7 @@ def rows (V : CKMMatrix) : Fin 3 → Fin 3 → ℂ := fun i =>
| 1 => cRow V
| 2 => tRow V
/-- The rows of a CKM matrix are linearly independent. -/
lemma rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ (rows V) := by
apply Fintype.linearIndependent_iff.mpr
intro g hg
@ -186,13 +196,11 @@ lemma rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ (rows V)
· exact h1
· exact h2
lemma rows_card : Fintype.card (Fin 3) = Module.finrank ℂ (Fin 3 → ℂ) := by
simp
/-- The rows of a CKM matrix as a basis of `ℂ³`. -/
@[simps!]
noncomputable def rowBasis (V : CKMMatrix) : Basis (Fin 3) ℂ (Fin 3 → ℂ) :=
basisOfLinearIndependentOfCardEqFinrank (rows_linearly_independent V) rows_card
basisOfLinearIndependentOfCardEqFinrank (rows_linearly_independent V)
(Module.finrank_fin_fun ℂ).symm
lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
∃ (κ : ℝ), [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t) := by

8
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
View file

@ -36,6 +36,7 @@ def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin
open CKMMatrix
/-- The standard parameterization forms a unitary matrix. -/
lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := by
funext j i
@ -115,6 +116,9 @@ def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩
namespace standParam
/-- The top-row of the standard parameterization is the cross product of the conjugate of the
up and charm rows. -/
lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
[standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t =
(conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by
@ -149,12 +153,16 @@ lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
rw [sin_sq]
ring
/-- A CKM matrix which has rows equal to that of a standard parameterisation is equal
to that standard parameterisation. -/
lemma eq_rows (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : [U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u)
(hc : [U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU : [U]t = conj [U]u ×₃ conj [U]c) :
U = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
apply ext_Rows hu hc
rw [hU, cross_product_t, hu, hc]
/-- Two standard parameterisations of CKM matrices are the same matrix if they have
the same angles and the exponential of their faces is equal. -/
lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) :
standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by
simp only [standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, neg_mul]

6
HepLean/Lorentz/ComplexTensor/Basic.lean
View file

@ -30,11 +30,17 @@ namespace complexLorentzTensor
/-- The colors associated with complex representations of SL(2, ℂ) of intrest to physics. -/
inductive Color
/-- The color associated with Left handed fermions. -/
| upL : Color
/-- The color associated with alt-Left handed fermions. -/
| downL : Color
/-- The color associated with Right handed fermions. -/
| upR : Color
/-- The color associated with alt-Right handed fermions. -/
| downR : Color
/-- The color associated with contravariant Lorentz vectors. -/
| up : Color
/-- The color associated with covariant Lorentz vectors. -/
| down : Color
/-- Color for complex Lorentz tensors is decidable. -/

6
HepLean/Lorentz/ComplexTensor/Basis.lean
View file

@ -63,6 +63,7 @@ lemma basis_eq_FD {n : ℕ} (c : Fin n → complexLorentzTensor.C)
subst h'
rfl
/-- The `perm` node acting on basis vectors corresponds to a basis vector. -/
lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
{c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1)
(b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
@ -79,6 +80,8 @@ lemma perm_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, LinearEquiv.ofLinear_apply]
rw [basis_eq_FD]
/-- The `perm` node acting on basis vectors corresponds to a basis vector, as a tensor tree
structue. -/
lemma perm_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
{c1 : Fin m → complexLorentzTensor.C} (σ : OverColor.mk c ⟶ OverColor.mk c1)
(b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
@ -168,6 +171,7 @@ def prodBasisVecEquiv {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
| Sum.inl _ => Equiv.refl _
| Sum.inr _ => Equiv.refl _
/-- The `prod` node acting on basis vectors corresponds to a basis vector. -/
lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
{c1 : Fin m → complexLorentzTensor.C}
(b : Π k, Fin (complexLorentzTensor.repDim (c k)))
@ -197,6 +201,7 @@ lemma prod_basisVector {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
| Sum.inl k => rfl
| Sum.inr k => rfl
/-- The prod node acting on a basis vectors is a basis vector, as a tensor tree structure. -/
lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
{c1 : Fin m → complexLorentzTensor.C}
(b : Π k, Fin (complexLorentzTensor.repDim (c k)))
@ -207,6 +212,7 @@ lemma prod_basisVector_tree {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
((HepLean.PiTensorProduct.elimPureTensor b b1) (finSumFinEquiv.symm i))))).tensor := by
exact prod_basisVector _ _
/-- The `eval` node acting on basis vectors corresponds to a basis vector. -/
lemma eval_basisVector {n : ℕ} {c : Fin n.succ → complexLorentzTensor.C}
{i : Fin n.succ} (j : Fin (complexLorentzTensor.repDim (c i)))
(b : Π k, Fin (complexLorentzTensor.repDim (c k))) :

14
HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean
View file

@ -87,6 +87,8 @@ lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
rfl
/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors as
a structured tensor tree. -/
lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
(TensorTree.add (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 0))) <|
TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 1)))) <|
@ -94,6 +96,7 @@ lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
(smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 3))))).tensor :=
contrMatrix_basis_expand
/-- The expansion of the Fermionic left metric in terms of basis vectors. -/
lemma leftMetric_expand : {εL | α β}ᵀ.tensor =
- basisVector ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)
+ basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by
@ -112,12 +115,15 @@ lemma leftMetric_expand : {εL | α β}ᵀ.tensor =
· rfl
· rfl
/-- The expansion of the Fermionic left metric in terms of basis vectors as a structured
tensor tree. -/
lemma leftMetric_expand_tree : {εL | α β}ᵀ.tensor =
(TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upL, Color.upL]
(fun | 0 => 0 | 1 => 1)))) <|
(tensorNode (basisVector ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0)))).tensor :=
leftMetric_expand
/-- The expansion of the Fermionic alt-left metric in terms of basis vectors. -/
lemma altLeftMetric_expand : {εL' | α β}ᵀ.tensor =
basisVector ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1)
- basisVector ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0) := by
@ -135,6 +141,8 @@ lemma altLeftMetric_expand : {εL' | α β}ᵀ.tensor =
· rfl
· rfl
/-- The expansion of the Fermionic alt-left metric in terms of basis vectors as a
structured tensor tree. -/
lemma altLeftMetric_expand_tree : {εL' | α β}ᵀ.tensor =
(TensorTree.add (tensorNode (basisVector ![Color.downL, Color.downL]
(fun | 0 => 0 | 1 => 1))) <|
@ -142,6 +150,7 @@ lemma altLeftMetric_expand_tree : {εL' | α β}ᵀ.tensor =
(fun | 0 => 1 | 1 => 0))))).tensor :=
altLeftMetric_expand
/-- The expansion of the Fermionic right metric in terms of basis vectors. -/
lemma rightMetric_expand : {εR | α β}ᵀ.tensor =
- basisVector ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1)
+ basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0) := by
@ -160,12 +169,15 @@ lemma rightMetric_expand : {εR | α β}ᵀ.tensor =
· rfl
· rfl
/-- The expansion of the Fermionic right metric in terms of basis vectors as a
structured tensor tree. -/
lemma rightMetric_expand_tree : {εR | α β}ᵀ.tensor =
(TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.upR, Color.upR]
(fun | 0 => 0 | 1 => 1)))) <|
(tensorNode (basisVector ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0)))).tensor :=
rightMetric_expand
/-- The expansion of the Fermionic alt-right metric in terms of basis vectors. -/
lemma altRightMetric_expand : {εR' | α β}ᵀ.tensor =
basisVector ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1)
- basisVector ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0) := by
@ -183,6 +195,8 @@ lemma altRightMetric_expand : {εR' | α β}ᵀ.tensor =
· rfl
· rfl
/-- The expansion of the Fermionic alt-right metric in terms of basis vectors as a
structured tensor tree. -/
lemma altRightMetric_expand_tree : {εR' | α β}ᵀ.tensor =
(TensorTree.add (tensorNode (basisVector
![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1))) <|

4
HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean
View file

@ -101,7 +101,7 @@ informal_lemma altRightMetric_contr_rightMetric where
def leftMetricMulRightMap := (Sum.elim ![Color.upL, Color.upL] ![Color.upR, Color.upR]) ∘
finSumFinEquiv.symm
/- Expansion of the product of `εL` and `εR` in terms of a basis. -/
/-- Expansion of the product of `εL` and `εR` in terms of a basis. -/
lemma leftMetric_prod_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
= basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1)
- basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0)
@ -134,7 +134,7 @@ lemma leftMetric_prod_rightMetric : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
funext x
fin_cases x <;> rfl
/- Expansion of the product of `εL` and `εR` in terms of a basis, as a tensor tree. -/
/-- Expansion of the product of `εL` and `εR` in terms of a basis, as a tensor tree. -/
lemma leftMetric_prod_rightMetric_tree : {εL | α α' ⊗ εR | β β'}ᵀ.tensor
= (TensorTree.add (tensorNode
(basisVector leftMetricMulRightMap (fun | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1))) <|

27
HepLean/Lorentz/Group/Orthochronous.lean
View file

@ -29,24 +29,33 @@ open Lorentz.Contr
/-- A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative. -/
def IsOrthochronous : Prop := 0 ≤ Λ.1 (Sum.inl 0) (Sum.inl 0)
/-- A Lorentz transformation is `orthochronous` if and only if its fist column is
future pointing. -/
lemma IsOrthochronous_iff_futurePointing :
IsOrthochronous Λ ↔ toNormOne Λ ∈ NormOne.FuturePointing d := by
simp only [IsOrthochronous]
rw [NormOne.FuturePointing.mem_iff_inl_nonneg, toNormOne_inl]
/-- A Lorentz transformation is orthochronous if and only if its transpose is orthochronous. -/
lemma IsOrthochronous_iff_transpose :
IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by rfl
/-- A Lorentz transformation is orthochronous if and only if its `0 0` element is greater
or equal to one. -/
lemma IsOrthochronous_iff_ge_one :
IsOrthochronous Λ ↔ 1 ≤ Λ.1 (Sum.inl 0) (Sum.inl 0) := by
rw [IsOrthochronous_iff_futurePointing, NormOne.FuturePointing.mem_iff_inl_one_le_inl,
toNormOne_inl]
/-- A Lorentz transformation is not orthochronous if and only if its `0 0` element is less then
or equal to minus one. -/
lemma not_orthochronous_iff_le_neg_one :
¬ IsOrthochronous Λ ↔ Λ.1 (Sum.inl 0) (Sum.inl 0) ≤ -1 := by
rw [IsOrthochronous_iff_futurePointing, NormOne.FuturePointing.not_mem_iff_inl_le_neg_one,
toNormOne_inl]
/-- A Lorentz transformation is not orthochronous if and only if its `0 0` element is
non-positive. -/
lemma not_orthochronous_iff_le_zero : ¬ IsOrthochronous Λ ↔ Λ.1 (Sum.inl 0) (Sum.inl 0) ≤ 0 := by
rw [IsOrthochronous_iff_futurePointing, NormOne.FuturePointing.not_mem_iff_inl_le_zero,
toNormOne_inl]
@ -55,11 +64,14 @@ lemma not_orthochronous_iff_le_zero : ¬ IsOrthochronous Λ ↔ Λ.1 (Sum.inl 0)
def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => Λ.1 (Sum.inl 0) (Sum.inl 0),
Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩
/-- An auxillary function used in the definition of `orthchroMapReal`. -/
/-- An auxillary function used in the definition of `orthchroMapReal`.
This function takes all elements of `ℝ` less then `-1` to `-1`,
all elements of `R` geater then `1` to `1` and peserves all other elements. -/
def stepFunction : ℝ → ℝ := fun t =>
if t ≤ -1 then -1 else
if 1 ≤ t then 1 else t
/-- The `stepFunction` is continuous. -/
lemma stepFunction_continuous : Continuous stepFunction := by
apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_const continuous_id)
<;> intro a ha
@ -76,6 +88,7 @@ taking Orthochronous elements to `1` and non-orthochronous to `-1`. -/
def orthchroMapReal : C(LorentzGroup d, ℝ) := ContinuousMap.comp
⟨stepFunction, stepFunction_continuous⟩ timeCompCont
/-- A Lorentz transformation which is orthochronous maps under `orthchroMapReal` to `1`. -/
lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) :
orthchroMapReal Λ = 1 := by
rw [IsOrthochronous_iff_ge_one] at h
@ -83,6 +96,7 @@ lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochron
rw [stepFunction, if_pos h, if_neg]
linarith
/-- A Lorentz transformation which is not-orthochronous maps under `orthchroMapReal` to `- 1`. -/
lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
orthchroMapReal Λ = - 1 := by
rw [not_orthochronous_iff_le_neg_one] at h
@ -90,6 +104,7 @@ lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrt
rw [stepFunction, if_pos]
exact h
/-- Every Lorentz transformation maps under `orthchroMapReal` to either `1` or `-1`. -/
lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) :
orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := by
by_cases h : IsOrthochronous Λ
@ -104,10 +119,14 @@ def orthchroMap : C(LorentzGroup d, ℤ₂) :=
toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
continuous_toFun := Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _}
/-- A Lorentz transformation which is orthochronous maps under `orthchroMap` to `1`
in `ℤ₂` (the identity element). -/
lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) :
orthchroMap Λ = 1 := by
simp [orthchroMap, orthchroMapReal_on_IsOrthochronous h]
/-- A Lorentz transformation which is not-orthochronous maps under `orthchroMap` to
the non-identity element of `ℤ₂`. -/
lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
orthchroMap Λ = Additive.toMul (1 : ZMod 2) := by
simp only [orthchroMap, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
@ -116,6 +135,7 @@ lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochron
· rfl
· linarith
/-- The product of two orthochronous Lorentz transfomations is orthochronous. -/
lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
(h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
rw [IsOrthochronous_iff_transpose] at h
@ -123,6 +143,7 @@ lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthoch
rw [IsOrthochronous, LorentzGroup.inl_inl_mul]
exact NormOne.FuturePointing.metric_reflect_mem_mem h h'
/-- The product of two non-orthochronous Lorentz transfomations is orthochronous. -/
lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ)
(h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
rw [IsOrthochronous_iff_transpose] at h
@ -130,6 +151,8 @@ lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h :
rw [IsOrthochronous, LorentzGroup.inl_inl_mul]
exact NormOne.FuturePointing.metric_reflect_not_mem_not_mem h h'
/-- The product of an orthochronous Lorentz transfomations with a
non-orthchronous Loentz transformation is not orthochronous. -/
lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
(h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
rw [not_orthochronous_iff_le_zero, LorentzGroup.inl_inl_mul]
@ -137,6 +160,8 @@ lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : I
rw [IsOrthochronous_iff_futurePointing] at h h'
exact NormOne.FuturePointing.metric_reflect_mem_not_mem h h'
/-- The product of a non-orthochronous Lorentz transfomations with an
orthchronous Loentz transformation is not orthochronous. -/
lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ)
(h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
rw [not_orthochronous_iff_le_zero, LorentzGroup.inl_inl_mul]

27
HepLean/Lorentz/MinkowskiMatrix.lean
View file

@ -30,6 +30,7 @@ variable {d : ℕ}
/-- Notation for `minkowskiMatrix`. -/
scoped[minkowskiMatrix] notation "η" => minkowskiMatrix
/-- The Minkowski matrix is self-inveting. -/
@[simp]
lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_mul_diagonal]
@ -50,20 +51,25 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
simp_all only [one_apply_eq]
· simp_all only [ne_eq, Sum.inr.injEq, not_false_eq_true, one_apply_ne]
/-- The Minkowski matrix is symmetric. -/
@[simp]
lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
/-- The deteminant of the Minkowski matrix is equal to `-1` to the power
of the number of spactial dimensions. -/
@[simp]
lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
/-- Multiplying any element on the diagonal of the Minkowski matrix by itself gives `1`. -/
@[simp]
lemma η_apply_mul_η_apply_diag (μ : Fin 1 ⊕ Fin d) : η μ μ * η μ μ = 1 := by
match μ with
| Sum.inl _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
| Sum.inr _ => simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
/-- The Minkowski matix as a block matrix. -/
lemma as_block : @minkowskiMatrix d =
Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ) := by
rw [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, ← fromBlocks_diagonal]
@ -73,24 +79,29 @@ lemma as_block : @minkowskiMatrix d =
rw [← diagonal_neg]
rfl
/-- The off diagonal elements of the Minkowski matrix are zero. -/
@[simp]
lemma off_diag_zero {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) : η μ ν = 0 := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
exact diagonal_apply_ne _ h
/-- The `time-time` component of the Minkowski matrix is `1`. -/
lemma inl_0_inl_0 : @minkowskiMatrix d (Sum.inl 0) (Sum.inl 0) = 1 := by
rfl
/-- The space diagonal components of the Minkowski matriz are `-1`. -/
lemma inr_i_inr_i (i : Fin d) : @minkowskiMatrix d (Sum.inr i) (Sum.inr i) = -1 := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
simp_all only [diagonal_apply_eq, Sum.elim_inr]
/-- The time components of a vector acted on by the Minkowski matrix remains unchanged. -/
@[simp]
lemma mulVec_inl_0 (v : (Fin 1 ⊕ Fin d) → ℝ) :
(η *ᵥ v) (Sum.inl 0)= v (Sum.inl 0) := by
simp only [mulVec, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mulVec_diagonal]
simp only [Fin.isValue, diagonal_dotProduct, Sum.elim_inl, one_mul]
/-- The space components of a vector acted on by the Minkowski matrix swaps sign. -/
@[simp]
lemma mulVec_inr_i (v : (Fin 1 ⊕ Fin d) → ℝ) (i : Fin d) :
(η *ᵥ v) (Sum.inr i)= - v (Sum.inr i) := by
@ -99,13 +110,16 @@ lemma mulVec_inr_i (v : (Fin 1 ⊕ Fin d) → ℝ) (i : Fin d) :
variable (Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
/-- The dual of a matrix with respect to the Minkowski metric. -/
/-- The dual of a matrix with respect to the Minkowski metric.
A suitable name fo this construction is the Minkowski dual. -/
def dual : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := η * Λᵀ * η
/-- The Minkowski dual of the identity is the identity. -/
@[simp]
lemma dual_id : @dual d 1 = 1 := by
simpa only [dual, transpose_one, mul_one] using minkowskiMatrix.sq
/-- The Minkowski dual swaps multiplications (acts contrvariantly). -/
@[simp]
lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
simp only [dual, transpose_mul]
@ -113,23 +127,28 @@ lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
· noncomm_ring [minkowskiMatrix.sq]
· noncomm_ring
/-- The Minkowski dual is involutive (i.e. `dual (dual Λ)) = Λ`). -/
@[simp]
lemma dual_dual : dual (dual Λ) = Λ := by
lemma dual_dual : Function.Involutive (@dual d) := by
intro Λ
simp only [dual, transpose_mul, transpose_transpose, eq_transpose]
trans (η * η) * Λ * (η * η)
· noncomm_ring
· noncomm_ring [minkowskiMatrix.sq]
/-- The Minkowski dual preserves the Minkowski matrix. -/
@[simp]
lemma dual_eta : @dual d η = η := by
simp only [dual, eq_transpose]
noncomm_ring [minkowskiMatrix.sq]
/-- The Minkowski dual commutes with the transpose. -/
@[simp]
lemma dual_transpose : dual Λᵀ = (dual Λ)ᵀ := by
simp only [dual, transpose_transpose, transpose_mul, eq_transpose]
noncomm_ring
/-- The Minkowski dual preserves determinants. -/
@[simp]
lemma det_dual : (dual Λ).det = Λ.det := by
simp only [dual, det_mul, minkowskiMatrix.det_eq_neg_one_pow_d, det_transpose]
@ -137,11 +156,15 @@ lemma det_dual : (dual Λ).det = Λ.det := by
norm_cast
simp
/-- Expansion of the components of the Minkowski dual interms of the components
of the original matrix. -/
lemma dual_apply (μ ν : Fin 1 ⊕ Fin d) :
dual Λ μ ν = η μ μ * Λ ν μ * η ν ν := by
simp only [dual, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
diagonal_mul, transpose_apply, diagonal_apply_eq]
/-- The components of the Minkowski dual of a matrix multiplied by the Minkowski matrix
in tems of the original matrix. -/
lemma dual_apply_minkowskiMatrix (μ ν : Fin 1 ⊕ Fin d) :
dual Λ μ ν * η ν ν = η μ μ * Λ ν μ := by
rw [dual_apply, mul_assoc]

2
HepLean/Lorentz/PauliMatrices/AsTensor.lean
View file

@ -189,6 +189,8 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗
CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj]
/-- The map `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗ rightHanded` corresponding
to Pauli matrices, when evaluated on `1` corresponds to the tensor `PauliMatrix.asTensor`. -/
lemma asConsTensor_apply_one : asConsTensor.hom (1 : ℂ) = asTensor := by
change asConsTensor.hom.toFun (1 : ℂ) = asTensor
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,

20
HepLean/Lorentz/PauliMatrices/Basic.lean
View file

@ -34,21 +34,25 @@ def σ2 : Matrix (Fin 2) (Fin 2) ℂ := !![0, -I; I, 0]
That is, the matrix `!![1, 0; 0, -1]`. -/
def σ3 : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, -1]
/-- The conjugate transpose of `σ0` is equal to `σ0`. -/
@[simp]
lemma σ0_selfAdjoint : σ0ᴴ = σ0 := by
rw [eta_fin_two σ0ᴴ]
simp [σ0]
/-- The conjugate transpose of `σ1` is equal to `σ1`. -/
@[simp]
lemma σ1_selfAdjoint : σ1ᴴ = σ1 := by
rw [eta_fin_two σ1ᴴ]
simp [σ1]
/-- The conjugate transpose of `σ2` is equal to `σ2`. -/
@[simp]
lemma σ2_selfAdjoint : σ2ᴴ = σ2 := by
rw [eta_fin_two σ2ᴴ]
simp [σ2]
/-- The conjugate transpose of `σ3` is equal to `σ3`. -/
@[simp]
lemma σ3_selfAdjoint : σ3ᴴ = σ3 := by
rw [eta_fin_two σ3ᴴ]
@ -60,6 +64,7 @@ lemma σ3_selfAdjoint : σ3ᴴ = σ3 := by
-/
/-- The trace of `σ0` multiplied by `σ0` is equal to `2`. -/
@[simp]
lemma σ0_σ0_trace : Matrix.trace (σ0 * σ0) = 2 := by
simp only [σ0, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,
@ -67,22 +72,27 @@ lemma σ0_σ0_trace : Matrix.trace (σ0 * σ0) = 2 := by
trace_fin_two_of]
norm_num
/-- The trace of `σ0` multiplied by `σ1` is equal to `0`. -/
@[simp]
lemma σ0_σ1_trace : Matrix.trace (σ0 * σ1) = 0 := by
simp [σ0, σ1]
/-- The trace of `σ0` multiplied by `σ2` is equal to `0`. -/
@[simp]
lemma σ0_σ2_trace : Matrix.trace (σ0 * σ2) = 0 := by
simp [σ0, σ2]
/-- The trace of `σ0` multiplied by `σ3` is equal to `0`. -/
@[simp]
lemma σ0_σ3_trace : Matrix.trace (σ0 * σ3) = 0 := by
simp [σ0, σ3]
/-- The trace of `σ1` multiplied by `σ0` is equal to `0`. -/
@[simp]
lemma σ1_σ0_trace : Matrix.trace (σ1 * σ0) = 0 := by
simp [σ1, σ0]
/-- The trace of `σ1` multiplied by `σ1` is equal to `2`. -/
@[simp]
lemma σ1_σ1_trace : Matrix.trace (σ1 * σ1) = 2 := by
simp only [σ1, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,
@ -90,22 +100,27 @@ lemma σ1_σ1_trace : Matrix.trace (σ1 * σ1) = 2 := by
trace_fin_two_of]
norm_num
/-- The trace of `σ1` multiplied by `σ2` is equal to `0`. -/
@[simp]
lemma σ1_σ2_trace : Matrix.trace (σ1 * σ2) = 0 := by
simp [σ1, σ2]
/-- The trace of `σ1` multiplied by `σ3` is equal to `0`. -/
@[simp]
lemma σ1_σ3_trace : Matrix.trace (σ1 * σ3) = 0 := by
simp [σ1, σ3]
/-- The trace of `σ2` multiplied by `σ0` is equal to `0`. -/
@[simp]
lemma σ2_σ0_trace : Matrix.trace (σ2 * σ0) = 0 := by
simp [σ2, σ0]
/-- The trace of `σ2` multiplied by `σ1` is equal to `0`. -/
@[simp]
lemma σ2_σ1_trace : Matrix.trace (σ2 * σ1) = 0 := by
simp [σ2, σ1]
/-- The trace of `σ2` multiplied by `σ2` is equal to `2`. -/
@[simp]
lemma σ2_σ2_trace : Matrix.trace (σ2 * σ2) = 2 := by
simp only [σ2, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,
@ -113,22 +128,27 @@ lemma σ2_σ2_trace : Matrix.trace (σ2 * σ2) = 2 := by
trace_fin_two_of]
norm_num
/-- The trace of `σ2` multiplied by `σ3` is equal to `0`. -/
@[simp]
lemma σ2_σ3_trace : Matrix.trace (σ2 * σ3) = 0 := by
simp [σ2, σ3]
/-- The trace of `σ3` multiplied by `σ0` is equal to `0`. -/
@[simp]
lemma σ3_σ0_trace : Matrix.trace (σ3 * σ0) = 0 := by
simp [σ3, σ0]
/-- The trace of `σ3` multiplied by `σ1` is equal to `0`. -/
@[simp]
lemma σ3_σ1_trace : Matrix.trace (σ3 * σ1) = 0 := by
simp [σ3, σ1]
/-- The trace of `σ3` multiplied by `σ2` is equal to `0`. -/
@[simp]
lemma σ3_σ2_trace : Matrix.trace (σ3 * σ2) = 0 := by
simp [σ3, σ2]
/-- The trace of `σ3` multiplied by `σ3` is equal to `2`. -/
@[simp]
lemma σ3_σ3_trace : Matrix.trace (σ3 * σ3) = 2 := by
simp only [σ3, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, one_smul,

30
HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
View file

@ -16,6 +16,7 @@ import HepLean.Lorentz.PauliMatrices.Basic
namespace PauliMatrix
open Matrix
/-- The trace of `σ0` multiplied by a self-adjiont `2×2` matrix is real. -/
lemma selfAdjoint_trace_σ0_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
(Matrix.trace (σ0 * A.1)).re = Matrix.trace (σ0 * A.1) := by
rw [eta_fin_two A.1]
@ -38,6 +39,7 @@ lemma selfAdjoint_trace_σ0_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))
cons_val_fin_one, head_fin_const] at h11
exact Complex.conj_eq_iff_re.mp h11
/-- The trace of `σ1` multiplied by a self-adjiont `2×2` matrix is real. -/
lemma selfAdjoint_trace_σ1_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
(Matrix.trace (σ1 * A.1)).re = Matrix.trace (σ1 * A.1) := by
rw [eta_fin_two A.1]
@ -57,6 +59,7 @@ lemma selfAdjoint_trace_σ1_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))
simp only [Fin.isValue, Complex.ofReal_mul, Complex.ofReal_ofNat]
ring
/-- The trace of `σ2` multiplied by a self-adjiont `2×2` matrix is real. -/
lemma selfAdjoint_trace_σ2_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
(Matrix.trace (σ2 * A.1)).re = Matrix.trace (σ2 * A.1) := by
rw [eta_fin_two A.1]
@ -80,6 +83,7 @@ lemma selfAdjoint_trace_σ2_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))
simp
· ring
/-- The trace of `σ3` multiplied by a self-adjiont `2×2` matrix is real. -/
lemma selfAdjoint_trace_σ3_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
(Matrix.trace (σ3 * A.1)).re = Matrix.trace (σ3 * A.1) := by
rw [eta_fin_two A.1]
@ -100,8 +104,10 @@ lemma selfAdjoint_trace_σ3_real (A : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ))
open Complex
/-- Two `2×2` self-adjiont matrices are equal if the (complex) traces of each matrix multiplied by
each of the Pauli-matrices are equal. -/
lemma selfAdjoint_ext_complex {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}
(h0 : ((Matrix.trace (PauliMatrix.σ0 * A.1)) = (Matrix.trace (PauliMatrix.σ0 * B.1))))
(h0 : Matrix.trace (PauliMatrix.σ0 * A.1) = Matrix.trace (PauliMatrix.σ0 * B.1))
(h1 : Matrix.trace (PauliMatrix.σ1 * A.1) = Matrix.trace (PauliMatrix.σ1 * B.1))
(h2 : Matrix.trace (PauliMatrix.σ2 * A.1) = Matrix.trace (PauliMatrix.σ2 * B.1))
(h3 : Matrix.trace (PauliMatrix.σ3 * A.1) = Matrix.trace (PauliMatrix.σ3 * B.1)) : A = B := by
@ -131,6 +137,8 @@ lemma selfAdjoint_ext_complex {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}
| 1, 1 =>
linear_combination (norm := ring_nf) (h0 - h3) / 2
/-- Two `2×2` self-adjiont matrices are equal if the real traces of each matrix multiplied by
each of the Pauli-matrices are equal. -/
lemma selfAdjoint_ext {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}
(h0 : ((Matrix.trace (PauliMatrix.σ0 * A.1))).re = ((Matrix.trace (PauliMatrix.σ0 * B.1))).re)
(h1 : ((Matrix.trace (PauliMatrix.σ1 * A.1))).re = ((Matrix.trace (PauliMatrix.σ1 * B.1))).re)
@ -159,6 +167,7 @@ def σSA' (i : Fin 1 ⊕ Fin 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
| Sum.inr 1 => ⟨σ2, σ2_selfAdjoint⟩
| Sum.inr 2 => ⟨σ3, σ3_selfAdjoint⟩
/-- The Pauli matrices are linearly independent. -/
lemma σSA_linearly_independent : LinearIndependent ℝ σSA' := by
apply Fintype.linearIndependent_iff.mpr
intro g hg
@ -177,6 +186,7 @@ lemma σSA_linearly_independent : LinearIndependent ℝ σSA' := by
| Sum.inr 2 =>
simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ3 * A.1))) hg
/-- The Pauli matrices span all self-adjoint matrices. -/
lemma σSA_span : ⊤ ≤ Submodule.span ℝ (Set.range σSA') := by
refine (top_le_span_range_iff_forall_exists_fun ℝ).mpr ?_
intro A
@ -228,6 +238,7 @@ def σSAL' (i : Fin 1 ⊕ Fin 3) : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) :=
| Sum.inr 1 => ⟨-σ2, by rw [neg_mem_iff]; exact σ2_selfAdjoint⟩
| Sum.inr 2 => ⟨-σ3, by rw [neg_mem_iff]; exact σ3_selfAdjoint⟩
/-- The Pauli matrices where `σi` are negated are linearly independent. -/
lemma σSAL_linearly_independent : LinearIndependent ℝ σSAL' := by
apply Fintype.linearIndependent_iff.mpr
intro g hg
@ -246,6 +257,7 @@ lemma σSAL_linearly_independent : LinearIndependent ℝ σSAL' := by
| Sum.inr 2 =>
simpa [mul_sub, mul_add] using congrArg (fun A => (Matrix.trace (PauliMatrix.σ3 * A.1))) hg
/-- The Pauli matrices where `σi` are negated span all Self-adjoint matrices. -/
lemma σSAL_span : ⊤ ≤ Submodule.span ℝ (Set.range σSAL') := by
refine (top_le_span_range_iff_forall_exists_fun ℝ).mpr ?_
intro A
@ -288,10 +300,12 @@ lemma σSAL_span : ⊤ ≤ Submodule.span ℝ (Set.range σSAL') := by
ring
/-- The basis of `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` formed by Pauli matrices
where the `1, 2, 3` pauli matrices are negated. -/
where the `1, 2, 3` pauli matrices are negated. These can be thought of as the
covariant Pauli-matrices. -/
def σSAL : Basis (Fin 1 ⊕ Fin 3) ℝ (selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :=
Basis.mk σSAL_linearly_independent σSAL_span
/-- The decomposition of a self-adjint matrix into the Pauli matrices (where `σi` are negated). -/
lemma σSAL_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
M = (1/2 * (Matrix.trace (σ0 * M.1)).re) • σSAL (Sum.inl 0)
+ (-1/2 * (Matrix.trace (σ1 * M.1)).re) • σSAL (Sum.inr 0)
@ -327,6 +341,8 @@ lemma σSAL_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
mul_zero, sub_zero, re_ofNat, mul_im, zero_mul, im_ofNat]
ring
/-- The component of a self-adjoint matrix in the direction `σ0` under
the basis formed by the covaraiant Pauli matrices. -/
@[simp]
lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
σSAL.repr M (Sum.inl 0) = 1 / 2 * Matrix.trace (σ0 * M.1) := by
@ -342,6 +358,8 @@ lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
linear_combination (norm := ring_nf) -h0
simp [σSAL]
/-- The component of a self-adjoint matrix in the direction `-σ1` under
the basis formed by the covaraiant Pauli matrices. -/
@[simp]
lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
σSAL.repr M (Sum.inr 0) = - 1 / 2 * Matrix.trace (σ1 * M.1) := by
@ -357,6 +375,8 @@ lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
linear_combination (norm := ring_nf) -h0
simp [σSAL]
/-- The component of a self-adjoint matrix in the direction `-σ2` under
the basis formed by the covaraiant Pauli matrices. -/
@[simp]
lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
σSAL.repr M (Sum.inr 1) = - 1 / 2 * Matrix.trace (σ2 * M.1) := by
@ -372,6 +392,8 @@ lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
linear_combination (norm := ring_nf) -h0
simp [σSAL]
/-- The component of a self-adjoint matrix in the direction `-σ3` under
the basis formed by the covaraiant Pauli matrices. -/
@[simp]
lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
σSAL.repr M (Sum.inr 2) = - 1 / 2 * Matrix.trace (σ3 * M.1) := by
@ -387,8 +409,10 @@ lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
linear_combination (norm := ring_nf) -h0
simp only [σSAL, Basis.mk_repr, Fin.isValue, sub_self]
/-- The relationship between the basis `σSA` of contrvariant Pauli-matrices and the basis
`σSAL` of covariant Pauli matrices is by multiplication by the Minkowski matrix. -/
lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
(σSA i) = minkowskiMatrix i i • (σSAL i) := by
σSA i = minkowskiMatrix i i • σSAL i := by
match i with
| Sum.inl 0 =>
simp [σSA, σSAL, σSA', σSAL', minkowskiMatrix.inl_0_inl_0]

2
HepLean/Lorentz/Weyl/Metric.lean
View file

@ -30,6 +30,8 @@ open CategoryTheory.MonoidalCategory
/-- The raw `2x2` matrix corresponding to the metric for fermions. -/
def metricRaw : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; -1, 0]
/-- Multiplying an element of `SL(2, ℂ)` on the left with the metric `𝓔` is equivalent
to multiplying the inverse-transpose of that element on the right with the metric. -/
lemma comm_metricRaw (M : SL(2,ℂ)) : M.1 * metricRaw = metricRaw * (M.1⁻¹)ᵀ := by
rw [metricRaw]
rw [Lorentz.SL2C.inverse_coe, eta_fin_two M.1]

9
HepLean/Mathematics/SO3/Basic.lean
View file

@ -56,6 +56,7 @@ lemma subtype_val_eq_toGL : (Subtype.val : SO3 → Matrix (Fin 3) (Fin 3) ℝ) =
Units.val ∘ toGL.toFun :=
rfl
/-- The inclusino of `SO(3)` into `GL(3,ℝ)` is an injection. -/
lemma toGL_injective : Function.Injective toGL := by
refine fun A B h ↦ Subtype.eq ?_
rw [@Units.ext_iff] at h
@ -116,6 +117,7 @@ lemma toGL_embedding : IsEmbedding toGL.toFun where
instance : TopologicalGroup SO(3) :=
IsInducing.topologicalGroup toGL toGL_embedding.toIsInducing
/-- The determinant of an `SO(3)` matrix minus the identity is equal to zero. -/
lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
have h1 : det (A.1 - 1) = - det (A.1 - 1) :=
calc
@ -129,6 +131,7 @@ lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
_ = - det (A.1 - 1) := by simp [pow_three]
exact CharZero.eq_neg_self_iff.mp h1
/-- The determinant of the identity minus an `SO(3)` matrix is zero. -/
@[simp]
lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
have h1 : det (1 - A.1) = - det (A.1 - 1) := by
@ -139,6 +142,7 @@ lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
rw [h1, det_minus_id]
exact neg_zero
/-- For every matrix in `SO(3)`, the real number `1` is in its spectrum. -/
@[simp]
lemma one_in_spectrum (A : SO(3)) : 1 ∈ spectrum ℝ (A.1) := by
rw [spectrum.mem_iff]
@ -155,11 +159,14 @@ def toEnd (A : SO(3)) : End ℝ (EuclideanSpace ℝ (Fin 3)) :=
Matrix.toLin (EuclideanSpace.basisFun (Fin 3) ℝ).toBasis
(EuclideanSpace.basisFun (Fin 3) ℝ).toBasis A.1
/-- Every `SO(3)` matrix has an eigenvalue equal to `1`. -/
lemma one_is_eigenvalue (A : SO(3)) : A.toEnd.HasEigenvalue 1 := by
rw [End.hasEigenvalue_iff_mem_spectrum]
erw [AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv (EuclideanSpace.basisFun (Fin 3) ℝ).toBasis) A.1]
exact one_in_spectrum A
/-- For every element of `SO(3)` there exists a vector which remains unchanged under the
action of that `SO(3)` element. -/
lemma exists_stationary_vec (A : SO(3)) :
∃ (v : EuclideanSpace ℝ (Fin 3)),
Orthonormal ℝ (({0} : Set (Fin 3)).restrict (fun _ => v))
@ -185,6 +192,8 @@ lemma exists_stationary_vec (A : SO(3)) :
· rw [_root_.map_smul, End.mem_eigenspace_iff.mp hv.1]
simp
/-- For every element of `SO(3)` there exists a basis indexed by `Fin 3` under which the first
element remains invariant. -/
lemma exists_basis_preserved (A : SO(3)) :
∃ (b : OrthonormalBasis (Fin 3) ℝ (EuclideanSpace ℝ (Fin 3))), A.toEnd (b 0) = b 0 := by
obtain ⟨v, hv⟩ := exists_stationary_vec A

7
HepLean/StandardModel/Basic.lean
View file

@ -71,9 +71,16 @@ informal_definition GaugeGroupℤ₃ where
/-- Specifies the allowed quotients of `SU(3) x SU(2) x U(1)` which give a valid
gauge group of the Standard Model. -/
inductive GaugeGroupQuot : Type
/-- The element of `GaugeGroupQuot` corresponding to the quotient of the full SM gauge group
by the sub-group `ℤ₆`. -/
| ℤ₆ : GaugeGroupQuot
/-- The element of `GaugeGroupQuot` corresponding to the quotient of the full SM gauge group
by the sub-group `ℤ₂`. -/
| ℤ₂ : GaugeGroupQuot
/-- The element of `GaugeGroupQuot` corresponding to the quotient of the full SM gauge group
by the sub-group `ℤ₃`. -/
| ℤ₃ : GaugeGroupQuot
/-- The element of `GaugeGroupQuot` corresponding to the full SM gauge group. -/
| I : GaugeGroupQuot
informal_definition GaugeGroup where

2
HepLean/StandardModel/HiggsBoson/Basic.lean
View file

@ -103,6 +103,8 @@ def HiggsVec.toField (φ : HiggsVec) : HiggsField where
rw [Bundle.contMDiffAt_section]
exact smoothAt_const
/-- For all spacetime points, the constant Higgs field defined by a Higgs vector,
returns that Higgs Vector. -/
@[simp]
lemma HiggsVec.toField_apply (φ : HiggsVec) (x : SpaceTime) : (φ.toField x) = φ := rfl

42
HepLean/Tensors/Tree/NodeIdentities/Basic.lean
View file

@ -54,10 +54,12 @@ lemma tensorNode_of_tree (t : TensorTree S c) : (tensorNode t.tensor).tensor = t
-/
/-- Two `neg` nodes of a tensor tree cancle. -/
@[simp]
lemma neg_neg (t : TensorTree S c) : (neg (neg t)).tensor = t.tensor := by
simp only [neg_tensor, _root_.neg_neg]
/-- A `neg` node can be moved out of the LHS of a `prod` node. -/
@[simp]
lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
(T2 : TensorTree S c2) :
@ -66,6 +68,7 @@ lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, neg_tmul, map_neg]
/-- A `neg` node can be moved out of the RHS of a `prod` node. -/
@[simp]
lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
(T2 : TensorTree S c2) :
@ -74,22 +77,26 @@ lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, tmul_neg, map_neg]
/-- A `neg` node can be moved through a `contr` node. -/
@[simp]
lemma neg_contr {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ}
{h : c (i.succAbove j) = S.τ (c i)}
(t : TensorTree S c) : (contr i j h (neg t)).tensor = (neg (contr i j h t)).tensor := by
simp only [Nat.succ_eq_add_one, contr_tensor, neg_tensor, map_neg]
/-- A `neg` node can be moved through a `perm` node. -/
lemma neg_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) :
(perm σ (neg t)).tensor = (neg (perm σ t)).tensor := by
simp only [perm_tensor, neg_tensor, map_neg]
/-- The negation of a tensor tree plus itself is zero. -/
@[simp]
lemma neg_add (t : TensorTree S c) : (add (neg t) t).tensor = 0 := by
rw [add_tensor, neg_tensor]
simp only [neg_add_cancel]
/-- A tensor tree plus its negation is zero. -/
@[simp]
lemma add_neg (t : TensorTree S c) : (add t (neg t)).tensor = 0 := by
rw [add_tensor, neg_tensor]
@ -117,6 +124,10 @@ lemma perm_eq_id {n : ℕ} {c : Fin n → S.C} (σ : (OverColor.mk c) ⟶ (OverC
(h : σ = 𝟙 _) (t : TensorTree S c) : (perm σ t).tensor = t.tensor := by
simp [perm_tensor, h]
/-- Given an equality of tensors corresponding to tensor trees where the tensor tree on the
left finishes with a permution node, this permutation node can be moved to the
tensor tree on the right. This lemma holds here for isomorphisms only, but holds in practice
more generally. -/
lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(σ : (OverColor.mk c) ≅ (OverColor.mk c1))
{t : TensorTree S c} {t2 : TensorTree S c1} (h : (perm σ.hom t).tensor = t2.tensor) :
@ -125,6 +136,8 @@ lemma perm_eq_of_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
change _ = (S.F.map σ.hom ≫ S.F.map σ.inv).hom _
simp only [Iso.map_hom_inv_id, Action.id_hom, ModuleCat.id_apply]
/-- A permutation of a tensor tree `t1` has equal tensor to a tensor tree `t2` if and only if
the inverse-permutation of `t2` has equal tensor to `t1`. -/
lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1))
{t : TensorTree S c} {t2 : TensorTree S c1} :
@ -162,15 +175,19 @@ These identities are related to the fact that all the maps are linear.
-/
/-- Two `smul` nodes can be replaced with a single `smul` node with
the product of the two scalars. -/
lemma smul_smul (t : TensorTree S c) (a b : S.k) :
(smul a (smul b t)).tensor = (smul (a * b) t).tensor := by
simp only [smul_tensor]
exact _root_.smul_smul a b t.tensor
/-- An `smul`-node with scalar `1` does nothing. -/
lemma smul_one (t : TensorTree S c) :
(smul 1 t).tensor = t.tensor := by
simp [smul_tensor]
/-- An `smul`-node with scalar equal to `1` does nothing. -/
lemma smul_eq_one (t : TensorTree S c) (a : S.k) (h : a = 1) :
(smul a t).tensor = t.tensor := by
rw [h]
@ -194,11 +211,14 @@ lemma add_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(add (perm σ t) (perm σ t1)).tensor = (perm σ (add t t1)).tensor := by
simp only [add_tensor, perm_tensor, map_add]
/-- When a `perm` acts on an add node, it can be moved through the add-node
to act on each of the two parts. -/
lemma perm_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t t1 : TensorTree S c) :
(perm σ (add t t1)).tensor = (add (perm σ t) (perm σ t1)).tensor := by
simp only [add_tensor, perm_tensor, map_add]
/-- A `smul` node can be moved through an `perm` node. -/
lemma perm_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (a : S.k) (t : TensorTree S c) :
(perm σ (smul a t)).tensor = (smul a (perm σ t)).tensor := by
@ -210,16 +230,21 @@ lemma add_eval {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t
(add (eval i e t) (eval i e t1)).tensor = (eval i e (add t t1)).tensor := by
simp only [add_tensor, eval_tensor, Nat.succ_eq_add_one, map_add]
/-- When a `contr` acts on an add node, it can be moved through the add-node
to act on each of the two parts. -/
lemma contr_add {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ}
{h : c (i.succAbove j) = S.τ (c i)} (t1 t2 : TensorTree S c) :
(contr i j h (add t1 t2)).tensor = (add (contr i j h t1) (contr i j h t2)).tensor := by
simp [contr_tensor, add_tensor]
/-- A `smul` node can be moved through an `contr` node. -/
lemma contr_smul {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ}
{h : c (i.succAbove j) = S.τ (c i)} (a : S.k) (t : TensorTree S c) :
(contr i j h (smul a t)).tensor = (smul a (contr i j h t)).tensor := by
simp [contr_tensor, smul_tensor]
/-- When a `prod` acts on an add node on the left, it can be moved through the add-node
to act on each of the two parts. -/
@[simp]
lemma add_prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(t1 t2 : TensorTree S c) (t3 : TensorTree S c1) :
@ -228,6 +253,8 @@ lemma add_prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, add_tensor, add_tmul, map_add]
/-- When a `prod` acts on an add node on the right, it can be moved through the add-node
to act on each of the two parts. -/
@[simp]
lemma prod_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(t1 : TensorTree S c) (t2 t3 : TensorTree S c1) :
@ -236,16 +263,20 @@ lemma prod_add {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, add_tensor, tmul_add, map_add]
/-- A `smul` node in the LHS of a `prod` node can be moved through that `prod` node. -/
lemma smul_prod {n m: ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
((prod (smul a t1) t2)).tensor = (smul a (prod t1 t2)).tensor := by
simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]
/-- A `smul` node in the RHS of a `prod` node can be moved through that `prod` node. -/
lemma prod_smul {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(a : S.k) (t1 : TensorTree S c) (t2 : TensorTree S c1) :
(prod t1 (smul a t2)).tensor = (smul a (prod t1 t2)).tensor := by
simp [prod_tensor, smul_tensor, tmul_smul, smul_tmul, map_smul]
/-- When a `prod` node acts on an `add` node in both the LHS and RHS entries,
it can be moved through both `add` nodes. -/
lemma prod_add_both {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(t1 t2 : TensorTree S c) (t3 t4 : TensorTree S c1) :
(prod (add t1 t2) (add t3 t4)).tensor = (add (add (prod t1 t3) (prod t1 t4))
@ -260,11 +291,12 @@ lemma prod_add_both {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
-/
/-- The action of a group element can be brought though a scalar multiplication. -/
/-- An `action` node can be moved through a `smul` node. -/
lemma smul_action {n : ℕ} {c : Fin n → S.C} (g : S.G) (a : S.k) (t : TensorTree S c) :
(smul a (action g t)).tensor = (action g (smul a t)).tensor := by
simp only [smul_tensor, action_tensor, map_smul]
/-- An `action` node can be moved through a `contr` node. -/
lemma contr_action {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ}
{h : c (i.succAbove j) = S.τ (c i)} (g : S.G) (t : TensorTree S c) :
(contr i j h (action g t)).tensor = (action g (contr i j h t)).tensor := by
@ -273,6 +305,7 @@ lemma contr_action {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ}
erw [(S.contrMap c i j h).comm g]
rfl
/-- An `action` node can be moved through a `prod` node when acting on both elements. -/
lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S.G)
(t : TensorTree S c) (t1 : TensorTree S c1) :
(prod (action g t) (action g t1)).tensor = (action g (prod t t1)).tensor := by
@ -290,10 +323,12 @@ lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S.
erw [← (S.F.μ (OverColor.mk c) (OverColor.mk c1)).comm g]
rfl
/-- An `action` node can be moved through a `add` node when acting on both elements. -/
lemma add_action {n : ℕ} {c : Fin n → S.C} (g : S.G) (t t1 : TensorTree S c) :
(add (action g t) (action g t1)).tensor = (action g (add t t1)).tensor := by
simp only [add_tensor, action_tensor, map_add]
/-- An `action` node can be moved through a `perm` node. -/
lemma perm_action {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (g : S.G) (t : TensorTree S c) :
(perm σ (action g t)).tensor = (action g (perm σ t)).tensor := by
@ -302,18 +337,22 @@ lemma perm_action {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
erw [(S.F.map σ).comm g]
rfl
/-- An `action` node can be moved through a `neg` node. -/
lemma neg_action {n : ℕ} {c : Fin n → S.C} (g : S.G) (t : TensorTree S c) :
(neg (action g t)).tensor = (action g (neg t)).tensor := by
simp only [neg_tensor, action_tensor, map_neg]
/-- Two `action` nodes can be combined into a single `action` node. -/
lemma action_action {n : ℕ} {c : Fin n → S.C} (g h : S.G) (t : TensorTree S c) :
(action g (action h t)).tensor = (action (g * h) t).tensor := by
simp only [action_tensor, map_mul, LinearMap.mul_apply]
/-- The `action` node for the identity leaves the tensor invariant. -/
lemma action_id {n : ℕ} {c : Fin n → S.C} (t : TensorTree S c) :
(action 1 t).tensor = t.tensor := by
simp only [action_tensor, map_one, LinearMap.one_apply]
/-- An `action` node on a `constTwoNode` leaves the tensor invariant. -/
lemma action_constTwoNode {c1 c2 : S.C}
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FD.obj (Discrete.mk c1) ⊗ S.FD.obj (Discrete.mk c2))
(g : S.G) : (action g (constTwoNode v)).tensor = (constTwoNode v).tensor := by
@ -327,6 +366,7 @@ lemma action_constTwoNode {c1 c2 : S.C}
erw [← v.comm g]
simp
/-- An `action` node on a `constThreeNode` leaves the tensor invariant. -/
lemma action_constThreeNode {c1 c2 c3 : S.C}
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FD.obj (Discrete.mk c1) ⊗ S.FD.obj (Discrete.mk c2) ⊗
S.FD.obj (Discrete.mk c3))