diff --git a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean index af133c8e31..03983b715c 100644 --- a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean +++ b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean @@ -59,21 +59,21 @@ lemma ext_of_fst_snd {H1 H2 : TwoHiggsDoublet} noncomputable instance : SMul StandardModel.GaugeGroupI TwoHiggsDoublet where smul g H := - { Φ1 := g • H.Φ1 - Φ2 := g • H.Φ2 } + { Φ1 := StandardModel.HiggsVec.repGaugeGroupI g H.Φ1 + Φ2 := StandardModel.HiggsVec.repGaugeGroupI g H.Φ2 } @[simp] lemma gaugeGroupI_smul_fst (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) : - (g • H).Φ1 = g • H.Φ1 := rfl + (g • H).Φ1 = StandardModel.HiggsVec.repGaugeGroupI g H.Φ1 := rfl @[simp] lemma gaugeGroupI_smul_snd (g : StandardModel.GaugeGroupI) (H : TwoHiggsDoublet) : - (g • H).Φ2 = g • H.Φ2 := rfl + (g • H).Φ2 = StandardModel.HiggsVec.repGaugeGroupI g H.Φ2 := rfl noncomputable instance : MulAction StandardModel.GaugeGroupI TwoHiggsDoublet where one_smul H := by ext <;> simp mul_smul g1 g2 H := by - ext <;> simp [mul_smul] + ext <;> simp [Module.End.mul_apply] end TwoHiggsDoublet diff --git a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean index e6e319dba1..e065eb1f6a 100644 --- a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean +++ b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean @@ -89,17 +89,17 @@ lemma gramMatrix_tr_nonneg (H : TwoHiggsDoublet) : lemma gaugeGroupI_exists_fst_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) : ∃ g : StandardModel.GaugeGroupI, - g • H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧ - (g • H.Φ2) 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ ∧ - ‖(g • H.Φ2) 1‖ = Real.sqrt (H.gramMatrix.det.re) / ‖H.Φ1‖ := by + HiggsVec.repGaugeGroupI g H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧ + (HiggsVec.repGaugeGroupI g H.Φ2) 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ ∧ + ‖(HiggsVec.repGaugeGroupI g H.Φ2) 1‖ = Real.sqrt (H.gramMatrix.det.re) / ‖H.Φ1‖ := by rw [gramMatrix_det_eq_real] - obtain ⟨g, h⟩ := (HiggsVec.mem_orbit_gaugeGroupI_iff (H.Φ1) (!₂[‖H.Φ1‖, 0] : HiggsVec)).mpr - (by simp [@PiLp.norm_eq_of_L2]) + obtain ⟨g, h⟩ := (HiggsVec.exists_repGaugeGroupI_eq_iff_norm_eq (H.Φ1) + (!₂[‖H.Φ1‖, 0] : HiggsVec)).mpr (by simp [@PiLp.norm_eq_of_L2]) use g - simp at h simp [h] - have h_fst : (g • H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ := by - have h2 : ⟪H.Φ1, H.Φ2⟫_ℂ = ⟪g • H.Φ1, g • H.Φ2⟫_ℂ := by + have h_fst : (HiggsVec.repGaugeGroupI g H.Φ2).ofLp 0 = ⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖ := by + have h2 : ⟪H.Φ1, H.Φ2⟫_ℂ = ⟪HiggsVec.repGaugeGroupI g H.Φ1, + HiggsVec.repGaugeGroupI g H.Φ2⟫_ℂ := by simp rw [h] at h2 conv_rhs at h2 => @@ -109,14 +109,16 @@ lemma gaugeGroupI_exists_fst_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) : simp_all field_simp apply And.intro h_fst - have hx : ‖g • H.Φ2‖ ^ 2 = ‖H.Φ2‖ ^ 2 := by + have hx : ‖HiggsVec.repGaugeGroupI g H.Φ2‖ ^ 2 = ‖H.Φ2‖ ^ 2 := by simp rw [PiLp.norm_sq_eq_of_L2] at hx simp at hx - have hx0 : ‖(g • H.Φ2).ofLp 1‖ ^ 2 = ‖H.Φ2‖ ^ 2 - ‖(g • H.Φ2).ofLp 0‖ ^ 2 := by + have hx0 : ‖(HiggsVec.repGaugeGroupI g H.Φ2).ofLp 1‖ ^ 2 = + ‖H.Φ2‖ ^ 2 - ‖(HiggsVec.repGaugeGroupI g H.Φ2).ofLp 0‖ ^ 2 := by rw [← hx] simp - have h0 : ‖(g • H.Φ2) 1‖ ^ 2 = (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2 := by + have h0 : ‖(HiggsVec.repGaugeGroupI g H.Φ2) 1‖ ^ 2 = + (‖H.Φ1‖ ^ 2 * ‖H.Φ2‖ ^ 2 - ‖⟪H.Φ1, H.Φ2⟫_ℂ‖ ^ 2) / ‖H.Φ1‖ ^ 2 := by field_simp rw [hx0, h_fst] simp only [Fin.isValue, Complex.norm_div, Complex.norm_real, norm_norm] @@ -133,18 +135,19 @@ lemma gaugeGroupI_exists_fst_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) : ring_nf · exact norm_ne_zero_iff.mpr h1 · simpa using h1 - · exact norm_nonneg ((g • H.Φ2).ofLp 1) + · exact norm_nonneg ((HiggsVec.repGaugeGroupI g H.Φ2).ofLp 1) lemma gaugeGroupI_exists_fst_eq_snd_eq {H : TwoHiggsDoublet} (h1 : H.Φ1 ≠ 0) : ∃ g : StandardModel.GaugeGroupI, - g • H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧ - g • H.Φ2 = (!₂[⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖, √(H.gramMatrix.det.re) / ‖H.Φ1‖] : HiggsVec) := by + HiggsVec.repGaugeGroupI g H.Φ1 = (!₂[‖H.Φ1‖, 0] : HiggsVec) ∧ + HiggsVec.repGaugeGroupI g H.Φ2 = + (!₂[⟪H.Φ1, H.Φ2⟫_ℂ / ‖H.Φ1‖, √(H.gramMatrix.det.re) / ‖H.Φ1‖] : HiggsVec) := by obtain ⟨g, h_fst, h_snd_0, h_snd_1⟩ := gaugeGroupI_exists_fst_eq h1 - obtain ⟨k, h1, h2, h3⟩ := HiggsVec.gaugeGroupI_smul_phase_snd (g • H.Φ2) + obtain ⟨k, h1, h2, h3⟩ := HiggsVec.repGaugeGroupI_phase_snd (HiggsVec.repGaugeGroupI g H.Φ2) use k * g apply And.intro - · rw [mul_smul, h_fst, h3] - · rw [mul_smul] + · rw [HiggsVec.repGaugeGroupI_mul_apply, h_fst, h3] + · rw [HiggsVec.repGaugeGroupI_mul_apply] ext i fin_cases i · simp @@ -162,10 +165,10 @@ lemma mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) : simp [← hg] by_cases Φ1_zero : H1.Φ1 = 0 · intro h - obtain ⟨g1, hg1⟩ := (HiggsVec.mem_orbit_gaugeGroupI_iff (H1.Φ2) (!₂[‖H1.Φ2‖, 0] : HiggsVec)).mpr - (by simp [@PiLp.norm_eq_of_L2]) - obtain ⟨g2, hg2⟩ := (HiggsVec.mem_orbit_gaugeGroupI_iff (H2.Φ2) (!₂[‖H2.Φ2‖, 0] : HiggsVec)).mpr - (by simp [@PiLp.norm_eq_of_L2]) + obtain ⟨g1, hg1⟩ := (HiggsVec.exists_repGaugeGroupI_eq_iff_norm_eq (H1.Φ2) + (!₂[‖H1.Φ2‖, 0] : HiggsVec)).mpr (by simp [@PiLp.norm_eq_of_L2]) + obtain ⟨g2, hg2⟩ := (HiggsVec.exists_repGaugeGroupI_eq_iff_norm_eq (H2.Φ2) + (!₂[‖H2.Φ2‖, 0] : HiggsVec)).mpr (by simp [@PiLp.norm_eq_of_L2]) use g1⁻¹ * g2 simp only ext:1 @@ -175,9 +178,8 @@ lemma mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) : rw [← eq_fst_norm_of_eq_gramMatrix h] simp [Φ1_zero] at hnorm simp [hnorm] - · simp [mul_smul] - refine inv_smul_eq_iff.mpr ?_ - simp at hg1 hg2 + · simp + refine (HiggsVec.repGaugeGroupI_inv_apply_eq_iff _ _ _).mpr ?_ simp [hg1, hg2] exact eq_snd_norm_of_eq_gramMatrix h.symm · intro h @@ -192,12 +194,12 @@ lemma mem_orbit_gaugeGroupI_iff_gramMatrix (H1 H2 : TwoHiggsDoublet) : use g1⁻¹ * g2 simp only ext:1 - · simp [mul_smul] - refine inv_smul_eq_iff.mpr ?_ + · simp + refine (HiggsVec.repGaugeGroupI_inv_apply_eq_iff _ _ _).mpr ?_ simp [H1_Φ1, H2_Φ1] apply eq_fst_norm_of_eq_gramMatrix h.symm - · simp [mul_smul] - refine inv_smul_eq_iff.mpr ?_ + · simp + refine (HiggsVec.repGaugeGroupI_inv_apply_eq_iff _ _ _).mpr ?_ simp [H1_Φ2, H2_Φ2] apply And.intro · congr 1 diff --git a/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean b/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean index 938ceecf2a..11791b1b20 100644 --- a/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean +++ b/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean @@ -32,8 +32,9 @@ In this module we define the Higgs field and prove some basic properties. - A.3. Orthonormal basis - A.4. Generating Higgs vectors from real numbers - A.5. Action of the gauge group on `HiggsVec` - - A.5.1. Definition of the action + - A.5.1. Definition of the representation - A.5.2. Unitary nature of the action + - A.5.3. Group properties of the representation applied to vectors - A.6. The Gauge orbit of a Higgs vector - A.6.1. The rotation matrix to ofReal - A.6.2. Members of orbits @@ -160,43 +161,37 @@ The gauge group of the Standard Model acts on `HiggsVec` by matrix multiplicatio /-! -#### A.5.1. Definition of the action +#### A.5.1. Definition of the representation -/ -instance : SMul StandardModel.GaugeGroupI HiggsVec where - smul g φ := WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp) +/-- The representation of the gauge group `GaugeGroupI` on `HiggsVec`: the `SU(2)` + factor acts by matrix multiplication, and the `U(1)` factor by scalar + multiplication with its third power. -/ +def repGaugeGroupI : Representation ℂ GaugeGroupI HiggsVec where + toFun g := + { toFun φ := WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp) + map_add' φ ψ := by simp [mulVec_add, smul_add] + map_smul' c φ := by simp [mulVec_smul, smul_comm c] } + map_one' := by + ext φ + simp + map_mul' g₁ g₂ := by + ext φ + simp [Module.End.mul_apply, smul_smul, mulVec_mulVec, mul_pow, mul_comm] -lemma gaugeGroupI_smul_eq (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : - g • φ = (WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)) := rfl +lemma repGaugeGroupI_apply (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : + repGaugeGroupI g φ = (WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)) := rfl -lemma gaugeGroupI_smul_eq_U1_mul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : - g • φ = (WithLp.toLp 2 <| g.toSU2.1 *ᵥ (g.toU1 ^ 3 • φ.ofLp)) := by - rw [gaugeGroupI_smul_eq, ← mulVec_smul] +lemma repGaugeGroupI_apply_eq_U1_mul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : + repGaugeGroupI g φ = (WithLp.toLp 2 <| g.toSU2.1 *ᵥ (g.toU1 ^ 3 • φ.ofLp)) := by + rw [repGaugeGroupI_apply, ← mulVec_smul] -lemma gaugeGroupI_smul_eq_U1_smul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : - g • φ = (WithLp.toLp 2 <| (g.toU1 ^ 3 • g.toSU2.1) *ᵥ φ.ofLp) := by - rw [gaugeGroupI_smul_eq] +lemma repGaugeGroupI_apply_eq_U1_smul_SU2 (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : + repGaugeGroupI g φ = (WithLp.toLp 2 <| (g.toU1 ^ 3 • g.toSU2.1) *ᵥ φ.ofLp) := by + rw [repGaugeGroupI_apply] rw [Matrix.smul_mulVec] -instance : MulAction StandardModel.GaugeGroupI HiggsVec where - one_smul φ := by simp [gaugeGroupI_smul_eq] - mul_smul g₁ g₂ φ := by - simp [gaugeGroupI_smul_eq, mulVec_smul, smul_smul, mulVec_mulVec, mul_pow] - -instance : DistribMulAction StandardModel.GaugeGroupI HiggsVec where - smul_zero g := by simp [gaugeGroupI_smul_eq_U1_smul_SU2] - smul_add g φ ψ := by simp [gaugeGroupI_smul_eq_U1_smul_SU2, mulVec_add] - -TODO "Change the action of `GaugeGroupI` on `HiggsVec` to be a representation - rather than a `MulAction`." - -instance : SMulCommClass ℂ GaugeGroupI HiggsVec where - smul_comm r g φ := by simp [gaugeGroupI_smul_eq, mulVec_smul, smul_comm r] - -instance : SMulCommClass ℝ GaugeGroupI HiggsVec where - smul_comm r g φ := by simp [gaugeGroupI_smul_eq, mulVec_smul, smul_comm r] - /-! #### A.5.2. Unitary nature of the action @@ -207,18 +202,36 @@ The action of `StandardModel.GaugeGroupI` on `HiggsVec` is unitary. open InnerProductSpace @[simp] -lemma gaugeGroupI_smul_inner (g : StandardModel.GaugeGroupI) (φ ψ : HiggsVec) : - ⟪g • φ, g • ψ⟫_ℂ = ⟪φ, ψ⟫_ℂ := by - rw [gaugeGroupI_smul_eq, gaugeGroupI_smul_eq, EuclideanSpace.inner_toLp_toLp, +lemma repGaugeGroupI_inner (g : StandardModel.GaugeGroupI) (φ ψ : HiggsVec) : + ⟪repGaugeGroupI g φ, repGaugeGroupI g ψ⟫_ℂ = ⟪φ, ψ⟫_ℂ := by + rw [repGaugeGroupI_apply, repGaugeGroupI_apply, EuclideanSpace.inner_toLp_toLp, EuclideanSpace.inner_eq_star_dotProduct, Submonoid.smul_def, Submonoid.smul_def, star_smul, smul_dotProduct, dotProduct_smul, smul_smul, Unitary.mul_star_self_of_mem (g.toU1 ^ 3).2, one_smul, star_mulVec, dotProduct_comm, dotProduct_mulVec, vecMul_vecMul, ← star_eq_conjTranspose, mem_unitaryGroup_iff'.mp g.toSU2.2.1, vecMul_one, dotProduct_comm] @[simp] -lemma gaugeGroupI_smul_norm (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : - ‖g • φ‖ = ‖φ‖ := by - rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), norm_eq_sqrt_re_inner (𝕜 := ℂ), gaugeGroupI_smul_inner] +lemma repGaugeGroupI_norm (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : + ‖repGaugeGroupI g φ‖ = ‖φ‖ := by + rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), norm_eq_sqrt_re_inner (𝕜 := ℂ), repGaugeGroupI_inner] + +/-! + +#### A.5.3. Group properties of the representation applied to vectors + +-/ + +lemma repGaugeGroupI_mul_apply (g₁ g₂ : StandardModel.GaugeGroupI) (φ : HiggsVec) : + repGaugeGroupI (g₁ * g₂) φ = repGaugeGroupI g₁ (repGaugeGroupI g₂ φ) := by + rw [map_mul, Module.End.mul_apply] + +lemma repGaugeGroupI_inv_apply_eq_iff (g : StandardModel.GaugeGroupI) (φ ψ : HiggsVec) : + repGaugeGroupI g⁻¹ φ = ψ ↔ φ = repGaugeGroupI g ψ := by + constructor + · rintro rfl + rw [Representation.self_inv_apply] + · rintro rfl + rw [Representation.inv_self_apply] /-! @@ -270,12 +283,12 @@ def toRealGroupElem (φ : HiggsVec) : GaugeGroupI := rw [← mul_conj, ← mul_conj] ring -lemma toRealGroupElem_smul_self (φ : HiggsVec) : - (toRealGroupElem φ) • φ = ofReal (‖φ‖ ^ 2) := by +lemma toRealGroupElem_apply_self (φ : HiggsVec) : + repGaugeGroupI (toRealGroupElem φ) φ = ofReal (‖φ‖ ^ 2) := by by_cases hφ : φ = 0 · ext i fin_cases i <;> simp [hφ, toRealGroupElem, ofReal] - rw [gaugeGroupI_smul_eq] + rw [repGaugeGroupI_apply] have h0' : (‖φ‖ ^ 2 : ℂ) = φ 0 * (starRingEnd ℂ) (φ 0) + φ 1 * (starRingEnd ℂ) (φ 1) := by rw [← ofReal_pow, ← @real_inner_self_eq_norm_sq] simp only [Fin.isValue, mul_conj, PiLp.inner_apply, Complex.inner, ofReal_re, @@ -301,16 +314,18 @@ Higgs vectors with the same norm. -/ -lemma mem_orbit_gaugeGroupI_iff (φ : HiggsVec) (ψ : HiggsVec) : - ψ ∈ MulAction.orbit GaugeGroupI φ ↔ ‖ψ‖ = ‖φ‖ := by +/-- Two Higgs vectors are in the same gauge orbit (i.e. related by `repGaugeGroupI`) + if and only if they have the same norm. -/ +lemma exists_repGaugeGroupI_eq_iff_norm_eq (φ : HiggsVec) (ψ : HiggsVec) : + (∃ g : GaugeGroupI, repGaugeGroupI g φ = ψ) ↔ ‖ψ‖ = ‖φ‖ := by constructor · rintro ⟨g, rfl⟩ simp · intro h use (toRealGroupElem ψ)⁻¹ * toRealGroupElem (φ) - simp only - rw [← smul_smul, toRealGroupElem_smul_self φ, ← h, ← toRealGroupElem_smul_self ψ] - exact inv_smul_smul _ ψ + rw [map_mul, Module.End.mul_apply, toRealGroupElem_apply_self φ, ← h, + ← toRealGroupElem_apply_self ψ, ← Module.End.mul_apply, ← map_mul, + inv_mul_cancel, map_one, Module.End.one_apply] /-! @@ -324,7 +339,7 @@ The items in this section are marked as `informal_lemma` as they are not yet for -/ /-- The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the -stability group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the +stability group of `repGaugeGroupI` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the `SU(3) × U(1)` subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` with the embedding given by `(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`. -/ @@ -333,8 +348,8 @@ informal_lemma stability_group_single where tag := "6V2MD" /-- The subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` which preserves every `HiggsVec` by the -action of `StandardModel.HiggsVec.rep` is given by `SU(3) × ℤ₆` where `ℤ₆` is the subgroup of -`SU(2) × U(1)` with elements `(α^(-3) * I₂, α)` where `α` is a sixth root of unity. +action of `StandardModel.HiggsVec.repGaugeGroupI` is given by `SU(3) × ℤ₆` where `ℤ₆` is the +subgroup of `SU(2) × U(1)` with elements `(α^(-3) * I₂, α)` where `α` is a sixth root of unity. -/ informal_lemma stability_group where deps := [``HiggsVec] @@ -346,10 +361,10 @@ informal_lemma stability_group where -/ -lemma ofU1Subgroup_smul_eq_smul (g : unitary ℂ) (φ : HiggsVec) : - (StandardModel.GaugeGroupI.ofU1Subgroup g) • φ = +lemma ofU1Subgroup_repGaugeGroupI_apply (g : unitary ℂ) (φ : HiggsVec) : + repGaugeGroupI (StandardModel.GaugeGroupI.ofU1Subgroup g) φ = (WithLp.toLp 2 <| !![1, 0; 0, g.1 ^ 6] *ᵥ φ.ofLp) := by - rw [gaugeGroupI_smul_eq_U1_smul_SU2] + rw [repGaugeGroupI_apply_eq_U1_smul_SU2] simp only [GaugeGroupI.ofU1Subgroup_toU1, GaugeGroupI.ofU1Subgroup_toSU2, SubmonoidClass.coe_pow, star_pow, RCLike.star_def, smul_of, smul_cons, smul_zero, smul_empty, cons_mulVec, cons_dotProduct, zero_mul, dotProduct_of_isEmpty, add_zero, zero_add, empty_mulVec, one_mul, @@ -362,17 +377,17 @@ lemma ofU1Subgroup_smul_eq_smul (g : unitary ℂ) (φ : HiggsVec) : · show (g : ℂ) ^ 3 * (g : ℂ) ^ 3 = (g : ℂ) ^ 6 ring -lemma gaugeGroupI_smul_phase_snd (φ : HiggsVec) : +lemma repGaugeGroupI_phase_snd (φ : HiggsVec) : ∃ g : StandardModel.GaugeGroupI, - (g • φ).ofLp 1 = ‖(φ.ofLp 1)‖ ∧ - (∀ φ1 : HiggsVec, (g • φ1).ofLp 0 = φ1.ofLp 0) ∧ - (∀ a : ℝ, g • (!₂[a, 0] : HiggsVec) = (!₂[a, 0] : HiggsVec)) := by + (repGaugeGroupI g φ).ofLp 1 = ‖(φ.ofLp 1)‖ ∧ + (∀ φ1 : HiggsVec, (repGaugeGroupI g φ1).ofLp 0 = φ1.ofLp 0) ∧ + (∀ a : ℝ, repGaugeGroupI g (!₂[a, 0] : HiggsVec) = (!₂[a, 0] : HiggsVec)) := by let θ := arg (φ 1) refine ⟨StandardModel.GaugeGroupI.ofU1Subgroup ⟨Complex.exp (-I * θ / 6), by simp [Unitary.mem_iff, ← Complex.exp_conj, ← Complex.exp_add, Complex.conj_ofNat] ring_nf simp⟩, ?_, ?_, ?_⟩ - · rw [ofU1Subgroup_smul_eq_smul] + · rw [ofU1Subgroup_repGaugeGroupI_apply] simp only [Fin.isValue, neg_mul, cons_mulVec, cons_dotProduct, one_mul, zero_mul, dotProduct_of_isEmpty, add_zero, zero_add, empty_mulVec, cons_val_one, cons_val_fin_one] rw [show vecHead (vecTail φ.ofLp) = φ.ofLp 1 from rfl] @@ -382,10 +397,10 @@ lemma gaugeGroupI_smul_phase_snd (φ : HiggsVec) : ring_nf simp · intro φ - simp [ofU1Subgroup_smul_eq_smul, vecHead] + simp [ofU1Subgroup_repGaugeGroupI_apply, vecHead] · intro a ext i - fin_cases i <;> simp [ofU1Subgroup_smul_eq_smul] + fin_cases i <;> simp [ofU1Subgroup_repGaugeGroupI_apply] /-! @@ -738,7 +753,8 @@ TODO "Define the global gauge action on HiggsField." TODO "Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary)" TODO "Prove invariance of potential under global gauge action." -/-- The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`. -/ +/-- The action of `gaugeTransformI` on `HiggsField` acting pointwise through + `HiggsVec.repGaugeGroupI`. -/ informal_definition gaugeAction where deps := [``gaugeTransformI] tag := "6V2NP" diff --git a/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean b/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean index 55ac72aa58..02a3bcd3f1 100644 --- a/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean +++ b/Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean @@ -44,13 +44,13 @@ namespace EffectivePotential /-- The proposition that the general potential is invariant under the global action of the gauge group. -/ def IsInvariant (V : EffectivePotential) : Prop := - ∀ (g : GaugeGroupI), ∀ (φ : HiggsVec), V (g • φ) = V φ + ∀ (g : GaugeGroupI), ∀ (φ : HiggsVec), V (HiggsVec.repGaugeGroupI g φ) = V φ namespace IsInvariant /-- An invariant potential is equal on gauge orbits. -/ lemma eq_on_orbits {φ1 φ2 : HiggsVec} {V : EffectivePotential} (h : IsInvariant V) - (hφ : φ1 ∈ MulAction.orbit GaugeGroupI φ2) : + (hφ : ∃ g : GaugeGroupI, HiggsVec.repGaugeGroupI g φ2 = φ1) : V φ1 = V φ2 := by obtain ⟨g, rfl⟩ := hφ exact h g φ2 @@ -58,7 +58,7 @@ lemma eq_on_orbits {φ1 φ2 : HiggsVec} {V : EffectivePotential} (h : IsInvarian /-- An invariant potential is equal on Higgs vectors with identical norms. -/ lemma eq_of_norm_eq {φ1 φ2 : HiggsVec} {V : EffectivePotential} (h : IsInvariant V) (hφ : ‖φ1‖ = ‖φ2‖) : - V φ1 = V φ2 := h.eq_on_orbits <| (HiggsVec.mem_orbit_gaugeGroupI_iff φ2 φ1).mpr hφ + V φ1 = V φ2 := h.eq_on_orbits <| (HiggsVec.exists_repGaugeGroupI_eq_iff_norm_eq φ2 φ1).mpr hφ lemma factors_through_norm {V : EffectivePotential} (h : IsInvariant V) : ∃ (f : ℝ → ℝ), V = f ∘ norm := by @@ -146,13 +146,15 @@ lemma termOfMassDim_isInvariant {V : EffectivePotential} {n : ℕ} (h : HasMaxMa (m : ℕ) (hV : IsInvariant V) : IsInvariant (termOfMassDim V h m) := by intro g φ have hV (t : ℝ) := hV g (t • φ) - have h1 (t : ℝ) : ∑ m ∈ Finset.range (n + 1), t ^ m * (termOfMassDim V h m (g • φ) - + have h1 (t : ℝ) : ∑ m ∈ Finset.range (n + 1), + t ^ m * (termOfMassDim V h m (HiggsVec.repGaugeGroupI g φ) - termOfMassDim V h m φ) = 0 := by simp [mul_sub, ← apply_smul_eq_sum_termOfMassDim] - rw [smul_comm, hV, sub_eq_zero] + rw [← LinearMap.map_smul_of_tower, hV, sub_eq_zero] by_cases hmn : m ≤ n · have hp : (∑ k ∈ Finset.range (n + 1), - Polynomial.C (termOfMassDim V h k (g • φ) - termOfMassDim V h k φ) * Polynomial.X ^ k) + Polynomial.C (termOfMassDim V h k (HiggsVec.repGaugeGroupI g φ) - + termOfMassDim V h k φ) * Polynomial.X ^ k) = 0 := by apply Polynomial.funext intro x diff --git a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeSlice.lean b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeSlice.lean index e221ed2206..5223f7efbb 100644 --- a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeSlice.lean +++ b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeSlice.lean @@ -88,10 +88,10 @@ lemma ofU1Subgroup_smul_sliceHiggs (c : unitary ℂ) (z w0 w1 : ℂ) : GaugeGroupI.ofU1Subgroup c • sliceHiggs z w0 w1 = sliceHiggs z w0 ((c : ℂ) ^ 6 * w1) := by apply ext_of_fst_snd - · rw [gaugeGroupI_smul_fst, HiggsVec.ofU1Subgroup_smul_eq_smul] + · rw [gaugeGroupI_smul_fst, HiggsVec.ofU1Subgroup_repGaugeGroupI_apply] ext i fin_cases i <;> simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two] - · rw [gaugeGroupI_smul_snd, HiggsVec.ofU1Subgroup_smul_eq_smul] + · rw [gaugeGroupI_smul_snd, HiggsVec.ofU1Subgroup_repGaugeGroupI_apply] ext i fin_cases i <;> simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two] diff --git a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeTorus.lean b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeTorus.lean index 9a358ad739..696714e4df 100644 --- a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeTorus.lean +++ b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/GaugeTorus.lean @@ -53,8 +53,9 @@ lemma gaugeCartan_toSU2_coe (a : unitary ℂ) : /-- The Cartan element acts as the diagonal matrix `diag(a, ā)`. -/ lemma gaugeCartan_smul_eq (a : unitary ℂ) (φ : HiggsVec) : - gaugeCartan a • φ = WithLp.toLp 2 (!![(a : ℂ), 0; 0, (star a : ℂ)] *ᵥ φ.ofLp) := by - rw [HiggsVec.gaugeGroupI_smul_eq, gaugeCartan_toU1, one_pow, one_smul, gaugeCartan_toSU2_coe] + HiggsVec.repGaugeGroupI (gaugeCartan a) φ = + WithLp.toLp 2 (!![(a : ℂ), 0; 0, (star a : ℂ)] *ᵥ φ.ofLp) := by + rw [HiggsVec.repGaugeGroupI_apply, gaugeCartan_toU1, one_pow, one_smul, gaugeCartan_toSU2_coe] end GaugeGroupI end StandardModel diff --git a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/OrbitRepresentative.lean b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/OrbitRepresentative.lean index 327de2bed9..cac84f5a0e 100644 --- a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/OrbitRepresentative.lean +++ b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/OrbitRepresentative.lean @@ -113,10 +113,10 @@ lemma exists_smul_eq_repHiggs (φ : TwoHiggsDoublet) : by_cases h : φ.Φ1 = 0 · refine ⟨![0, ‖φ.Φ2‖, 0, 0], HiggsVec.toRealGroupElem φ.Φ2, ?_⟩ ext1 - · rw [gaugeGroupI_smul_fst, h, smul_zero, repHiggs_Φ1] + · rw [gaugeGroupI_smul_fst, h, map_zero, repHiggs_Φ1] ext i fin_cases i <;> simp - · rw [gaugeGroupI_smul_snd, HiggsVec.toRealGroupElem_smul_self, repHiggs_Φ2, + · rw [gaugeGroupI_smul_snd, HiggsVec.toRealGroupElem_apply_self, repHiggs_Φ2, HiggsVec.ofReal] ext i fin_cases i <;> simp [Real.sqrt_sq, norm_nonneg]