The Higgs field

i. Overview

The Higgs field describes is the underlying field of the Higgs boson. It is a map from SpaceTime to a 2-dimensional complex vector space. In this module we define the Higgs field and prove some basic properties.

ii. Key results

• HiggsVec: The 2-dimensional complex vector space which is the target space of the Higgs field. This vector space is equipped with an action of the global gauge group of the Standard Model.
• HiggsBundle: The trivial vector bundle over SpaceTime with fiber HiggsVec.
• HiggsField: The type of smooth sections of the HiggsBundle, i.e., the type of Higgs fields.

iii. Table of contents

• A. The Higgs vector space
  • A.1. Definition of the Higgs vector space
  • A.2. Relation to (Fin 2 → ℂ)
  • A.3. Orthonormal basis
  • A.4. Generating Higgs vectors from real numbers
  • A.5. Action of the gauge group on HiggsVec
    • A.5.1. Definition of the action
    • A.5.2. Unitary nature of the action
  • A.6. The Gauge orbit of a Higgs vector
    • A.6.1. The rotation matrix to ofReal
    • A.6.2. Members of orbits
  • A.7. The stability group of a Higgs vector
• B. The Higgs bundle
  • B.1. Definition of the Higgs bundle
  • B.2. Instance of a vector bundle
• C. The Higgs fields
  • C.1. Relations between HiggsField and HiggsVec
    • C.1.1. The constant Higgs field
    • C.1.2. The map from HiggsField to SpaceTime → HiggsVec
  • C.2. Smoothness properties of components
  • C.3. The pointwise inner product
    • C.3.1. Basic equalities
    • C.3.2. Symmetry properties
    • C.3.3. Linearity conditions
    • C.3.4. Smoothness of the inner product
  • C.4. The pointwise norm
    • C.4.1. Basic equalities
    • C.4.2. Positivity
    • C.4.3. On the zero section
    • C.4.4. Smoothness of the norm-squared
    • C.4.5. Norm-squared of constant Higgs fields
  • C.5. The action of the gauge group on Higgs fields

iv. References

• The particle data group has properties of the Higgs boson Review of Particle Physics, PDG

A. The Higgs vector space

The target space of the Higgs field is a 2-dimensional complex vector space. In this section we will define this vector space, and the action of the global gauge group on it.

A.1. Definition of the Higgs vector space

@[reducible, inline]

abbrev StandardModel.HiggsVec : Type

The vector space HiggsVec is defined to be the complex Euclidean space of dimension 2. For a given spacetime point a Higgs field gives a value in HiggsVec.

Equations

• StandardModel.HiggsVec = EuclideanSpace ℂ (Fin 2)

A.2. Relation to (Fin 2 → ℂ)

We define the continuous linear map from HiggsVec to (Fin 2 → ℂ) achieved by casting vectors, we also show that this map is smooth.

def StandardModel.HiggsVec.toFin2ℂ : HiggsVec →L[ℝ] Fin 2 → ℂ

The continuous linear map from the vector space HiggsVec to (Fin 2 → ℂ) achieved by casting vectors.

Equations

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

theorem StandardModel.HiggsVec.smooth_toFin2ℂ : ContMDiff (modelWithCornersSelf ℝ HiggsVec) (modelWithCornersSelf ℝ (Fin 2 → ℂ)) ⊤ ⇑toFin2ℂ

The map toFin2ℂ is smooth.

A.3. Orthonormal basis

We define an orthonormal basis of HiggsVec.

def StandardModel.HiggsVec.orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec

An orthonormal basis of HiggsVec.

Equations

• StandardModel.HiggsVec.orthonormBasis = EuclideanSpace.basisFun (Fin 2) ℂ

A.4. Generating Higgs vectors from real numbers

Given a real number a we define the Higgs vector corresponding to that real number as (√a, 0). This has the property that it's norm is equal to a.

def StandardModel.HiggsVec.ofReal (a : ℝ) : HiggsVec

Generating a Higgs vector from a real number, such that the norm-squared of that Higgs vector is the given real number.

Equations

• StandardModel.HiggsVec.ofReal a = ![↑√a, 0]

@[simp]

theorem StandardModel.HiggsVec.ofReal_normSq {a : ℝ} (ha : 0 ≤ a) : ‖ofReal a‖ ^ 2 = a

A.5. Action of the gauge group on HiggsVec

The gauge group of the Standard Model acts on HiggsVec by matrix multiplication.

A.5.1. Definition of the action

instance StandardModel.HiggsVec.instSMulGaugeGroupI : SMul GaugeGroupI HiggsVec

Equations

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

theorem StandardModel.HiggsVec.gaugeGroupI_smul_eq (g : GaugeGroupI) (φ : HiggsVec) : g • φ = GaugeGroupI.toU1 g ^ 3 • (↑(GaugeGroupI.toSU2 g)).mulVec φ

theorem StandardModel.HiggsVec.gaugeGroupI_smul_eq_U1_mul_SU2 (g : GaugeGroupI) (φ : HiggsVec) : g • φ = (↑(GaugeGroupI.toSU2 g)).mulVec (GaugeGroupI.toU1 g ^ 3 • φ)

instance StandardModel.HiggsVec.instMulActionGaugeGroupI : MulAction GaugeGroupI HiggsVec

Equations

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

A.5.2. Unitary nature of the action

The action of StandardModel.GaugeGroupI on HiggsVec is unitary.

@[simp]

theorem StandardModel.HiggsVec.gaugeGroupI_smul_inner (g : GaugeGroupI) (φ ψ : HiggsVec) : inner ℂ (g • φ) (g • ψ) = inner ℂ φ ψ

@[simp]

theorem StandardModel.HiggsVec.gaugeGroupI_smul_norm (g : GaugeGroupI) (φ : HiggsVec) : ‖g • φ‖ = ‖φ‖

A.6. The Gauge orbit of a Higgs vector

We show that two Higgs vectors are in the same gauge orbit if and only if they have the same norm.

A.6.1. The rotation matrix to ofReal

We define an element of GaugeGroupI which takes a given Higgs vector to the corresponding ofReal Higgs vector.

def StandardModel.HiggsVec.toRealGroupElem (φ : HiggsVec) : GaugeGroupI

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

Equations

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

theorem StandardModel.HiggsVec.toRealGroupElem_smul_self (φ : HiggsVec) : φ.toRealGroupElem • φ = ofReal (‖φ‖ ^ 2)

A.6.2. Members of orbits

Members of the orbit of a Higgs vector under the action of GaugeGroupI are exactly those Higgs vectors with the same norm.

theorem StandardModel.HiggsVec.mem_orbit_gaugeGroupI_iff (φ ψ : HiggsVec) : ψ ∈ MulAction.orbit GaugeGroupI φ ↔ ‖ψ‖ = ‖φ‖

A.7. The stability group of a Higgs vector

We find the stability group of a Higgs vector, and the stability group of the set of all Higgs vectors.

The items in this section are marked as informal_lemma as they are not yet formalized.

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], tag := "6V2MD" }

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], tag := "6V2MO" }

B. The Higgs bundle

We define the Higgs bundle as the trivial vector bundle with base SpaceTime and fiber HiggsVec. The Higgs field will then be defined as smooth sections of this bundle.

B.1. Definition of the Higgs bundle

We define the Higgs bundle.

@[reducible, inline]

abbrev StandardModel.HiggsBundle : SpaceTime → Type

The HiggsBundle is defined as the trivial vector bundle with base SpaceTime and fiber HiggsVec. Thus as a manifold it corresponds to ℝ⁴ × ℂ².

Equations

• StandardModel.HiggsBundle = Bundle.Trivial SpaceTime StandardModel.HiggsVec

B.2. Instance of a vector bundle

We given the Higgs bundle an instance of a smooth vector bundle.

instance StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeOfNatNatHiggsVecHiggsBundleVectorAsSmoothManifold : ContMDiffVectorBundle ⊤ HiggsVec HiggsBundle (Lorentz.Vector.asSmoothManifold 3)

The instance of a smooth vector bundle with total space HiggsBundle and fiber HiggsVec.

C. The Higgs fields

Higgs fields are smooth sections of the Higgs bundle. This corresponds to smooth maps from SpaceTime to HiggsVec. We here define the type of Higgs fields and create an API around them.

@[reducible, inline]

abbrev StandardModel.HiggsField : Type

The type HiggsField is defined such that elements are smooth sections of the trivial vector bundle HiggsBundle. Such elements are Higgs fields. Since HiggsField is trivial as a vector bundle, a Higgs field is equivalent to a smooth map from SpaceTime to HiggsVec.

Equations

• StandardModel.HiggsField = ContMDiffSection (Lorentz.Vector.asSmoothManifold 3) StandardModel.HiggsVec ⊤ StandardModel.HiggsBundle

C.1. Relations between HiggsField and HiggsVec

C.1.1. The constant Higgs field

We define the constant Higgs field associated to a given Higgs vector.

def StandardModel.HiggsField.const : HiggsVec →ₗ[ℝ] HiggsField

Given a vector in HiggsVec the constant Higgs field with value equal to that section.

Equations

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

@[simp]

theorem StandardModel.HiggsField.const_apply (φ : HiggsVec) (x : SpaceTime) : (const φ) x = φ

For all spacetime points, the constant Higgs field defined by a Higgs vector, returns that Higgs Vector.

C.1.2. The map from HiggsField to SpaceTime → HiggsVec

def StandardModel.HiggsField.toHiggsVec (φ : HiggsField) : SpaceTime → HiggsVec

Given a HiggsField, the corresponding map from SpaceTime to HiggsVec.

Equations

• φ.toHiggsVec = ⇑φ

theorem StandardModel.HiggsField.toHiggsVec_smooth (φ : HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ HiggsVec) ⊤ φ.toHiggsVec

theorem StandardModel.HiggsField.const_toHiggsVec_apply (φ : HiggsField) (x : SpaceTime) : (const (φ.toHiggsVec x)) x = φ x

theorem StandardModel.HiggsField.toFin2ℂ_comp_toHiggsVec (φ : HiggsField) : ⇑HiggsVec.toFin2ℂ ∘ φ.toHiggsVec = ⇑φ

C.2. Smoothness properties of components

We prove some smoothness properties of the components of a Higgs field.

theorem StandardModel.HiggsField.toVec_smooth (φ : HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ (Fin 2 → ℂ)) ⊤ ⇑φ

theorem StandardModel.HiggsField.apply_smooth (φ : HiggsField) (i : Fin 2) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℂ) ⊤ fun (x : SpaceTime) => φ x i

theorem StandardModel.HiggsField.apply_re_smooth (φ : HiggsField) (i : Fin 2) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℝ) ⊤ (⇑Complex.reCLM ∘ fun (x : SpaceTime) => φ x i)

theorem StandardModel.HiggsField.apply_im_smooth (φ : HiggsField) (i : Fin 2) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℝ) ⊤ (⇑Complex.imCLM ∘ fun (x : SpaceTime) => φ x i)

C.3. The pointwise inner product

The pointwise inner product on the Higgs field.

instance StandardModel.HiggsField.instInnerForallSpaceTimeOfNatNatComplex : Inner (SpaceTime → ℂ) HiggsField

Equations

• StandardModel.HiggsField.instInnerForallSpaceTimeOfNatNatComplex = { inner := fun (φ1 φ2 : StandardModel.HiggsField) (x : SpaceTime) => inner ℂ (φ1 x) (φ2 x) }

C.3.1. Basic equalities

theorem StandardModel.HiggsField.inner_apply (φ1 φ2 : HiggsField) (x : SpaceTime) : inner (SpaceTime → ℂ) φ1 φ2 x = inner ℂ (φ1 x) (φ2 x)

theorem StandardModel.HiggsField.inner_eq_expand (φ1 φ2 : HiggsField) : inner (SpaceTime → ℂ) φ1 φ2 = fun (x : SpaceTime) => Complex.equivRealProdCLM.symm ((φ1 x 0).re * (φ2 x 0).re + (φ1 x 1).re * (φ2 x 1).re + (φ1 x 0).im * (φ2 x 0).im + (φ1 x 1).im * (φ2 x 1).im, (φ1 x 0).re * (φ2 x 0).im + (φ1 x 1).re * (φ2 x 1).im - (φ1 x 0).im * (φ2 x 0).re - (φ1 x 1).im * (φ2 x 1).re)

theorem StandardModel.HiggsField.inner_expand_conj (φ1 φ2 : HiggsField) (x : SpaceTime) : inner (SpaceTime → ℂ) φ1 φ2 x = (starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (φ1 x 0) * φ2 x 0 + (starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (φ1 x 1) * φ2 x 1

Expands the inner product on Higgs fields in terms of complex components of the Higgs fields.

C.3.2. Symmetry properties

theorem StandardModel.HiggsField.inner_symm (φ1 φ2 : HiggsField) : (starRingEnd (SpaceTime → ℂ)) (inner (SpaceTime → ℂ) φ2 φ1) = inner (SpaceTime → ℂ) φ1 φ2

C.3.3. Linearity conditions

theorem StandardModel.HiggsField.inner_add_left (φ1 φ2 φ3 : HiggsField) : inner (SpaceTime → ℂ) (φ1 + φ2) φ3 = inner (SpaceTime → ℂ) φ1 φ3 + inner (SpaceTime → ℂ) φ2 φ3

theorem StandardModel.HiggsField.inner_add_right (φ1 φ2 φ3 : HiggsField) : inner (SpaceTime → ℂ) φ1 (φ2 + φ3) = inner (SpaceTime → ℂ) φ1 φ2 + inner (SpaceTime → ℂ) φ1 φ3

@[simp]

theorem StandardModel.HiggsField.inner_zero_left (φ : HiggsField) : inner (SpaceTime → ℂ) 0 φ = 0

@[simp]

theorem StandardModel.HiggsField.inner_zero_right (φ : HiggsField) : inner (SpaceTime → ℂ) φ 0 = 0

theorem StandardModel.HiggsField.inner_neg_left (φ1 φ2 : HiggsField) : inner (SpaceTime → ℂ) (-φ1) φ2 = -inner (SpaceTime → ℂ) φ1 φ2

theorem StandardModel.HiggsField.inner_neg_right (φ1 φ2 : HiggsField) : inner (SpaceTime → ℂ) φ1 (-φ2) = -inner (SpaceTime → ℂ) φ1 φ2

C.3.4. Smoothness of the inner product

theorem StandardModel.HiggsField.inner_smooth (φ1 φ2 : HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℂ) ⊤ (inner (SpaceTime → ℂ) φ1 φ2)

C.4. The pointwise norm

We define the pointwise norm-squared of a Higgs field.

def StandardModel.HiggsField.normSq (φ : HiggsField) : SpaceTime → ℝ

Given an element φ of HiggsField, normSq φ is defined as the the function SpaceTime → ℝ obtained by taking the square norm of the pointwise Higgs vector. In other words, normSq φ x = ‖φ x‖ ^ 2.

The notation ‖φ‖_H^2 is used for the normSq φ.

Equations

• φ.normSq x = ‖φ x‖ ^ 2

def StandardModel.HiggsField.«term‖_‖_H^2» : Lean.ParserDescr

Given an element φ of HiggsField, normSq φ is defined as the the function SpaceTime → ℝ obtained by taking the square norm of the pointwise Higgs vector. In other words, normSq φ x = ‖φ x‖ ^ 2.

The notation ‖φ‖_H^2 is used for the normSq φ.

Equations

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

C.4.1. Basic equalities

theorem StandardModel.HiggsField.inner_self_eq_normSq (φ : HiggsField) (x : SpaceTime) : inner (SpaceTime → ℂ) φ φ x = ↑(φ.normSq x)

theorem StandardModel.HiggsField.normSq_eq_inner_self_re (φ : HiggsField) (x : SpaceTime) : φ.normSq x = (inner (SpaceTime → ℂ) φ φ x).re

theorem StandardModel.HiggsField.normSq_expand (φ : HiggsField) : φ.normSq = fun (x : SpaceTime) => ((starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (φ x 0) * φ x 0 + (starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (φ x 1) * φ x 1).re

The expansion of the norm squared of into components.

C.4.2. Positivity

theorem StandardModel.HiggsField.normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x

C.4.3. On the zero section

@[simp]

theorem StandardModel.HiggsField.normSq_zero : normSq 0 = 0

C.4.4. Smoothness of the norm-squared

theorem StandardModel.HiggsField.normSq_smooth (φ : HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℝ) ⊤ φ.normSq

The norm squared of the Higgs field is a smooth function on space-time.

C.4.5. Norm-squared of constant Higgs fields

@[simp]

theorem StandardModel.HiggsField.const_normSq (φ : HiggsVec) (x : SpaceTime) : (const φ).normSq x = ‖φ‖ ^ 2

C.5. The action of the gauge group on Higgs fields

The results in this section are currently informal.

def StandardModel.HiggsField.gaugeAction : InformalDefinition

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

Equations

• StandardModel.HiggsField.gaugeAction = { deps := [`StandardModel.gaugeTransformI], tag := "6V2NP" }

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], tag := "6V2NX" }

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], tag := "6V2OC" }