The Two Higgs Doublet Model

The two Higgs doublet model is the standard model plus an additional Higgs doublet.

i. Overview

The two Higgs doublet model (2HDM) is an extension of the Standard Model which adds a second Higgs doublet.

References

• https://arxiv.org/abs/hep-ph/0605184
• https://arxiv.org/abs/1605.03237

A. The configuration space

structure TwoHiggsDoublet : Type

The configuration space of the two Higgs doublet model. In otherwords, the underlying vector space associated with the model.

• Φ1 : StandardModel.HiggsVec

  The first Higgs doublet.

• Φ2 : StandardModel.HiggsVec

  The second Higgs doublet.

theorem TwoHiggsDoublet.ext_of_fst_snd {H1 H2 : TwoHiggsDoublet} (h1 : H1.Φ1 = H2.Φ1) (h2 : H1.Φ2 = H2.Φ2) : H1 = H2

theorem TwoHiggsDoublet.ext_of_fst_snd_iff {H1 H2 : TwoHiggsDoublet} : H1 = H2 ↔ H1.Φ1 = H2.Φ1 ∧ H1.Φ2 = H2.Φ2

B. Gauge group actions

noncomputable instance TwoHiggsDoublet.instSMulGaugeGroupI : SMul StandardModel.GaugeGroupI TwoHiggsDoublet

Equations

• TwoHiggsDoublet.instSMulGaugeGroupI = { smul := fun (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) => { Φ1 := g • H.Φ1, Φ2 := g • H.Φ2 } }

@[simp]

theorem TwoHiggsDoublet.gaugeGroupI_smul_fst (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) : (g • H).Φ1 = g • H.Φ1

@[simp]

theorem TwoHiggsDoublet.gaugeGroupI_smul_snd (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) : (g • H).Φ2 = g • H.Φ2

noncomputable instance TwoHiggsDoublet.instMulActionGaugeGroupI : MulAction StandardModel.GaugeGroupI TwoHiggsDoublet

Equations

• TwoHiggsDoublet.instMulActionGaugeGroupI = { toSMul := TwoHiggsDoublet.instSMulGaugeGroupI, mul_smul := ⋯, one_smul := ⋯ }