Gauge orbits for the 2HDM

The main reference for material in this section is https://arxiv.org/pdf/hep-ph/0605184.

def TwoHDM.prodMatrix (Φ1 Φ2 : StandardModel.HiggsField) (x : SpaceTime) : Matrix (Fin 2) (Fin 2) ℂ

For two Higgs fields Φ₁ and Φ₂, the map from space time to 2 x 2 complex matrices defined by ((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂)).

Equations

• TwoHDM.prodMatrix Φ1 Φ2 x = !![inner (SpaceTime → ℂ) Φ1 Φ1 x, inner (SpaceTime → ℂ) Φ2 Φ1 x; inner (SpaceTime → ℂ) Φ1 Φ2 x, inner (SpaceTime → ℂ) Φ2 Φ2 x]

def TwoHDM.fieldCompMatrix (Φ1 Φ2 : StandardModel.HiggsField) (x : SpaceTime) : Matrix (Fin 2) (Fin 2) ℂ

The 2 x 2 complex matrices made up of components of the two Higgs fields.

Equations

• TwoHDM.fieldCompMatrix Φ1 Φ2 x = !![Φ1 x 0, Φ1 x 1; Φ2 x 0, Φ2 x 1]

theorem TwoHDM.prodMatrix_eq_fieldCompMatrix_sq (Φ1 Φ2 : StandardModel.HiggsField) (x : SpaceTime) : prodMatrix Φ1 Φ2 x = fieldCompMatrix Φ1 Φ2 x * (fieldCompMatrix Φ1 Φ2 x).conjTranspose

The matrix prodMatrix Φ1 Φ2 x is equal to the square of fieldCompMatrix Φ1 Φ2 x.

def TwoHDM.instPartialOrderComplex_physLean : PartialOrder ℂ

An instance of PartialOrder on ℂ defined through Complex.partialOrder.

Equations

• TwoHDM.instPartialOrderComplex_physLean = Complex.partialOrder

def TwoHDM.instNormedAddCommGroupMatrixFinOfNatNatComplex_physLean : NormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℂ)

An instance of NormedAddCommGroup on Matrix (Fin 2) (Fin 2) ℂ defined through Matrix.normedAddCommGroup.

Equations

• TwoHDM.instNormedAddCommGroupMatrixFinOfNatNatComplex_physLean = Matrix.normedAddCommGroup

def TwoHDM.instNormedSpaceRealMatrixFinOfNatNatComplex_physLean : NormedSpace ℝ (Matrix (Fin 2) (Fin 2) ℂ)

An instance of NormedSpace on Matrix (Fin 2) (Fin 2) ℂ defined through Matrix.normedSpace.

Equations

• TwoHDM.instNormedSpaceRealMatrixFinOfNatNatComplex_physLean = Matrix.normedSpace

theorem TwoHDM.prodMatrix_posSemiDef (Φ1 Φ2 : StandardModel.HiggsField) (x : SpaceTime) : (prodMatrix Φ1 Φ2 x).PosSemidef

The matrix prodMatrix is positive semi-definite.

theorem TwoHDM.prodMatrix_hermitian (Φ1 Φ2 : StandardModel.HiggsField) (x : SpaceTime) : (prodMatrix Φ1 Φ2 x).IsHermitian

The matrix prodMatrix is hermitian.

theorem TwoHDM.prodMatrix_smooth (Φ1 Φ2 : StandardModel.HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ (Matrix (Fin 2) (Fin 2) ℂ)) ⊤ (prodMatrix Φ1 Φ2)

The map prodMatrix is a smooth function on spacetime.

def TwoHDM.prodMatrix_invariant : InformalLemma

The map prodMatrix is invariant under the simultaneous action of gaugeAction on the two Higgs fields.

Equations

• TwoHDM.prodMatrix_invariant = { deps := [`TwoHDM.prodMatrix, `StandardModel.HiggsField.gaugeAction], tag := "6V2VS" }

def TwoHDM.prodMatrix_to_higgsField : InformalLemma

Given any smooth map f from spacetime to 2-by-2 complex matrices landing on positive semi-definite matrices, there exist smooth Higgs fields Φ1 and Φ2 such that f is equal to prodMatrix Φ1 Φ2.

See https://arxiv.org/pdf/hep-ph/0605184

Equations

• TwoHDM.prodMatrix_to_higgsField = { deps := [`TwoHDM.prodMatrix, `StandardModel.HiggsField, `TwoHDM.prodMatrix_smooth], tag := "6V2V2" }