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.
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 (Fin.append c c1)`.
Description: The tensor product of two tensors as a bi-linear map from `S.Tensor c` and `S.Tensor c1` to `S.Tensor (Fin.append c c1)`.
Electromagnetism.ThreeDimPointParticle.electricField
Description: The electric field of a point particle of charge `q` in 3d space sitting at `r₀`. In physics notation this corresponds to the 'function' `(q/(4 * π * ε)) • ‖r - r₀‖⁻¹ ^ 3 • (r - r₀)`. Here it is defined as the distribution corresponding to that function.
Description: The electric field of a point particle of charge `q` in 3d space sitting at `r₀`. In physics notation this corresponds to the 'function' `(q/(4 * π * ε)) • ‖r - r₀‖⁻¹ ^ 3 • (r - r₀)`. Here it is defined as the distribution corresponding to that function.
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.
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 `((Φ₁^†Φ₁, Φ₂^†Φ₁), (Φ₁^†Φ₂, Φ₂^†Φ₂))`.
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.
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.
CanonicalEnsemble.twoState
Description: The canonical ensemble corresponding to state system, with one state of energy `E` and the other state of energy `0`.
Description: The canonical ensemble corresponding to state system, with one state of energy `E` and the other state of energy `0`.
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`.
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`.
SpaceTime
Description: `SpaceTime d` corresponds to `d+1` dimensional space-time. This is equipped with an instaance of the action of a Lorentz group, corresponding to Minkowski-spacetime.
Description: `SpaceTime d` corresponds to `d+1` dimensional space-time. This is equipped with an instaance of the action of a Lorentz group, corresponding to Minkowski-spacetime.
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
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`.
complexLorentzTensor.leftMetric
Description: The metric `εᵃᵃ` as a complex Lorentz tensor.
Description: The metric `εᵃᵃ` as a complex Lorentz tensor.
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.coBispinorDown
Description: A bispinor `pₐₐ` created from a lorentz vector `p_μ`.
Description: A bispinor `pₐₐ` created from a lorentz vector `p_μ`.
RigidBody
Description: A Rigid body defined by its mass distribution.
Description: A Rigid body defined by its mass distribution.
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`.
CanonicalEnsemble.thermodynamicEntropy
Description: The absolute thermodynamic entropy, defined from its statistical mechanical foundation as the Gibbs-Shannon entropy of the dimensionless physical probability distribution. This corresponds to Landau & Lifshitz, Statistical Physics, §7, Eq. 7.12.
Description: The absolute thermodynamic entropy, defined from its statistical mechanical foundation as the Gibbs-Shannon entropy of the dimensionless physical probability distribution. This corresponds to Landau & Lifshitz, Statistical Physics, §7, Eq. 7.12.
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) → 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) → 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.
RigidBody.kineticEnergy
Description: The kinetic energy of a rigid body.
Description: The kinetic energy of a rigid body.
RigidBody.coordinate_system
Description: One can describe the motion of rigid body with a fixed (inertial) coordinate system (X,Y,Z) and a moving system (x₁,x₂,x₃) rigidly attached to the body.
Description: One can describe the motion of rigid body with a fixed (inertial) coordinate system (X,Y,Z) and a moving system (x₁,x₂,x₃) rigidly attached to the body.
RigidBody.rigid_body_dof
Description: A rigid body in three-dimensional space has six degrees of freedom: three translational (for the position of its centre of mass) and three rotational (for its orientation).
Description: A rigid body in three-dimensional space has six degrees of freedom: three translational (for the position of its centre of mass) and three rotational (for its orientation).
RigidBody.velocity_decomposition
Description: The velocity v of any point in a rigid body is v = V + Ω × r, where V is the velocity of the origin of the moving system and Ω is the angular velocity.
Description: The velocity v of any point in a rigid body is v = V + Ω × r, where V is the velocity of the origin of the moving system and Ω is the angular velocity.
RigidBody.angular_velocity_is_well_defined
Description: The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen.
Description: The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen.
RigidBody.decomposition_of_motion
Description: The motion of a rigid body can be decomposed into a translation of some reference point plus a rotation about that point. There exists a time-dependent vector V(t) and angular velocity ω(t) such that v(r) = V + ω × r, where r is measured from the reference point.
Description: The motion of a rigid body can be decomposed into a translation of some reference point plus a rotation about that point. There exists a time-dependent vector V(t) and angular velocity ω(t) such that v(r) = V + ω × r, where r is measured from the reference point.
RigidBody.center_of_mass_point_moves_as_particle
Description: The centre of mass of a rigid body moves as if all mass were concentrated at that point and acted upon by the resultant external force: M a_CM = ∑ F_ext.
Description: The centre of mass of a rigid body moves as if all mass were concentrated at that point and acted upon by the resultant external force: M a_CM = ∑ F_ext.
RigidBody.angular_momentum_about_point
Description: The total angular momentum about a point O is L = ∫ r × v dm. With v = V + ω × r about the centre of mass, L = R × (M V) + I_CM ω, where R is the centre of mass position.
Description: The total angular momentum about a point O is L = ∫ r × v dm. With v = V + ω × r about the centre of mass, L = R × (M V) + I_CM ω, where R is the centre of mass position.
RigidBody.translational_equation_inertial
Description: In the inertial frame, the translational equation of motion of a rigid body is given by dP/dt = F, where `P` is the total linear momentum and `F` is the total external force acting on the body.
Description: In the inertial frame, the translational equation of motion of a rigid body is given by dP/dt = F, where `P` is the total linear momentum and `F` is the total external force acting on the body.
RigidBody.rotational_equation_inertial
Description: In the inertial frame, the rotational equation of motion of a rigid body about the center of mass is given by dM/dt = K, where `M` is the total angular momentum and `K` is the total external torque.
Description: In the inertial frame, the rotational equation of motion of a rigid body about the center of mass is given by dM/dt = K, where `M` is the total angular momentum and `K` is the total external torque.
RigidBody.kinetic_energy_decomposition
Description: The kinetic energy decomposes into translational and rotational parts: T = (1/2) M |V|² + (1/2) ω ⋅ I_CM ω. Here V is the velocity of the centre of mass and I_CM is the inertia tensor about that point.
Description: The kinetic energy decomposes into translational and rotational parts: T = (1/2) M |V|² + (1/2) ω ⋅ I_CM ω. Here V is the velocity of the centre of mass and I_CM is the inertia tensor about that point.
RigidBody.parallel_axis_theorem
Description: If I_O is the inertia tensor about a point O, then the inertia tensor about a parallel point O' displaced by a is I_{O'} = I_O + M(|a|² 1 − a ⊗ a). This is the parallel-axis theorem.
Description: If I_O is the inertia tensor about a point O, then the inertia tensor about a parallel point O' displaced by a is I_{O'} = I_O + M(|a|² 1 − a ⊗ a). This is the parallel-axis theorem.
RigidBody.principal_axes_of_inertia
Description: Because the inertia tensor is real symmetric, there exists an orthonormal basis of principal axes in which it is diagonal. The corresponding directions are the principal axes of inertia.
Description: Because the inertia tensor is real symmetric, there exists an orthonormal basis of principal axes in which it is diagonal. The corresponding directions are the principal axes of inertia.
RigidBody.principal_axes_of_inertia_bound
Description: None of the principal moments of inertia can exceed the sum of other two.
Description: None of the principal moments of inertia can exceed the sum of other two.
RigidBody.asymmetrical_top
Description: An asymmetrical top is when none of the principal moments of inertia are equal.
Description: An asymmetrical top is when none of the principal moments of inertia are equal.
RigidBody.symmetrical_top
Description: A symmetrical top is when only two of the principal moments of inertia are equal.
Description: A symmetrical top is when only two of the principal moments of inertia are equal.
RigidBody.spherical_top
Description: A spherical top is when all three of the principal moments of inertia are equal.
Description: A spherical top is when all three of the principal moments of inertia are equal.
RigidBody.RotatingFrame
Description: A rotating body-fixed frame is a coordinate system attached to the body that rotates with the body relative to an inertial (fixed) frame. The frame is characterised by its angular velocity vector Ω(t).
Description: A rotating body-fixed frame is a coordinate system attached to the body that rotates with the body relative to an inertial (fixed) frame. The frame is characterised by its angular velocity vector Ω(t).
RigidBody.rotating_frame_derivative
Description: The time derivative in the rotating frame, d'/dt, is the derivative of the components of a vector with respect to time when expressed in the rotating (body-fixed) frame.
Description: The time derivative in the rotating frame, d'/dt, is the derivative of the components of a vector with respect to time when expressed in the rotating (body-fixed) frame.
RigidBody.transport_law_inertial_rotating
Description: For any vector field A(t), its inertial-frame time derivative equals the rotating-frame derivative plus the contribution from the frame rotation: (dA/dt)_inertial = (dA/dt)_rotating + Ω × A. Here Ω is the angular velocity of the rotating frame.
Description: For any vector field A(t), its inertial-frame time derivative equals the rotating-frame derivative plus the contribution from the frame rotation: (dA/dt)_inertial = (dA/dt)_rotating + Ω × A. Here Ω is the angular velocity of the rotating frame.
RigidBody.transport_law_for_momentum
Description: For linear momentum, the relation between inertial and rotating derivatives is (dP/dt)_inertial = d'P/dt + Ω × P. So, d'P/dt + Ω × P = F which is the linear-momentum equation in the rotating frame.
Description: For linear momentum, the relation between inertial and rotating derivatives is (dP/dt)_inertial = d'P/dt + Ω × P. So, d'P/dt + Ω × P = F which is the linear-momentum equation in the rotating frame.
RigidBody.transport_law_for_angular_momentum
Description: For angular momentum, the relation between inertial and rotating derivatives is (dM/dt)_inertial = d'M/dt + Ω × M, and with the rotational form of Newton's law M_tot = (dM/dt)_inertial this yields d'M/dt + Ω × M = K, the angular-momentum equation in the rotating frame.
Description: For angular momentum, the relation between inertial and rotating derivatives is (dM/dt)_inertial = d'M/dt + Ω × M, and with the rotational form of Newton's law M_tot = (dM/dt)_inertial this yields d'M/dt + Ω × M = K, the angular-momentum equation in the rotating frame.
RigidBody.euler_equations
Description: When motion is described in body-fixed principal axes (I₁, I₂, I₃ diagonal), the equations of rotational motion (Euler’s equations) are: I₁ dω₁/dt + (I₃ − I₂) ω₂ ω₃ = M₁, with cyclic permutations. M is the external torque about the centre of mass.
Description: When motion is described in body-fixed principal axes (I₁, I₂, I₃ diagonal), the equations of rotational motion (Euler’s equations) are: I₁ dω₁/dt + (I₃ − I₂) ω₂ ω₃ = M₁, with cyclic permutations. M is the external torque about the centre of mass.
RigidBody.steady_rotation_conditions
Description: A rigid body can perform steady (uniform) rotation about any principal axis if the torque about that axis vanishes. Stability depends on the ordering of principal moments.
Description: A rigid body can perform steady (uniform) rotation about any principal axis if the torque about that axis vanishes. Stability depends on the ordering of principal moments.
RigidBody.intermediate_axis_instability
Description: Rotations about the largest and smallest principal axes are stable under small perturbations; rotation about the intermediate axis is unstable (tennis-racket effect).
Description: Rotations about the largest and smallest principal axes are stable under small perturbations; rotation about the intermediate axis is unstable (tennis-racket effect).
RigidBody.reduction_to_two_body
Description: If a rigid body is confined to planar motion, its dynamics reduce to a two-dimensional problem: the inertia reduces to a scalar moment and rotation is described by a single angular velocity.
Description: If a rigid body is confined to planar motion, its dynamics reduce to a two-dimensional problem: the inertia reduces to a scalar moment and rotation is described by a single angular velocity.
RigidBody.rigid_body_work_and_power
Description: The power delivered to a rigid body by forces is P = ∑ Fᵢ ⋅ vᵢ = F_tot ⋅ V + M ⋅ ω, where F_tot is total force, V the reference point velocity, and M the torque. Translational and rotational contributions separate.
Description: The power delivered to a rigid body by forces is P = ∑ Fᵢ ⋅ vᵢ = F_tot ⋅ V + M ⋅ ω, where F_tot is total force, V the reference point velocity, and M the torque. Translational and rotational contributions separate.
RigidBody.small_oscillations_about_equilibrium
Description: Small oscillations about a stable equilibrium orientation are governed by linearised equations obtained by expanding energy to second order in angular displacements. Normal modes and frequencies depend on inertia and restoring torques.
Description: Small oscillations about a stable equilibrium orientation are governed by linearised equations obtained by expanding energy to second order in angular displacements. Normal modes and frequencies depend on inertia and restoring torques.
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`.
Electromagnetism.ThreeDimPointParticle.electricField_rotationally_invariant
Description: The electrostatic field of a point particle is rotationally invariant.
Description: The electrostatic field of a point particle is rotationally invariant.
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.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.
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.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.
SpaceTime.space_equivariant
Description: The function `space` is equivariant with respect to rotations.
Description: The function `space` is equivariant with respect to rotations.
CanonicalEnsemble.twoState_entropy_eq
Description: A simplification of the `entropy` of the two-state canonical ensemble.
Description: A simplification of the `entropy` of the two-state canonical ensemble.
CanonicalEnsemble.twoState_helmholtzFreeEnergy_eq
Description: A simplification of the `helmholtzFreeEnergy` of the two-state canonical ensemble.
Description: A simplification of the `helmholtzFreeEnergy` of the two-state canonical ensemble.