The action of the gauge group on the Higgs field

The representation of the gauge group on the Higgs vector space

noncomputable def StandardModel.HiggsVec.higgsRepUnitary : GaugeGroupI →* ↥(Matrix.unitaryGroup (Fin 2) ℂ)

The Higgs representation as a homomorphism from the gauge group to unitary 2×2-matrices.

Equations

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

@[simp]

theorem StandardModel.HiggsVec.higgsRepUnitary_apply_coe (g : GaugeGroupI) : ↑(higgsRepUnitary g) = g.2.2 ^ 3 • ↑g.2.1

noncomputable def StandardModel.HiggsVec.matrixToLin : Matrix (Fin 2) (Fin 2) ℂ →* HiggsVec →L[ℂ] HiggsVec

Using the orthonormal basis of HiggsVec, turns a 2×2-matrix into a linear map of HiggsVec.

Equations

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

theorem StandardModel.HiggsVec.matrixToLin_star (g : Matrix (Fin 2) (Fin 2) ℂ) : matrixToLin (star g) = star (matrixToLin g)

The map matrixToLin commutes with the star operation.

theorem StandardModel.HiggsVec.matrixToLin_unitary (g : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : matrixToLin ↑g ∈ unitary (HiggsVec →L[ℂ] HiggsVec)

If g is a member of the 2 × 2 unitary group, then as a linear map from HiggsVec →L[ℂ] HiggsVec formed by the orthonormal basis on HiggsVec, it is unitary.

noncomputable def StandardModel.HiggsVec.unitaryToLin : ↥(Matrix.unitaryGroup (Fin 2) ℂ) →* ↥(unitary (HiggsVec →L[ℂ] HiggsVec))

The natural homomorphism from unitary 2×2 complex matrices to unitary transformations of higgsVec.

Equations

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

def StandardModel.HiggsVec.unitToLinear : ↥(unitary (HiggsVec →L[ℂ] HiggsVec)) →* HiggsVec →ₗ[ℂ] HiggsVec

The inclusion of unitary transformations on higgsVec into all linear transformations.

Equations

• StandardModel.HiggsVec.unitToLinear = DistribMulAction.toModuleEnd ℂ StandardModel.HiggsVec

@[simp]

theorem StandardModel.HiggsVec.unitToLinear_apply_apply (s : ↥(unitary (HiggsVec →L[ℂ] HiggsVec))) (a✝ : HiggsVec) : (unitToLinear s) a✝ = s • a✝

def StandardModel.HiggsVec.rep : Representation ℂ GaugeGroupI HiggsVec

The representation of the gauge group acting on higgsVec.

Equations

• StandardModel.HiggsVec.rep = StandardModel.HiggsVec.unitToLinear.comp (StandardModel.HiggsVec.unitaryToLin.comp StandardModel.HiggsVec.higgsRepUnitary)

@[simp]

theorem StandardModel.HiggsVec.rep_apply_apply (a✝ : GaugeGroupI) (a✝¹ : HiggsVec) : (rep a✝) a✝¹ = unitaryToLin (higgsRepUnitary a✝) • a✝¹

theorem StandardModel.HiggsVec.higgsRepUnitary_mul (g : GaugeGroupI) (φ : HiggsVec) : (↑(higgsRepUnitary g)).mulVec φ = g.2.2 ^ 3 • (↑g.2.1).mulVec φ

theorem StandardModel.HiggsVec.rep_apply (g : GaugeGroupI) (φ : HiggsVec) : (rep g) φ = g.2.2 ^ 3 • (↑g.2.1).mulVec φ

The application of gauge group on a Higgs vector can be decomposed in to an smul with the U(1)-factor and a multiplication by the SU(2)-factor.

Gauge freedom

def StandardModel.HiggsVec.rotateMatrix (φ : HiggsVec) : Matrix (Fin 2) (Fin 2) ℂ

Given a Higgs vector, a rotation matrix which puts the first component of the vector to zero, and the second component to a real

Equations

• φ.rotateMatrix = ![![φ 1 / ↑‖φ‖, -φ 0 / ↑‖φ‖], ![(starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (φ 0) / ↑‖φ‖, (starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (φ 1) / ↑‖φ‖]]

theorem StandardModel.HiggsVec.rotateMatrix_star (φ : HiggsVec) : star φ.rotateMatrix = ![![(starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (φ 1) / ↑‖φ‖, φ 0 / ↑‖φ‖], ![-(starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (φ 0) / ↑‖φ‖, φ 1 / ↑‖φ‖]]

An expansion of the conjugate of the rotateMatrix for a higgs vector.

theorem StandardModel.HiggsVec.rotateMatrix_det {φ : HiggsVec} (hφ : φ ≠ 0) : φ.rotateMatrix.det = 1

The determinant of the rotateMatrix for a non-zero Higgs vector is 1.

theorem StandardModel.HiggsVec.rotateMatrix_unitary {φ : HiggsVec} (hφ : φ ≠ 0) : φ.rotateMatrix ∈ Matrix.unitaryGroup (Fin 2) ℂ

The rotateMatrix for a non-zero Higgs vector is unitary.

theorem StandardModel.HiggsVec.rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) : φ.rotateMatrix ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ

The rotateMatrix for a non-zero Higgs vector is special unitary.

def StandardModel.HiggsVec.rotateGaugeGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroupI

Given a Higgs vector, an element of the gauge group which puts the first component of the vector to zero, and the second component to a real number.

Equations

• StandardModel.HiggsVec.rotateGaugeGroup hφ = (1, ⟨φ.rotateMatrix, ⋯⟩, 1)

theorem StandardModel.HiggsVec.rotateGaugeGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) : (rep (rotateGaugeGroup hφ)) φ = ![0, Complex.ofRealHom ‖φ‖]

Acting on a non-zero Higgs vector with its rotation matrix gives a vector which is zero in the first component and a positive real in the second component.

theorem StandardModel.HiggsVec.rotate_fst_zero_snd_real (φ : HiggsVec) : ∃ (g : GaugeGroupI), (rep g) φ = ![0, ↑‖φ‖]

For every Higgs vector there exists an element of the gauge group which rotates that Higgs vector to have 0 in the first component and be a non-negative real in the second component.

theorem StandardModel.HiggsVec.rotate_fst_real_snd_zero (φ : HiggsVec) : ∃ (g : GaugeGroupI), (rep g) φ = ![↑‖φ‖, 0]

For every Higgs vector there exists an element of the gauge group which rotates that Higgs vector to have 0 in the second component and be a non-negative real in the first component.

def StandardModel.HiggsVec.guage_orbit : InformalLemma

There exists a g in GaugeGroupI such that rep g φ = φ' iff ‖φ‖ = ‖φ'‖.

Equations

• StandardModel.HiggsVec.guage_orbit = { deps := [`StandardModel.HiggsVec.rotate_fst_zero_snd_real] }

def StandardModel.HiggsVec.stability_group_single : InformalLemma

The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the stability group of the action of rep on ![0, Complex.ofReal ‖φ‖], for non-zero ‖φ‖, is the SU(3) × U(1) subgroup of gaugeGroup := SU(3) × SU(2) × U(1) with the embedding given by (g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ}).

Equations

• StandardModel.HiggsVec.stability_group_single = { deps := [`StandardModel.HiggsVec, `StandardModel.HiggsVec.rep] }

def StandardModel.HiggsVec.stability_group : InformalLemma

The subgroup of gaugeGroup := SU(3) × SU(2) × U(1) which preserves every HiggsVec by the action of StandardModel.HiggsVec.rep is given by SU(3) × ℤ₆ where ℤ₆ is the subgroup of SU(2) × U(1) with elements (α^(-3) * I₂, α) where α is a sixth root of unity.

Equations

• StandardModel.HiggsVec.stability_group = { deps := [`StandardModel.HiggsVec, `StandardModel.HiggsVec.rep] }

Gauge transformations acting on Higgs fields.

def StandardModel.HiggsField.gaugeAction : InformalDefinition

The action of gaugeTransformI on HiggsField acting pointwise through HiggsVec.rep.

Equations

• StandardModel.HiggsField.gaugeAction = { deps := [`StandardModel.HiggsVec.rep, `StandardModel.gaugeTransformI] }

def StandardModel.HiggsField.guage_orbit : InformalLemma

There exists a g in gaugeTransformI such that gaugeAction g φ = φ' iff φ(x)^† φ(x) = φ'(x)^† φ'(x).

Equations

• StandardModel.HiggsField.guage_orbit = { deps := [`StandardModel.HiggsField.gaugeAction] }

def StandardModel.HiggsField.gauge_orbit_surject : InformalLemma

For every smooth map f from SpaceTime to ℝ such that f is positive semidefinite, there exists a Higgs field φ such that f = φ^† φ.

Equations

• StandardModel.HiggsField.gauge_orbit_surject = { deps := [`StandardModel.HiggsField, `SpaceTime] }