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.
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
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 `λ`.
TensorSpecies.Tensor.prodT
Description: The tensor product of two tensors as a bi-linear map from `S.Tensor c` and `S.Tensor c1` to `S.Tensor (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)`.
Description: The tensor product of two tensors as a bi-linear map from `S.Tensor c` and `S.Tensor c1` to `S.Tensor (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)`.
StandardModel.HiggsField.zero
Description: The higgs field which is all zero.
Description: The higgs field which is all zero.
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 `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
LorentzGroup.restricted
Description: The restricted Lorentz group comprises the proper and orthochronous elements of the Lorentz group.
Description: The restricted Lorentz group comprises the proper and orthochronous elements of the Lorentz group.
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^μ`.
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_μ`.
SpaceTime.space
Description: The space part of spacetime.
Description: The space part of spacetime.
TensorSpecies.Tensor.permT
Description: Given a permutation `σ : Fin m → Fin n` of indices satisfying `PermCond` through `h`, and a tensor `t`, `permT σ h t` is the tensor tensor permuted accordinge to `σ`.
Description: Given a permutation `σ : Fin m → Fin n` of indices satisfying `PermCond` through `h`, and a tensor `t`, `permT σ h t` is the tensor tensor permuted accordinge to `σ`.
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`.
TensorSpecies.Tensor.evalT
Description: Given a `i : Fin (n + 1)`, a `b : Fin (S.repDim (c i))` and a tensor `t : Tensor S c`, `evalT i b t` is the tensor formed by evaluating the `i`th index of `t` at `b`.
Description: Given a `i : Fin (n + 1)`, a `b : Fin (S.repDim (c i))` and a tensor `t : Tensor S c`, `evalT i b t` is the tensor formed by evaluating the `i`th index of `t` at `b`.
TwoHDM.prodMatrix_smooth
Description: The map `prodMatrix` is a smooth function on spacetime.
Description: The map `prodMatrix` is a smooth function on spacetime.
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.
TensorSpecies.Tensor.contrT
Description: For `c : Fin (n + 1 + 1) → S.C`, `i j : Fin (n + 1 + 1)` with dual color, and a tensor `t : Tensor S c`, `contrT i j _ t` is the tensor formed by contracting the `i`th index of `t` with the `j`th index.
Description: For `c : Fin (n + 1 + 1) → S.C`, `i j : Fin (n + 1 + 1)` with dual color, and a tensor `t : Tensor S c`, `contrT i j _ t` is the tensor formed by contracting the `i`th index of `t` with the `j`th index.
SpecialRelativity.InstantaneousTwinParadox.ageGap
Description: The proper time of twin A minus the proper time of twin B.
Description: The proper time of twin A minus the proper time of twin B.
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`.
Cosmology.SpatialGeometry.limit_S_saddle
Description: The limit of `S (Saddle k) r` as `k → ∞` is equal to `S (Flat) r`.
Description: The limit of `S (Saddle k) r` as `k → ∞` is equal to `S (Flat) r`.
Cosmology.SpatialGeometry.limit_S_sphere
Description: The limit of `S (Sphere k) r` as `k → ∞` is equal to `S (Flat) r`.
Description: The limit of `S (Sphere k) r` as `k → ∞` is equal to `S (Flat) r`.
Cosmology.FLRW.hubbleConstant
Description: The hubble constant defined in terms of the scale factor as `(dₜ a) / a`. The notation `H` is used for the `hubbleConstant`. Semiformal implementation note: Implement also scoped notation.
Description: The hubble constant defined in terms of the scale factor as `(dₜ a) / a`. The notation `H` is used for the `hubbleConstant`. Semiformal implementation note: Implement also scoped notation.
Cosmology.FLRW.decelerationParameter
Description: The deceleration parameter defined in terms of the scale factor as `- (dₜdₜ a) a / (dₜ a)^2`. The notation `q` is used for the `decelerationParameter`. Semiformal implementation note: Implement also scoped notation.
Description: The deceleration parameter defined in terms of the scale factor as `- (dₜdₜ a) a / (dₜ a)^2`. The notation `q` is used for the `decelerationParameter`. Semiformal implementation note: Implement also scoped notation.
Cosmology.FLRW.decelerationParameter_eq_one_plus_hubbleConstant
Description: The deceleration parameter is equal to `- (1 + (dₜ H)/H^2)`.
Description: The deceleration parameter is equal to `- (1 + (dₜ H)/H^2)`.
Cosmology.FLRW.time_evolution_hubbleConstant
Description: The time evolution of the hubble parameter is equal to `dₜ H = - H^2 (1 + q)`.
Description: The time evolution of the hubble parameter is equal to `dₜ H = - H^2 (1 + q)`.
Cosmology.FLRW.hubbleConstant_decrease_iff
Description: There exists a time at which the hubble constant decreases if and only if there exists a time where the deceleration parameter is less then `-1`.
Description: There exists a time at which the hubble constant decreases if and only if there exists a time where the deceleration parameter is less then `-1`.
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` 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.
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.
SpaceTime.space_equivariant
Description: The function `space` is equivariant with respect to rotations.
Description: The function `space` is equivariant with respect to rotations.
SpecialRelativity.InstantaneousTwinParadox.ageGap_nonneg
Description: In the twin paradox with instantous acceleration, Twin A is always older then Twin B.
Description: In the twin paradox with instantous acceleration, Twin A is always older then Twin B.
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)`.
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`.
realLorentzTensor.toComplex_injective
Description: The map `toComplex` is injective.
Description: The map `toComplex` is injective.
realLorentzTensor.toComplex_equivariant
Description: The map `toComplex` is equivariant.
Description: The map `toComplex` is equivariant.
realLorentzTensor.permT_toComplex
Description: The map `toComplex` commutes with permT.
Description: The map `toComplex` commutes with permT.
realLorentzTensor.prodT_toComplex
Description: The map `toComplex` commutes with prodT.
Description: The map `toComplex` commutes with prodT.
realLorentzTensor.contrT_toComplex
Description: The map `toComplex` commutes with contrT.
Description: The map `toComplex` commutes with contrT.
realLorentzTensor.evalT_toComplex
Description: The map `toComplex` commutes with evalT.
Description: The map `toComplex` commutes with evalT.