Physlib.Particles.BeyondTheStandardModel.TwoHDM.Basic

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.StandardModel.HiggsBoson.Basic

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

@[expose] public section

A. The configuration space

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

The first Higgs doublet.

The second Higgs doublet.

              structure TwoHiggsDoublet where  Φ1 : HiggsVec  Φ2 : HiggsVec

@[ext]
lemma ext_of_fst_snd {H1 H2 : TwoHiggsDoublet}
    (h1 : H1.Φ1 = H2.Φ1) (h2 : H1.Φ2 = H2.Φ2) : H1 = H2 := byH1:TwoHiggsDoubletH2:TwoHiggsDoubleth1:H1.Φ1 = H2.Φ1h2:H1.Φ2 = H2.Φ2⊢ H1 = H2
  cases H1mkH2:TwoHiggsDoubletΦ1✝:HiggsVecΦ2✝:HiggsVech1:{ Φ1 := Φ1✝, Φ2 := Φ2✝ }.Φ1 = H2.Φ1h2:{ Φ1 := Φ1✝, Φ2 := Φ2✝ }.Φ2 = H2.Φ2⊢ { Φ1 := Φ1✝, Φ2 := Φ2✝ } = H2
  congrAll goals completed! 🐙

B. Gauge group actions

@[simp]
lemma gaugeGroupI_smul_fst (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) :
    (g • H).Φ1 = g • H.Φ1 := rfl

@[simp]
lemma gaugeGroupI_smul_snd (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) :
    (g • H).Φ2 = g • H.Φ2 := rfl