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

Merge branch 'master' into FeynmanDiagrams

Browse source
This commit is contained in:
jstoobysmith 2024-11-29 05:37:18 +00:00
commit f49f670354
29 changed files with 722 additions and 439 deletions
Download patch file Download diff file Expand all files Collapse all files

47
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,43 +127,41 @@ 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
· rfl
· rename_i k hl
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
have hlt := hl (f ∘ Fin.castSucc)
erw [← hlt]
erw [← hl (f ∘ Fin.castSucc)]
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
· rfl
· rename_i k hl
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
have hlt := hl (f ∘ Fin.castSucc)
erw [← hlt]
erw [← hl (f ∘ Fin.castSucc)]
rfl
end PureU1

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)

314
HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
View file

@ -28,47 +28,53 @@ namespace VectorLikeEvenPlane
lemma n_cond₂ (n : ℕ) : 1 + ((n + n) + 1) = 2 * n.succ := by
linarith
section theδs
/-- The inclusion of `Fin n.succ` into `Fin (n.succ + n.succ)` via the first `n.succ`,
casted into `Fin (2 * n.succ)`. -/
def evenFst (j : Fin n.succ) : Fin (2 * n.succ) :=
Fin.cast (split_equal n.succ) (Fin.castAdd n.succ j)
/-- A helper function for what follows. -/
def δ₁ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.castAdd n.succ j)
/-- The inclusion of `Fin n.succ` into `Fin (n.succ + n.succ)` via the second `n.succ`,
casted into `Fin (2 * n.succ)`. -/
def evenSnd (j : Fin n.succ) : Fin (2 * n.succ) :=
Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j)
/-- A helper function for what follows. -/
def δ₂ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j)
/-- A helper function for what follows. -/
def δ!₁ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
/-- The inclusion of `Fin n` into `Fin (1 + (n + n + 1))` via the first `n`,
casted into `Fin (2 * n.succ)`. -/
def evenShiftFst (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
(Fin.natAdd 1 (Fin.castAdd 1 (Fin.castAdd n j)))
/-- A helper function for what follows. -/
def δ!₂ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
/-- The inclusion of `Fin n` into `Fin (1 + (n + n + 1))` via the second `n`,
casted into `Fin (2 * n.succ)`. -/
def evenShiftSnd (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
(Fin.natAdd 1 (Fin.castAdd 1 (Fin.natAdd n j)))
/-- A helper function for what follows. -/
def δ!₃ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.castAdd ((n + n) + 1) 0))
/-- The element of `Fin (1 + (n + n + 1))` corresponding to the first `1`,
casted into `Fin (2 * n.succ)`. -/
def evenShiftZero : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.castAdd ((n + n) + 1) 0))
/-- A helper function for what follows. -/
def δ!₄ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0)))
/-- The element of `Fin (1 + (n + n + 1))` corresponding to the second `1`,
casted into `Fin (2 * n.succ)`. -/
def evenShiftLast : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0)))
lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ₁ i))
(h2 : ∀ i, S (δ₂ i) = T (δ₂ i)) : S = T := by
lemma ext_even (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (evenFst i) = T (evenFst i))
(h2 : ∀ i, S (evenSnd i) = T (evenSnd i)) : S = T := by
funext i
by_cases hi : i.val < n.succ
· let j : Fin n.succ := ⟨i, hi⟩
have h2 := h1 j
have h3 : δ₁ j = i := rfl
have h3 : evenFst j = i := rfl
rw [h3] at h2
exact h2
· let j : Fin n.succ := ⟨i - n.succ, by omega⟩
have h2 := h2 j
have h3 : δ₂ j = i := by
simp only [succ_eq_add_one, δ₂, Fin.ext_iff, Fin.coe_cast, Fin.coe_natAdd]
have h3 : evenSnd j = i := by
simp only [succ_eq_add_one, evenSnd, Fin.ext_iff, Fin.coe_cast, Fin.coe_natAdd]
omega
rw [h3] at h2
exact h2
lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
lemma sum_even (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ evenFst) i + (S ∘ evenSnd) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
· intro i
@ -77,18 +83,9 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
· intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
· exact fun _ _ => rfl
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = S δ!₃ + S δ!₄ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
lemma sum_evenShift (S : Fin (2 * n.succ) → ℚ) :
∑ i, S i = S evenShiftZero + S evenShiftLast +
∑ i : Fin n, ((S ∘ evenShiftFst) i + (S ∘ evenShiftSnd) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (1 + ((n + n) + 1)), S (Fin.cast (n_cond₂ n) i) := by
rw [Finset.sum_equiv (Fin.castOrderIso (n_cond₂ n)).symm.toEquiv]
· intro i
@ -106,35 +103,33 @@ lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
nth_rewrite 2 [Rat.add_comm]
rfl
lemma δ!₃_δ₁0 : @δ!₃ n = δ₁ 0 := rfl
lemma evenShiftZero_eq_evenFst_zero : @evenShiftZero n = evenFst 0 := rfl
lemma δ!₄_δ₂Last: @δ!₄ n = δ₂ (Fin.last n) := by
lemma evenShiftLast_eq_evenSnd_last: @evenShiftLast n = evenSnd (Fin.last n) := by
rw [Fin.ext_iff]
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.val_eq_zero,
add_zero, δ₂, Fin.natAdd_last, Fin.val_last]
simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd,
Fin.val_eq_zero, add_zero, evenSnd, Fin.natAdd_last, Fin.val_last]
omega
lemma δ!₁_δ₁ (j : Fin n) : δ!₁ j = δ₁ j.succ := by
rw [Fin.ext_iff, δ₁, δ!₁]
lemma evenShiftFst_eq_evenFst_succ (j : Fin n) : evenShiftFst j = evenFst j.succ := by
rw [Fin.ext_iff, evenFst, evenShiftFst]
simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_succ]
ring
lemma δ!₂_δ₂ (j : Fin n) : δ!₂ j = δ₂ j.castSucc := by
rw [Fin.ext_iff, δ₂, δ!₂]
lemma evenShiftSnd_eq_evenSnd_castSucc (j : Fin n) : evenShiftSnd j = evenSnd j.castSucc := by
rw [Fin.ext_iff, evenSnd, evenShiftSnd]
simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.coe_castSucc]
ring_nf
rw [Nat.succ_eq_add_one]
ring
end theδs
/-- The first part of the basis as charges. -/
def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges :=
fun i =>
if i = δ₁ j then
if i = evenFst j then
1
else
if i = δ₂ j then
if i = evenSnd j then
- 1
else
0
@ -142,23 +137,23 @@ def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges :=
/-- The second part of the basis as charges. -/
def basis!AsCharges (j : Fin n) : (PureU1 (2 * n.succ)).Charges :=
fun i =>
if i = δ!₁ j then
if i = evenShiftFst j then
1
else
if i = δ!₂ j then
if i = evenShiftSnd j then
- 1
else
0
lemma basis_on_δ₁_self (j : Fin n.succ) : basisAsCharges j (δ₁ j) = 1 := by
lemma basis_on_evenFst_self (j : Fin n.succ) : basisAsCharges j (evenFst j) = 1 := by
simp [basisAsCharges]
lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by
lemma basis!_on_evenShiftFst_self (j : Fin n) : basis!AsCharges j (evenShiftFst j) = 1 := by
simp [basis!AsCharges]
lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) :
basisAsCharges k (δ₁ j) = 0 := by
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, δ₁, succ_eq_add_one, δ₂]
lemma basis_on_evenFst_other {k j : Fin n.succ} (h : k ≠ j) :
basisAsCharges k (evenFst j) = 0 := by
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, evenFst, evenSnd]
split
· rename_i h1
rw [Fin.ext_iff] at h1
@ -173,20 +168,20 @@ lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) :
omega
· rfl
lemma basis_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) :
basisAsCharges k j = 0 := by
lemma basis_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ evenFst k)
(h2 : j ≠ evenSnd k) : basisAsCharges k j = 0 := by
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ δ!₁ k) (h2 : j ≠ δ!₂ k) :
basis!AsCharges k j = 0 := by
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ evenShiftFst k)
(h2 : j ≠ evenShiftSnd k) : basis!AsCharges k j = 0 := by
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (δ!₁ j) = 0 := by
lemma basis!_on_evenShiftFst_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (evenShiftFst j) = 0 := by
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
simp only [δ!₁, succ_eq_add_one, δ!₂]
simp only [evenShiftFst, succ_eq_add_one, evenShiftSnd]
split
· rename_i h1
rw [Fin.ext_iff] at h1
@ -201,9 +196,9 @@ lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
omega
· rfl
lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, δ₂, δ₁]
lemma basis_evenSnd_eq_neg_evenFst (j i : Fin n.succ) :
basisAsCharges j (evenSnd i) = - basisAsCharges j (evenFst i) := by
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, evenSnd, evenFst]
split <;> split
any_goals split
any_goals rfl
@ -219,9 +214,9 @@ lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
simp_all
all_goals omega
lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges, δ!₂, δ!₁]
lemma basis!_evenShftSnd_eq_neg_evenShiftFst (j i : Fin n) :
basis!AsCharges j (evenShiftSnd i) = - basis!AsCharges j (evenShiftFst i) := by
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges, evenShiftSnd, evenShiftFst]
split <;> split
any_goals split
any_goals split
@ -236,75 +231,76 @@ lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
all_goals simp_all
all_goals omega
lemma basis_on_δ₂_self (j : Fin n.succ) : basisAsCharges j (δ₂ j) = - 1 := by
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self]
lemma basis_on_evenSnd_self (j : Fin n.succ) : basisAsCharges j (evenSnd j) = - 1 := by
rw [basis_evenSnd_eq_neg_evenFst, basis_on_evenFst_self]
lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (δ!₂ j) = - 1 := by
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self]
lemma basis!_on_evenShiftSnd_self (j : Fin n) : basis!AsCharges j (evenShiftSnd j) = - 1 := by
rw [basis!_evenShftSnd_eq_neg_evenShiftFst, basis!_on_evenShiftFst_self]
lemma basis_on_δ₂_other {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (δ₂ j) = 0 := by
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h]
lemma basis_on_evenSnd_other {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (evenSnd j) = 0 := by
rw [basis_evenSnd_eq_neg_evenFst, basis_on_evenFst_other h]
rfl
lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ!₂ j) = 0 := by
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h]
lemma basis!_on_evenShiftSnd_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (evenShiftSnd j) = 0 := by
rw [basis!_evenShftSnd_eq_neg_evenShiftFst, basis!_on_evenShiftFst_other h]
rfl
lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
lemma basis!_on_evenShiftZero (j : Fin n) : basis!AsCharges j evenShiftZero = 0 := by
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
split<;> rename_i h
· simp only [δ!₃, succ_eq_add_one, Fin.isValue, δ!₁, Fin.ext_iff, Fin.coe_cast, Fin.coe_castAdd,
Fin.val_eq_zero, Fin.coe_natAdd] at h
· simp only [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftFst, Fin.ext_iff,
Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, Fin.coe_natAdd] at h
omega
· split <;> rename_i h2
· simp only [δ!₃, succ_eq_add_one, Fin.isValue, δ!₂, Fin.ext_iff, Fin.coe_cast,
Fin.coe_castAdd, Fin.val_eq_zero, Fin.coe_natAdd] at h2
· simp only [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftSnd, Fin.ext_iff,
Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, Fin.coe_natAdd] at h2
omega
· rfl
lemma basis!_on_δ!₄ (j : Fin n) : basis!AsCharges j δ!₄ = 0 := by
lemma basis!_on_evenShiftLast (j : Fin n) : basis!AsCharges j evenShiftLast = 0 := by
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
split <;> rename_i h
· rw [Fin.ext_iff] at h
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.val_eq_zero,
add_zero, δ!₁, Fin.coe_castAdd, add_right_inj] at h
simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd,
Fin.val_eq_zero, add_zero, evenShiftFst, Fin.coe_castAdd, add_right_inj] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.val_eq_zero,
add_zero, δ!₂, Fin.coe_castAdd, add_right_inj] at h2
simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd,
Fin.val_eq_zero, add_zero, evenShiftSnd, Fin.coe_castAdd, add_right_inj] at h2
omega
· rfl
lemma basis_linearACC (j : Fin n.succ) : (accGrav (2 * n.succ)) (basisAsCharges j) = 0 := by
rw [accGrav]
simp only [LinearMap.coe_mk, AddHom.coe_mk]
rw [sum_δ₁_δ₂]
simp [basis_δ₂_eq_minus_δ₁]
rw [sum_even]
simp [basis_evenSnd_eq_neg_evenFst]
lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n.succ)) (basis!AsCharges j) = 0 := by
rw [accGrav]
simp only [LinearMap.coe_mk, AddHom.coe_mk]
rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
simp [basis!_δ!₂_eq_minus_δ!₁]
rw [sum_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast]
simp [basis!_evenShftSnd_eq_neg_evenShiftFst]
lemma basis_accCube (j : Fin n.succ) :
accCube (2 * n.succ) (basisAsCharges j) = 0 := by
rw [accCube_explicit, sum_δ₁_δ₂]
rw [accCube_explicit, sum_even]
apply Finset.sum_eq_zero
intro i _
simp only [succ_eq_add_one, Function.comp_apply, basis_δ₂_eq_minus_δ₁]
simp only [succ_eq_add_one, Function.comp_apply, basis_evenSnd_eq_neg_evenFst]
ring
lemma basis!_accCube (j : Fin n) :
accCube (2 * n.succ) (basis!AsCharges j) = 0 := by
rw [accCube_explicit, sum_δ!₁_δ!₂]
rw [basis!_on_δ!₄, basis!_on_δ!₃]
rw [accCube_explicit, sum_evenShift]
rw [basis!_on_evenShiftLast, basis!_on_evenShiftZero]
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply,
zero_add]
apply Finset.sum_eq_zero
intro i _
simp only [basis!_δ!₂_eq_minus_δ!₁]
simp only [basis!_evenShftSnd_eq_neg_evenShiftFst]
ring
/-- The first part of the basis as `LinSols`. -/
@ -333,22 +329,23 @@ def basisa : (Fin n.succ) ⊕ (Fin n) → (PureU1 (2 * n.succ)).LinSols := fun i
| .inl i => basis i
| .inr i => basis! i
/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/
/-- Swapping the elements evenShiftFst j and evenShiftSnd j is equivalent to
adding a vector basis!AsCharges j. -/
lemma swap!_as_add {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
(hS : ((FamilyPermutations (2 * n.succ)).linSolRep
(pairSwap (δ!₁ j) (δ!₂ j))) S = S') :
S'.val = S.val + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j := by
(pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S') :
S'.val = S.val + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j := by
funext i
rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
by_cases hi : i = δ!₁ j
by_cases hi : i = evenShiftFst j
· subst hi
simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
· by_cases hi2 : i = δ!₂ j
· simp [HSMul.hSMul, hi2, basis!_on_δ!₂_self, pairSwap_inv_snd]
simp [HSMul.hSMul, basis!_on_evenShiftFst_self, pairSwap_inv_fst]
· by_cases hi2 : i = evenShiftSnd j
· simp [HSMul.hSMul, hi2, basis!_on_evenShiftSnd_self, pairSwap_inv_snd]
· simp only [succ_eq_add_one, Equiv.invFun_as_coe, HSMul.hSMul,
ACCSystemCharges.chargesAddCommMonoid_add, ACCSystemCharges.chargesModule_smul]
rw [basis!_on_other hi hi2]
change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
change S.val ((pairSwap (evenShiftFst j) (evenShiftSnd j)).invFun i) =_
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
simp
@ -361,106 +358,107 @@ def P! (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • bas
/-- A point in the span of the basis as a charge. -/
def Pa (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := P f + P! g
lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j := by
lemma P_evenFst (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenFst j) = f j := by
rw [P, sum_of_charges]
simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₁_self]
· rw [basis_on_evenFst_self]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis_on_δ₁_other hkj]
rw [basis_on_evenFst_other hkj]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
lemma P!_evenShiftFst (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftFst j) = f j := by
rw [P!, sum_of_charges]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₁_self]
· rw [basis!_on_evenShiftFst_self]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₁_other hkj]
rw [basis!_on_evenShiftFst_other hkj]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma Pa_δ!₁ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
Pa f g (δ!₁ j) = f j.succ + g j := by
lemma Pa_evenShiftFst (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
Pa f g (evenShiftFst j) = f j.succ + g j := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
rw [P!_δ!₁, δ!₁_δ₁, P_δ₁]
rw [P!_evenShiftFst, evenShiftFst_eq_evenFst_succ, P_evenFst]
lemma P_δ₂ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₂ j) = - f j := by
lemma P_evenSnd (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenSnd j) = - f j := by
rw [P, sum_of_charges]
simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· simp only [basis_on_δ₂_self, mul_neg, mul_one]
· simp only [basis_on_evenSnd_self, mul_neg, mul_one]
· intro k _ hkj
simp only [basis_on_δ₂_other hkj, mul_zero]
simp only [basis_on_evenSnd_other hkj, mul_zero]
· simp
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
lemma P!_evenShiftSnd (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftSnd j) = - f j := by
rw [P!, sum_of_charges]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₂_self]
· rw [basis!_on_evenShiftSnd_self]
exact mul_neg_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₂_other hkj]
rw [basis!_on_evenShiftSnd_other hkj]
exact Rat.mul_zero (f k)
· simp
lemma Pa_δ!₂ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
Pa f g (δ!₂ j) = - f j.castSucc - g j := by
lemma Pa_evenShiftSnd (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
Pa f g (evenShiftSnd j) = - f j.castSucc - g j := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
rw [P!_δ!₂, δ!₂_δ₂, P_δ₂]
rw [P!_evenShiftSnd, evenShiftSnd_eq_evenSnd_castSucc, P_evenSnd]
ring
lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (δ!₃) = 0 := by
lemma P!_evenShiftZero (f : Fin n → ℚ) : P! f (evenShiftZero) = 0 := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃]
simp [HSMul.hSMul, SMul.smul, basis!_on_evenShiftZero]
lemma Pa_δ!₃ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₃) = f 0 := by
lemma Pa_evenShitZero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (evenShiftZero) = f 0 := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
rw [P!_δ!₃, δ!₃_δ₁0, P_δ₁]
rw [P!_evenShiftZero, evenShiftZero_eq_evenFst_zero, P_evenFst]
exact Rat.add_zero (f 0)
lemma P!_δ!₄ (f : Fin n → ℚ) : P! f (δ!₄) = 0 := by
lemma P!_evenShiftLast (f : Fin n → ℚ) : P! f (evenShiftLast) = 0 := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₄]
simp [HSMul.hSMul, SMul.smul, basis!_on_evenShiftLast]
lemma Pa_δ!₄ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₄) = - f (Fin.last n) := by
lemma Pa_evenShiftLast (f : Fin n.succ → ℚ) (g : Fin n → ℚ) :
Pa f g (evenShiftLast) = - f (Fin.last n) := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
rw [P!_δ!₄, δ!₄_δ₂Last, P_δ₂]
rw [P!_evenShiftLast, evenShiftLast_eq_evenSnd_last, P_evenSnd]
exact Rat.add_zero (-f (Fin.last n))
lemma P_δ₁_δ₂ (f : Fin n.succ → ℚ) : P f ∘ δ₂ = - P f ∘ δ₁ := by
lemma P_evenSnd_evenFst (f : Fin n.succ → ℚ) : P f ∘ evenSnd = - P f ∘ evenFst := by
funext j
simp only [PureU1_numberCharges, Function.comp_apply, Pi.neg_apply]
rw [P_δ₁, P_δ₂]
rw [P_evenFst, P_evenSnd]
lemma P_linearACC (f : Fin n.succ → ℚ) : (accGrav (2 * n.succ)) (P f) = 0 := by
rw [accGrav]
simp only [LinearMap.coe_mk, AddHom.coe_mk]
rw [sum_δ₁_δ₂]
simp [P_δ₂, P_δ₁]
rw [sum_even]
simp [P_evenSnd, P_evenFst]
lemma P_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (P f) = 0 := by
rw [accCube_explicit, sum_δ₁_δ₂]
rw [accCube_explicit, sum_even]
apply Finset.sum_eq_zero
intro i _
simp only [succ_eq_add_one, Function.comp_apply, P_δ₁, P_δ₂]
simp only [succ_eq_add_one, Function.comp_apply, P_evenFst, P_evenSnd]
ring
lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by
rw [accCube_explicit, sum_δ!₁_δ!₂, P!_δ!₃, P!_δ!₄]
rw [accCube_explicit, sum_evenShift, P!_evenShiftZero, P!_evenShiftLast]
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply,
zero_add]
apply Finset.sum_eq_zero
intro i _
simp only [P!_δ!₁, P!_δ!₂]
simp only [P!_evenShiftFst, P!_evenShiftSnd]
ring
lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
@ -468,47 +466,47 @@ lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
= g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by
simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges,
TriLinearSymm.mk₃_toFun_apply_apply]
rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
rw [sum_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast]
simp only [mul_zero, add_zero, Function.comp_apply, zero_add]
rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
· simp only [δ!₁_δ₁, mul_one, δ!₂_δ₂, mul_neg]
rw [P_δ₁, P_δ₂]
rw [Finset.sum_eq_single j, basis!_on_evenShiftFst_self, basis!_on_evenShiftSnd_self]
· simp only [evenShiftFst_eq_evenFst_succ, mul_one, evenShiftSnd_eq_evenSnd_castSucc, mul_neg]
rw [P_evenFst, P_evenSnd]
ring
· intro k _ hkj
erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
erw [basis!_on_evenShiftFst_other hkj.symm, basis!_on_evenShiftSnd_other hkj.symm]
simp only [mul_zero, add_zero]
· simp
lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) :
accCubeTriLinSymm (P! g) (P! g) (basisAsCharges j)
= (P! g (δ₁ j))^2 - (P! g (δ₂ j))^2 := by
= (P! g (evenFst j))^2 - (P! g (evenSnd j))^2 := by
simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges,
TriLinearSymm.mk₃_toFun_apply_apply]
rw [sum_δ₁_δ₂]
rw [sum_even]
simp only [Function.comp_apply]
rw [Finset.sum_eq_single j, basis_on_δ₁_self, basis_on_δ₂_self]
rw [Finset.sum_eq_single j, basis_on_evenFst_self, basis_on_evenSnd_self]
· simp only [mul_one, mul_neg]
ring
· intro k _ hkj
erw [basis_on_δ₁_other hkj.symm, basis_on_δ₂_other hkj.symm]
erw [basis_on_evenFst_other hkj.symm, basis_on_evenSnd_other hkj.symm]
simp only [mul_zero, add_zero]
· simp
lemma P_zero (f : Fin n.succ → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
intro i
erw [← P_δ₁ f]
erw [← P_evenFst f]
rw [h]
rfl
lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by
intro i
rw [← P!_δ!₁ f]
rw [← P!_evenShiftFst f]
rw [h]
rfl
lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
∀ i, f i = 0 := by
have h₃ := Pa_δ!₃ f g
have h₃ := Pa_evenShitZero f g
rw [h] at h₃
change 0 = f 0 at h₃
intro i
@ -518,8 +516,8 @@ lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
rename_i iv hi
have hivi : iv < n.succ := lt_of_succ_lt hiv
have hi2 := hi hivi
have h1 := Pa_δ!₁ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
have h2 := Pa_δ!₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
have h1 := Pa_evenShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
have h2 := Pa_evenShiftSnd f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
rw [h] at h1 h2
simp only [Fin.succ_mk, succ_eq_add_one, Fin.castSucc_mk] at h1 h2
erw [hi2] at h2
@ -679,7 +677,7 @@ lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range ba
rfl
lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin n) :
(S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈
(S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∈
Submodule.span ℚ (Set.range basis!AsCharges) := by
apply Submodule.smul_mem
apply SetLike.mem_of_subset
@ -688,11 +686,11 @@ lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin
lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
(hS : ((FamilyPermutations (2 * n.succ)).linSolRep
(pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ)
(pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ)
(h : S.val = P g + P! f) : ∃ (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ),
S'.val = P g' + P! f' ∧ P! f' = P! f +
(S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by
let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j
(S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = g := by
let X := P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j
have hX : X ∈ Submodule.span ℚ (Set.range (basis!AsCharges)) := by
apply Submodule.add_mem
exact (P!_in_span f)
@ -715,20 +713,20 @@ lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols)
use (Tuple.sort S.val).symm
change sortAFL S ∈ Submodule.span ℚ (Set.range basis)
rw [mem_span_range_iff_exists_fun ℚ]
let f : Fin n.succ → ℚ := fun i => (sortAFL S).val (δ₁ i)
let f : Fin n.succ → ℚ := fun i => (sortAFL S).val (evenFst i)
use f
apply ACCSystemLinear.LinSols.ext
rw [sortAFL_val]
erw [P'_val]
apply ext_δ
apply ext_even
· intro i
rw [P_δ₁]
rw [P_evenFst]
rfl
· intro i
rw [P_δ₂]
rw [P_evenSnd]
have ht := hS i
change sort S.val (δ₁ i) = - sort S.val (δ₂ i) at ht
have h : sort S.val (δ₂ i) = - sort S.val (δ₁ i) := by
change sort S.val (evenFst i) = - sort S.val (evenSnd i) at ht
have h : sort S.val (evenSnd i) = - sort S.val (evenFst i) := by
rw [ht]
ring
rw [h]

46
HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
View file

@ -91,15 +91,18 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols}
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
(LIC : LineInCubicPerm S) :
∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f),
(S.val (δ!₂ j) - S.val (δ!₁ j))
(S.val (evenShiftSnd j) - S.val (evenShiftFst j))
* accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
intro j g f h
let S' := (FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j)) S
have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl
let S' := (FamilyPermutations (2 * n.succ)).linSolRep
(pairSwap (evenShiftFst j) (evenShiftSnd j)) S
have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep
(pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S' := rfl
obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h
have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h
have h2 := line_in_cubic_P_P_P!
(lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1
(lineInCubicPerm_self (lineInCubicPerm_permute LIC
(pairSwap (evenShiftFst j) (evenShiftSnd j)))) g' f' hall.1
rw [hall.2.1, hall.2.2] at h2
rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2
simpa using h2
@ -107,20 +110,22 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
(f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) :
accCubeTriLinSymm (P f) (P f) (basis!AsCharges (Fin.last n)) =
- (S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) * (2 * S.val δ!₄ +
S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) := by
- (S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
(2 * S.val evenShiftLast +
S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) := by
rw [P_P_P!_accCube f (Fin.last n)]
have h1 := Pa_δ!₄ f g
have h2 := Pa_δ!₁ f g (Fin.last n)
have h3 := Pa_δ!₂ f g (Fin.last n)
have h1 := Pa_evenShiftLast f g
have h2 := Pa_evenShiftFst f g (Fin.last n)
have h3 := Pa_evenShiftSnd f g (Fin.last n)
simp only [Fin.succ_last, Nat.succ_eq_add_one] at h1 h2 h3
have hl : f (Fin.succ (Fin.last n)) = - Pa f g δ!₄ := by
have hl : f (Fin.succ (Fin.last n)) = - Pa f g evenShiftLast := by
simp_all only [Fin.succ_last, neg_neg]
erw [hl] at h2
have hg : g (Fin.last n) = Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄ := by
have hg : g (Fin.last n) = Pa f g (evenShiftFst (Fin.last n)) + Pa f g evenShiftLast := by
linear_combination -(1 * h2)
have hll : f (Fin.castSucc (Fin.last n)) =
- (Pa f g (δ!₂ (Fin.last n)) + Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄) := by
- (Pa f g (evenShiftSnd (Fin.last n)) + Pa f g (evenShiftFst (Fin.last n))
+ Pa f g evenShiftLast) := by
linear_combination h3 - 1 * hg
rw [← hS] at hl hll
rw [hl, hll]
@ -129,7 +134,8 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
(LIC : LineInCubicPerm S) :
LineInPlaneProp
((S.val (δ!₂ (Fin.last n))), ((S.val (δ!₁ (Fin.last n))), (S.val δ!₄))) := by
((S.val (evenShiftSnd (Fin.last n))), ((S.val (evenShiftFst (Fin.last n))),
(S.val evenShiftLast))) := by
obtain ⟨g, f, hfg⟩ := span_basis S
have h1 := lineInCubicPerm_swap LIC (Fin.last n) g f hfg
rw [P_P_P!_accCube' g f hfg] at h1
@ -144,12 +150,14 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ)).LinSols}
(LIC : LineInCubicPerm S) : LineInPlaneCond S := by
refine @Prop_three (2 * n.succ.succ) LineInPlaneProp S (δ!₂ (Fin.last n)) (δ!₁ (Fin.last n))
δ!₄ ?_ ?_ ?_ ?_
· simp [Fin.ext_iff, δ!₂, δ!₁]
· simp [Fin.ext_iff, δ!₂, δ!₄]
· simp only [Nat.succ_eq_add_one, δ!₁, δ!₄, Fin.isValue, ne_eq, Fin.ext_iff, Fin.coe_cast,
Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_last, Fin.val_eq_zero, add_zero, add_right_inj]
refine @Prop_three (2 * n.succ.succ) LineInPlaneProp S
(evenShiftSnd (Fin.last n)) (evenShiftFst (Fin.last n))
evenShiftLast ?_ ?_ ?_ ?_
· simp [Fin.ext_iff, evenShiftSnd, evenShiftFst]
· simp [Fin.ext_iff, evenShiftSnd, evenShiftLast]
· simp only [Nat.succ_eq_add_one, evenShiftFst, evenShiftLast, Fin.isValue, ne_eq, Fin.ext_iff,
Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_last, Fin.val_eq_zero, add_zero,
add_right_inj]
omega
· exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)

329
HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
View file

@ -25,93 +25,105 @@ variable {n : ℕ}
namespace VectorLikeOddPlane
lemma split_odd! (n : ℕ) : (1 + n) + n = 2 * n +1 := by
lemma odd_shift_eq (n : ℕ) : (1 + n) + n = 2 * n +1 := by
omega
lemma split_adda (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by
lemma odd_shift_shift_eq (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by
omega
section theDeltas
/-- A helper function for what follows. -/
def δ₁ (j : Fin n) : Fin (2 * n + 1) :=
/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the first `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def oddFst (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd n) (Fin.castAdd n (Fin.castAdd 1 j))
/-- A helper function for what follows. -/
def δ₂ (j : Fin n) : Fin (2 * n + 1) :=
/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the second `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def oddSnd (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd n) (Fin.natAdd (n+1) j)
/-- A helper function for what follows. -/
def δ₃ : Fin (2 * n + 1) :=
/-- The element representing `1` in `Fin ((n + 1) + n)`.
This is then casted to `Fin (2 * n + 1)`. -/
def oddMid : Fin (2 * n + 1) :=
Fin.cast (split_odd n) (Fin.castAdd n (Fin.natAdd n 1))
/-- A helper function for what follows. -/
def δ!₁ (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd! n) (Fin.castAdd n (Fin.natAdd 1 j))
/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the first `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def oddShiftFst (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (odd_shift_eq n) (Fin.castAdd n (Fin.natAdd 1 j))
/-- A helper function for what follows. -/
def δ!₂ (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd! n) (Fin.natAdd (1 + n) j)
/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the second `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def oddShiftSnd (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (odd_shift_eq n) (Fin.natAdd (1 + n) j)
/-- A helper function for what follows. -/
def δ!₃ : Fin (2 * n + 1) :=
Fin.cast (split_odd! n) (Fin.castAdd n (Fin.castAdd n 1))
/-- The element representing the `1` in `Fin (1 + n + n)`.
This is then casted to `Fin (2 * n + 1)`. -/
def oddShiftZero : Fin (2 * n + 1) :=
Fin.cast (odd_shift_eq n) (Fin.castAdd n (Fin.castAdd n 1))
/-- A helper function for what follows. -/
def δa₁ : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))
/-- The element representing the first `1` in `Fin (1 + n + 1 + n.succ)` casted
to `Fin (2 * n.succ + 1)`. -/
def oddShiftShiftZero : Fin (2 * n.succ + 1) :=
Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))
/-- A helper function for what follows. -/
def δa₂ (j : Fin n) : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))
/-- The inclusion of `Fin n` into `Fin (1 + n + 1 + n.succ)` via the first `n` and casted
to `Fin (2 * n.succ + 1)`. -/
def oddShiftShiftFst (j : Fin n) : Fin (2 * n.succ + 1) :=
Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))
/-- A helper function for what follows. -/
def δa₃ : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1))
/-- The element representing the second `1` in `Fin (1 + n + 1 + n.succ)` casted
to `2 * n.succ + 1`. -/
def oddShiftShiftMid : Fin (2 * n.succ + 1) :=
Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1))
/-- A helper function for what follows. -/
def δa₄ (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.natAdd ((1+n)+1) j)
/-- The inclusion of `Fin n.succ` into `Fin (1 + n + 1 + n.succ)` via the `n.succ` and casted
to `Fin (2 * n.succ + 1)`. -/
def oddShiftShiftSnd (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
Fin.cast (odd_shift_shift_eq n) (Fin.natAdd ((1+n)+1) j)
lemma δa₁_δ₁ : @δa₁ n = δ₁ 0 := by
exact Fin.rev_inj.mp rfl
lemma oddShiftShiftZero_eq_oddFst_zero : @oddShiftShiftZero n = oddFst 0 :=
Fin.rev_inj.mp rfl
lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by
rfl
lemma oddShiftShiftZero_eq_oddShiftZero : @oddShiftShiftZero n = oddShiftZero := rfl
lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by
lemma oddShiftShiftFst_eq_oddFst_succ (j : Fin n) :
oddShiftShiftFst j = oddFst j.succ := by
rw [Fin.ext_iff]
simp only [succ_eq_add_one, δa₂, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, δ₁, Fin.val_succ]
simp only [succ_eq_add_one, oddShiftShiftFst, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd,
oddFst, Fin.val_succ]
exact Nat.add_comm 1 ↑j
lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
lemma oddShiftShiftFst_eq_oddShiftFst_castSucc (j : Fin n) :
oddShiftShiftFst j = oddShiftFst j.castSucc := by
rfl
lemma δa₃_δ₃ : @δa₃ n = δ₃ := by
lemma oddShiftShiftMid_eq_oddMid : @oddShiftShiftMid n = oddMid := by
rw [Fin.ext_iff]
simp only [succ_eq_add_one, δa₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd,
Fin.val_eq_zero, add_zero, δ₃]
simp only [succ_eq_add_one, oddShiftShiftMid, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd,
Fin.coe_natAdd, Fin.val_eq_zero, add_zero, oddMid]
exact Nat.add_comm 1 n
lemma δa₃_δ!₁ : δa₃ = δ!₁ (Fin.last n) := by
lemma oddShiftShiftMid_eq_oddShiftFst_last : oddShiftShiftMid = oddShiftFst (Fin.last n) := by
rfl
lemma δa₄_δ₂ (j : Fin n.succ) : δa₄ j = δ₂ j := by
lemma oddShiftShiftSnd_eq_oddSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddSnd j := by
rw [Fin.ext_iff]
simp only [succ_eq_add_one, δa₄, Fin.coe_cast, Fin.coe_natAdd, δ₂, add_left_inj]
simp only [succ_eq_add_one, oddShiftShiftSnd, Fin.coe_cast, Fin.coe_natAdd, oddSnd, add_left_inj]
exact Nat.add_comm 1 n
lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by
lemma oddShiftShiftSnd_eq_oddShiftSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddShiftSnd j := by
rw [Fin.ext_iff]
rfl
lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by
lemma oddSnd_eq_oddShiftSnd (j : Fin n) : oddSnd j = oddShiftSnd j := by
rw [Fin.ext_iff]
simp only [δ₂, Fin.coe_cast, Fin.coe_natAdd, δ!₂, add_left_inj]
simp only [oddSnd, Fin.coe_cast, Fin.coe_natAdd, oddShiftSnd, add_left_inj]
exact Nat.add_comm n 1
lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
∑ i, S i = S δ₃ + ∑ i : Fin n, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
lemma sum_odd (S : Fin (2 * n + 1) → ℚ) :
∑ i, S i = S oddMid + ∑ i : Fin n, ((S ∘ oddFst) i + (S ∘ oddSnd) i) := by
have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) := by
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd n)).symm.toEquiv]
· intro i
@ -125,10 +137,10 @@ lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
rw [Finset.sum_add_distrib]
rfl
lemma sum_δ! (S : Fin (2 * n + 1) → ℚ) :
∑ i, S i = S δ!₃ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (split_odd! n) i) := by
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd! n)).symm.toEquiv]
lemma sum_oddShift (S : Fin (2 * n + 1) → ℚ) :
∑ i, S i = S oddShiftZero + ∑ i : Fin n, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i) := by
have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (odd_shift_eq n) i) := by
rw [Finset.sum_equiv (Fin.castOrderIso (odd_shift_eq n)).symm.toEquiv]
· intro i
simp only [mem_univ, Fin.castOrderIso, RelIso.coe_fn_toEquiv]
· exact fun _ _ => rfl
@ -144,10 +156,10 @@ section theBasisVectors
/-- The first part of the basis as charge assignments. -/
def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
fun i =>
if i = δ₁ j then
if i = oddFst j then
1
else
if i = δ₂ j then
if i = oddSnd j then
- 1
else
0
@ -155,24 +167,24 @@ def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
/-- The second part of the basis as charge assignments. -/
def basis!AsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
fun i =>
if i = δ!₁ j then
if i = oddShiftFst j then
1
else
if i = δ!₂ j then
if i = oddShiftSnd j then
- 1
else
0
lemma basis_on_δ₁_self (j : Fin n) : basisAsCharges j (δ₁ j) = 1 := by
lemma basis_on_oddFst_self (j : Fin n) : basisAsCharges j (oddFst j) = 1 := by
simp [basisAsCharges]
lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by
lemma basis!_on_oddShiftFst_self (j : Fin n) : basis!AsCharges j (oddShiftFst j) = 1 := by
simp [basis!AsCharges]
lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
basisAsCharges k (δ₁ j) = 0 := by
lemma basis_on_oddFst_other {k j : Fin n} (h : k ≠ j) :
basisAsCharges k (oddFst j) = 0 := by
simp only [basisAsCharges, PureU1_numberCharges]
simp only [δ₁, δ₂]
simp only [oddFst, oddSnd]
split
· rename_i h1
rw [Fin.ext_iff] at h1
@ -187,10 +199,10 @@ lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
omega
· rfl
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (δ!₁ j) = 0 := by
lemma basis!_on_oddShiftFst_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (oddShiftFst j) = 0 := by
simp only [basis!AsCharges, PureU1_numberCharges]
simp only [δ!₁, δ!₂]
simp only [oddShiftFst, oddShiftSnd]
split
· rename_i h1
rw [Fin.ext_iff] at h1
@ -205,19 +217,20 @@ lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
omega
rfl
lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) :
lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddFst k) (h2 : j ≠ oddSnd k) :
basisAsCharges k j = 0 := by
simp only [basisAsCharges, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ!₁ k) (h2 : j ≠ δ!₂ k) :
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n + 1)}
(h1 : j ≠ oddShiftFst k) (h2 : j ≠ oddShiftSnd k) :
basis!AsCharges k j = 0 := by
simp only [basis!AsCharges, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) :
basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by
simp only [basisAsCharges, PureU1_numberCharges, δ₂, δ₁]
lemma basis_oddSnd_eq_minus_oddFst (j i : Fin n) :
basisAsCharges j (oddSnd i) = - basisAsCharges j (oddFst i) := by
simp only [basisAsCharges, PureU1_numberCharges, oddSnd, oddFst]
split <;> split
any_goals split
any_goals split
@ -230,9 +243,9 @@ lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) :
all_goals simp_all
all_goals omega
lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by
simp only [basis!AsCharges, PureU1_numberCharges, δ!₂, δ!₁]
lemma basis!_oddShiftSnd_eq_minus_oddShiftFst (j i : Fin n) :
basis!AsCharges j (oddShiftSnd i) = - basis!AsCharges j (oddShiftFst i) := by
simp only [basis!AsCharges, PureU1_numberCharges, oddShiftSnd, oddShiftFst]
split <;> split
any_goals split
any_goals split
@ -247,59 +260,60 @@ lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
all_goals simp_all
all_goals omega
lemma basis_on_δ₂_self (j : Fin n) : basisAsCharges j (δ₂ j) = - 1 := by
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self]
lemma basis_on_oddSnd_self (j : Fin n) : basisAsCharges j (oddSnd j) = - 1 := by
rw [basis_oddSnd_eq_minus_oddFst, basis_on_oddFst_self]
lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (δ!₂ j) = - 1 := by
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self]
lemma basis!_on_oddShiftSnd_self (j : Fin n) : basis!AsCharges j (oddShiftSnd j) = - 1 := by
rw [basis!_oddShiftSnd_eq_minus_oddShiftFst, basis!_on_oddShiftFst_self]
lemma basis_on_δ₂_other {k j : Fin n} (h : k ≠ j) : basisAsCharges k (δ₂ j) = 0 := by
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h]
lemma basis_on_oddSnd_other {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddSnd j) = 0 := by
rw [basis_oddSnd_eq_minus_oddFst, basis_on_oddFst_other h]
rfl
lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ!₂ j) = 0 := by
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h]
lemma basis!_on_oddShiftSnd_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (oddShiftSnd j) = 0 := by
rw [basis!_oddShiftSnd_eq_minus_oddShiftFst, basis!_on_oddShiftFst_other h]
rfl
lemma basis_on_δ₃ (j : Fin n) : basisAsCharges j δ₃ = 0 := by
lemma basis_on_oddMid (j : Fin n) : basisAsCharges j oddMid = 0 := by
simp only [basisAsCharges, PureU1_numberCharges]
split <;> rename_i h
· rw [Fin.ext_iff] at h
simp only [δ₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, Fin.val_eq_zero,
add_zero, δ₁] at h
simp only [oddMid, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, Fin.val_eq_zero,
add_zero, oddFst] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp only [δ₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, Fin.val_eq_zero,
add_zero, δ₂] at h2
simp only [oddMid, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd,
Fin.val_eq_zero, add_zero, oddSnd] at h2
omega
· rfl
lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
lemma basis!_on_oddShiftZero (j : Fin n) : basis!AsCharges j oddShiftZero = 0 := by
simp only [basis!AsCharges, PureU1_numberCharges]
split <;> rename_i h
· rw [Fin.ext_iff] at h
simp only [δ!₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, δ!₁,
Fin.coe_natAdd] at h
simp only [oddShiftZero, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero,
oddShiftFst, Fin.coe_natAdd] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp only [δ!₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, δ!₂,
Fin.coe_natAdd] at h2
simp only [oddShiftZero, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero,
oddShiftSnd, Fin.coe_natAdd] at h2
omega
· rfl
lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := by
rw [accGrav]
simp only [LinearMap.coe_mk, AddHom.coe_mk]
erw [sum_δ]
simp [basis_δ₂_eq_minus_δ₁, basis_on_δ₃]
erw [sum_odd]
simp [basis_oddSnd_eq_minus_oddFst, basis_on_oddMid]
lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basis!AsCharges j) = 0 := by
rw [accGrav]
simp only [LinearMap.coe_mk, AddHom.coe_mk]
rw [sum_δ!, basis!_on_δ!₃]
simp [basis!_δ!₂_eq_minus_δ!₁]
rw [sum_oddShift, basis!_on_oddShiftZero]
simp [basis!_oddShiftSnd_eq_minus_oddShiftFst]
/-- The first part of the basis as `LinSols`. -/
@[simps!]
@ -329,23 +343,24 @@ def basisa : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols := fun i =>
end theBasisVectors
/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/
/-- Swapping the elements oddShiftFst j and oddShiftSnd j is equivalent to adding a vector
basis!AsCharges j. -/
lemma swap!_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n)
(hS : ((FamilyPermutations (2 * n + 1)).linSolRep
(pairSwap (δ!₁ j) (δ!₂ j))) S = S') :
S'.val = S.val + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j := by
(pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S') :
S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j := by
funext i
rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
by_cases hi : i = δ!₁ j
by_cases hi : i = oddShiftFst j
· subst hi
simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
· by_cases hi2 : i = δ!₂ j
simp [HSMul.hSMul, basis!_on_oddShiftFst_self, pairSwap_inv_fst]
· by_cases hi2 : i = oddShiftSnd j
· subst hi2
simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
simp [HSMul.hSMul,basis!_on_oddShiftSnd_self, pairSwap_inv_snd]
· simp only [Equiv.invFun_as_coe, HSMul.hSMul, ACCSystemCharges.chargesAddCommMonoid_add,
ACCSystemCharges.chargesModule_smul]
rw [basis!_on_other hi hi2]
change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
change S.val ((pairSwap (oddShiftFst j) (oddShiftSnd j)).invFun i) =_
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
simp
@ -358,146 +373,148 @@ def P! (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basi
/-- A point in the span of the basis as a charge. -/
def Pa (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := P f + P! g
lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
lemma P_oddFst (f : Fin n → ℚ) (j : Fin n) : P f (oddFst j) = f j := by
rw [P, sum_of_charges]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₁_self]
· rw [basis_on_oddFst_self]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis_on_δ₁_other hkj]
rw [basis_on_oddFst_other hkj]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
lemma P!_oddShiftFst (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftFst j) = f j := by
rw [P!, sum_of_charges]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₁_self]
· rw [basis!_on_oddShiftFst_self]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₁_other hkj]
rw [basis!_on_oddShiftFst_other hkj]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
lemma P_oddSnd (f : Fin n → ℚ) (j : Fin n) : P f (oddSnd j) = - f j := by
rw [P, sum_of_charges]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₂_self]
· rw [basis_on_oddSnd_self]
exact mul_neg_one (f j)
· intro k _ hkj
rw [basis_on_δ₂_other hkj]
rw [basis_on_oddSnd_other hkj]
exact Rat.mul_zero (f k)
· simp
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
lemma P!_oddShiftSnd (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftSnd j) = - f j := by
rw [P!, sum_of_charges]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₂_self]
· rw [basis!_on_oddShiftSnd_self]
exact mul_neg_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₂_other hkj]
rw [basis!_on_oddShiftSnd_other hkj]
exact Rat.mul_zero (f k)
· simp
lemma P_δ₃ (f : Fin n → ℚ) : P f (δ₃) = 0 := by
lemma P_oddMid (f : Fin n → ℚ) : P f (oddMid) = 0 := by
rw [P, sum_of_charges]
simp [HSMul.hSMul, SMul.smul, basis_on_δ₃]
simp [HSMul.hSMul, SMul.smul, basis_on_oddMid]
lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (δ!₃) = 0 := by
lemma P!_oddShiftZero (f : Fin n → ℚ) : P! f (oddShiftZero) = 0 := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃]
simp [HSMul.hSMul, SMul.smul, basis!_on_oddShiftZero]
lemma Pa_δa₁ (f g : Fin n.succ → ℚ) : Pa f g δa₁ = f 0 := by
lemma Pa_oddShiftShiftZero (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftZero = f 0 := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
nth_rewrite 1 [δa₁_δ₁]
rw [δa₁_δ!₃]
rw [P_δ₁, P!_δ!₃]
nth_rewrite 1 [oddShiftShiftZero_eq_oddFst_zero]
rw [oddShiftShiftZero_eq_oddShiftZero]
rw [P_oddFst, P!_oddShiftZero]
exact Rat.add_zero (f 0)
lemma Pa_δa₂ (f g : Fin n.succ → ℚ) (j : Fin n) : Pa f g (δa₂ j) = f j.succ + g j.castSucc := by
lemma Pa_oddShiftShiftFst (f g : Fin n.succ → ℚ) (j : Fin n) :
Pa f g (oddShiftShiftFst j) = f j.succ + g j.castSucc := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
nth_rewrite 1 [δa₂_δ₁]
rw [δa₂_δ!₁]
rw [P_δ₁, P!_δ!₁]
nth_rewrite 1 [oddShiftShiftFst_eq_oddFst_succ]
rw [oddShiftShiftFst_eq_oddShiftFst_castSucc]
rw [P_oddFst, P!_oddShiftFst]
lemma Pa_δa₃ (f g : Fin n.succ → ℚ) : Pa f g (δa₃) = g (Fin.last n) := by
lemma Pa_oddShiftShiftMid (f g : Fin n.succ → ℚ) : Pa f g (oddShiftShiftMid) = g (Fin.last n) := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
nth_rewrite 1 [δa₃_δ₃]
rw [δa₃_δ!₁]
rw [P_δ₃, P!_δ!₁]
nth_rewrite 1 [oddShiftShiftMid_eq_oddMid]
rw [oddShiftShiftMid_eq_oddShiftFst_last]
rw [P_oddMid, P!_oddShiftFst]
exact Rat.zero_add (g (Fin.last n))
lemma Pa_δa₄ (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (δa₄ j) = - f j - g j := by
lemma Pa_oddShiftShiftSnd (f g : Fin n.succ → ℚ) (j : Fin n.succ) :
Pa f g (oddShiftShiftSnd j) = - f j - g j := by
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
nth_rewrite 1 [δa₄_δ₂]
rw [δa₄_δ!₂]
rw [P_δ₂, P!_δ!₂]
nth_rewrite 1 [oddShiftShiftSnd_eq_oddSnd]
rw [oddShiftShiftSnd_eq_oddShiftSnd]
rw [P_oddSnd, P!_oddShiftSnd]
ring
lemma P_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P f) = 0 := by
rw [accGrav]
simp only [LinearMap.coe_mk, AddHom.coe_mk]
rw [sum_δ]
simp [P_δ₂, P_δ₁, P_δ₃]
rw [sum_odd]
simp [P_oddSnd, P_oddFst, P_oddMid]
lemma P!_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P! f) = 0 := by
rw [accGrav]
simp only [LinearMap.coe_mk, AddHom.coe_mk]
rw [sum_δ!]
simp [P!_δ!₂, P!_δ!₁, P!_δ!₃]
rw [sum_oddShift]
simp [P!_oddShiftSnd, P!_oddShiftFst, P!_oddShiftZero]
lemma P_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P f) = 0 := by
rw [accCube_explicit, sum_δ, P_δ₃]
rw [accCube_explicit, sum_odd, P_oddMid]
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]
apply Finset.sum_eq_zero
intro i _
simp only [P_δ₁, P_δ₂]
simp only [P_oddFst, P_oddSnd]
ring
lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by
rw [accCube_explicit, sum_δ!, P!_δ!₃]
rw [accCube_explicit, sum_oddShift, P!_oddShiftZero]
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]
apply Finset.sum_eq_zero
intro i _
simp only [P!_δ!₁, P!_δ!₂]
simp only [P!_oddShiftFst, P!_oddShiftSnd]
ring
lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)
= (P g (δ!₁ j))^2 - (g j)^2 := by
= (P g (oddShiftFst j))^2 - (g j)^2 := by
simp only [accCubeTriLinSymm, PureU1Charges_numberCharges, TriLinearSymm.mk₃_toFun_apply_apply]
rw [sum_δ!, basis!_on_δ!₃]
rw [sum_oddShift, basis!_on_oddShiftZero]
simp only [mul_zero, Function.comp_apply, zero_add]
rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
· rw [← δ₂_δ!₂, P_δ₂]
rw [Finset.sum_eq_single j, basis!_on_oddShiftFst_self, basis!_on_oddShiftSnd_self]
· rw [← oddSnd_eq_oddShiftSnd, P_oddSnd]
ring
· intro k _ hkj
erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
erw [basis!_on_oddShiftFst_other hkj.symm, basis!_on_oddShiftSnd_other hkj.symm]
simp only [mul_zero, add_zero]
· simp
lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
intro i
erw [← P_δ₁ f]
erw [← P_oddFst f]
rw [h]
rfl
lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by
intro i
rw [← P!_δ!₁ f]
rw [← P!_oddShiftFst f]
rw [h]
rfl
lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
∀ i, f i = 0 := by
have h₃ := Pa_δa₁ f g
have h₃ := Pa_oddShiftShiftZero f g
rw [h] at h₃
change 0 = _ at h₃
simp only at h₃
@ -508,11 +525,11 @@ lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
rename_i iv hi
have hivi : iv < n.succ := lt_of_succ_lt hiv
have hi2 := hi hivi
have h1 := Pa_δa₄ f g ⟨iv, hivi⟩
have h1 := Pa_oddShiftShiftSnd f g ⟨iv, hivi⟩
rw [h, hi2] at h1
change 0 = _ at h1
simp only [neg_zero, succ_eq_add_one, zero_sub, zero_eq_neg] at h1
have h2 := Pa_δa₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
have h2 := Pa_oddShiftShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
simp only [succ_eq_add_one, h, Fin.succ_mk, Fin.castSucc_mk, h1, add_zero] at h2
exact h2.symm
exact hinduc i.val i.prop
@ -668,16 +685,16 @@ lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) :
lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)
(hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
(pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g f : Fin n.succ → ℚ) (hS1 : S.val = P g + P! f) :
∃ (g' f' : Fin n.succ → ℚ),
(pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S') (g f : Fin n.succ → ℚ)
(hS1 : S.val = P g + P! f) : ∃ (g' f' : Fin n.succ → ℚ),
S'.val = P g' + P! f' ∧ P! f' = P! f +
(S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by
let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j
(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g := by
let X := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j
have hf : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by
rw [(mem_span_range_iff_exists_fun ℚ)]
use f
rfl
have hP : (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈
have hP : (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈
Submodule.span ℚ (Set.range basis!AsCharges) := by
apply Submodule.smul_mem
apply SetLike.mem_of_subset

41
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -40,6 +40,9 @@ def LineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ),
accCube (2 * n + 1) (a • P g + b • P! f) = 0
/-- The condition that a linear solution sits on a line between the two planes
within the cubic expands into a on `accCubeTriLinSymm` applied to the points
within the planes. -/
lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) :
∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ),
3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f)
@ -79,17 +82,17 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
(LIC : LineInCubicPerm S) :
∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f),
(S.val (δ!₂ j) - S.val (δ!₁ j))
(S.val (oddShiftSnd j) - S.val (oddShiftFst j))
* accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
intro j g f h
let S' := (FamilyPermutations (2 * n.succ + 1)).linSolRep
(pairSwap (δ!₁ j) (δ!₂ j)) S
(pairSwap (oddShiftFst j) (oddShiftSnd j)) S
have hSS' : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
(pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl
(pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S' := rfl
obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h
have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h
have h2 := line_in_cubic_P_P_P!
(lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1
have h2 := line_in_cubic_P_P_P! (lineInCubicPerm_self (lineInCubicPerm_permute LIC
(pairSwap (oddShiftFst j) (oddShiftSnd j)))) g' f' hall.1
rw [hall.2.1, hall.2.2] at h2
rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2
simpa using h2
@ -97,26 +100,30 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
(f g : Fin n.succ.succ → ℚ) (hS : S.val = Pa f g) :
accCubeTriLinSymm (P f) (P f) (basis!AsCharges 0) =
(S.val (δ!₁ 0) + S.val (δ!₂ 0)) * (2 * S.val δ!₃ + S.val (δ!₁ 0) + S.val (δ!₂ 0)) := by
(S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
(2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) := by
rw [P_P_P!_accCube f 0]
rw [← Pa_δa₁ f g]
rw [← Pa_oddShiftShiftZero f g]
rw [← hS]
have ht : δ!₁ (0 : Fin n.succ.succ) = δ₁ 1 := rfl
have ht : oddShiftFst (0 : Fin n.succ.succ) = oddFst 1 := rfl
nth_rewrite 1 [ht]
rw [P_δ₁]
have h1 := Pa_δa₁ f g
have h4 := Pa_δa₄ f g 0
have h2 := Pa_δa₂ f g 0
rw [P_oddFst]
have h1 := Pa_oddShiftShiftZero f g
have h4 := Pa_oddShiftShiftSnd f g 0
have h2 := Pa_oddShiftShiftFst f g 0
rw [← hS] at h1 h2 h4
simp only [Nat.succ_eq_add_one, Fin.succ_zero_eq_one, Fin.castSucc_zero] at h2
have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0) := by
have h5 : f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero +
S.val (oddShiftShiftSnd 0) := by
linear_combination -(1 * h1) - 1 * h4 - 1 * h2
rw [h5, δa₄_δ!₂, show (δa₂ (0 : Fin n.succ)) = δ!₁ 0 from rfl, δa₁_δ!₃]
rw [h5, oddShiftShiftSnd_eq_oddShiftSnd,
show (oddShiftShiftFst (0 : Fin n.succ)) = oddShiftFst 0 from rfl,
oddShiftShiftZero_eq_oddShiftZero]
ring
lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
(LIC : LineInCubicPerm S) :
LineInPlaneProp ((S.val (δ!₂ 0)), ((S.val (δ!₁ 0)), (S.val δ!₃))) := by
LineInPlaneProp ((S.val (oddShiftSnd 0)), ((S.val (oddShiftFst 0)), (S.val oddShiftZero))) := by
obtain ⟨g, f, hfg⟩ := span_basis S
have h1 := lineInCubicPerm_swap LIC 0 g f hfg
rw [P_P_P!_accCube' g f hfg] at h1
@ -132,8 +139,8 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
(LIC : LineInCubicPerm S) : LineInPlaneCond S := by
refine @Prop_three (2 * n.succ.succ + 1) LineInPlaneProp S (δ!₂ 0) (δ!₁ 0)
δ!₃ ?_ ?_ ?_ ?_
refine @Prop_three (2 * n.succ.succ + 1) LineInPlaneProp S (oddShiftSnd 0) (oddShiftFst 0)
oddShiftZero ?_ ?_ ?_ ?_
· exact ne_of_beq_false rfl
· exact ne_of_beq_false rfl
· exact ne_of_beq_false rfl

5
HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
View file

@ -30,7 +30,7 @@ variable {n : ℕ}
open VectorLikeOddPlane
/-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a linear solution. We will later
show that this can be extended to a complete solution. -/
show that this can be extended to a complete solution. -/
def parameterizationAsLinear (g f : Fin n → ℚ) (a : ℚ) :
(PureU1 (2 * n + 1)).LinSols :=
a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P' g +
@ -44,8 +44,9 @@ lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) :
change a • (_ • (P' g).val + _ • (P!' f).val) = _
rw [P'_val, P!'_val]
/-- The parameterization satisfies the cubic ACC. -/
lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ) :
(accCube (2 * n + 1)) (parameterizationAsLinear g f a).val = 0 := by
accCube (2 * n + 1) (parameterizationAsLinear g f a).val = 0 := by
change accCubeTriLinSymm.toCubic _ = 0
rw [parameterizationAsLinear_val]
rw [HomogeneousCubic.map_smul]

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)

30
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,16 @@ 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 +98,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 +113,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 +125,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 +134,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 +177,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 +198,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 +210,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 +222,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 +235,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 +247,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 +259,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 +273,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 +286,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 +305,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 +422,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))