1. PhyslibAlpha
  2. Particles
  3. BeyondTheStandardModel
  4. TwoHDM
  5. Module
Imports
/- Copyright (c) 2026 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.BeyondTheStandardModel.TwoHDM.Basic

The Module structure on the two Higgs doublet model

@[expose] public section

The structure of a module

instance : Add TwoHiggsDoublet where add H1 H2 := { Φ1 := H1.Φ1 + H2.Φ1, Φ2 := H1.Φ2 + H2.Φ2 }@[simp] lemma add_fst (H1 H2 : TwoHiggsDoublet) : (H1 + H2).Φ1 = H1.Φ1 + H2.Φ1 := rfl@[simp] lemma add_snd (H1 H2 : TwoHiggsDoublet) : (H1 + H2).Φ2 = H1.Φ2 + H2.Φ2 := rflinstance : Zero TwoHiggsDoublet where zero := { Φ1 := 0, Φ2 := 0 }@[simp] lemma zero_fst : (0 : TwoHiggsDoublet).Φ1 = 0 := rfl@[simp] lemma zero_snd : (0 : TwoHiggsDoublet).Φ2 = 0 := rflinstance : SMul ℂ TwoHiggsDoublet where smul c H := { Φ1 := c • H.Φ1, Φ2 := c • H.Φ2 }@[simp] lemma smul_fst (c : ℂ) (H : TwoHiggsDoublet) : (c • H).Φ1 = c • H.Φ1 := rfl@[simp] lemma smul_snd (c : ℂ) (H : TwoHiggsDoublet) : (c • H).Φ2 = c • H.Φ2 := rflinstance : Neg TwoHiggsDoublet where neg H := { Φ1 := -H.Φ1, Φ2 := -H.Φ2 }@[simp] lemma neg_fst (H : TwoHiggsDoublet) : (-H).Φ1 = -H.Φ1 := rfl@[simp] lemma neg_snd (H : TwoHiggsDoublet) : (-H).Φ2 = -H.Φ2 := rflinstance : AddCommGroup TwoHiggsDoublet where add_assoc H1 H2 H3 := H1:TwoHiggsDoubletH2:TwoHiggsDoubletH3:TwoHiggsDoublet⊢ H1 + H2 + H3 = H1 + (H2 + H3) H1:TwoHiggsDoubletH2:TwoHiggsDoubletH3:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2 + H3).Φ1.ofLp i✝ = (H1 + (H2 + H3)).Φ1.ofLp i✝H1:TwoHiggsDoubletH2:TwoHiggsDoubletH3:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2 + H3).Φ2.ofLp i✝ = (H1 + (H2 + H3)).Φ2.ofLp i✝ H1:TwoHiggsDoubletH2:TwoHiggsDoubletH3:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2 + H3).Φ1.ofLp i✝ = (H1 + (H2 + H3)).Φ1.ofLp i✝H1:TwoHiggsDoubletH2:TwoHiggsDoubletH3:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2 + H3).Φ2.ofLp i✝ = (H1 + (H2 + H3)).Φ2.ofLp i✝ All goals completed! 🐙 zero_add H := H:TwoHiggsDoublet⊢ 0 + H = H H:TwoHiggsDoubleti✝:Fin 2⊢ (0 + H).Φ1.ofLp i✝ = H.Φ1.ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (0 + H).Φ2.ofLp i✝ = H.Φ2.ofLp i✝ H:TwoHiggsDoubleti✝:Fin 2⊢ (0 + H).Φ1.ofLp i✝ = H.Φ1.ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (0 + H).Φ2.ofLp i✝ = H.Φ2.ofLp i✝ All goals completed! 🐙 add_zero H := H:TwoHiggsDoublet⊢ H + 0 = H H:TwoHiggsDoubleti✝:Fin 2⊢ (H + 0).Φ1.ofLp i✝ = H.Φ1.ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (H + 0).Φ2.ofLp i✝ = H.Φ2.ofLp i✝ H:TwoHiggsDoubleti✝:Fin 2⊢ (H + 0).Φ1.ofLp i✝ = H.Φ1.ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (H + 0).Φ2.ofLp i✝ = H.Φ2.ofLp i✝ All goals completed! 🐙 nsmul := nsmulRec add_comm H1 H2 := H1:TwoHiggsDoubletH2:TwoHiggsDoublet⊢ H1 + H2 = H2 + H1 H1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2).Φ1.ofLp i✝ = (H2 + H1).Φ1.ofLp i✝H1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2).Φ2.ofLp i✝ = (H2 + H1).Φ2.ofLp i✝ H1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2).Φ1.ofLp i✝ = (H2 + H1).Φ1.ofLp i✝H1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (H1 + H2).Φ2.ofLp i✝ = (H2 + H1).Φ2.ofLp i✝ All goals completed! 🐙 zsmul := zsmulRec neg_add_cancel H := H:TwoHiggsDoublet⊢ -H + H = 0 H:TwoHiggsDoubleti✝:Fin 2⊢ (-H + H).Φ1.ofLp i✝ = (Φ1 0).ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (-H + H).Φ2.ofLp i✝ = (Φ2 0).ofLp i✝ H:TwoHiggsDoubleti✝:Fin 2⊢ (-H + H).Φ1.ofLp i✝ = (Φ1 0).ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (-H + H).Φ2.ofLp i✝ = (Φ2 0).ofLp i✝ All goals completed! 🐙instance : Module ℂ TwoHiggsDoublet where smul_add c H1 H2 := c:ℂH1:TwoHiggsDoubletH2:TwoHiggsDoublet⊢ c • (H1 + H2) = c • H1 + c • H2 c:ℂH1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (c • (H1 + H2)).Φ1.ofLp i✝ = (c • H1 + c • H2).Φ1.ofLp i✝c:ℂH1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (c • (H1 + H2)).Φ2.ofLp i✝ = (c • H1 + c • H2).Φ2.ofLp i✝ c:ℂH1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (c • (H1 + H2)).Φ1.ofLp i✝ = (c • H1 + c • H2).Φ1.ofLp i✝c:ℂH1:TwoHiggsDoubletH2:TwoHiggsDoubleti✝:Fin 2⊢ (c • (H1 + H2)).Φ2.ofLp i✝ = (c • H1 + c • H2).Φ2.ofLp i✝ All goals completed! 🐙 add_smul c1 c2 H := c1:ℂc2:ℂH:TwoHiggsDoublet⊢ (c1 + c2) • H = c1 • H + c2 • H c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 + c2) • H).Φ1.ofLp i✝ = (c1 • H + c2 • H).Φ1.ofLp i✝c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 + c2) • H).Φ2.ofLp i✝ = (c1 • H + c2 • H).Φ2.ofLp i✝ c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 + c2) • H).Φ1.ofLp i✝ = (c1 • H + c2 • H).Φ1.ofLp i✝c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 + c2) • H).Φ2.ofLp i✝ = (c1 • H + c2 • H).Φ2.ofLp i✝ All goals completed! 🐙 one_smul H := H:TwoHiggsDoublet⊢ 1 • H = H H:TwoHiggsDoubleti✝:Fin 2⊢ (1 • H).Φ1.ofLp i✝ = H.Φ1.ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (1 • H).Φ2.ofLp i✝ = H.Φ2.ofLp i✝ H:TwoHiggsDoubleti✝:Fin 2⊢ (1 • H).Φ1.ofLp i✝ = H.Φ1.ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (1 • H).Φ2.ofLp i✝ = H.Φ2.ofLp i✝ All goals completed! 🐙 mul_smul c1 c2 H := c1:ℂc2:ℂH:TwoHiggsDoublet⊢ (c1 * c2) • H = c1 • c2 • H c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 * c2) • H).Φ1.ofLp i✝ = (c1 • c2 • H).Φ1.ofLp i✝c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 * c2) • H).Φ2.ofLp i✝ = (c1 • c2 • H).Φ2.ofLp i✝ c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 * c2) • H).Φ1.ofLp i✝ = (c1 • c2 • H).Φ1.ofLp i✝c1:ℂc2:ℂH:TwoHiggsDoubleti✝:Fin 2⊢ ((c1 * c2) • H).Φ2.ofLp i✝ = (c1 • c2 • H).Φ2.ofLp i✝ All goals completed! 🐙 smul_zero c := c:ℂ⊢ c • 0 = 0 c:ℂi✝:Fin 2⊢ (c • 0).Φ1.ofLp i✝ = (Φ1 0).ofLp i✝c:ℂi✝:Fin 2⊢ (c • 0).Φ2.ofLp i✝ = (Φ2 0).ofLp i✝ c:ℂi✝:Fin 2⊢ (c • 0).Φ1.ofLp i✝ = (Φ1 0).ofLp i✝c:ℂi✝:Fin 2⊢ (c • 0).Φ2.ofLp i✝ = (Φ2 0).ofLp i✝ All goals completed! 🐙 zero_smul H := H:TwoHiggsDoublet⊢ 0 • H = 0 H:TwoHiggsDoubleti✝:Fin 2⊢ (0 • H).Φ1.ofLp i✝ = (Φ1 0).ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (0 • H).Φ2.ofLp i✝ = (Φ2 0).ofLp i✝ H:TwoHiggsDoubleti✝:Fin 2⊢ (0 • H).Φ1.ofLp i✝ = (Φ1 0).ofLp i✝H:TwoHiggsDoubleti✝:Fin 2⊢ (0 • H).Φ2.ofLp i✝ = (Φ2 0).ofLp i✝ All goals completed! 🐙