Electric charge as the unbroken generator

The electroweak gauge algebra is 𝔰𝔲(2) ⊕ 𝔲(1). We write its elements as pairs (A, β) with A ∈ 𝔰𝔲(2) a skew-Hermitian traceless 2 × 2 matrix and β : ℝ the hypercharge parameter. On a weak-isospin doublet of hypercharge y the pair acts by A + i β (y / 2), and on a singlet of hypercharge y by i β (y / 2). The Hermitian generators are T³ = σ³ / 2 and Y / 2, with hypercharges normalised so that the Higgs doublet has Y = 1 and the left-handed lepton doublet has Y = -1.

The Higgs vacuum (0, v) with v ≠ 0 lies in the lower, T³ = -1/2, component of the Higgs doublet. The generators that annihilate it form the line through electricChargeGenerator = (i T³, 1). This is the unique unbroken direction, and it lies in the Cartan subalgebra of diagonal generators. It acts on a doublet of hypercharge y as i times the electric charge operator electricChargeOperator y = T³ + y / 2, and on a singlet as i (y / 2). So for the doublets and singlets treated here the electric charge of a state with weak-isospin third component T³ and hypercharge Y is Q = T³ + Y / 2.

Main results

• doubletStabilizer_higgsVacuum: the generators annihilating the Higgs vacuum are the real multiples of electricChargeGenerator. finrank_doubletStabilizer_higgsVacuum says there is exactly one.
• doubletAction_electricChargeGenerator: on a doublet of hypercharge y the unbroken generator acts as i times electricChargeOperator y = T³ + y / 2. isospinT3_mulVec_single gives the weights isospinWeight k = ±1/2 of T³ on the two components, electricChargeOperator_mulVec_single the charges doubletElectricCharge y k = ±1/2 + y / 2, and doubletAction_electricChargeGenerator_mulVec_single combines the two; the parallel isospinT3_col, electricChargeOperator_col and I_smul_electricChargeOperator_col are their simp-normal forms, since Matrix.mulVec_single rewrites M *ᵥ Pi.single k 1 to M.col k. singletAction_electricChargeGenerator is the singlet version, with charge singletElectricCharge y = y / 2.

References

• S. Weinberg, A model of leptons, Phys. Rev. Lett. 19 (1967) 1264.
• Particle Data Group, Electroweak model and constraints on new physics, for the normalisation Q = T³ + Y/2.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinWeight : Fin 2 → ℝ

The weak-isospin weights of a doublet: the T³ eigenvalue 1/2 of the upper component and -1/2 of the lower one.

Equations

• EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinWeight = ![1 / 2, -1 / 2]

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinWeight_zero : isospinWeight 0 = 1 / 2

The upper component of a doublet has weak isospin 1/2.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinWeight_one : isospinWeight 1 = -1 / 2

The lower component of a doublet has weak isospin -1/2.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3 : Matrix (Fin 2) (Fin 2) ℂ

The weak-isospin generator T³ = σ³ / 2 on a doublet. Its eigenvalues are the weights isospinWeight.

Equations

• EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3 = (1 / 2) • PauliMatrix.pauliMatrix (Sum.inr 2)

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3_def : isospinT3 = (1 / 2) • PauliMatrix.pauliMatrix (Sum.inr 2)

T³ is σ³ / 2.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3_apply_eq_su2GenEntry (i j : Fin 2) : isospinT3 i j = QCD.RepresentationColor.su2GenEntry 2 i j

T³ is the third fundamental su(2) generator σ³ / 2 of su2GenEntry.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3_eq_diagonal : isospinT3 = Matrix.diagonal fun (k : Fin 2) => ↑(isospinWeight k)

T³ is diagonal, with the weights isospinWeight on the diagonal.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3_col (k : Fin 2) : isospinT3.col k = Pi.single k ↑(isospinWeight k)

The k-th column of T³ is the k-th basis vector scaled by the weight isospinWeight k. This is the simp-normal form of isospinT3_mulVec_single: Matrix.mulVec_single rewrites that lemma's left-hand side to isospinT3.col k.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.singletAction (y : ℝ) : ↥(LieAlgebra.SpecialUnitary.su (Fin 2)) × ℝ →ₗ[ℝ] ℂ

The action of (A, β) ∈ 𝔰𝔲(2) ⊕ 𝔲(1) on a weak-isospin singlet of hypercharge y: the 𝔰𝔲(2) component acts trivially and the hypercharge acts by i β (y / 2).

Equations

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

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.singletAction_apply (y : ℝ) (x : ↥(LieAlgebra.SpecialUnitary.su (Fin 2)) × ℝ) : (singletAction y) x = Complex.I * (↑x.2 * ↑(y / 2))

The singlet action unfolded.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletAction (y : ℝ) : ↥(LieAlgebra.SpecialUnitary.su (Fin 2)) × ℝ →ₗ[ℝ] Matrix (Fin 2) (Fin 2) ℂ

The action of (A, β) ∈ 𝔰𝔲(2) ⊕ 𝔲(1) on a weak-isospin doublet of hypercharge y: the matrix A + i β (y / 2), whose hypercharge part is the singlet action.

Equations

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

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletAction_apply (y : ℝ) (x : ↥(LieAlgebra.SpecialUnitary.su (Fin 2)) × ℝ) : (doubletAction y) x = ↑x.1 + (singletAction y) x • 1

The doublet action unfolded.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletStabilizer (y : ℝ) (φ : Fin 2 → ℂ) : Submodule ℝ (↥(LieAlgebra.SpecialUnitary.su (Fin 2)) × ℝ)

The stabilizer of a vector φ in a doublet of hypercharge y: the generators of 𝔰𝔲(2) ⊕ 𝔲(1) whose doublet action annihilates φ. These are the directions of the gauge algebra left unbroken when φ is the vacuum.

Equations

• EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletStabilizer y φ = ((Matrix.mulVecBilin ℝ ℂ).flip φ ∘ₗ EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletAction y).ker

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.mem_doubletStabilizer_iff (y : ℝ) (φ : Fin 2 → ℂ) (x : ↥(LieAlgebra.SpecialUnitary.su (Fin 2)) × ℝ) : x ∈ doubletStabilizer y φ ↔ ((doubletAction y) x).mulVec φ = 0

Membership in the stabilizer is the vanishing of the doublet action on φ.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isHermitian_isospinT3 : isospinT3.IsHermitian

T³ is Hermitian.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.trace_isospinT3 : isospinT3.trace = 0

T³ is traceless.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.I_smul_isospinT3_mem_su : Complex.I • isospinT3 ∈ LieAlgebra.SpecialUnitary.su (Fin 2)

i T³ is skew-Hermitian and traceless, so it lies in 𝔰𝔲(2).

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeGenerator : ↥(LieAlgebra.SpecialUnitary.su (Fin 2)) × ℝ

The electric-charge generator (i T³, 1) ∈ 𝔰𝔲(2) ⊕ 𝔲(1), whose associated Hermitian generator, -i times its doublet action, is T³ + Y / 2.

Equations

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

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.coe_electricChargeGenerator_fst : ↑electricChargeGenerator.1 = Complex.I • isospinT3

The 𝔰𝔲(2) component of the electric charge generator is i T³.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeGenerator_snd : electricChargeGenerator.2 = 1

The hypercharge component of the electric charge generator is 1.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isDiag_electricChargeGenerator_fst : (↑electricChargeGenerator.1).IsDiag

The electric charge generator lies in the Cartan subalgebra: its 𝔰𝔲(2) component is diagonal.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeGenerator_ne_zero : electricChargeGenerator ≠ 0

The electric charge generator is nonzero.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletElectricCharge (y : ℝ) (k : Fin 2) : ℝ

The electric charge T³ₖ + y / 2 of the k-th component of a doublet of hypercharge y.

Equations

• EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletElectricCharge y k = EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinWeight k + y / 2

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletElectricCharge_apply (y : ℝ) (k : Fin 2) : doubletElectricCharge y k = isospinWeight k + y / 2

The doublet electric charge unfolded.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.singletElectricCharge (y : ℝ) : ℝ

The electric charge y / 2 of a weak-isospin singlet of hypercharge y.

Equations

• EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.singletElectricCharge y = y / 2

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.singletElectricCharge_def (y : ℝ) : singletElectricCharge y = y / 2

The singlet electric charge unfolded.

noncomputable def EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeOperator (y : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The electric-charge operator Q = T³ + y / 2 on a weak-isospin doublet of hypercharge y.

Equations

• EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeOperator y = EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3 + ↑(y / 2) • 1

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeOperator_def (y : ℝ) : electricChargeOperator y = isospinT3 + ↑(y / 2) • 1

The electric charge operator unfolded.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeOperator_eq_diagonal (y : ℝ) : electricChargeOperator y = Matrix.diagonal fun (k : Fin 2) => ↑(doubletElectricCharge y k)

The electric charge operator is diagonal, with the charges doubletElectricCharge y on the diagonal.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeOperator_col (y : ℝ) (k : Fin 2) : (electricChargeOperator y).col k = Pi.single k ↑(doubletElectricCharge y k)

The k-th column of the charge operator T³ + y / 2 is the k-th basis vector scaled by the charge doubletElectricCharge y k. This is the simp-normal form of electricChargeOperator_mulVec_single: Matrix.mulVec_single rewrites that lemma's left-hand side to (electricChargeOperator y).col k.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isHermitian_electricChargeOperator (y : ℝ) : (electricChargeOperator y).IsHermitian

The charge operator is Hermitian.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isDiag_electricChargeOperator (y : ℝ) : (electricChargeOperator y).IsDiag

The charge operator is diagonal.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletAction_electricChargeGenerator (y : ℝ) : (doubletAction y) electricChargeGenerator = Complex.I • electricChargeOperator y

The charge is T³ + Y/2. On a doublet of hypercharge y the unbroken generator acts as i times the charge operator T³ + y / 2.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.singletAction_electricChargeGenerator (y : ℝ) : (singletAction y) electricChargeGenerator = Complex.I * ↑(singletElectricCharge y)

On a singlet of hypercharge y the unbroken generator acts as i times the singlet electric charge singletElectricCharge y = y / 2: the electric charge of a weak-isospin singlet is Y / 2.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.isospinT3_mulVec_single (k : Fin 2) : isospinT3.mulVec (Pi.single k 1) = ↑(isospinWeight k) • Pi.single k 1

The weak-isospin weights of a doublet: T³ scales the k-th basis vector by isospinWeight k.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.electricChargeOperator_mulVec_single (y : ℝ) (k : Fin 2) : (electricChargeOperator y).mulVec (Pi.single k 1) = ↑(doubletElectricCharge y k) • Pi.single k 1

The charges of a doublet: the electric charge operator T³ + y / 2 scales the k-th basis vector by doubletElectricCharge y k.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletAction_electricChargeGenerator_mulVec_single (y : ℝ) (k : Fin 2) : ((doubletAction y) electricChargeGenerator).mulVec (Pi.single k 1) = (Complex.I * ↑(doubletElectricCharge y k)) • Pi.single k 1

On a doublet of hypercharge y the unbroken generator scales the k-th basis vector by i times its electric charge doubletElectricCharge y k.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.I_smul_electricChargeOperator_col (y : ℝ) (k : Fin 2) : (Complex.I • electricChargeOperator y).col k = Pi.single k (Complex.I * ↑(doubletElectricCharge y k))

The k-th column of I • electricChargeOperator y, the doublet action of the electric charge generator on a doublet of hypercharge y, is the k-th basis vector scaled by i times the charge doubletElectricCharge y k. This is the simp-normal form of doubletAction_electricChargeGenerator_mulVec_single, which simp reaches through doubletAction_electricChargeGenerator and Matrix.mulVec_single.

@[simp]

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.doubletStabilizer_higgsVacuum {v : ℂ} (hv : v ≠ 0) : doubletStabilizer 1 (Particles.StandardModel.HiggsBoson.higgsVacuum v).ofLp = ℝ ∙ electricChargeGenerator

Electric charge is the unbroken generator. For v ≠ 0 the generators of 𝔰𝔲(2) ⊕ 𝔲(1) annihilating the Higgs vacuum (0, v) are exactly the real multiples of electricChargeGenerator.

theorem EpsilonEridani.QFT.Scattering.DIS.PVES.Electroweak.finrank_doubletStabilizer_higgsVacuum {v : ℂ} (hv : v ≠ 0) : Module.finrank ℝ ↥(doubletStabilizer 1 (Particles.StandardModel.HiggsBoson.higgsVacuum v).ofLp) = 1

There is exactly one unbroken direction: the stabilizer of the Higgs vacuum is a line.