Lepton doublets

i. Overview

The Standard Model lepton doublet is a left-handed Weyl spinor in the (1, 2)_{-3} representation. Here charges are normalized as 6Y, so -3 is the usual hypercharge Y = -1/2.

LeptonDoublet is the target vector space of one lepton multiplet. Its Weyl factor carries the Lorentz index and its two-dimensional factor carries the weak index. The absence of a colour factor makes it an SU(3) singlet.

The Lorentz and gauge actions are first defined separately. The gauge action is then computed on a basis, used to identify its kernel, and descended to each supported global form of the Standard Model gauge group.

ii. Key results

LeptonDoublet : the target space of the (1, 2)_{-3} multiplet.

repLorentzGroup : the left-handed Lorentz action.

repGaugeGroupI : the action of the unquotiented gauge group.

repGaugeGroupI_tmul_basis_eq_sum : the gauge action in a tensor-product basis.

mem_repGaugeGroupI_ker_iff_eq : the kernel of the full-group action.

gaugeGroup_subgroup_ℤ₆_le_ker_repGaugeGroupI : triviality of the central ℤ₆.

repGaugeGroup : the action descended to every supported gauge-group quotient.

iii. Table of contents

A. The lepton-doublet space

B. Linear structure

C. Lorentz action

D. Gauge action

E. Kernel of the gauge action

F. Descent to quotient gauge groups

A. The lepton-doublet space

The Weyl factor carries the left-handed Lorentz index, while EuclideanSpace ℂ (Fin 2) carries the weak index.

The target vector space of one Standard Model lepton doublet. It carries the (1, 2)_{-3} representation of the gauge group.

The left-handed Weyl spinor with its weak-doublet index.

B. Linear structure

The wrapper distinguishes lepton doublets from other isomorphic vector spaces. The following equivalences transfer the linear structure of the tensor product and expose that model when defining representations.

Identifies a lepton doublet with its underlying tensor-product value.

The linear identification with the underlying tensor product.

C. Lorentz action

The Lorentz group acts on the left-handed Weyl factor and leaves the weak index fixed.

D. Gauge action

The colour factor acts trivially, while SU(2) acts on the weak index. The U(1) action is star z ^ 3; since z is unitary, star z = z⁻¹, so this represents charge -3.

The tensor and basis formulas below expose the coefficients used to compare actions and compute the kernel.

The gauge action on a pure spinor–weak tensor.

E. Kernel of the gauge action

An element acts trivially when its weak action is scalar and that scalar cancels its U(1) phase. Its colour component is unrestricted because the lepton doublet is an SU(3) singlet.

Characterizes the full-group elements acting trivially on the lepton doublet.