1. Physlib
  2. Particles
  3. StandardModel
  4. HiggsBoson
  5. 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.Basic public import Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

The Higgs field

i. Overview

The Higgs field describes is the underlying field of the Higgs boson. It is a map from SpaceTime to a 2-dimensional complex vector space. In this module we define the Higgs field and prove some basic properties.

ii. Key results

    HiggsVec: The 2-dimensional complex vector space which is the target space of the Higgs field. This vector space is equipped with an action of the global gauge group of the Standard Model.

    HiggsBundle: The trivial vector bundle over SpaceTime with fiber HiggsVec.

    HiggsField: The type of smooth sections of the HiggsBundle, i.e., the type of Higgs fields.

iii. Table of contents

    A. The Higgs vector space

      A.1. Definition of the Higgs vector space

      A.2. Relation to (Fin 2 → ℂ)

      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.2. Unitary nature of the action

      A.6. The Gauge orbit of a Higgs vector

        A.6.1. The rotation matrix to ofReal

        A.6.2. Members of orbits

      A.7. The stability group of a Higgs vector

      A.8. Gauge action removing phase from second component

      A.9. To real scalars

    B. The Higgs bundle

      B.1. Definition of the Higgs bundle

      B.2. Instance of a vector bundle

    C. The Higgs fields

      C.1. Relations between HiggsField and HiggsVec

        C.1.1. The constant Higgs field

        C.1.2. The map from HiggsField to SpaceTime → HiggsVec

      C.2. Smoothness properties of components

      C.3. The pointwise inner product

        C.3.1. Basic equalities

        C.3.2. Symmetry properties

        C.3.3. Linearity conditions

        C.3.4. Smoothness of the inner product

      C.4. The pointwise norm

        C.4.1. Basic equalities

        C.4.2. Positivity

        C.4.3. On the zero section

        C.4.4. Smoothness of the norm-squared

        C.4.5. Norm-squared of constant Higgs fields

      C.5. The action of the gauge group on Higgs fields

iv. References

    The particle data group has properties of the Higgs boson [Review of Particle Physics, PDG][ParticleDataGroup:2018ovx]

@[expose] public section

A. The Higgs vector space

The target space of the Higgs field is a 2-dimensional complex vector space. In this section we will define this vector space, and the action of the global gauge group on it.

A.1. Definition of the Higgs vector space

The vector space HiggsVec is defined to be the complex Euclidean space of dimension 2. For a given spacetime point a Higgs field gives a value in HiggsVec.

abbrev HiggsVec := EuclideanSpace ℂ (Fin 2)

A.2. Relation to (Fin 2 → ℂ)

We define the continuous linear map from HiggsVec to (Fin 2 → ℂ) achieved by casting vectors, we also show that this map is smooth.

The continuous linear map from the vector space HiggsVec to (Fin 2 → ℂ) achieved by casting vectors.

def toFin2ℂ : HiggsVec →L[ℝ] (Fin 2 → ℂ) where toFun x := x map_add' x y := rfl map_smul' a x := rfl

The map toFin2ℂ is smooth.

lemma smooth_toFin2ℂ : ContMDiff 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 → ℂ) ⊤ toFin2ℂ := toFin2ℂ.contMDiff

A.3. Orthonormal basis

We define an orthonormal basis of HiggsVec.

An orthonormal basis of HiggsVec.

def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec := EuclideanSpace.basisFun (Fin 2) ℂ

A.4. Generating Higgs vectors from real numbers

Given a real number a we define the Higgs vector corresponding to that real number as (√a, 0). This has the property that it's norm is equal to a.

Generating a Higgs vector from a real number, such that the norm-squared of that Higgs vector is the given real number.

def ofReal (a : ℝ) : HiggsVec := !2[Real.sqrt a, 0]
@[simp] lemma ofReal_normSq {a : ℝ} (ha : 0 ≤ a) : ‖ofReal a‖ ^ 2 = a := a:ℝha:0 ≤ a⊢ ‖ofReal a‖ ^ 2 = a All goals completed! 🐙

A.5. Action of the gauge group on HiggsVec

The gauge group of the Standard Model acts on HiggsVec by matrix multiplication.

A.5.1. Definition of the action
instance : SMul StandardModel.GaugeGroupI HiggsVec where smul g φ := WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)lemma gaugeGroupI_smul_eq (g : StandardModel.GaugeGroupI) (φ : HiggsVec) : g • φ = (WithLp.toLp 2 <| g.toU1 ^ 3 • (g.toSU2.1 *ᵥ φ.ofLp)) := rflAll goals completed! 🐙All goals completed! 🐙instance : MulAction StandardModel.GaugeGroupI HiggsVec where one_smul φ := φ:HiggsVec⊢ 1 • φ = φ All goals completed! 🐙 mul_smul g₁ g₂ φ := g₁:GaugeGroupIg₂:GaugeGroupIφ:HiggsVec⊢ (g₁ * g₂) • φ = g₁ • g₂ • φ All goals completed! 🐙instance : DistribMulAction StandardModel.GaugeGroupI HiggsVec where smul_zero g := g:GaugeGroupI⊢ g • 0 = 0 All goals completed! 🐙 smul_add g φ ψ := g:GaugeGroupIφ:HiggsVecψ:HiggsVec⊢ g • (φ + ψ) = g • φ + g • ψ All goals completed! 🐙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 φ := r:ℂg:GaugeGroupIφ:HiggsVec⊢ r • g • φ = g • r • φ All goals completed! 🐙instance : SMulCommClass ℝ GaugeGroupI HiggsVec where smul_comm r g φ := r:ℝg:GaugeGroupIφ:HiggsVec⊢ r • g • φ = g • r • φ All goals completed! 🐙
A.5.2. Unitary nature of the action

The action of StandardModel.GaugeGroupI on HiggsVec is unitary.

All goals completed! 🐙All goals completed! 🐙

A.6. The Gauge orbit of a Higgs vector

We show that two Higgs vectors are in the same gauge orbit if and only if they have the same norm.

A.6.1. The rotation matrix to ofReal

We define an element of GaugeGroupI which takes a given Higgs vector to the corresponding ofReal Higgs vector.

Given a Higgs vector, a rotation matrix which puts the second component of the vector to zero, and the first component to a real

φ:HiggsVechφ:¬φ = 0h0':↑‖φ‖ ^ 2 = φ.ofLp 0 * (starRingEnd ℂ) (φ.ofLp 0) + φ.ofLp 1 * (starRingEnd ℂ) (φ.ofLp 1)h1:↑‖φ‖ ≠ 0⊢ (starRingEnd ℂ) (φ.ofLp 0) * φ.ofLp 0 - -((starRingEnd ℂ) (φ.ofLp 1) * φ.ofLp 1) = φ.ofLp 0 * (starRingEnd ℂ) (φ.ofLp 0) + φ.ofLp 1 * (starRingEnd ℂ) (φ.ofLp 1) All goals completed! 🐙
φ:HiggsVechφ:¬φ = 0h0':↑‖φ‖ ^ 2 = φ.ofLp 0 * (starRingEnd ℂ) (φ.ofLp 0) + φ.ofLp 1 * (starRingEnd ℂ) (φ.ofLp 1)hn:↑‖φ‖ ≠ 0⊢ (starRingEnd ℂ) (φ.ofLp 0) * φ.ofLp 0 + (starRingEnd ℂ) (φ.ofLp 1) * φ.ofLp 1 = φ.ofLp 0 * (starRingEnd ℂ) (φ.ofLp 0) + φ.ofLp 1 * (starRingEnd ℂ) (φ.ofLp 1) All goals completed! 🐙 φ:HiggsVechφ:¬φ = 0h0':↑‖φ‖ ^ 2 = φ.ofLp 0 * (starRingEnd ℂ) (φ.ofLp 0) + φ.ofLp 1 * (starRingEnd ℂ) (φ.ofLp 1)hn:↑‖φ‖ ≠ 0⊢ !₂[(starRingEnd ℂ) (φ.ofLp 0) / ↑‖φ‖ * vecHead φ.ofLp + (starRingEnd ℂ) (φ.ofLp 1) / ↑‖φ‖ * vecHead (vecTail φ.ofLp), -φ.ofLp 1 / ↑‖φ‖ * vecHead φ.ofLp + φ.ofLp 0 / ↑‖φ‖ * vecHead (vecTail φ.ofLp)].ofLp ((fun i => i) ⟨1, ⋯⟩) = (ofReal (‖φ‖ ^ 2)).ofLp ((fun i => i) ⟨1, ⋯⟩) φ:HiggsVechφ:¬φ = 0h0':↑‖φ‖ ^ 2 = φ.ofLp 0 * (starRingEnd ℂ) (φ.ofLp 0) + φ.ofLp 1 * (starRingEnd ℂ) (φ.ofLp 1)hn:↑‖φ‖ ≠ 0⊢ -φ.ofLp 1 / ↑‖φ‖ * φ.ofLp 0 + φ.ofLp 0 / ↑‖φ‖ * φ.ofLp 1 = 0 φ:HiggsVechφ:¬φ = 0h0':↑‖φ‖ ^ 2 = φ.ofLp 0 * (starRingEnd ℂ) (φ.ofLp 0) + φ.ofLp 1 * (starRingEnd ℂ) (φ.ofLp 1)hn:↑‖φ‖ ≠ 0⊢ φ.ofLp 1 * φ.ofLp 0 * (-1 + 1) = ↑‖φ‖ * 0 All goals completed! 🐙
A.6.2. Members of orbits

Members of the orbit of a Higgs vector under the action of GaugeGroupI are exactly those Higgs vectors with the same norm.

φ:HiggsVecψ:HiggsVech:‖ψ‖ = ‖φ‖⊢ ψ.toRealGroupElem⁻¹ • ψ.toRealGroupElem • ψ = ψ All goals completed! 🐙

A.7. The stability group of a Higgs vector

We find the stability group of a Higgs vector, and the stability group of the set of all Higgs vectors.

The items in this section are marked as informal_lemma as they are not yet formalized.

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 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 θ}).

informal_lemma stability_group_single where deps := [``StandardModel.HiggsVec] 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.

informal_lemma stability_group where deps := [``HiggsVec] tag := "6V2MO"

A.8. Gauge action removing phase from second component

g:↥(unitary ℂ)φ:HiggsVech0:g ^ 3 • (starRingEnd ℂ) ↑g ^ 3 = 1⊢ g ^ 3 • (starRingEnd ℂ) ↑g ^ 3 * vecHead φ.ofLp = vecHead φ.ofLp All goals completed! 🐙 g:↥(unitary ℂ)φ:HiggsVec⊢ g ^ 3 • ↑g ^ 3 = ↑g ^ 6 g:↥(unitary ℂ)φ:HiggsVec⊢ ↑g ^ 3 * ↑g ^ 3 = ↑g ^ 6 All goals completed! 🐙φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)⊢ ↑‖φ.ofLp 1‖ * cexp (↑6 * (-(I * ↑θ) / 6) + ↑(arg (φ.ofLp 1)) * I) = ↑‖φ.ofLp 1‖ φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)⊢ ↑‖φ.ofLp 1‖ * cexp (6 * (-(I * ↑(φ.ofLp 1).arg) / 6) + ↑(φ.ofLp 1).arg * I) = ↑‖φ.ofLp 1‖ φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)⊢ ↑‖φ.ofLp 1‖ * cexp 0 = ↑‖φ.ofLp 1‖ All goals completed! 🐙 φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)⊢ ∀ (φ1 : HiggsVec), (GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • φ1).ofLp 0 = φ1.ofLp 0 φ✝:HiggsVecθ:ℝ := arg (φ.ofLp 1)φ:HiggsVec⊢ (GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • φ).ofLp 0 = φ.ofLp 0 All goals completed! 🐙 φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)⊢ ∀ (a : ℝ), GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • !₂[↑a, 0] = !₂[↑a, 0] φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)a:ℝ⊢ GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • !₂[↑a, 0] = !₂[↑a, 0] φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)a:ℝi:Fin 2⊢ (GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • !₂[↑a, 0]).ofLp i = !₂[↑a, 0].ofLp i φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)a:ℝ⊢ (GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • !₂[↑a, 0]).ofLp ((fun i => i) ⟨0, ⋯⟩) = !₂[↑a, 0].ofLp ((fun i => i) ⟨0, ⋯⟩)φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)a:ℝ⊢ (GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • !₂[↑a, 0]).ofLp ((fun i => i) ⟨1, ⋯⟩) = !₂[↑a, 0].ofLp ((fun i => i) ⟨1, ⋯⟩) φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)a:ℝ⊢ (GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • !₂[↑a, 0]).ofLp ((fun i => i) ⟨0, ⋯⟩) = !₂[↑a, 0].ofLp ((fun i => i) ⟨0, ⋯⟩)φ:HiggsVecθ:ℝ := arg (φ.ofLp 1)a:ℝ⊢ (GaugeGroupI.ofU1Subgroup ⟨cexp (-I * ↑θ / 6), ⋯⟩ • !₂[↑a, 0]).ofLp ((fun i => i) ⟨1, ⋯⟩) = !₂[↑a, 0].ofLp ((fun i => i) ⟨1, ⋯⟩) All goals completed! 🐙

A.9 To real scalars

The underlying real values of the Higgs vector.

def toRealScalars : HiggsVec →ₗ[ℝ] (Fin 4 → ℝ) where toFun x := fun | 0 => (x 0).re | 1 => (x 0).im | 2 => (x 1).re | 3 => (x 1).im map_add' x y := x:HiggsVecy:HiggsVec⊢ (fun x_1 => match x_1 with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = (fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im x:HiggsVecy:HiggsVeci:Fin 4⊢ (match i with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) i x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨0, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨0, ⋯⟩)x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨1, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨1, ⋯⟩)x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨2, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨2, ⋯⟩)x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨3, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨3, ⋯⟩) x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨0, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨0, ⋯⟩)x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨1, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨1, ⋯⟩)x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨2, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨2, ⋯⟩)x:HiggsVecy:HiggsVec⊢ (match (fun i => i) ⟨3, ⋯⟩ with | 0 => ((x + y).ofLp 0).re | 1 => ((x + y).ofLp 0).im | 2 => ((x + y).ofLp 1).re | 3 => ((x + y).ofLp 1).im) = ((fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) + fun x => match x with | 0 => (y.ofLp 0).re | 1 => (y.ofLp 0).im | 2 => (y.ofLp 1).re | 3 => (y.ofLp 1).im) ((fun i => i) ⟨3, ⋯⟩) All goals completed! 🐙 map_smul' a x := a:ℝx:HiggsVec⊢ (fun x_1 => match x_1 with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = (RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im a:ℝx:HiggsVeci:Fin 4⊢ (match i with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) i a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨0, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨0, ⋯⟩)a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨1, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨1, ⋯⟩)a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨2, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨2, ⋯⟩)a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨3, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨3, ⋯⟩) a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨0, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨0, ⋯⟩)a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨1, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨1, ⋯⟩)a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨2, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨2, ⋯⟩)a:ℝx:HiggsVec⊢ (match (fun i => i) ⟨3, ⋯⟩ with | 0 => ((a • x).ofLp 0).re | 1 => ((a • x).ofLp 0).im | 2 => ((a • x).ofLp 1).re | 3 => ((a • x).ofLp 1).im) = ((RingHom.id ℝ) a • fun x_1 => match x_1 with | 0 => (x.ofLp 0).re | 1 => (x.ofLp 0).im | 2 => (x.ofLp 1).re | 3 => (x.ofLp 1).im) ((fun i => i) ⟨3, ⋯⟩) All goals completed! 🐙
lemma toRealScalars_smul_real (a : ℝ) (φ : HiggsVec) : toRealScalars (a • φ) = a • toRealScalars φ := map_smul toRealScalars a φlemma ofReal_toRealScalars (a : ℝ) : toRealScalars (ofReal a) = !4[Real.sqrt a, 0, 0, 0] := a:ℝ⊢ toRealScalars (ofReal a) = !₄[√a, 0, 0, 0].ofLp a:ℝi:Fin 4⊢ toRealScalars (ofReal a) i = !₄[√a, 0, 0, 0].ofLp i a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨0, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨0, ⋯⟩)a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨1, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨1, ⋯⟩)a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨2, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨2, ⋯⟩)a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨3, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨3, ⋯⟩) a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨0, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨0, ⋯⟩)a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨1, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨1, ⋯⟩)a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨2, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨2, ⋯⟩)a:ℝ⊢ toRealScalars (ofReal a) ((fun i => i) ⟨3, ⋯⟩) = !₄[√a, 0, 0, 0].ofLp ((fun i => i) ⟨3, ⋯⟩) All goals completed! 🐙All goals completed! 🐙

B. The Higgs bundle

We define the Higgs bundle as the trivial vector bundle with base SpaceTime and fiber HiggsVec. The Higgs field will then be defined as smooth sections of this bundle.

B.1. Definition of the Higgs bundle

We define the Higgs bundle.

TODO "Make `HiggsBundle` an associated bundle."

The HiggsBundle is defined as the trivial vector bundle with base SpaceTime and fiber HiggsVec. Thus as a manifold it corresponds to ℝ⁴ × ℂ².

abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec

B.2. Instance of a vector bundle

We given the Higgs bundle an instance of a smooth vector bundle.

The instance of a smooth vector bundle with total space HiggsBundle and fiber HiggsVec.

instance : ContMDiffVectorBundle ⊤ HiggsVec HiggsBundle (Lorentz.Vector.asSmoothManifold 3) := Bundle.Trivial.contMDiffVectorBundle HiggsVec

C. The Higgs fields

Higgs fields are smooth sections of the Higgs bundle. This corresponds to smooth maps from SpaceTime to HiggsVec. We here define the type of Higgs fields and create an API around them.

The type HiggsField is defined such that elements are smooth sections of the trivial vector bundle HiggsBundle. Such elements are Higgs fields. Since HiggsField is trivial as a vector bundle, a Higgs field is equivalent to a smooth map from SpaceTime to HiggsVec.

abbrev HiggsField : Type := ContMDiffSection (Lorentz.Vector.asSmoothManifold 3) HiggsVec ⊤ HiggsBundle

C.1. Relations between HiggsField and HiggsVec

C.1.1. The constant Higgs field

We define the constant Higgs field associated to a given Higgs vector.

Given a vector in HiggsVec the constant Higgs field with value equal to that section.

φ:HiggsVecx:SpaceTime⊢ ContMDiffAt (Lorentz.Vector.asSmoothManifold 3) 𝓘(ℝ, HiggsVec) ⊤ (fun x_1 => (↑(trivializationAt HiggsVec (Bundle.Trivial SpaceTime HiggsVec) x) ⟨x_1, φ⟩).2) x All goals completed! 🐙} map_add' φ ψ := φ:HiggsVecψ:HiggsVec⊢ { toFun := fun x => φ + ψ, contMDiff_toFun := ⋯ } = { toFun := fun x => φ, contMDiff_toFun := ⋯ } + { toFun := fun x => ψ, contMDiff_toFun := ⋯ } φ:HiggsVecψ:HiggsVecx:SpaceTime⊢ { toFun := fun x => φ + ψ, contMDiff_toFun := ⋯ } x = ({ toFun := fun x => φ, contMDiff_toFun := ⋯ } + { toFun := fun x => ψ, contMDiff_toFun := ⋯ }) x All goals completed! 🐙 map_smul' a φ := a:ℝφ:HiggsVec⊢ { toFun := fun x => a • φ, contMDiff_toFun := ⋯ } = (RingHom.id ℝ) a • { toFun := fun x => φ, contMDiff_toFun := ⋯ } a:ℝφ:HiggsVecx:SpaceTime⊢ { toFun := fun x => a • φ, contMDiff_toFun := ⋯ } x = ((RingHom.id ℝ) a • { toFun := fun x => φ, contMDiff_toFun := ⋯ }) x All goals completed! 🐙

For all spacetime points, the constant Higgs field defined by a Higgs vector, returns that Higgs Vector.

@[simp] lemma const_apply (φ : HiggsVec) (x : SpaceTime) : const φ x = φ := rfl
C.1.2. The map from HiggsField to SpaceTime → HiggsVec

Given a HiggsField, the corresponding map from SpaceTime to HiggsVec.

def toHiggsVec (φ : HiggsField) : SpaceTime → HiggsVec := φ
lemma toHiggsVec_smooth (φ : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, HiggsVec) ⊤ φ.toHiggsVec := fun x0 => (Bundle.contMDiffAt_section x0).mp (φ.contMDiff x0)lemma const_toHiggsVec_apply (φ : HiggsField) (x : SpaceTime) : const (φ.toHiggsVec x) x = φ x := rfllemma toFin2ℂ_comp_toHiggsVec (φ : HiggsField) : φ.toHiggsVec = φ := rfl

C.2. Smoothness properties of components

We prove some smoothness properties of the components of a Higgs field.

@[fun_prop] lemma contDiff (φ : HiggsField) : ContDiff ℝ ⊤ φ := contMDiff_iff_contDiff.mp φ.toHiggsVec_smoothlemma toVec_smooth (φ : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, EuclideanSpace ℂ (Fin 2)) ⊤ φ := φ.toHiggsVec_smoothlemma apply_smooth (φ : HiggsField) : ∀ i, ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) ⊤ (fun (x : SpaceTime) => (φ x i)) := fun i => ((contDiff_piLp 2).mp φ.contDiff i).contMDifflemma apply_re_smooth (φ : HiggsField) (i : Fin 2) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ (reCLM ∘ (fun (x : SpaceTime) => (φ x i))) := reCLM.contMDiff.comp (φ.apply_smooth i)lemma apply_im_smooth (φ : HiggsField) (i : Fin 2) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ (imCLM ∘ (fun (x : SpaceTime) => (φ x i))) := imCLM.contMDiff.comp (φ.apply_smooth i)

C.3. The pointwise inner product

The pointwise inner product on the Higgs field.

instance : Inner (SpaceTime → ℂ) (HiggsField) where inner φ1 φ2 := fun x => ⟪φ1 x, φ2 x⟫_ℂ
C.3.1. Basic equalities
lemma inner_apply (φ1 φ2 : HiggsField) (x : SpaceTime) : ⟪φ1, φ2⟫_(SpaceTime → ℂ) x = ⟪φ1 x, φ2 x⟫_ℂ := rfllemma inner_eq_expand (φ1 φ2 : HiggsField) : ⟪φ1, φ2⟫_(SpaceTime → ℂ) = fun x => equivRealProdCLM.symm (((φ1 x 0).re * (φ2 x 0).re + (φ1 x 1).re * (φ2 x 1).re+ (φ1 x 0).im * (φ2 x 0).im + (φ1 x 1).im * (φ2 x 1).im), ((φ1 x 0).re * (φ2 x 0).im + (φ1 x 1).re * (φ2 x 1).im - (φ1 x 0).im * (φ2 x 0).re - (φ1 x 1).im * (φ2 x 1).re)) := φ1:HiggsFieldφ2:HiggsField⊢ ⟪φ1, φ2⟫_(SpaceTime → ℂ) = fun x => equivRealProdCLM.symm (((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).re + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).re + ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).im, ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re) φ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ ⟪φ1, φ2⟫_(SpaceTime → ℂ) x = equivRealProdCLM.symm (((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).re + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).re + ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).im, ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re) φ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ (⟪φ1, φ2⟫_(SpaceTime → ℂ) x).re = (equivRealProdCLM.symm (((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).re + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).re + ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).im, ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re)).reφ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ (⟪φ1, φ2⟫_(SpaceTime → ℂ) x).im = (equivRealProdCLM.symm (((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).re + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).re + ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).im, ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re)).im φ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ (⟪φ1, φ2⟫_(SpaceTime → ℂ) x).re = (equivRealProdCLM.symm (((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).re + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).re + ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).im, ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re)).reφ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ (⟪φ1, φ2⟫_(SpaceTime → ℂ) x).im = (equivRealProdCLM.symm (((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).re + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).re + ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).im, ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re)).im φ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ -(((φ2 x).ofLp 0).re * ((φ1 x).ofLp 0).im) + ((φ2 x).ofLp 0).im * ((φ1 x).ofLp 0).re + (-(((φ2 x).ofLp 1).re * ((φ1 x).ofLp 1).im) + ((φ2 x).ofLp 1).im * ((φ1 x).ofLp 1).re) = ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re φ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ ((φ2 x).ofLp 0).re * ((φ1 x).ofLp 0).re + ((φ2 x).ofLp 0).im * ((φ1 x).ofLp 0).im + (((φ2 x).ofLp 1).re * ((φ1 x).ofLp 1).re + ((φ2 x).ofLp 1).im * ((φ1 x).ofLp 1).im) = ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).re + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).re + ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).imφ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ -(((φ2 x).ofLp 0).re * ((φ1 x).ofLp 0).im) + ((φ2 x).ofLp 0).im * ((φ1 x).ofLp 0).re + (-(((φ2 x).ofLp 1).re * ((φ1 x).ofLp 1).im) + ((φ2 x).ofLp 1).im * ((φ1 x).ofLp 1).re) = ((φ1 x).ofLp 0).re * ((φ2 x).ofLp 0).im + ((φ1 x).ofLp 1).re * ((φ2 x).ofLp 1).im - ((φ1 x).ofLp 0).im * ((φ2 x).ofLp 0).re - ((φ1 x).ofLp 1).im * ((φ2 x).ofLp 1).re All goals completed! 🐙

Expands the inner product on Higgs fields in terms of complex components of the Higgs fields.

lemma inner_expand_conj (φ1 φ2 : HiggsField) (x : SpaceTime) : ⟪φ1, φ2⟫_(SpaceTime → ℂ) x = conj (φ1 x 0) * φ2 x 0 + conj (φ1 x 1) * φ2 x 1 := φ1:HiggsFieldφ2:HiggsFieldx:SpaceTime⊢ ⟪φ1, φ2⟫_(SpaceTime → ℂ) x = (starRingEnd ((fun x => ℂ) 0)) ((φ1 x).ofLp 0) * (φ2 x).ofLp 0 + (starRingEnd ((fun x => ℂ) 1)) ((φ1 x).ofLp 1) * (φ2 x).ofLp 1 All goals completed! 🐙
C.3.2. Symmetry properties
lemma inner_symm (φ1 φ2 : HiggsField) : conj ⟪φ2, φ1⟫_(SpaceTime → ℂ) = ⟪φ1, φ2⟫_(SpaceTime → ℂ) := funext fun x => inner_conj_symm (φ1 x) (φ2 x)
C.3.3. Linearity conditions
lemma inner_add_left (φ1 φ2 φ3 : HiggsField) : ⟪φ1 + φ2, φ3⟫_(SpaceTime → ℂ) = ⟪φ1, φ3⟫_(SpaceTime → ℂ) + ⟪φ2, φ3⟫_(SpaceTime → ℂ) := funext fun x => _root_.inner_add_left (φ1 x) (φ2 x) (φ3 x)lemma inner_add_right (φ1 φ2 φ3 : HiggsField) : ⟪φ1, φ2 + φ3⟫_(SpaceTime → ℂ) = ⟪φ1, φ2⟫_(SpaceTime → ℂ) + ⟪φ1, φ3⟫_(SpaceTime → ℂ) := funext fun x => _root_.inner_add_right (φ1 x) (φ2 x) (φ3 x)@[simp] lemma inner_zero_left (φ : HiggsField) : ⟪0, φ⟫_(SpaceTime → ℂ) = 0 := funext fun x => _root_.inner_zero_left (φ x)@[simp] lemma inner_zero_right (φ : HiggsField) : ⟪φ, 0⟫_(SpaceTime → ℂ) = 0 := funext fun x => _root_.inner_zero_right (φ x)lemma inner_neg_left (φ1 φ2 : HiggsField) : ⟪-φ1, φ2⟫_(SpaceTime → ℂ) = -⟪φ1, φ2⟫_(SpaceTime → ℂ) := funext fun x => _root_.inner_neg_left (φ1 x) (φ2 x)lemma inner_neg_right (φ1 φ2 : HiggsField) : ⟪φ1, -φ2⟫_(SpaceTime → ℂ) = -⟪φ1, φ2⟫_(SpaceTime → ℂ) := funext fun x => _root_.inner_neg_right (φ1 x) (φ2 x)
C.3.4. Smoothness of the inner product
lemma inner_smooth (φ1 φ2 : HiggsField) : ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) ⊤ ⟪φ1, φ2⟫_(SpaceTime → ℂ) := ContDiff.contMDiff <| (isBoundedBilinearMap_inner (𝕜 := ℂ)).contDiff.comp (φ1.contDiff.prodMk φ2.contDiff)

C.4. The pointwise norm

We define the pointwise norm-squared of a Higgs field.

Given an element φ of HiggsField, normSq φ is defined as the the function SpaceTime → ℝ obtained by taking the square norm of the pointwise Higgs vector. In other words, normSq φ x = ‖φ x‖ ^ 2.

The notation ‖φ‖_H^2 is used for the normSq φ.

@[simp] def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ‖φ x‖ ^ 2
@[inherit_doc normSq] scoped[StandardModel.HiggsField] notation "‖" φ1 "‖_H^2" => normSq φ1
C.4.1. Basic equalities
lemma inner_self_eq_normSq (φ : HiggsField) (x : SpaceTime) : ⟪φ, φ⟫_(SpaceTime → ℂ) x = ‖φ‖_H^2 x := φ:HiggsFieldx:SpaceTime⊢ ⟪φ, φ⟫_(SpaceTime → ℂ) x = ↑(‖φ‖_H^2 x) All goals completed! 🐙All goals completed! 🐙

The expansion of the norm squared of into components.

All goals completed! 🐙
C.4.2. Positivity
lemma normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ ‖φ‖_H^2 x := sq_nonneg _
C.4.3. On the zero section
@[simp] lemma normSq_zero : ‖0‖_H^2 = 0 := ⊢ ‖0‖_H^2 = 0 x:SpaceTime⊢ ‖0‖_H^2 x = 0 x All goals completed! 🐙
C.4.4. Smoothness of the norm-squared

The norm squared of the Higgs field is a smooth function on space-time.

φ:HiggsField⊢ ContMDiff 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) ⊤ (⇑reCLM ∘ ⟪φ, φ⟫_(SpaceTime → ℂ)) All goals completed! 🐙
C.4.5. Norm-squared of constant Higgs fields
@[simp] lemma const_normSq (φ : HiggsVec) (x : SpaceTime) : ‖const φ‖_H^2 x = ‖φ‖ ^ 2 := φ:HiggsVecx:SpaceTime⊢ ‖const φ‖_H^2 x = ‖φ‖ ^ 2 All goals completed! 🐙

C.5. The action of the gauge group on Higgs fields

The results in this section are currently informal.

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.

informal_definition gaugeAction where deps := [``gaugeTransformI] tag := "6V2NP"

There exists a g in gaugeTransformI such that gaugeAction g φ = φ' iff φ(x)^† φ(x) = φ'(x)^† φ'(x).

informal_lemma guage_orbit where deps := [``gaugeAction] tag := "6V2NX"

For every smooth map f from SpaceTime to ℝ such that f is positive semidefinite, there exists a Higgs field φ such that f = φ^† φ.

informal_lemma gauge_orbit_surject where deps := [``HiggsField, ``SpaceTime] tag := "6V2OC"