docs: CKM matrix rows
This commit is contained in:
jstoobysmith
parent
88b2d28431
commit
5659dca7c8
1 changed files with 52 additions and 44 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue