Informal dependency graph for PhysLean
Click on a node to display the text associated with it.
This graph only shows informal results (gray) and their direct formal dependencies (blue). It does not show all results formalised into PhysLean.
TensorSpecies.dualRepIsoDiscrete
Description: The isomorphism between the representation associated with a color, and that associated with its dual.
Description: The isomorphism between the representation associated with a color, and that associated with its dual.
IndexNotation.OverColor.forget
Description: The forgetful map from `BraidedFunctor (OverColor C) (Rep k G)` to `Discrete C ⥤ Rep k G` built on the inclusion `incl` and forgetting the monoidal structure.
Description: The forgetful map from `BraidedFunctor (OverColor C) (Rep k G)` to `Discrete C ⥤ Rep k G` built on the inclusion `incl` and forgetting the monoidal structure.
SpaceTime
Description: The space-time
Description: The space-time
LorentzGroup.IsOrthochronous
Description: A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative.
Description: A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative.
TensorSpecies.contractSelfField
Description: The contraction of two vectors in a tensor species of the same color, as a linear map to the underlying field.
Description: The contraction of two vectors in a tensor species of the same color, as a linear map to the underlying field.
Fermion.rightHanded
Description: The vector space ℂ^2 carrying the conjugate representation of SL(2,C). In index notation corresponds to a Weyl fermion with indices ψ^{dot a}.
Description: The vector space ℂ^2 carrying the conjugate representation of SL(2,C). In index notation corresponds to a Weyl fermion with indices ψ^{dot a}.
StandardModel.HiggsField.Potential
Description: The structure `Potential` is defined with two fields, `μ2` corresponding to the mass-squared of the Higgs boson, and `l` corresponding to the coefficent of the quartic term in the Higgs potential. Note that `l` is usually denoted `λ`.
Description: The structure `Potential` is defined with two fields, `μ2` corresponding to the mass-squared of the Higgs boson, and `l` corresponding to the coefficent of the quartic term in the Higgs potential. Note that `l` is usually denoted `λ`.
StandardModel.HiggsField.zero
Description: The higgs field which is all zero.
Description: The higgs field which is all zero.
TensorSpecies.unitTensor
Description: The unit of a tensor species in a `PiTensorProduct`.
Description: The unit of a tensor species in a `PiTensorProduct`.
StandardModel.GaugeGroupQuot
Description: Specifies the allowed quotients of `SU(3) x SU(2) x U(1)` which give a valid gauge group of the Standard Model.
Description: Specifies the allowed quotients of `SU(3) x SU(2) x U(1)` which give a valid gauge group of the Standard Model.
StandardModel.HiggsVec.rotate_fst_zero_snd_real
Description: For every Higgs vector there exists an element of the gauge group which rotates that Higgs vector to have `0` in the first component and be a non-negative real in the second component.
Description: For every Higgs vector there exists an element of the gauge group which rotates that Higgs vector to have `0` in the first component and be a non-negative real in the second component.
complexLorentzTensor.rightMetric
Description: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
Description: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
StandardModel.HiggsVec
Description: 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`.
Description: 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`.
Lorentz.SL2C.toLorentzGroup
Description: The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
Description: The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
Fermion.altRightHanded
Description: The vector space ℂ^2 carrying the representation of SL(2,C) given by M → (M⁻¹)^†. In index notation this corresponds to a Weyl fermion with index `ψ_{dot a}`.
Description: The vector space ℂ^2 carrying the representation of SL(2,C) given by M → (M⁻¹)^†. In index notation this corresponds to a Weyl fermion with index `ψ_{dot a}`.
TwoHDM.prodMatrix
Description: For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices defined by `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
Description: For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices defined by `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
complexLorentzTensor.leftMetric
Description: The metric `εᵃᵃ` as a complex Lorentz tensor.
Description: The metric `εᵃᵃ` as a complex Lorentz tensor.
complexLorentzTensor.coBispinorDown
Description: A bispinor `pₐₐ` created from a lorentz vector `p_μ`.
Description: A bispinor `pₐₐ` created from a lorentz vector `p_μ`.
Lorentz.SL2C.toLorentzGroup_det_one
Description: The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one.
Description: The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one.
StandardModel.HiggsVec.rep
Description: The representation of the gauge group acting on `higgsVec`.
Description: The representation of the gauge group acting on `higgsVec`.
Lorentz.SL2C.toLorentzGroup_isOrthochronous
Description: The image of `SL(2, ℂ)` in the Lorentz group is orthochronous.
Description: The image of `SL(2, ℂ)` in the Lorentz group is orthochronous.
complexLorentzTensor.contrBispinorDown
Description: A bispinor `pₐₐ` created from a lorentz vector `p^μ`.
Description: A bispinor `pₐₐ` created from a lorentz vector `p^μ`.
TensorSpecies.metricTensor
Description: The metric of a tensor species in a `PiTensorProduct`.
Description: The metric of a tensor species in a `PiTensorProduct`.
complexLorentzTensor.contrBispinorUp
Description: A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`.
Description: A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`.
complexLorentzTensor.coBispinorUp
Description: A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`.
Description: A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`.
IndexNotation.OverColor.lift
Description: The functor taking functors in `Discrete C ⥤ Rep k G` to monoidal functors in `BraidedFunctor (OverColor C) (Rep k G)`, built on the PiTensorProduct.
Description: The functor taking functors in `Discrete C ⥤ Rep k G` to monoidal functors in `BraidedFunctor (OverColor C) (Rep k G)`, built on the PiTensorProduct.
StandardModel.HiggsField
Description: 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`.
Description: 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`.
TensorTree
Description: A syntax tree for tensor expressions.
Description: A syntax tree for tensor expressions.
LorentzGroup
Description: The Lorentz group is the subset of matrices for which `Λ * dual Λ = 1`.
Description: The Lorentz group is the subset of matrices for which `Λ * dual Λ = 1`.
TensorTree.constTwoNode
Description: A constant two tensor (e.g. metric and unit).
Description: A constant two tensor (e.g. metric and unit).
TwoHDM.prodMatrix_smooth
Description: The map `prodMatrix` is a smooth function on spacetime.
Description: The map `prodMatrix` is a smooth function on spacetime.
LorentzGroup.IsProper
Description: A Lorentz Matrix is proper if its determinant is 1.
Description: A Lorentz Matrix is proper if its determinant is 1.
StandardModel.GaugeGroupI
Description: 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.
Description: 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.
TensorTree.constVecNode
Description: A constant vector.
Description: A constant vector.
TensorTree.vecNode
Description: A node consisting of a single vector.
Description: A node consisting of a single vector.
TensorTree.twoNode
Description: A node consisting of a two tensor.
Description: A node consisting of a two tensor.
StandardModel.HiggsField.Potential.IsBounded
Description: Given a element `P` of `Potential`, the proposition `IsBounded P` is true if and only if there exists a real `c` such that for all Higgs fields `φ` and spacetime points `x`, the Higgs potential corresponding to `φ` at `x` is greater then or equal to`c`. I.e. `∀ Φ x, c ≤ P.toFun Φ x`.
Description: Given a element `P` of `Potential`, the proposition `IsBounded P` is true if and only if there exists a real `c` such that for all Higgs fields `φ` and spacetime points `x`, the Higgs potential corresponding to `φ` at `x` is greater then or equal to`c`. I.e. `∀ Φ x, c ≤ P.toFun Φ x`.
GeorgiGlashow.GaugeGroupI
Description: The gauge group of the Georgi-Glashow model, i.e., `SU(5)`.
Description: The gauge group of the Georgi-Glashow model, i.e., `SU(5)`.
GeorgiGlashow.inclSM
Description: The homomorphism of the Standard Model gauge group into the Georgi-Glashow gauge group, i.e., the group homomorphism `SU(3) × SU(2) × U(1) → SU(5)` taking `(h, g, α)` to `blockdiag (α ^ 3 g, α ^ (-2) h)`. See page 34 of https://math.ucr.edu/home/baez/guts.pdf
Description: The homomorphism of the Standard Model gauge group into the Georgi-Glashow gauge group, i.e., the group homomorphism `SU(3) × SU(2) × U(1) → SU(5)` taking `(h, g, α)` to `blockdiag (α ^ 3 g, α ^ (-2) h)`. See page 34 of https://math.ucr.edu/home/baez/guts.pdf
GeorgiGlashow.inclSM_ker
Description: The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₆SubGroup`. See page 34 of https://math.ucr.edu/home/baez/guts.pdf
Description: The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₆SubGroup`. See page 34 of https://math.ucr.edu/home/baez/guts.pdf
GeorgiGlashow.embedSMℤ₆
Description: The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.
Description: The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.
PatiSalam.GaugeGroupI
Description: The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., `SU(4) × SU(2) × SU(2)`.
Description: The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., `SU(4) × SU(2) × SU(2)`.
PatiSalam.inclSM
Description: The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group, i.e., the group homomorphism `SU(3) × SU(2) × U(1) → SU(4) × SU(2) × SU(2)` taking `(h, g, α)` to `(blockdiag (α h, α ^ (-3)), g, diag (α ^ 3, α ^(-3))`. See page 54 of https://math.ucr.edu/home/baez/guts.pdf
Description: The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group, i.e., the group homomorphism `SU(3) × SU(2) × U(1) → SU(4) × SU(2) × SU(2)` taking `(h, g, α)` to `(blockdiag (α h, α ^ (-3)), g, diag (α ^ 3, α ^(-3))`. See page 54 of https://math.ucr.edu/home/baez/guts.pdf
PatiSalam.inclSM_ker
Description: The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₃SubGroup`. See footnote 10 of https://arxiv.org/pdf/2201.07245
Description: The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₃SubGroup`. See footnote 10 of https://arxiv.org/pdf/2201.07245
PatiSalam.embedSMℤ₃
Description: The group embedding from `StandardModel.GaugeGroupℤ₃` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.
Description: The group embedding from `StandardModel.GaugeGroupℤ₃` to `GaugeGroupI` induced by `inclSM` by quotienting by the kernel `inclSM_ker`.
PatiSalam.gaugeGroupISpinEquiv
Description: The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`.
Description: The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`.
PatiSalam.gaugeGroupℤ₂SubGroup
Description: The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` with the non-trivial element `(-1, -1, -1)`. See https://math.ucr.edu/home/baez/guts.pdf
Description: The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` with the non-trivial element `(-1, -1, -1)`. See https://math.ucr.edu/home/baez/guts.pdf
PatiSalam.GaugeGroupℤ₂
Description: The gauge group of the Pati-Salam model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
Description: The gauge group of the Pati-Salam model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
PatiSalam.sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup
Description: The group `StandardModel.gaugeGroupℤ₆SubGroup` under the homomorphism `embedSM` factors through the subgroup `gaugeGroupℤ₂SubGroup`.
Description: The group `StandardModel.gaugeGroupℤ₆SubGroup` under the homomorphism `embedSM` factors through the subgroup `gaugeGroupℤ₂SubGroup`.
PatiSalam.embedSMℤ₆Toℤ₂
Description: The group homomorphism from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupℤ₂` induced by `embedSM`.
Description: The group homomorphism from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupℤ₂` induced by `embedSM`.
Spin10Model.GaugeGroupI
Description: The gauge group of the Spin(10) model, i.e., the group `Spin(10)`.
Description: The gauge group of the Spin(10) model, i.e., the group `Spin(10)`.
Spin10Model.inclPatiSalam
Description: The inclusion of the Pati-Salam gauge group into Spin(10), i.e., the lift of the embedding `SO(6) × SO(4) → SO(10)` to universal covers, giving a homomorphism `Spin(6) × Spin(4) → Spin(10)`. Precomposed with the isomorphism, `PatiSalam.gaugeGroupISpinEquiv`, between `SU(4) × SU(2) × SU(2)` and `Spin(6) × Spin(4)`. See page 56 of https://math.ucr.edu/home/baez/guts.pdf
Description: The inclusion of the Pati-Salam gauge group into Spin(10), i.e., the lift of the embedding `SO(6) × SO(4) → SO(10)` to universal covers, giving a homomorphism `Spin(6) × Spin(4) → Spin(10)`. Precomposed with the isomorphism, `PatiSalam.gaugeGroupISpinEquiv`, between `SU(4) × SU(2) × SU(2)` and `Spin(6) × Spin(4)`. See page 56 of https://math.ucr.edu/home/baez/guts.pdf
Spin10Model.inclSM
Description: The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of `embedPatiSalam` and `PatiSalam.inclSM`. See page 56 of https://math.ucr.edu/home/baez/guts.pdf
Description: The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of `embedPatiSalam` and `PatiSalam.inclSM`. See page 56 of https://math.ucr.edu/home/baez/guts.pdf
Spin10Model.inclGeorgiGlashow
Description: The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism from `SU(n) → Spin(2n)` discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for `n = 5`.
Description: The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism from `SU(n) → Spin(2n)` discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for `n = 5`.
Spin10Model.inclSMThruGeorgiGlashow
Description: The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of `inclGeorgiGlashow` and `GeorgiGlashow.inclSM`.
Description: The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of `inclGeorgiGlashow` and `GeorgiGlashow.inclSM`.
Spin10Model.inclSM_eq_inclSMThruGeorgiGlashow
Description: The inclusion `inclSM` is equal to the inclusion `inclSMThruGeorgiGlashow`.
Description: The inclusion `inclSM` is equal to the inclusion `inclSMThruGeorgiGlashow`.
TwoHDM.prodMatrix_invariant
Description: The map `prodMatrix` is invariant under the simultaneous action of `gaugeAction` on the two Higgs fields.
Description: The map `prodMatrix` is invariant under the simultaneous action of `gaugeAction` on the two Higgs fields.
TwoHDM.prodMatrix_to_higgsField
Description: 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
Description: 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
StandardModel.gaugeGroupℤ₆SubGroup
Description: The subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₆-subgroup of `GaugeGroupI` with elements `(α^2 * I₃, α^(-3) * I₂, α)`, where `α` is a sixth complex root of unity. See https://math.ucr.edu/home/baez/guts.pdf
Description: The subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₆-subgroup of `GaugeGroupI` with elements `(α^2 * I₃, α^(-3) * I₂, α)`, where `α` is a sixth complex root of unity. See https://math.ucr.edu/home/baez/guts.pdf
StandardModel.GaugeGroupℤ₆
Description: The smallest possible gauge group of the Standard Model, i.e., the quotient of `GaugeGroupI` by the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
Description: The smallest possible gauge group of the Standard Model, i.e., the quotient of `GaugeGroupI` by the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
StandardModel.gaugeGroupℤ₂SubGroup
Description: The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` derived from the ℤ₂ subgroup of `gaugeGroupℤ₆SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
Description: The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` derived from the ℤ₂ subgroup of `gaugeGroupℤ₆SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
StandardModel.GaugeGroupℤ₂
Description: The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
Description: The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
StandardModel.gaugeGroupℤ₃SubGroup
Description: The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₃-subgroup of `GaugeGroupI` derived from the ℤ₃ subgroup of `gaugeGroupℤ₆SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
Description: The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on all particles in the standard model, i.e., the ℤ₃-subgroup of `GaugeGroupI` derived from the ℤ₃ subgroup of `gaugeGroupℤ₆SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
StandardModel.GaugeGroupℤ₃
Description: The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
Description: The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`. See https://math.ucr.edu/home/baez/guts.pdf
StandardModel.GaugeGroup
Description: The (global) gauge group of the Standard Model given a choice of quotient, i.e., the map from `GaugeGroupQuot` to `Type` which gives the gauge group of the Standard Model for a given choice of quotient. See https://math.ucr.edu/home/baez/guts.pdf
Description: The (global) gauge group of the Standard Model given a choice of quotient, i.e., the map from `GaugeGroupQuot` to `Type` which gives the gauge group of the Standard Model for a given choice of quotient. See https://math.ucr.edu/home/baez/guts.pdf
StandardModel.gaugeGroupI_lie
Description: The gauge group `GaugeGroupI` is a Lie group.
Description: The gauge group `GaugeGroupI` is a Lie group.
StandardModel.gaugeGroup_lie
Description: For every `q` in `GaugeGroupQuot` the group `GaugeGroup q` is a Lie group.
Description: For every `q` in `GaugeGroupQuot` the group `GaugeGroup q` is a Lie group.
StandardModel.gaugeBundleI
Description: The trivial principal bundle over SpaceTime with structure group `GaugeGroupI`.
Description: The trivial principal bundle over SpaceTime with structure group `GaugeGroupI`.
StandardModel.gaugeTransformI
Description: A global section of `gaugeBundleI`.
Description: A global section of `gaugeBundleI`.
StandardModel.HiggsField.zero_is_zero_section
Description: The zero Higgs field is the zero section of the Higgs bundle, i.e., the HiggsField `zero` defined by `ofReal 0` is the constant zero-section of the bundle `HiggsBundle`.
Description: The zero Higgs field is the zero section of the Higgs bundle, i.e., the HiggsField `zero` defined by `ofReal 0` is the constant zero-section of the bundle `HiggsBundle`.
StandardModel.HiggsVec.guage_orbit
Description: There exists a `g` in `GaugeGroupI` such that `rep g φ = φ'` iff `‖φ‖ = ‖φ'‖`.
Description: There exists a `g` in `GaugeGroupI` such that `rep g φ = φ'` iff `‖φ‖ = ‖φ'‖`.
StandardModel.HiggsVec.stability_group_single
Description: 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 θ})`.
Description: 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 θ})`.
StandardModel.HiggsVec.stability_group
Description: 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.
Description: 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.
StandardModel.HiggsField.gaugeAction
Description: The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`.
Description: The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`.
StandardModel.HiggsField.guage_orbit
Description: There exists a `g` in `gaugeTransformI` such that `gaugeAction g φ = φ'` iff `φ(x)^† φ(x) = φ'(x)^† φ'(x)`.
Description: There exists a `g` in `gaugeTransformI` such that `gaugeAction g φ = φ'` iff `φ(x)^† φ(x) = φ'(x)^† φ'(x)`.
StandardModel.HiggsField.gauge_orbit_surject
Description: For every smooth map `f` from `SpaceTime` to `ℝ` such that `f` is positive semidefinite, there exists a Higgs field `φ` such that `f = φ^† φ`.
Description: For every smooth map `f` from `SpaceTime` to `ℝ` such that `f` is positive semidefinite, there exists a Higgs field `φ` such that `f = φ^† φ`.
StandardModel.HiggsField.Potential.isBounded_iff_of_𝓵_zero
Description: When there is no quartic coupling, the potential is bounded iff the mass squared is non-positive, i.e., for `P : Potential` then `P.IsBounded` iff `P.μ2 ≤ 0`. That is to say `- P.μ2 * ‖φ‖_H^2 x` is bounded below iff `P.μ2 ≤ 0`.
Description: When there is no quartic coupling, the potential is bounded iff the mass squared is non-positive, i.e., for `P : Potential` then `P.IsBounded` iff `P.μ2 ≤ 0`. That is to say `- P.μ2 * ‖φ‖_H^2 x` is bounded below iff `P.μ2 ≤ 0`.
complexLorentzTensor.contrBispinorUp_eq_metric_contr_contrBispinorDown
Description: `{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ`. Proof: expand `contrBispinorDown` and use fact that metrics contract to the identity.
Description: `{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ`. Proof: expand `contrBispinorDown` and use fact that metrics contract to the identity.
complexLorentzTensor.coBispinorUp_eq_metric_contr_coBispinorDown
Description: `{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ`. proof: expand `coBispinorDown` and use fact that metrics contract to the identity.
Description: `{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ`. proof: expand `coBispinorDown` and use fact that metrics contract to the identity.
LorentzGroup.Restricted
Description: The subgroup of the Lorentz group consisting of elements which are proper and orthochronous.
Description: The subgroup of the Lorentz group consisting of elements which are proper and orthochronous.
Lorentz.SL2C.toRestrictedLorentzGroup
Description: The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group.
Description: The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group.
Fermion.rightHandedWeylAltEquiv
Description: The linear equivalence between `rightHandedWeyl` and `altRightHandedWeyl` given by multiplying an element of `rightHandedWeyl` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`.
Description: The linear equivalence between `rightHandedWeyl` and `altRightHandedWeyl` given by multiplying an element of `rightHandedWeyl` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`.
Fermion.rightHandedWeylAltEquiv_equivariant
Description: The linear equivalence `rightHandedWeylAltEquiv` is equivariant with respect to the action of `SL(2,C)` on `rightHandedWeyl` and `altRightHandedWeyl`.
Description: The linear equivalence `rightHandedWeylAltEquiv` is equivariant with respect to the action of `SL(2,C)` on `rightHandedWeyl` and `altRightHandedWeyl`.
IndexNotation.OverColor.forgetLift
Description: The natural isomorphism between `lift (C := C) ⋙ forget` and `Functor.id (Discrete C ⥤ Rep k G)`.
Description: The natural isomorphism between `lift (C := C) ⋙ forget` and `Functor.id (Discrete C ⥤ Rep k G)`.
TensorSpecies.contractSelfField_non_degenerate
Description: The contraction of two vectors of the same color is non-degenerate, i.e., `⟪ψ, φ⟫ₜₛ = 0` for all `φ` implies `ψ = 0`. Proof: the basic idea is that being degenerate contradicts the assumption of having a unit in the tensor species.
Description: The contraction of two vectors of the same color is non-degenerate, i.e., `⟪ψ, φ⟫ₜₛ = 0` for all `φ` implies `ψ = 0`. Proof: the basic idea is that being degenerate contradicts the assumption of having a unit in the tensor species.
TensorSpecies.contractSelfField_tensorTree
Description: The contraction `⟪ψ, φ⟫ₜₛ` is related to the tensor tree `{ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ`.
Description: The contraction `⟪ψ, φ⟫ₜₛ` is related to the tensor tree `{ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ`.
TensorSpecies.dualRepIso
Description: Given a `i : Fin n` the isomorphism between `S.F.obj (OverColor.mk c)` and `S.F.obj (OverColor.mk (Function.update c i (S.τ (c i))))` induced by `dualRepIsoDiscrete` acting on the `i`-th component of the color.
Description: Given a `i : Fin n` the isomorphism between `S.F.obj (OverColor.mk c)` and `S.F.obj (OverColor.mk (Function.update c i (S.τ (c i))))` induced by `dualRepIsoDiscrete` acting on the `i`-th component of the color.
TensorSpecies.dualRepIso_unitTensor_fst
Description: Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric.
Description: Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric.
TensorSpecies.dualRepIso_unitTensor_snd
Description: Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric.
Description: Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric.
TensorSpecies.dualRepIso_metricTensor_fst
Description: Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor.
Description: Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor.
TensorSpecies.dualRepIso_metricTensor_snd
Description: Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor.
Description: Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor.
TensorTree.constVecNode_eq_vecNode
Description: A `constVecNode` has equal tensor to the `vecNode` with the map evaluated at 1.
Description: A `constVecNode` has equal tensor to the `vecNode` with the map evaluated at 1.
TensorTree.constTwoNode_eq_twoNode
Description: A `constTwoNode` has equal tensor to the `twoNode` with the map evaluated at 1.
Description: A `constTwoNode` has equal tensor to the `twoNode` with the map evaluated at 1.