Informal dependency graph for HepLean
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.HiggsVec
Docstring: The complex vector space in which the Higgs field takes values.
SpaceTime
Docstring: The space-time
SpaceTime
Docstring: The space-time
SpaceTime
Docstring: The space-time
LorentzGroup
Docstring: The Lorentz group is the subset of matrices which preserve the minkowski metric.
LorentzGroup.IsProper
Docstring: A Lorentz Matrix is proper if its determinant is 1.
LorentzGroup.IsOrthochronous
Docstring: A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative.
SpaceTime.SL2C.toLorentzGroup
Docstring: The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`.
SpaceTime.SL2C.toLorentzGroup
Docstring: The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`.
LorentzGroup.timeComp
Docstring: The time like element of a Lorentz matrix.
SpaceTime.SL2C.toLorentzGroup
Docstring: The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupQuot
Docstring: Specifies the allowed quotients of `SU(3) x SU(2) x U(1)` which give a valid
gauge group of the Standard Model.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
StandardModel.GaugeGroupI
Docstring: The global gauge group of the Standard Model with no discrete quotients.
The `I` in the Name is an indication of the statement that this has no discrete quotients.
SpaceTime
Docstring: The space-time
StandardModel.HiggsField.zero
Docstring: The higgs field which is all zero.
StandardModel.HiggsVec
Docstring: The complex vector space in which the Higgs field takes values.
StandardModel.HiggsVec.rep
Docstring: The representation of the gauge group acting on `higgsVec`.
StandardModel.HiggsVec
Docstring: The complex vector space in which the Higgs field takes values.
StandardModel.HiggsVec.rep
Docstring: The representation of the gauge group acting on `higgsVec`.
StandardModel.HiggsVec.rep
Docstring: The representation of the gauge group acting on `higgsVec`.
StandardModel.HiggsField
Docstring: A Higgs field is a smooth section of the Higgs bundle.
SpaceTime
Docstring: The space-time
StandardModel.HiggsField.Potential.IsBounded
Docstring: The proposition on the coefficents for a potential to be bounded.
StandardModel.HiggsField.Potential
Docstring: The parameters of the Higgs potential.
GeorgiGlashow.GaugeGroupI
Math description: The group `SU(5)`.
Physics description: The gauge group of the Georgi-Glashow model.
GeorgiGlashow.inclSM
Math description: The group homomorphism `SU(3) x SU(2) x U(1) -> SU(5)`
taking (h, g, α) to (blockdiag (α ^ 3 g, α ^ (-2) h).
Physics description: The homomorphism of the Standard Model gauge group into the
Georgi-Glashow gauge group.
GeorgiGlashow.inclSM_ker
Math description: The kernel of the map ``inclSM is equal to the subgroup
``StandardModel.gaugeGroupℤ₆SubGroup.
Physics description: No physics description provided
GeorgiGlashow.embedSMℤ₆
Math description: The group embedding from ``StandardModel.GaugeGroupℤ₆ to ``GaugeGroupI
induced by ``inclSM by quotienting by the kernal ``inclSM_ker.
Physics description: No physics description provided
PatiSalam.GaugeGroupI
Math description: The group `SU(4) x SU(2) x SU(2)`.
Physics description: The gauge group of the Pati-Salam model (unquotiented by ℤ₂).
PatiSalam.inclSM
Math description: The group homomorphism `SU(3) x SU(2) x U(1) -> SU(4) x SU(2) x SU(2)`
taking (h, g, α) to (blockdiag (α h, α ^ (-3)), g, diag(α ^ (3), α ^(-3))).
Physics description: The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group.
PatiSalam.inclSM_ker
Math description: The kernel of the map ``inclSM is equal to the subgroup
``StandardModel.gaugeGroupℤ₃SubGroup.
Physics description: No physics description provided
PatiSalam.embedSMℤ₃
Math description: The group embedding from ``StandardModel.GaugeGroupℤ₃ to ``GaugeGroupI
induced by ``inclSM by quotienting by the kernal ``inclSM_ker.
Physics description: No physics description provided
PatiSalam.gaugeGroupISpinEquiv
Math description: The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`.
Physics description: No physics description provided
PatiSalam.gaugeGroupℤ₂SubGroup
Math description: The ℤ₂-subgroup of ``GaugeGroupI with the non-trivial element (-1, -1, -1).
Physics description: The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on
all particles in the standard model.
PatiSalam.GaugeGroupℤ₂
Math description: The quotient of ``GaugeGroupI by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`.
Physics description: The gauge group of the Pati-Salam model with a ℤ₂ quotient.
PatiSalam.sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup
Math description: The group ``StandardModel.gaugeGroupℤ₆SubGroup under the homomorphism ``embedSM factors
through the subgroup ``gaugeGroupℤ₂SubGroup.
Physics description: No physics description provided
PatiSalam.embedSMℤ₆Toℤ₂
Math description: The group homomorphism from ``StandardModel.GaugeGroupℤ₆ to ``GaugeGroupℤ₂
induced by ``embedSM.
Physics description: No physics description provided
Spin10Model.GaugeGroupI
Math description: The group `Spin(10)`.
Physics description: The gauge group of the Spin(10) model (aka SO(10)-model.)
Spin10Model.inclPatiSalam
Math description: The lift of the embedding `SO(6) x SO(4) → SO(10)` to universal covers,
giving a homomorphism `Spin(6) x Spin(4) → Spin(10)`. Precomposed with the isomorphism,
``PatiSalam.gaugeGroupISpinEquiv, between `SU(4) x SU(2) x SU(2)` and `Spin(6) x Spin(4)`.
Physics description: The inclusion of the Pati-Salam gauge group into Spin(10).
Spin10Model.inclSM
Math description: The compoisiton of ``embedPatiSalam and ``PatiSalam.inclSM.
Physics description: The inclusion of the Standard Model gauge group into Spin(10).
Spin10Model.inclGeorgiGlashow
Math description: The Lie group homomorphism from SU(n) → Spin(2n) dicussed on page 46 of
https://math.ucr.edu/home/baez/guts.pdf for n = 5.
Physics description: The inclusion of the Georgi-Glashow gauge group into Spin(10).
Spin10Model.inclSMThruGeorgiGlashow
Math description: The composition of ``inclGeorgiGlashow and ``GeorgiGlashow.inclSM.
Physics description: The inclusion of the Standard Model gauge group into Spin(10).
Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow
Math description: The inclusion ``inclSM is equal to the inclusion ``inclSMThruGeorgiGlashow.
Physics description: No physics description provided
TwoHDM.prodMatrix
Math description: For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices
defined by ((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂)).
Physics description: No physics description provided
TwoHDM.prodMatrix_positive_semidefinite
Math description: For all x in ``SpaceTime, ``prodMatrix at `x` is positive semidefinite.
Physics description: No physics description provided
TwoHDM.prodMatrix_hermitian
Math description: For all x in ``SpaceTime, ``prodMatrix at `x` is hermitian.
Physics description: No physics description provided
TwoHDM.prodMatrix_smooth
Math description: The map ``prodMatrix is a smooth function on spacetime.
Physics description: No physics description provided
LorentzGroup.Restricted
Math description: The subgroup of the Lorentz group consisting of elements which
are proper and orthochronous.
Physics description: No physics description provided
SpaceTime.SL2C.toLorentzGroup_det_one
Math description: The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one.
Physics description: No physics description provided
SpaceTime.SL2C.toLorentzGroup_timeComp_nonneg
Math description: The time coponent of the image of `SL(2, ℂ)` in the Lorentz group is non-negative.
Physics description: No physics description provided
SpaceTime.SL2C.toRestrictedLorentzGroup
Math description: The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group.
Physics description: No physics description provided
Fermion.leftHandedWeyl
Math description: The vector space ℂ^2 carrying the fundamental representation of SL(2,C).
Physics description: A Weyl fermion with indices ψ_a.
Fermion.rightHandedWeyl
Math description: The vector space ℂ^2 carrying the conjguate representation of SL(2,C).
Physics description: A Weyl fermion with indices ψ_{dot a}.
Fermion.altLeftHandedWeyl
Math description: The vector space ℂ^2 carrying the representation of SL(2,C) given by
M → (M⁻¹)ᵀ.
Physics description: A Weyl fermion with indices ψ^a.
Fermion.altRightHandedWeyl
Math description: The vector space ℂ^2 carrying the representation of SL(2,C) given by
M → (M⁻¹)^†.
Physics description: A Weyl fermion with indices ψ^{dot a}.
Fermion.leftHandedWeylAltEquiv
Math description: The linear equiv between leftHandedWeyl and altLeftHandedWeyl given
by multiplying an element of rightHandedWeyl by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`.
Physics description: No physics description provided
Fermion.leftHandedWeylAltEquiv_equivariant
Math description: The linear equiv leftHandedWeylAltEquiv is equivariant with respect to the
action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl.
Physics description: No physics description provided
Fermion.rightHandedWeylAltEquiv
Math description: The linear equiv between rightHandedWeyl and altRightHandedWeyl given
by multiplying an element of rightHandedWeyl by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`
Physics description: No physics description provided
Fermion.rightHandedWeylAltEquiv_equivariant
Math description: The linear equiv rightHandedWeylAltEquiv is equivariant with respect to the
action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl.
Physics description: No physics description provided
Fermion.leftAltWeylContraction
Math description: The linear map from leftHandedWeyl ⊗ altLeftHandedWeyl to ℂ given by
summing over components of leftHandedWeyl and altLeftHandedWeyl in the
standard basis (i.e. the dot product).
Physics description: The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
In index notation this is ψ_a φ^a.
Fermion.leftAltWeylContraction_invariant
Math description: The contraction leftAltWeylContraction is invariant with respect to
the action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl.
Physics description: No physics description provided
Fermion.altLeftWeylContraction
Math description: The linear map from altLeftHandedWeyl ⊗ leftHandedWeyl to ℂ given by
summing over components of altLeftHandedWeyl and leftHandedWeyl in the
standard basis (i.e. the dot product).
Physics description: The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
In index notation this is φ^a ψ_a .
Fermion.leftAltWeylContraction_symm_altLeftWeylContraction
Math description: The linear map altLeftWeylContraction is leftAltWeylContraction composed
with the braiding of the tensor product.
Physics description: No physics description provided
Fermion.altLeftWeylContraction_invariant
Math description: The contraction altLeftWeylContraction is invariant with respect to
the action of SL(2,C) on leftHandedWeyl and altLeftHandedWeyl.
Physics description: No physics description provided
Fermion.rightAltWeylContraction
Math description: The linear map from rightHandedWeyl ⊗ altRightHandedWeyl to ℂ given by
summing over components of rightHandedWeyl and altRightHandedWeyl in the
standard basis (i.e. the dot product).
Physics description: The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
In index notation this is ψ_{dot a} φ^{dot a}.
Fermion.rightAltWeylContraction_invariant
Math description: The contraction rightAltWeylContraction is invariant with respect to
the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl.
Physics description: No physics description provided
Fermion.altRightWeylContraction
Math description: The linear map from altRightHandedWeyl ⊗ rightHandedWeyl to ℂ given by
summing over components of altRightHandedWeyl and rightHandedWeyl in the
standard basis (i.e. the dot product).
Physics description: The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
In index notation this is φ^{dot a} ψ_{dot a}.
Fermion.rightAltWeylContraction_symm_altRightWeylContraction
Math description: The linear map altRightWeylContraction is rightAltWeylContraction composed
with the braiding of the tensor product.
Physics description: No physics description provided
Fermion.altRightWeylContraction_invariant
Math description: The contraction altRightWeylContraction is invariant with respect to
the action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl.
Physics description: No physics description provided
StandardModel.gaugeGroupℤ₆SubGroup
Math description: The ℤ₆-subgroup of ``GaugeGroupI with elements (α^2 * I₃, α^(-3) * I₂, α), where `α`
is a sixth complex root of unity.
Physics description: The subgroup of the un-quotiented gauge group which acts trivially on
all particles in the standard model.
StandardModel.GaugeGroupℤ₆
Math description: The quotient of ``GaugeGroupI by the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`.
Physics description: The smallest possible gauge group of the Standard Model.
StandardModel.gaugeGroupℤ₂SubGroup
Math description: The ℤ₂-subgroup of ``GaugeGroupI derived from the ℤ₂ subgroup of `gaugeGroupℤ₆SubGroup`.
Physics description: The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on
all particles in the standard model.
StandardModel.GaugeGroupℤ₂
Math description: The quotient of ``GaugeGroupI by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`.
Physics description: The guage group of the Standard Model with a ℤ₂ quotient.
StandardModel.gaugeGroupℤ₃SubGroup
Math description: The ℤ₃-subgroup of ``GaugeGroupI derived from the ℤ₃ subgroup of `gaugeGroupℤ₆SubGroup`.
Physics description: The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on
all particles in the standard model.
StandardModel.GaugeGroupℤ₃
Math description: The quotient of ``GaugeGroupI by the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`.
Physics description: The guage group of the Standard Model with a ℤ₃-quotient.
StandardModel.GaugeGroup
Math description: The map from `GaugeGroupQuot` to `Type` which gives the gauge group of the Standard Model
for a given choice of quotient.
Physics description: The (global) gauge group of the Standard Model given a choice of quotient.
StandardModel.gaugeGroupI_lie
Math description: The gauge group `GaugeGroupI` is a Lie group..
Physics description: No physics description provided
StandardModel.gaugeGroup_lie
Math description: For every q in ``GaugeGroupQuot the group ``GaugeGroup q is a Lie group.
Physics description: No physics description provided
StandardModel.gaugeBundleI
Math description: The trivial principal bundle over SpaceTime with structure group ``GaugeGroupI.
Physics description: No physics description provided
StandardModel.HiggsField.zero_is_zero_section
Math description: The HiggsField `zero` defined by `ofReal 0`
is the constant zero-section of the bundle `HiggsBundle`.
Physics description: The zero Higgs field is the zero section of the Higgs bundle.
StandardModel.HiggsVec.guage_orbit
Math description: There exists a `g` in ``GaugeGroupI such that `rep g φ = φ'` if and only if
‖φ‖ = ‖φ'‖.
Physics description: No physics description provided
StandardModel.HiggsVec.stability_group_single
Math description: The stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`,
for non-zero `‖φ‖` is the `SU(3) x U(1)` subgroup of
`gaugeGroup := SU(3) x SU(2) x U(1)` with the embedding given by
`(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`.
Physics description: The Higgs boson breaks electroweak symmetry down to the electromagnetic force.
StandardModel.HiggsVec.stability_group
Math description: The subgroup of `gaugeGroup := SU(3) x SU(2) x U(1)` which preserves every `HiggsVec`
by the action of ``StandardModel.HiggsVec.rep is given by `SU(3) x ℤ₆` where ℤ₆
is the subgroup of `SU(2) x U(1)` with elements `(α^(-3) * I₂, α)` where
α is a sixth root of unity.
Physics description: No physics description provided
StandardModel.HiggsField.gaugeAction
Math description: The action of ``gaugeTransformI on ``HiggsField acting pointwise through
``HiggsVec.rep.
Physics description: No physics description provided
StandardModel.HiggsField.guage_orbit
Math description: There exists a `g` in ``gaugeTransformI such that `gaugeAction g φ = φ'` if and only if
φ(x)^† φ(x) = φ'(x)^† φ'(x).
Physics description: No physics description provided
StandardModel.HiggsField.gauge_orbit_surject
Math description: For every smooth map f from ``SpaceTime to ℝ such that `f` is positive semidefinite,
there exists a Higgs field φ such that `f = φ^† φ`.
Physics description: No physics description provided
StandardModel.HiggsField.Potential.isBounded_iff_of_𝓵_zero
Math description: For `P : Potential` then P.IsBounded if and only if P.μ2 ≤ 0.
That is to say `- P.μ2 * ‖φ‖_H ^ 2 x` is bounded below if and only if `P.μ2 ≤ 0`.
Physics description: When there is no quartic coupling, the potential is bounded iff the mass squared is
non-positive.