Informal dependency graph for HepLean
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 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.
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.
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.
TwoHDM.prodMatrix
Docstring: For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices defined by `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
Docstring: For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices defined by `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
TwoHDM.prodMatrix
Docstring: For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices defined by `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
Docstring: For two Higgs fields `Φ₁` and `Φ₂`, the map from space time to 2 x 2 complex matrices defined by `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
StandardModel.HiggsField
Docstring: A Higgs field is a smooth section of the Higgs bundle.
Docstring: A Higgs field is a smooth section of the Higgs bundle.
TwoHDM.prodMatrix_smooth
Docstring: The map `prodMatrix` is a smooth function on spacetime.
Docstring: The map `prodMatrix` is a smooth function on spacetime.
complexLorentzTensor.contrBispinorUp
Docstring: A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`.
Docstring: A bispinor `pᵃᵃ` created from a lorentz vector `p^μ`.
complexLorentzTensor.contrBispinorDown
Docstring: A bispinor `pₐₐ` created from a lorentz vector `p^μ`.
Docstring: A bispinor `pₐₐ` created from a lorentz vector `p^μ`.
complexLorentzTensor.leftMetric
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
complexLorentzTensor.rightMetric
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.coBispinorUp
Docstring: A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`.
Docstring: A bispinor `pᵃᵃ` created from a lorentz vector `p_μ`.
complexLorentzTensor.coBispinorDown
Docstring: A bispinor `pₐₐ` created from a lorentz vector `p_μ`.
Docstring: A bispinor `pₐₐ` created from a lorentz vector `p_μ`.
complexLorentzTensor.leftMetric
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
complexLorentzTensor.rightMetric
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.coMetric
Docstring: The metric `ηᵢᵢ` as a complex Lorentz tensor.
Docstring: The metric `ηᵢᵢ` as a complex Lorentz tensor.
complexLorentzTensor.contrMetric
Docstring: The metric `ηⁱⁱ` as a complex Lorentz tensor.
Docstring: The metric `ηⁱⁱ` as a complex Lorentz tensor.
complexLorentzTensor.leftMetric
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
complexLorentzTensor.rightMetric
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.altLeftMetric
Docstring: The metric `εₐₐ` as a complex Lorentz tensor.
Docstring: The metric `εₐₐ` as a complex Lorentz tensor.
complexLorentzTensor.altRightMetric
Docstring: The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.coMetric
Docstring: The metric `ηᵢᵢ` as a complex Lorentz tensor.
Docstring: The metric `ηᵢᵢ` as a complex Lorentz tensor.
complexLorentzTensor.contrMetric
Docstring: The metric `ηⁱⁱ` as a complex Lorentz tensor.
Docstring: The metric `ηⁱⁱ` as a complex Lorentz tensor.
complexLorentzTensor.coContrUnit
Docstring: The unit `δᵢⁱ` as a complex Lorentz tensor.
Docstring: The unit `δᵢⁱ` as a complex Lorentz tensor.
complexLorentzTensor.contrMetric
Docstring: The metric `ηⁱⁱ` as a complex Lorentz tensor.
Docstring: The metric `ηⁱⁱ` as a complex Lorentz tensor.
complexLorentzTensor.coMetric
Docstring: The metric `ηᵢᵢ` as a complex Lorentz tensor.
Docstring: The metric `ηᵢᵢ` as a complex Lorentz tensor.
complexLorentzTensor.contrCoUnit
Docstring: The unit `δⁱᵢ` as a complex Lorentz tensor.
Docstring: The unit `δⁱᵢ` as a complex Lorentz tensor.
complexLorentzTensor.leftMetric
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
complexLorentzTensor.altLeftMetric
Docstring: The metric `εₐₐ` as a complex Lorentz tensor.
Docstring: The metric `εₐₐ` as a complex Lorentz tensor.
complexLorentzTensor.leftAltLeftUnit
Docstring: The unit `δᵃₐ` as a complex Lorentz tensor.
Docstring: The unit `δᵃₐ` as a complex Lorentz tensor.
complexLorentzTensor.rightMetric
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.altRightMetric
Docstring: The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.rightAltRightUnit
Docstring: The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor.
Docstring: The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.altLeftMetric
Docstring: The metric `εₐₐ` as a complex Lorentz tensor.
Docstring: The metric `εₐₐ` as a complex Lorentz tensor.
complexLorentzTensor.leftMetric
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
Docstring: The metric `εᵃᵃ` as a complex Lorentz tensor.
complexLorentzTensor.altLeftLeftUnit
Docstring: The unit `δₐᵃ` as a complex Lorentz tensor.
Docstring: The unit `δₐᵃ` as a complex Lorentz tensor.
complexLorentzTensor.altRightMetric
Docstring: The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε_{dot a}_{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.rightMetric
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The metric `ε^{dot a}^{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.altRightRightUnit
Docstring: The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.coContrUnit
Docstring: The unit `δᵢⁱ` as a complex Lorentz tensor.
Docstring: The unit `δᵢⁱ` as a complex Lorentz tensor.
complexLorentzTensor.contrCoUnit
Docstring: The unit `δⁱᵢ` as a complex Lorentz tensor.
Docstring: The unit `δⁱᵢ` as a complex Lorentz tensor.
complexLorentzTensor.contrCoUnit
Docstring: The unit `δⁱᵢ` as a complex Lorentz tensor.
Docstring: The unit `δⁱᵢ` as a complex Lorentz tensor.
complexLorentzTensor.coContrUnit
Docstring: The unit `δᵢⁱ` as a complex Lorentz tensor.
Docstring: The unit `δᵢⁱ` as a complex Lorentz tensor.
complexLorentzTensor.altLeftLeftUnit
Docstring: The unit `δₐᵃ` as a complex Lorentz tensor.
Docstring: The unit `δₐᵃ` as a complex Lorentz tensor.
complexLorentzTensor.leftAltLeftUnit
Docstring: The unit `δᵃₐ` as a complex Lorentz tensor.
Docstring: The unit `δᵃₐ` as a complex Lorentz tensor.
complexLorentzTensor.leftAltLeftUnit
Docstring: The unit `δᵃₐ` as a complex Lorentz tensor.
Docstring: The unit `δᵃₐ` as a complex Lorentz tensor.
complexLorentzTensor.altLeftLeftUnit
Docstring: The unit `δₐᵃ` as a complex Lorentz tensor.
Docstring: The unit `δₐᵃ` as a complex Lorentz tensor.
complexLorentzTensor.altRightRightUnit
Docstring: The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.rightAltRightUnit
Docstring: The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor.
Docstring: The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.rightAltRightUnit
Docstring: The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor.
Docstring: The unit `δ^{dot a}_{dot a}` as a complex Lorentz tensor.
complexLorentzTensor.altRightRightUnit
Docstring: The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor.
Docstring: The unit `δ_{dot a}^{dot a}` as a complex Lorentz tensor.
LorentzGroup
Docstring: The Lorentz group is the subset of matrices for which `Λ * dual Λ = 1`.
Docstring: The Lorentz group is the subset of matrices for which `Λ * dual Λ = 1`.
LorentzGroup.IsProper
Docstring: A Lorentz Matrix is proper if its determinant is 1.
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.
Docstring: A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative.
Lorentz.SL2C.toLorentzGroup
Docstring: The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
Docstring: The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
Lorentz.SL2C.toLorentzGroup
Docstring: The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
Docstring: The group homomorphism from `SL(2, ℂ)` to the Lorentz group `𝓛`.
Lorentz.SL2C.toLorentzGroup_isOrthochronous
Docstring: The image of `SL(2, ℂ)` in the Lorentz group is orthochronous.
Docstring: The image of `SL(2, ℂ)` in the Lorentz group is orthochronous.
Fermion.rightHanded
Docstring: The vector space ℂ^2 carrying the conjugate representation of SL(2,C). In index notation corresponds to a Weyl fermion with indices ψ^{dot a}.
Docstring: The vector space ℂ^2 carrying the conjugate representation of SL(2,C). In index notation corresponds to a Weyl fermion with indices ψ^{dot a}.
Fermion.altRightHanded
Docstring: 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}`.
Docstring: 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}`.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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
Docstring: The space-time
StandardModel.HiggsField.zero
Docstring: The higgs field which is all zero.
Docstring: The higgs field which is all zero.
StandardModel.HiggsVec.rotate_fst_zero_snd_real
Docstring: 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 componenet.
Docstring: 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 componenet.
StandardModel.HiggsVec
Docstring: The complex vector space in which the Higgs field takes values.
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`.
Docstring: The representation of the gauge group acting on `higgsVec`.
StandardModel.HiggsVec
Docstring: The complex vector space in which the Higgs field takes values.
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`.
Docstring: The representation of the gauge group acting on `higgsVec`.
StandardModel.HiggsVec.rep
Docstring: The representation of the gauge group acting on `higgsVec`.
Docstring: The representation of the gauge group acting on `higgsVec`.
StandardModel.HiggsField
Docstring: A Higgs field is a smooth section of the Higgs bundle.
Docstring: A Higgs field is a smooth section of the Higgs bundle.
SpaceTime
Docstring: The space-time
Docstring: The space-time
StandardModel.HiggsField.Potential.IsBounded
Docstring: The proposition on the coefficents for a potential to be bounded.
Docstring: The proposition on the coefficents for a potential to be bounded.
StandardModel.HiggsField.Potential
Docstring: The parameters of the Higgs potential.
Docstring: The parameters of the Higgs potential.
IndexNotation.OverColor.forget
Docstring: 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.
Docstring: 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.
IndexNotation.OverColor.lift
Docstring: The functor taking functors in `Discrete C ⥤ Rep k G` to monoidal functors in `BraidedFunctor (OverColor C) (Rep k G)`, built on the PiTensorProduct.
Docstring: The functor taking functors in `Discrete C ⥤ Rep k G` to monoidal functors in `BraidedFunctor (OverColor C) (Rep k G)`, built on the PiTensorProduct.
TensorSpecies.contractSelfField
Docstring: The contraction of two vectors in a tensor species of the same color, as a linear map to the underlying field.
Docstring: The contraction of two vectors in a tensor species of the same color, as a linear map to the underlying field.
TensorSpecies.contractSelfField
Docstring: The contraction of two vectors in a tensor species of the same color, as a linear map to the underlying field.
Docstring: The contraction of two vectors in a tensor species of the same color, as a linear map to the underlying field.
TensorTree
Docstring: A syntax tree for tensor expressions.
Docstring: A syntax tree for tensor expressions.
TensorSpecies.dualRepIsoDiscrete
Docstring: The isomorphism between the representation associated with a color, and that associated with its dual.
Docstring: The isomorphism between the representation associated with a color, and that associated with its dual.
TensorSpecies.unitTensor
Docstring: The unit of a tensor species in a `PiTensorProduct`.
Docstring: The unit of a tensor species in a `PiTensorProduct`.
TensorSpecies.metricTensor
Docstring: The metric of a tensor species in a `PiTensorProduct`.
Docstring: The metric of a tensor species in a `PiTensorProduct`.
TensorSpecies.unitTensor
Docstring: The unit of a tensor species in a `PiTensorProduct`.
Docstring: The unit of a tensor species in a `PiTensorProduct`.
TensorSpecies.metricTensor
Docstring: The metric of a tensor species in a `PiTensorProduct`.
Docstring: The metric of a tensor species in a `PiTensorProduct`.
TensorSpecies.unitTensor
Docstring: The unit of a tensor species in a `PiTensorProduct`.
Docstring: The unit of a tensor species in a `PiTensorProduct`.
TensorSpecies.metricTensor
Docstring: The metric of a tensor species in a `PiTensorProduct`.
Docstring: The metric of a tensor species in a `PiTensorProduct`.
TensorSpecies.unitTensor
Docstring: The unit of a tensor species in a `PiTensorProduct`.
Docstring: The unit of a tensor species in a `PiTensorProduct`.
TensorSpecies.metricTensor
Docstring: The metric of a tensor species in a `PiTensorProduct`.
Docstring: The metric of a tensor species in a `PiTensorProduct`.
TensorTree.constVecNode
Docstring: A constant vector.
Docstring: A constant vector.
TensorTree.vecNode
Docstring: A node consisting of a single vector.
Docstring: A node consisting of a single vector.
TensorTree.constTwoNode
Docstring: A constant two tensor (e.g. metric and unit).
Docstring: A constant two tensor (e.g. metric and unit).
TensorTree.twoNode
Docstring: A node consisting of a two tensor.
Docstring: A node consisting of a two tensor.
GeorgiGlashow.GaugeGroupI
Math description: The group `SU(5)`.
Physics description: The gauge group of the Georgi-Glashow model.
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.
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
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
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 ℤ₂).
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.
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
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
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
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.
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.
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
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
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.)
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).
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).
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).
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).
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
Math description: The inclusion ``inclSM is equal to the inclusion ``inclSMThruGeorgiGlashow.
Physics description: No physics description provided
TwoHDM.prodMatrix_invariant
Math description: The map ``prodMatrix is invariant under the simultanous action of ``gaugeAction on the two Higgs fields.
Physics description: No physics description provided
Math description: The map ``prodMatrix is invariant under the simultanous action of ``gaugeAction on the two Higgs fields.
Physics description: No physics description provided
TwoHDM.prodMatrix_to_higgsField
Math description: Given any smooth map ``f from spacetime to 2 x 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.
Physics description: No physics description provided
Math description: Given any smooth map ``f from spacetime to 2 x 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.
Physics description: No physics description provided
complexLorentzTensor.contrBispinorUp_eq_metric_contr_contrBispinorDown
Math description: {contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ
Physics description: No physics description provided
Math description: {contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ
Physics description: No physics description provided
complexLorentzTensor.coBispinorUp_eq_metric_contr_coBispinorDown
Math description: {coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ
Physics description: No physics description provided
Math description: {coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ
Physics description: No physics description provided
complexLorentzTensor.coMetric_symm
Math description: The covariant metric is symmetric {η' | μ ν = η' | ν μ}ᵀ
Physics description: No physics description provided
Math description: The covariant metric is symmetric {η' | μ ν = η' | ν μ}ᵀ
Physics description: No physics description provided
complexLorentzTensor.contrMetric_symm
Math description: The contravariant metric is symmetric {η | μ ν = η | ν μ}ᵀ
Physics description: No physics description provided
Math description: The contravariant metric is symmetric {η | μ ν = η | ν μ}ᵀ
Physics description: No physics description provided
complexLorentzTensor.leftMetric_antisymm
Math description: The left metric is antisymmetric {εL | α α' = - εL | α' α}ᵀ
Physics description: No physics description provided
Math description: The left metric is antisymmetric {εL | α α' = - εL | α' α}ᵀ
Physics description: No physics description provided
complexLorentzTensor.rightMetric_antisymm
Math description: The right metric is antisymmetric {εR | β β' = - εR | β' β}ᵀ
Physics description: No physics description provided
Math description: The right metric is antisymmetric {εR | β β' = - εR | β' β}ᵀ
Physics description: No physics description provided
complexLorentzTensor.altLeftMetric_antisymm
Math description: The alt-left metric is antisymmetric {εL' | α α' = - εL' | α' α}ᵀ
Physics description: No physics description provided
Math description: The alt-left metric is antisymmetric {εL' | α α' = - εL' | α' α}ᵀ
Physics description: No physics description provided
complexLorentzTensor.altRightMetric_antisymm
Math description: The alt-right metric is antisymmetric {εR' | β β' = - εR' | β' β}ᵀ
Physics description: No physics description provided
Math description: The alt-right metric is antisymmetric {εR' | β β' = - εR' | β' β}ᵀ
Physics description: No physics description provided
complexLorentzTensor.coMetric_contr_contrMetric
Math description: The contraction of the covariant metric with the contravariant metric is the unit {η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ
Physics description: No physics description provided
Math description: The contraction of the covariant metric with the contravariant metric is the unit {η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ
Physics description: No physics description provided
complexLorentzTensor.contrMetric_contr_coMetric
Math description: The contraction of the contravariant metric with the covariant metric is the unit {η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ
Physics description: No physics description provided
Math description: The contraction of the contravariant metric with the covariant metric is the unit {η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ
Physics description: No physics description provided
complexLorentzTensor.leftMetric_contr_altLeftMetric
Math description: The contraction of the left metric with the alt-left metric is the unit {εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ
Physics description: No physics description provided
Math description: The contraction of the left metric with the alt-left metric is the unit {εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ
Physics description: No physics description provided
complexLorentzTensor.rightMetric_contr_altRightMetric
Math description: The contraction of the right metric with the alt-right metric is the unit {εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ
Physics description: No physics description provided
Math description: The contraction of the right metric with the alt-right metric is the unit {εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ
Physics description: No physics description provided
complexLorentzTensor.altLeftMetric_contr_leftMetric
Math description: The contraction of the alt-left metric with the left metric is the unit {εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ
Physics description: No physics description provided
Math description: The contraction of the alt-left metric with the left metric is the unit {εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ
Physics description: No physics description provided
complexLorentzTensor.altRightMetric_contr_rightMetric
Math description: The contraction of the alt-right metric with the right metric is the unit {εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ
Physics description: No physics description provided
Math description: The contraction of the alt-right metric with the right metric is the unit {εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ
Physics description: No physics description provided
complexLorentzTensor.coContrUnit_symm
Math description: Swapping indices of coContrUnit returns contrCoUnit, i.e. {δ' | μ ν = δ | ν μ}.ᵀ
Physics description: No physics description provided
Math description: Swapping indices of coContrUnit returns contrCoUnit, i.e. {δ' | μ ν = δ | ν μ}.ᵀ
Physics description: No physics description provided
complexLorentzTensor.contrCoUnit_symm
Math description: Swapping indices of contrCoUnit returns coContrUnit, i.e. {δ | μ ν = δ' | ν μ}ᵀ
Physics description: No physics description provided
Math description: Swapping indices of contrCoUnit returns coContrUnit, i.e. {δ | μ ν = δ' | ν μ}ᵀ
Physics description: No physics description provided
complexLorentzTensor.altLeftLeftUnit_symm
Math description: Swapping indices of altLeftLeftUnit returns leftAltLeftUnit, i.e. {δL' | α α' = δL | α' α}ᵀ
Physics description: No physics description provided
Math description: Swapping indices of altLeftLeftUnit returns leftAltLeftUnit, i.e. {δL' | α α' = δL | α' α}ᵀ
Physics description: No physics description provided
complexLorentzTensor.leftAltLeftUnit_symm
Math description: Swapping indices of leftAltLeftUnit returns altLeftLeftUnit, i.e. {δL | α α' = δL' | α' α}ᵀ
Physics description: No physics description provided
Math description: Swapping indices of leftAltLeftUnit returns altLeftLeftUnit, i.e. {δL | α α' = δL' | α' α}ᵀ
Physics description: No physics description provided
complexLorentzTensor.altRightRightUnit_symm
Math description: Swapping indices of altRightRightUnit returns rightAltRightUnit, i.e. {δR' | β β' = δR | β' β}ᵀ
Physics description: No physics description provided
Math description: Swapping indices of altRightRightUnit returns rightAltRightUnit, i.e. {δR' | β β' = δR | β' β}ᵀ
Physics description: No physics description provided
complexLorentzTensor.rightAltRightUnit_symm
Math description: Swapping indices of rightAltRightUnit returns altRightRightUnit, i.e. {δR | β β' = δR' | β' β}ᵀ
Physics description: No physics description provided
Math description: Swapping indices of rightAltRightUnit returns altRightRightUnit, i.e. {δR | β β' = δR' | β' β}ᵀ
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
Math description: The subgroup of the Lorentz group consisting of elements which are proper and orthochronous.
Physics description: No physics description provided
Lorentz.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
Math description: The determinant of the image of `SL(2, ℂ)` in the Lorentz group is one.
Physics description: No physics description provided
Lorentz.SL2C.toRestrictedLorentzGroup
Math description: The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group.
Physics description: No physics description provided
Math description: The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group.
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
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
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
SuperAlgebra
Math description: A super algebra is a graded algebra A with a ℤ₂ grading.
Physics description: A super algebra is used to model the commutator of fermionic operators among themselves, aswell as among bosonic operators.
Math description: A super algebra is a graded algebra A with a ℤ₂ grading.
Physics description: A super algebra is used to model the commutator of fermionic operators among themselves, aswell as among bosonic operators.
SuperAlgebra.superCommuator
Math description: The commutator which for `a ∈ Aᵢ` and `b ∈ Aⱼ` is defined as `ab - (-1)^(i * j) ba`.
Physics description: No physics description provided
Math description: The commutator which for `a ∈ Aᵢ` and `b ∈ Aⱼ` is defined as `ab - (-1)^(i * j) ba`.
Physics description: No physics description provided
Wick.Contractions.equivInvolution
Math description: There is an isomorphism between the type of contractions of a list `l` and the type of involutions from `Fin l.length` to `Fin l.length.
Physics description: No physics description provided
Math description: There is an isomorphism between the type of contractions of a list `l` and the type of involutions from `Fin l.length` to `Fin l.length.
Physics description: No physics description provided
Wick.Contractions.equivFullInvolution
Math description: There is an isomorphism from the type of full contractions of a list `l` and the type of fixed-point free involutions from `Fin l.length` to `Fin l.length.
Physics description: No physics description provided
Math description: There is an isomorphism from the type of full contractions of a list `l` and the type of fixed-point free involutions from `Fin l.length` to `Fin l.length.
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.
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.
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.
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.
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.
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.
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.
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
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
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
Math description: The trivial principal bundle over SpaceTime with structure group ``GaugeGroupI.
Physics description: No physics description provided
StandardModel.gaugeTransformI
Math description: A global section of ``gaugeBundleI.
Physics description: No physics description provided
Math description: A global section of ``gaugeBundleI.
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.
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
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.
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
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
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
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
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.
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.
IndexNotation.OverColor.forgetLift
Math description: The natural isomorphism between `lift (C := C) ⋙ forget` and `Functor.id (Discrete C ⥤ Rep k G)`.
Physics description: No physics description provided
Math description: The natural isomorphism between `lift (C := C) ⋙ forget` and `Functor.id (Discrete C ⥤ Rep k G)`.
Physics description: No physics description provided
TensorSpecies.contractSelfField_non_degenerate
Math description: The contraction of two vectors of the same color is non-degenerate. I.e. ⟪ψ, φ⟫ₜₛ = 0 for all φ implies ψ = 0.
Physics description: No physics description provided
Math description: The contraction of two vectors of the same color is non-degenerate. I.e. ⟪ψ, φ⟫ₜₛ = 0 for all φ implies ψ = 0.
Physics description: No physics description provided
TensorSpecies.contractSelfField_tensorTree
Math description: The contraction ⟪ψ, φ⟫ₜₛ is related to the tensor tree {ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ
Physics description: No physics description provided
Math description: The contraction ⟪ψ, φ⟫ₜₛ is related to the tensor tree {ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ
Physics description: No physics description provided
TensorSpecies.dualRepIso
Math 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.
Physics description: No physics description provided
Math 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.
Physics description: No physics description provided
TensorSpecies.dualRepIso_unitTensor_fst
Math description: Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric.
Physics description: No physics description provided
Math description: Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric.
Physics description: No physics description provided
TensorSpecies.dualRepIso_unitTensor_snd
Math description: Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric.
Physics description: No physics description provided
Math description: Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric.
Physics description: No physics description provided
TensorSpecies.dualRepIso_metricTensor_fst
Math description: Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor.
Physics description: No physics description provided
Math description: Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor.
Physics description: No physics description provided
TensorSpecies.dualRepIso_metricTensor_snd
Math description: Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor.
Physics description: No physics description provided
Math description: Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor.
Physics description: No physics description provided
TensorTree.constVecNode_eq_vecNode
Math description: A constVecNode has equal tensor to the vecNode with the map evaluated at 1.
Physics description: No physics description provided
Math description: A constVecNode has equal tensor to the vecNode with the map evaluated at 1.
Physics description: No physics description provided
TensorTree.constTwoNode_eq_twoNode
Math description: A constTwoNode has equal tensor to the twoNode with the map evaluated at 1.
Physics description: No physics description provided
Math description: A constTwoNode has equal tensor to the twoNode with the map evaluated at 1.
Physics description: No physics description provided