Rows for the CKM Matrix

This file contains the definition extracting the rows of the CKM matrix and proves some properties between them.

The first row can be extracted as [V]u for a CKM matrix V.

def CKMMatrix.uRow (V : CKMMatrix) : Fin 3 → ℂ

The uth row of the CKM matrix.

Equations

• V.uRow = ![↑V 0 0, ↑V 0 1, ↑V 0 2]

def CKMMatrix.u_row : Lean.ParserDescr

The uth row of the CKM matrix.

Equations

• One or more equations did not get rendered due to their size.

def CKMMatrix.cRow (V : CKMMatrix) : Fin 3 → ℂ

The cth row of the CKM matrix.

Equations

• V.cRow = ![↑V 1 0, ↑V 1 1, ↑V 1 2]

def CKMMatrix.c_row : Lean.ParserDescr

The cth row of the CKM matrix.

Equations

• One or more equations did not get rendered due to their size.

def CKMMatrix.tRow (V : CKMMatrix) : Fin 3 → ℂ

The tth row of the CKM matrix.

Equations

• V.tRow = ![↑V 2 0, ↑V 2 1, ↑V 2 2]

def CKMMatrix.t_row : Lean.ParserDescr

The tth row of the CKM matrix.

Equations

• One or more equations did not get rendered due to their size.

theorem CKMMatrix.uRow_normalized (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.uRow ⬝ᵥ V.uRow = 1

The up-quark row of the CKM matrix is normalized to 1.

theorem CKMMatrix.cRow_normalized (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.cRow ⬝ᵥ V.cRow = 1

The charm-quark row of the CKM matrix is normalized to 1.

theorem CKMMatrix.tRow_normalized (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.tRow ⬝ᵥ V.tRow = 1

The top-quark row of the CKM matrix is normalized to 1.

theorem CKMMatrix.uRow_cRow_orthog (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.uRow ⬝ᵥ V.cRow = 0

The up-quark row of the CKM matrix is orthogonal to the charm-quark row.

theorem CKMMatrix.uRow_tRow_orthog (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.uRow ⬝ᵥ V.tRow = 0

The up-quark row of the CKM matrix is orthogonal to the top-quark row.

theorem CKMMatrix.cRow_uRow_orthog (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.cRow ⬝ᵥ V.uRow = 0

The charm-quark row of the CKM matrix is orthogonal to the up-quark row.

theorem CKMMatrix.cRow_tRow_orthog (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.cRow ⬝ᵥ V.tRow = 0

The charm-quark row of the CKM matrix is orthogonal to the top-quark row.

theorem CKMMatrix.tRow_uRow_orthog (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.tRow ⬝ᵥ V.uRow = 0

The top-quark row of the CKM matrix is orthogonal to the up-quark row.

theorem CKMMatrix.tRow_cRow_orthog (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) V.tRow ⬝ᵥ V.cRow = 0

The top-quark row of the CKM matrix is orthogonal to the charm-quark row.

theorem CKMMatrix.uRow_cross_cRow_conj (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) ((crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)) = (crossProduct V.uRow) V.cRow

theorem CKMMatrix.cRow_cross_tRow_conj (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) ((crossProduct ((starRingEnd (Fin 3 → ℂ)) V.cRow)) ((starRingEnd (Fin 3 → ℂ)) V.tRow)) = (crossProduct V.cRow) V.tRow

theorem CKMMatrix.uRow_cross_cRow_normalized (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) ((crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)) ⬝ᵥ (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow) = 1

theorem CKMMatrix.cRow_cross_tRow_normalized (V : CKMMatrix) : (starRingEnd (Fin 3 → ℂ)) ((crossProduct ((starRingEnd (Fin 3 → ℂ)) V.cRow)) ((starRingEnd (Fin 3 → ℂ)) V.tRow)) ⬝ᵥ (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.cRow)) ((starRingEnd (Fin 3 → ℂ)) V.tRow) = 1

def CKMMatrix.rows (V : CKMMatrix) : Fin 3 → Fin 3 → ℂ

A map from Fin 3 to each row of a CKM matrix.

Equations

• V.rows 0 = V.uRow
• V.rows 1 = V.cRow
• V.rows 2 = V.tRow

theorem CKMMatrix.rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ V.rows

The rows of a CKM matrix are linearly independent.

noncomputable def CKMMatrix.rowBasis (V : CKMMatrix) : Basis (Fin 3) ℂ (Fin 3 → ℂ)

The rows of a CKM matrix as a basis of ℂ³.

Equations

• V.rowBasis = basisOfLinearIndependentOfCardEqFinrank ⋯ CKMMatrix.rowBasis.proof_2

@[simp]

theorem CKMMatrix.rowBasis_repr_apply (V : CKMMatrix) (a✝ : Fin 3 → ℂ) : V.rowBasis.repr a✝ = ⋯.repr ((LinearMap.codRestrict (Submodule.span ℂ (Set.range V.rows)) LinearMap.id ⋯) a✝)

@[simp]

theorem CKMMatrix.rowBasis_repr_symm_apply (V : CKMMatrix) (a : Fin 3 →₀ ℂ) (a✝ : Fin 3) : V.rowBasis.repr.symm a a✝ = (Finsupp.linearCombination ℂ V.rows) a a✝

theorem CKMMatrix.cRow_cross_tRow_eq_uRow (V : CKMMatrix) : ∃ (κ : ℝ), V.uRow = Complex.exp (↑κ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.cRow)) ((starRingEnd (Fin 3 → ℂ)) V.tRow)

theorem CKMMatrix.uRow_cross_cRow_eq_tRow (V : CKMMatrix) : ∃ (τ : ℝ), V.tRow = Complex.exp (↑τ * Complex.I) • (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow)

theorem CKMMatrix.ext_Rows {U V : CKMMatrix} (hu : U.uRow = V.uRow) (hc : U.cRow = V.cRow) (ht : U.tRow = V.tRow) : U = V

def phaseShiftApply.ucCross (V : CKMMatrix) (a b c d e f : ℝ) : Fin 3 → ℂ

The cross product of the conjugate of the u and c rows of a CKM matrix.

Equations

• phaseShiftApply.ucCross V a b c d e f = (crossProduct ((starRingEnd (Fin 3 → ℂ)) (phaseShiftApply V a b c d e f).uRow)) ((starRingEnd (Fin 3 → ℂ)) (phaseShiftApply V a b c d e f).cRow)

theorem phaseShiftApply.ucCross_fst (a b c d e f : ℝ) (V : CKMMatrix) : ucCross V a b c d e f 0 = Complex.exp (-↑a * Complex.I + -↑b * Complex.I + -↑e * Complex.I + -↑f * Complex.I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow) 0

theorem phaseShiftApply.ucCross_snd (a b c d e f : ℝ) (V : CKMMatrix) : ucCross V a b c d e f 1 = Complex.exp (-↑a * Complex.I + -↑b * Complex.I + -↑d * Complex.I + -↑f * Complex.I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow) 1

theorem phaseShiftApply.ucCross_thd (a b c d e f : ℝ) (V : CKMMatrix) : ucCross V a b c d e f 2 = Complex.exp (-↑a * Complex.I + -↑b * Complex.I + -↑d * Complex.I + -↑e * Complex.I) * (crossProduct ((starRingEnd (Fin 3 → ℂ)) V.uRow)) ((starRingEnd (Fin 3 → ℂ)) V.cRow) 2

theorem phaseShiftApply.uRow_mul (V : CKMMatrix) (a b c : ℝ) : (phaseShiftApply V a b c 0 0 0).uRow = Complex.exp (↑a * Complex.I) • V.uRow

theorem phaseShiftApply.cRow_mul (V : CKMMatrix) (a b c : ℝ) : (phaseShiftApply V a b c 0 0 0).cRow = Complex.exp (↑b * Complex.I) • V.cRow

theorem phaseShiftApply.tRow_mul (V : CKMMatrix) (a b c : ℝ) : (phaseShiftApply V a b c 0 0 0).tRow = Complex.exp (↑c * Complex.I) • V.tRow