Informal definitions and lemmas

See informal definitions and lemmas as a dependency graph.

This file is automatically generated using informal_lemma and informal_definition commands appearing in the raw Lean code of HepLean.

There is an implicit invitation to the reader to contribute to the formalization of informal definitions and lemmas. You may also wish to contribute to HepLean by including informal definitions and lemmas in the raw Lean code, especially if you do not have a background in Lean.

HepLean.BeyondTheStandardModel.PatiSalam.Basic

Informal def: GaugeGroupI := The group SU(4) x SU(2) x SU(2).

Informal def: embedSM := 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))).

Informal def: gaugeGroupISpinEquiv := The equivalence between GaugeGroupI and Spin(6) × Spin(4).

Informal def: gaugeGroupℤ₂SubGroup := The ℤ₂-subgroup of ``GaugeGroupI with the non-trivial element (-1, -1, -1).

Informal def: GaugeGroupℤ₂ := The quotient of ``GaugeGroupI by the ℤ₂-subgroup gaugeGroupℤ₂SubGroup.

Informal lemma: sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup := The group StandardModel.gaugeGroupℤ₆SubGroup under the homomorphismembedSM factors through the subgroup ``gaugeGroupℤ₂SubGroup.

Informal def: embedSMℤ₆Toℤ₂ := The group homomorphism from StandardModel.GaugeGroupℤ₆ toGaugeGroupℤ₂ induced by ``embedSM.

HepLean.BeyondTheStandardModel.Spin10.Basic

Informal def: GaugeGroupI := The group Spin(10).

Informal def: embedPatiSalam := 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).

HepLean.SpaceTime.LorentzGroup.Restricted

Informal def: Restricted := The subgroup of the Lorentz group consisting of elements which are proper and orthochronous.

HepLean.SpaceTime.SL2C.Basic

Informal lemma: toLorentzGroup_det_one := The determinant of the image of SL(2, ℂ) in the Lorentz group is one.

Informal lemma: toLorentzGroup_timeComp_nonneg := The time coponent of the image of SL(2, ℂ) in the Lorentz group is non-negative.

Informal lemma: toRestrictedLorentzGroup := The homomorphism from SL(2, ℂ) to the restricted Lorentz group.

HepLean.SpaceTime.WeylFermion.Basic

Informal def: leftHandedWeylFermion := The vector space ℂ^2 carrying the fundamental representation of SL(2,C).

Informal def: rightHandedWeylFermion := The vector space ℂ^2 carrying the conjguate representation of SL(2,C).

Informal def: altLeftHandedWeylFermion := The vector space ℂ^2 carrying the representation of SL(2,C) given by M → (M⁻¹)ᵀ.

Informal def: altRightHandedWeylFermion := The vector space ℂ^2 carrying the representation of SL(2,C) given by M → (M⁻¹)^†.

Informal def: leftHandedWeylFermionAltEquiv := The linear equiv between leftHandedWeylFermion and altLeftHandedWeylFermion given by multiplying an element of rightHandedWeylFermion by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]].

Informal lemma: leftHandedWeylFermionAltEquiv_equivariant := The linear equiv leftHandedWeylFermionAltEquiv is equivariant with respect to the action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion.

Informal def: rightHandedWeylFermionAltEquiv := The linear equiv between rightHandedWeylFermion and altRightHandedWeylFermion given by multiplying an element of rightHandedWeylFermion by the matrix εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]

Informal lemma: rightHandedWeylFermionAltEquiv_equivariant := The linear equiv rightHandedWeylFermionAltEquiv is equivariant with respect to the action of SL(2,C) on rightHandedWeylFermion and altRightHandedWeylFermion.

Informal def: leftAltWeylFermionContraction := The linear map from leftHandedWeylFermion ⊗ altLeftHandedWeylFermion to ℂ given by summing over components of leftHandedWeylFermion and altLeftHandedWeylFermion in the standard basis (i.e. the dot product).

Informal lemma: leftAltWeylFermionContraction_invariant := The contraction leftAltWeylFermionContraction is invariant with respect to the action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion.

Informal def: altLeftWeylFermionContraction := The linear map from altLeftHandedWeylFermion ⊗ leftHandedWeylFermion to ℂ given by summing over components of altLeftHandedWeylFermion and leftHandedWeylFermion in the standard basis (i.e. the dot product).

Informal lemma: leftAltWeylFermionContraction_symm_altLeftWeylFermionContraction := The linear map altLeftWeylFermionContraction is leftAltWeylFermionContraction composed with the braiding of the tensor product.

Informal lemma: altLeftWeylFermionContraction_invariant := The contraction altLeftWeylFermionContraction is invariant with respect to the action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion.

Informal def: rightAltWeylFermionContraction := The linear map from rightHandedWeylFermion ⊗ altRightHandedWeylFermion to ℂ given by summing over components of rightHandedWeylFermion and altRightHandedWeylFermion in the standard basis (i.e. the dot product).

Informal lemma: rightAltWeylFermionContraction_invariant := The contraction rightAltWeylFermionContraction is invariant with respect to the action of SL(2,C) on rightHandedWeylFermion and altRightHandedWeylFermion.

Informal def: altRightWeylFermionContraction := The linear map from altRightHandedWeylFermion ⊗ rightHandedWeylFermion to ℂ given by summing over components of altRightHandedWeylFermion and rightHandedWeylFermion in the standard basis (i.e. the dot product).

Informal lemma: rightAltWeylFermionContraction_symm_altRightWeylFermionContraction := The linear map altRightWeylFermionContraction is rightAltWeylFermionContraction composed with the braiding of the tensor product.

Informal lemma: altRightWeylFermionContraction_invariant := The contraction altRightWeylFermionContraction is invariant with respect to the action of SL(2,C) on rightHandedWeylFermion and altRightHandedWeylFermion.

HepLean.StandardModel.Basic

Informal def: gaugeGroupℤ₆SubGroup := The ℤ₆-subgroup of ``GaugeGroupI with elements (α^2 * I₃, α^(-3) * I₂, α), where α is a sixth complex root of unity.

Informal def: GaugeGroupℤ₆ := The quotient of ``GaugeGroupI by the ℤ₆-subgroup gaugeGroupℤ₆SubGroup.

Informal def: gaugeGroupℤ₂SubGroup := The ℤ₂-subgroup of ``GaugeGroupI derived from the ℤ₂ subgroup of gaugeGroupℤ₆SubGroup.

Informal def: GaugeGroupℤ₂ := The quotient of ``GaugeGroupI by the ℤ₂-subgroup gaugeGroupℤ₂SubGroup.

Informal def: gaugeGroupℤ₃SubGroup := The ℤ₃-subgroup of ``GaugeGroupI derived from the ℤ₃ subgroup of gaugeGroupℤ₆SubGroup.

Informal def: GaugeGroupℤ₃ := The quotient of ``GaugeGroupI by the ℤ₃-subgroup gaugeGroupℤ₃SubGroup.

Informal def: GaugeGroup := The map from GaugeGroupQuot to Type which gives the gauge group of the Standard Model for a given choice of quotient.

HepLean.StandardModel.HiggsBoson.Basic

Informal lemma: zero_is_zero_section := The HiggsField zero defined by ofReal 0 is the constant zero-section of the bundle HiggsBundle.

HepLean.StandardModel.HiggsBoson.GaugeAction

Informal lemma: stability_group_single := 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 θ}).

Informal lemma: stability_group := 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.

HepLean.StandardModel.HiggsBoson.Potential

Informal lemma: isBounded_iff_of_𝓵_zero := 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.