The Higgs field

This file defines the basic properties for the Higgs field in the standard model.

References

• We use conventions given in: Review of Particle Physics, PDG

The definition of the Higgs vector space.

In other words, the target space of the Higgs field.

@[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)

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.

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

An orthonormal basis of HiggsVec.

Equations

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

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

Definition of the Higgs Field

We also 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

instance StandardModel.instContMDiffVectorBundleTopWithTopENatRealSpaceTimeHiggsVecHiggsBundleAsSmoothManifold : ContMDiffVectorBundle ⊤ HiggsVec HiggsBundle SpaceTime.asSmoothManifold

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

@[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 SpaceTime.asSmoothManifold StandardModel.HiggsVec ⊤ StandardModel.HiggsBundle

def StandardModel.HiggsVec.toField (φ : HiggsVec) : HiggsField

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

Equations

• φ.toField = { toFun := fun (x : SpaceTime) => φ, contMDiff_toFun := ⋯ }

@[simp]

theorem StandardModel.HiggsVec.toField_apply (φ : HiggsVec) (x : SpaceTime) : φ.toField x = φ

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

Relation to 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.toField_toHiggsVec_apply (φ : HiggsField) (x : SpaceTime) : (φ.toHiggsVec x).toField x = φ x

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

Smoothness properties of components

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)

Constant Higgs fields

def StandardModel.HiggsField.IsConst (Φ : HiggsField) : Prop

A Higgs field is constant if it is equal for all x y in spaceTime.

Equations

• Φ.IsConst = ∀ (x y : SpaceTime), Φ x = Φ y

theorem StandardModel.HiggsField.isConst_of_higgsVec (φ : HiggsVec) : φ.toField.IsConst

theorem StandardModel.HiggsField.isConst_iff_of_higgsVec (Φ : HiggsField) : Φ.IsConst ↔ ∃ (φ : HiggsVec), Φ = φ.toField

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

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

Equations

• StandardModel.HiggsField.ofReal a = (StandardModel.HiggsVec.ofReal a).toField

def StandardModel.HiggsField.zero : HiggsField

The higgs field which is all zero.

Equations

• StandardModel.HiggsField.zero = StandardModel.HiggsField.ofReal 0

def StandardModel.HiggsField.zero_is_zero_section : InformalLemma

The zero Higgs field is the zero section of the Higgs bundle, i.e., the HiggsField zero defined by ofReal 0 is the constant zero-section of the bundle HiggsBundle.

Equations

• StandardModel.HiggsField.zero_is_zero_section = { deps := [`StandardModel.HiggsField.zero] }